← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (3969 chars)
I left a sorry and an incomplete expression in scaledZeta_analytic. The issue: getting AnalyticAt ζ at a point from DifferentiableAt. The clean route: ζ is DifferentiableOn {z ≠ 1} (open set) ⟹ AnalyticOnNhd on {z ≠ 1} via DifferentiableOn.analyticOnNhd — wait — HolomorphicOn_riemannZeta : HolomorphicOn ζ {s ≠ 1} — HolomorphicOn is DifferentiableOn — so `(HolomorphicOn_riemannZeta).analyticOnNhd isOpen_compl_singleton : AnalyticOnNhd ℂ riemannZeta {z | z ≠ 1}` ✓. Then at our point: `(that) _ (hU-membership)` — AnalyticOnNhd f s = ∀ x ∈ s, AnalyticAt f x — so `that _ (hne : point ∈ {z ≠ 1})`. Fix:
```lean
have hζ : AnalyticAt ℂ riemannZeta (discCenter t + (5 / 2 : ℂ) * w) :=
(HolomorphicOn_riemannZeta.analyticOnNhd isOpen_compl_singleton) _ hne
```
Wait — HolomorphicOn_riemannZeta : HolomorphicOn ζ {s | s ≠ 1} — HolomorphicOn ℂ f s is DifferentiableOn ℂ f s? In current Mathlib, HolomorphicOn is a def for DifferentiableOn ℂ. So HolomorphicOn_riemannZeta.analyticOnNhd (isOpen_compl_singleton : IsOpen {z | z ≠ 1})... the set in the lemma is {s : ℂ | s ≠ 1} — isOpen_compl_singleton : IsOpen ({1}ᶜ) — {s | s ≠ 1} = {1}ᶜ ✓ defeq. Then membership hne : point ∈ {z | z ≠ 1} — hne : point ≠ 1 ✓ defeq.
Hmm — does `DifferentiableOn.analyticOnNhd` accept HolomorphicOn (they're the same def)? HolomorphicOn = DifferentiableOn ℂ ✓ defeq ✓.
Then the full analyticity of scaledZeta: F(w) = ζ(g w)/ζ(s₀) with g w = s₀ + (5/2)w analytic everywhere: AnalyticAt via comp:
```lean
have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w :=
(analyticAt_const.mul analyticAt_id).const_add _ -- hmm forms
```
analyticAt_id.const_mul? `AnalyticAt.const_mul`? there's `analyticAt_const.mul analyticAt_id` for (fun w => c * w) ✓ then .const_add for + s₀: `AnalyticAt.add analyticAt_const that`... the function is s₀ + (5/2)·w: (analyticAt_const).add ((analyticAt_const).mul analyticAt_id)?? analyticAt_const : AnalyticAt ℂ (fun _ => c) w ✓; .add : AnalyticAt (f + g)... pointwise — the lambda fun w => s₀ + (5/2)*w — matches (fun w => s₀) + (fun w => (5/2)*w) via Pi.add_apply ✓ defeq for exact? Use:
```lean
have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w :=
analyticAt_const.add (analyticAt_const.mul analyticAt_id)
```
the unification: fun w => s₀ + (5/2)*w vs (fun w => s₀) + (fun w => (5/2)*w)?? AnalyticAt.add hf hg : AnalyticAt (fun x => f x + g x) — hmm — AnalyticAt.add (hf : AnalyticAt f) (hg : AnalyticAt g) : AnalyticAt (f + g)? or (fun x => f x + g x)? In current Mathlib: `AnalyticAt.add (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (f + g) z` — the Pi.add form (f + g)(x) = f x + g x by Pi.add_apply — the lambda fun w => s₀ + (5/2)*w — Lean needs to see (f + g) w = s₀ + (5/2)*w — with f = const s₀, g = (5/2)·id: (f+g) w = s₀ + (5/2)*w ✓ via Pi.add_apply — the exact/unification should handle (defeq).
Then:
```lean
exact (hζ.comp haff).div_const _ -- ζ(g w)/ζ(s₀): AnalyticAt.div_const? or .div analyticAt_const (ζ(s₀) ≠ 0)
```
scaledZeta t w = riemannZeta (...) / riemannZeta (...) = fun w => ζ(g w) / const: AnalyticAt.div (hζ.comp haff) analyticAt_const (by norm_num? no — ζ(s₀) ≠ 0 from the lower bound): `AnalyticAt.div (hf) (hg : AnalyticAt g) (hg0 : g w ≠ 0)`: g = const ζ(s₀): hg0 : ζ(s₀) ≠ 0 ✓ from zeta_lower_bound_two (1/3 ≤ ‖ζ‖ ⟹ ≠ 0).
Hmm — but my goal in scaledZeta_analytic is AnalyticOnNhd ℂ (scaledZeta t) (closedBall 0 1) — intro w hw gave AnalyticAt at w with hw : w ∈ closedBall 0 1. The hne argument used hw (the disc membership for the im-lower-bound). So the full proof: per point w in the closed unit ball: the evaluation point is in the 5/2-disc, ≠ 1, ζ analytic there, F analytic via comp/div. ✓.
Also — I realize my §1 theorem zeroDisc_isNontrivial's h2 hypothesis usage: fine.
Let me rewrite the whole scaledZeta_analytic cleanly, and continue with the rest of §2 (finiteness + ZerosBound + gap). Let me rewrite the current broken block first.
Restructuring `scaledZeta_analytic` cleanly (the HolomorphicOn→AnalyticOnNhd route).
tool: Edit ok
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
"old_string": "/-- F is analytic on the closed unit disc (\u03b6 is analytic on B(s\u2080, 5/2),\nwhich avoids the pole at 1 since |t| \u2265 10 \u27f9 |im| \u2265 15/2). -/\ntheorem scaledZeta_analytic {t : \u211d} (ht : 10 \u2264 |t|) :\n AnalyticOnNhd \u2102 (scaledZeta t) (Metric.closedBall 0 1) := by\n intro w hw\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n have hw' : \u2016(5 / 2 : \u2102) * w\u2016 \u2264 5 / 2 := by\n rw [norm_mul]\n calc \u2016(5 / 2 : \u2102)\u2016 * \u2016w\u2016 \u2264 (5 / 2) * 1 := by\n apply mul_le_mul _ hw (norm_nonneg _) (by norm_num)\n \u00b7 rw [norm_div, norm_one]; norm_num\n _ = 5 / 2 := by norm_num\n have hmem : discCenter t + (5 / 2 : \u2102) * w \u2208 Metric.closedBall (discCenter t) (5 / 2) := by\n rw [Metric.mem_closedBall, Complex.dist_eq]\n rw [add_sub_cancel_left]\n exact hw'\n -- the point is not 1 (its imaginary part is \u2265 15/2 in absolute value)\n have hne : discCenter t + (5 / 2 : \u2102) * w \u2260 1 := by\n intro h\n have him : (discCenter t + (5 / 2 : \u2102) * w).im = t + (5 / 2) * w.im := by\n simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, mul_re]\n have h1 : |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im| \u2264 5 / 2 := by\n calc |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im|\n \u2264 \u2016discCenter t + (5 / 2 : \u2102) * w - discCenter t\u2016 := abs_im_le_norm _\n _ \u2264 5 / 2 := by rw [add_sub_cancel_left]; exact hw'\n rw [show (discCenter t + (5 / 2 : \u2102) * w - discCenter t) = (5 / 2 : \u2102) * w by ring] at h1\n rw [h] at him\n simp at him -- him : (1:\u2102).im = t + (5/2)*w.im; (1:\u2102).im = 0\n -- |t + (5/2) w.im| \u2265 |t| \u2212 (5/2)|w.im| \u2265 10 \u2212 5/2 = 15/2 > 0\n have hwim : |w.im| \u2264 1 := (abs_im_le_norm _).trans hw\n have : |t + (5 / 2) * w.im| \u2265 15 / 2 := by\n have h2 : |t + (5 / 2) * w.im| \u2265 |t| - |(5 / 2) * w.im| := by\n have h3 : |t| \u2264 |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by\n calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf\n _ \u2264 |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _\n _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]\n linarith [h3]\n have h4 : |(5 / 2) * w.im| \u2264 5 / 2 := by\n rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5/2)]\n calc (5 / 2) * |w.im| \u2264 (5 / 2) * 1 := by\n apply mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h2, h4, ht]\n rw [him] at this\n norm_num at this\n -- \u03b6 analytic at the point\n have h\u03b6 : AnalyticAt \u2102 riemannZeta (discCenter t + (5 / 2 : \u2102) * w) := by\n have hd := differentiableAt_riemannZeta hne\n -- DifferentiableAt at a point doesn't give AnalyticAt directly; use the\n -- neighborhood differentiability on {z \u2260 1}.\n have hU : {z : \u2102 | z \u2260 1} \u2208 \ud835\udcdd (discCenter t + (5 / 2 : \u2102) * w) :=\n isOpen_compl_singleton.mem_nhds hne\n exact ((HolomorphicOn_riemannZeta.mono (Set.subset_univ _) |>.analyticOnNhd\n isOpen_compl_singleton) _ hU ... )\n sorry\n\nend NguyenRH1\n\nend",
"new_string": "/-- \u03b6 is analytic on neighborhoods of every point \u2260 1. -/\ntheorem analyticAt_riemannZeta_of_ne_one {z : \u2102} (hz : z \u2260 1) :\n AnalyticAt \u2102 riemannZeta z :=\n (HolomorphicOn_riemannZeta.analyticOnNhd isOpen_compl_singleton) z hz\n\n/-- F is analytic on the closed unit disc (\u03b6 is analytic on B(s\u2080, 5/2),\nwhich avoids the pole at 1 since |t| \u2265 10 \u27f9 |im| \u2265 15/2). -/\ntheorem scaledZeta_analytic {t : \u211d} (ht : 10 \u2264 |t|) :\n AnalyticOnNhd \u2102 (scaledZeta t) (Metric.closedBall 0 1) := by\n intro w hw\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n have hw' : \u2016(5 / 2 : \u2102) * w\u2016 \u2264 5 / 2 := by\n rw [norm_mul, show \u2016(5 / 2 : \u2102)\u2016 = 5 / 2 by norm_num [Complex.norm_ofNat, Complex.norm_two]]\n exact mul_le_mul_of_nonneg_left hw (by norm_num)\n -- the evaluation point is not 1 (its imaginary part is large)\n have hne : discCenter t + (5 / 2 : \u2102) * w \u2260 1 := by\n intro h\n have hwim : |w.im| \u2264 1 := (abs_im_le_norm _).trans hw\n have him : (discCenter t + (5 / 2 : \u2102) * w).im = t + (5 / 2) * w.im := by\n simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]\n have hbig : 15 / 2 \u2264 |t + (5 / 2) * w.im| := by\n have h2 : |t| \u2264 |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by\n calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf\n _ \u2264 |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _\n _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]\n have h4 : |(5 / 2) * w.im| \u2264 5 / 2 := by\n rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5 / 2)]\n calc (5 / 2) * |w.im| \u2264 (5 / 2) * 1 :=\n mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h2, h4, ht]\n rw [h] at him\n rw [Complex.one_im] at him\n rw [him] at hbig\n norm_num at hbig\n have haff : AnalyticAt \u2102 (fun w : \u2102 => discCenter t + (5 / 2 : \u2102) * w) w :=\n analyticAt_const.add (analyticAt_const.mul analyticAt_id)\n exact ((analyticAt_riemannZeta_of_ne_one hne).comp haff).div analyticAt_const\n (by\n intro h0\n have h := RvM.zeta_lower_bound_two t\n rw [h0, norm_zero] at h\n norm_num at h)\n\nend NguyenRH1\n\nend"
}
result 2026-08-22 19:58:22Z → 2026-08-22 19:58:22Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
"oldString": "/-- F is analytic on the closed unit disc (\u03b6 is analytic on B(s\u2080, 5/2),\nwhich avoids the pole at 1 since |t| \u2265 10 \u27f9 |im| \u2265 15/2). -/\ntheorem scaledZeta_analytic {t : \u211d} (ht : 10 \u2264 |t|) :\n AnalyticOnNhd \u2102 (scaledZeta t) (Metric.closedBall 0 1) := by\n intro w hw\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n have hw' : \u2016(5 / 2 : \u2102) * w\u2016 \u2264 5 / 2 := by\n rw [norm_mul]\n calc \u2016(5 / 2 : \u2102)\u2016 * \u2016w\u2016 \u2264 (5 / 2) * 1 := by\n apply mul_le_mul _ hw (norm_nonneg _) (by norm_num)\n \u00b7 rw [norm_div, norm_one]; norm_num\n _ = 5 / 2 := by norm_num\n have hmem : discCenter t + (5 / 2 : \u2102) * w \u2208 Metric.closedBall (discCenter t) (5 / 2) := by\n rw [Metric.mem_closedBall, Complex.dist_eq]\n rw [add_sub_cancel_left]\n exact hw'\n -- the point is not 1 (its imaginary part is \u2265 15/2 in absolute value)\n have hne : discCenter t + (5 / 2 : \u2102) * w \u2260 1 := by\n intro h\n have him : (discCenter t + (5 / 2 : \u2102) * w).im = t + (5 / 2) * w.im := by\n simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, mul_re]\n have h1 : |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im| \u2264 5 / 2 := by\n calc |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im|\n \u2264 \u2016discCenter t + (5 / 2 : \u2102) * w - discCenter t\u2016 := abs_im_le_norm _\n _ \u2264 5 / 2 := by rw [add_sub_cancel_left]; exact hw'\n rw [show (discCenter t + (5 / 2 : \u2102) * w - discCenter t) = (5 / 2 : \u2102) * w by ring] at h1\n rw [h] at him\n simp at him -- him : (1:\u2102).im = t + (5/2)*w.im; (1:\u2102).im = 0\n -- |t + (5/2) w.im| \u2265 |t| \u2212 (5/2)|w.im| \u2265 10 \u2212 5/2 = 15/2 > 0\n have hwim : |w.im| \u2264 1 := (abs_im_le_norm _).trans hw\n have : |t + (5 / 2) * w.im| \u2265 15 / 2 := by\n have h2 : |t + (5 / 2) * w.im| \u2265 |t| - |(5 / 2) * w.im| := by\n have h3 : |t| \u2264 |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by\n calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf\n _ \u2264 |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _\n _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]\n linarith [h3]\n have h4 : |(5 / 2) * w.im| \u2264 5 / 2 := by\n rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5/2)]\n calc (5 / 2) * |w.im| \u2264 (5 / 2) * 1 := by\n apply mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h2, h4, ht]\n rw [him] at this\n norm_num at this\n -- \u03b6 analytic at the point\n have h\u03b6 : AnalyticAt \u2102 riemannZeta (discCenter t + (5 / 2 : \u2102) * w) := by\n have hd := differentiableAt_riemannZeta hne\n -- DifferentiableAt at a point doesn't give AnalyticAt directly; use the\n -- neighborhood differentiability on {z \u2260 1}.\n have hU : {z : \u2102 | z \u2260 1} \u2208 \ud835\udcdd (discCenter t + (5 / 2 : \u2102) * w) :=\n isOpen_compl_singleton.mem_nhds hne\n exact ((HolomorphicOn_riemannZeta.mono (Set.subset_univ _) |>.analyticOnNhd\n isOpen_compl_singleton) _ hU ... )\n sorry\n\nend NguyenRH1\n\nend",
"newString": "/-- \u03b6 is analytic on neighborhoods of every point \u2260 1. -/\ntheorem analyticAt_riemannZeta_of_ne_one {z : \u2102} (hz : z \u2260 1) :\n AnalyticAt \u2102 riemannZeta z :=\n (HolomorphicOn_riemannZeta.analyticOnNhd isOpen_compl_singleton) z hz\n\n/-- F is analytic on the closed unit disc (\u03b6 is analytic on B(s\u2080, 5/2),\nwhich avoids the pole at 1 since |t| \u2265 10 \u27f9 |im| \u2265 15/2). -/\ntheorem scaledZeta_analytic {t : \u211d} (ht : 10 \u2264 |t|) :\n AnalyticOnNhd \u2102 (scaledZeta t) (Metric.closedBall 0 1) := by\n intro w hw\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n have hw' : \u2016(5 / 2 : \u2102) * w\u2016 \u2264 5 / 2 := by\n rw [norm_mul, show \u2016(5 / 2 : \u2102)\u2016 = 5 / 2 by norm_num [Complex.norm_ofNat, Complex.norm_two]]\n exact mul_le_mul_of_nonneg_left hw (by norm_num)\n -- the evaluation point is not 1 (its imaginary part is large)\n have hne : discCenter t + (5 / 2 : \u2102) * w \u2260 1 := by\n intro h\n have hwim : |w.im| \u2264 1 := (abs_im_le_norm _).trans hw\n have him : (discCenter t + (5 / 2 : \u2102) * w).im = t + (5 / 2) * w.im := by\n simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]\n have hbig : 15 / 2 \u2264 |t + (5 / 2) * w.im| := by\n have h2 : |t| \u2264 |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by\n calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf\n _ \u2264 |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _\n _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]\n have h4 : |(5 / 2) * w.im| \u2264 5 / 2 := by\n rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5 / 2)]\n calc (5 / 2) * |w.im| \u2264 (5 / 2) * 1 :=\n mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h2, h4, ht]\n rw [h] at him\n rw [Complex.one_im] at him\n rw [him] at hbig\n norm_num at hbig\n have haff : AnalyticAt \u2102 (fun w : \u2102 => discCenter t + (5 / 2 : \u2102) * w) w :=\n analyticAt_const.add (analyticAt_const.mul analyticAt_id)\n exact ((analyticAt_riemannZeta_of_ne_one hne).comp haff).div analyticAt_const\n (by\n intro h0\n have h := RvM.zeta_lower_bound_two t\n rw [h0, norm_zero] at h\n norm_num at h)\n\nend NguyenRH1\n\nend",
"originalFile": "/-\nNguyenRH1/LiDisc.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5c (D-067 \u00a73 + \u00a76 revision):\nthe LOOSE Davenport-disc R-bound on \u03c3 \u2208 [1/2, 7/2], |t| \u2265 10 \u2014 the\nGROWTH INPUT for the partial-fraction identity (ii\u2032-5e). Its constants\nare deliberately loose (D-067 \u00a76: no disc-only constant can reach the\nbaked A = 10.5, B\u2080 = 48; tightness comes from the identity stage).\n\nStructure (all on the disc B(2+it, R), R \u2208 [2.4, 2.5] chosen in a gap of\nthe zero-distance values):\n* \u00a71 the zero collection + count (perimeter ZeroCountProp, ii\u2032-4);\n* \u00a72 the R-gap selection (scaled midpoint pigeonhole from ii\u2032-4);\n* \u00a73 g := \u03b6/\u220f(s\u2212\u03c1\u2096)^{m\u2096} analytic + nonvanishing on the closed disc;\n* \u00a74 the bounds: |g| on the outer circle (ii\u2032-5b's |\u03b6|-bound +\n clearance), the center lower bound (1/\u03b6 = \u03a3 \u03bc(n)n^{\u2212s}), then\n LogOfAnalyticFunction + BorelCaratheodoryDeriv (StrongPNTPrefix)\n giving \u2016(log g)\u2032\u2016 \u226a (log|t|)\u00b2, hence the loose R-bound.\n\nArchive references: D-067, D-064 \u00a74 R3, journal-022.\n-/\nimport Mathlib\nimport Zeta23.FromPNTPlus.StrongPNTPrefix\nimport NguyenRH1.LiRBound\n\nopen Zeta23 Complex Filter Topology MeasureTheory\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The zero collection and its count -/\n\n/-- The disc center s\u2080 = 2 + it. -/\ndef discCenter (t : \u211d) : \u2102 := 2 + t * Complex.I\n\n/-- The zeros of \u03b6 in the closed disc of radius 5/2 about 2+it, as a\nfinset (finiteness from Mathlib's discrete-zero-set machinery). -/\nnoncomputable def zeroDiscFinset (t : \u211d) : Finset \u2102 :=\n ((isCompact_closedBall (discCenter t) (5 / 2)).inter_riemannZetaZeros_finite).toFinset\n\ntheorem mem_zeroDiscFinset {t : \u211d} {\u03c1 : \u2102} :\n \u03c1 \u2208 zeroDiscFinset t \u2194\n \u03c1 \u2208 Metric.closedBall (discCenter t) (5 / 2) \u2227 riemannZeta \u03c1 = 0 := by\n unfold zeroDiscFinset\n rw [Set.Finite.mem_toFinset]\n constructor\n \u00b7 intro h\n exact \u27e8h.1, h.2\u27e9\n \u00b7 intro h\n exact \u27e8h.1, mem_riemannZetaZeros.mpr h.2\u27e9\n\n/-- Every zero of \u03b6 in the disc is a nontrivial zero (re \u2265 1 excluded by\n`riemannZeta_ne_zero_of_one_le_re`; re \u2264 0 excluded by the FE since the\ndisc avoids {\u22122n} and 0). -/\ntheorem zeroDisc_isNontrivial {t : \u211d} {\u03c1 : \u2102} (h\u03c1 : \u03c1 \u2208 zeroDiscFinset t) :\n IsNontrivialZero \u03c1 := by\n have h2 := (mem_zeroDiscFinset.mp h\u03c1).2\n have hball := (mem_zeroDiscFinset.mp h\u03c1).1\n -- \u03c1 \u2208 closedBall (2+it) (5/2) \u27f9 re \u03c1 \u2208 [\u22121/2, 9/2]\n have hre : -1 / 2 \u2264 \u03c1.re \u2227 \u03c1.re \u2264 9 / 2 := by\n rw [Metric.mem_closedBall, Complex.dist_eq] at hball\n have h1 : |(\u03c1 - discCenter t).re| \u2264 5 / 2 := (abs_re_le_norm _).trans hball\n have h2re : (\u03c1 - discCenter t).re = \u03c1.re - 2 := by\n simp [discCenter, sub_re, mul_re, ofReal_re, ofReal_im, I_re, I_im]\n rw [h2re] at h1\n have := abs_le.mp h1\n constructor <;> linarith [this.1, this.2]\n -- re \u03c1 \u2265 1 excluded\n have hnot1 : \u03c1.re < 1 := by\n by_contra h\n push Not at h\n exact riemannZeta_ne_zero_of_one_le_re h h2\n -- re \u03c1 \u2264 0 excluded (would force \u03c1 \u2208 {\u22122n} \u222a {0}, all outside the disc)\n have hpos : 0 < \u03c1.re := by\n by_contra h\n push Not at h\n by_cases hG : Complex.Gamma\u211d \u03c1 = 0\n \u00b7 -- \u0393R(\u03c1) = 0 \u27f9 \u03c1 = \u22122n: n = 0 gives \u03b6(0) = \u22121/2 \u2260 0; n \u2265 1 gives re \u2264 \u22122\n rw [Complex.Gamma\u211d_eq_zero_iff] at hG\n obtain \u27e8n, hn\u27e9 := hG\n have hre' : \u03c1.re = -2 * (n : \u211d) := by\n rw [hn]\n simp [neg_re, mul_re]\n rcases Nat.eq_zero_or_pos n with hn0 | hnpos\n \u00b7 subst hn0\n norm_num at hre'\n rw [hn] at h2\n norm_num at h2\n rw [riemannZeta_zero] at h2\n norm_num at h2\n \u00b7 have hn1 : (1:\u211d) \u2264 (n : \u211d) := by exact_mod_cast hnpos\n linarith [hre.1, hre']\n \u00b7 have h\u03c10 : \u03c1 \u2260 0 := by\n intro h0\n rw [h0, riemannZeta_zero] at h2\n norm_num at h2\n have h\u039b : completedRiemannZeta \u03c1 = 0 := by\n rw [RvM.completedRiemannZeta_eq_Gamma\u211d_mul h\u03c10 hG, h2, mul_zero]\n exact absurd (RvM.completedRiemannZeta_eq_zero_iff.mp h\u039b).2.1 (not_lt.mpr h)\n exact \u27e8h2, hpos, hnot1\u27e9\n\n/-! ## 2. The scaled function, the Jensen count, and the R-gap\n\nThe scaled function F(w) = \u03b6(s\u2080 + (5/2)w)/\u03b6(s\u2080) on the unit disc, to\nwhich Zeta23's `ZerosBound` (Jensen) applies: F(0) = 1 (the center lower\nbound \u2016\u03b6(2+it)\u2016 \u2265 1/3 is Zeta23's `RvM.zeta_lower_bound_two`), and\n\u2016F\u2016 \u2264 (9/4)|t|\u00b2 on the closed unit disc (ii\u2032-5b's disc bound). -/\n\n/-- The scaled function F(w) = \u03b6(s\u2080 + (5/2)\u00b7w)/\u03b6(s\u2080), s\u2080 = 2+it. -/\nnoncomputable def scaledZeta (t : \u211d) (w : \u2102) : \u2102 :=\n riemannZeta (discCenter t + (5 / 2 : \u2102) * w) / riemannZeta (discCenter t)\n\ntheorem scaledZeta_zero (t : \u211d) : scaledZeta t 0 = 1 := by\n unfold scaledZeta\n simp only [mul_zero, add_zero]\n exact div_self (by\n have h := RvM.zeta_lower_bound_two t\n intro h0\n rw [h0, norm_zero] at h\n norm_num at h)\n\n/-- F is analytic on the closed unit disc (\u03b6 is analytic on B(s\u2080, 5/2),\nwhich avoids the pole at 1 since |t| \u2265 10 \u27f9 |im| \u2265 15/2). -/\ntheorem scaledZeta_analytic {t : \u211d} (ht : 10 \u2264 |t|) :\n AnalyticOnNhd \u2102 (scaledZeta t) (Metric.closedBall 0 1) := by\n intro w hw\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n have hw' : \u2016(5 / 2 : \u2102) * w\u2016 \u2264 5 / 2 := by\n rw [norm_mul]\n calc \u2016(5 / 2 : \u2102)\u2016 * \u2016w\u2016 \u2264 (5 / 2) * 1 := by\n apply mul_le_mul _ hw (norm_nonneg _) (by norm_num)\n \u00b7 rw [norm_div, norm_one]; norm_num\n _ = 5 / 2 := by norm_num\n have hmem : discCenter t + (5 / 2 : \u2102) * w \u2208 Metric.closedBall (discCenter t) (5 / 2) := by\n rw [Metric.mem_closedBall, Complex.dist_eq]\n rw [add_sub_cancel_left]\n exact hw'\n -- the point is not 1 (its imaginary part is \u2265 15/2 in absolute value)\n have hne : discCenter t + (5 / 2 : \u2102) * w \u2260 1 := by\n intro h\n have him : (discCenter t + (5 / 2 : \u2102) * w).im = t + (5 / 2) * w.im := by\n simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, mul_re]\n have h1 : |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im| \u2264 5 / 2 := by\n calc |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im|\n \u2264 \u2016discCenter t + (5 / 2 : \u2102) * w - discCenter t\u2016 := abs_im_le_norm _\n _ \u2264 5 / 2 := by rw [add_sub_cancel_left]; exact hw'\n rw [show (discCenter t + (5 / 2 : \u2102) * w - discCenter t) = (5 / 2 : \u2102) * w by ring] at h1\n rw [h] at him\n simp at him -- him : (1:\u2102).im = t + (5/2)*w.im; (1:\u2102).im = 0\n -- |t + (5/2) w.im| \u2265 |t| \u2212 (5/2)|w.im| \u2265 10 \u2212 5/2 = 15/2 > 0\n have hwim : |w.im| \u2264 1 := (abs_im_le_norm _).trans hw\n have : |t + (5 / 2) * w.im| \u2265 15 / 2 := by\n have h2 : |t + (5 / 2) * w.im| \u2265 |t| - |(5 / 2) * w.im| := by\n have h3 : |t| \u2264 |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by\n calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf\n _ \u2264 |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _\n _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]\n linarith [h3]\n have h4 : |(5 / 2) * w.im| \u2264 5 / 2 := by\n rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5/2)]\n calc (5 / 2) * |w.im| \u2264 (5 / 2) * 1 := by\n apply mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h2, h4, ht]\n rw [him] at this\n norm_num at this\n -- \u03b6 analytic at the point\n have h\u03b6 : AnalyticAt \u2102 riemannZeta (discCenter t + (5 / 2 : \u2102) * w) := by\n have hd := differentiableAt_riemannZeta hne\n -- DifferentiableAt at a point doesn't give AnalyticAt directly; use the\n -- neighborhood differentiability on {z \u2260 1}.\n have hU : {z : \u2102 | z \u2260 1} \u2208 \ud835\udcdd (discCenter t + (5 / 2 : \u2102) * w) :=\n isOpen_compl_singleton.mem_nhds hne\n exact ((HolomorphicOn_riemannZeta.mono (Set.subset_univ _) |>.analyticOnNhd\n isOpen_compl_singleton) _ hU ... )\n sorry\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 119,
"oldLines": 6,
"newStart": 119,
"newLines": 11,
"lines": [
" rw [h0, norm_zero] at h",
" norm_num at h)",
" ",
"+/-- \u03b6 is analytic on neighborhoods of every point \u2260 1. -/",
"+theorem analyticAt_riemannZeta_of_ne_one {z : \u2102} (hz : z \u2260 1) :",
"+ AnalyticAt \u2102 riemannZeta z :=",
"+ (HolomorphicOn_riemannZeta.analyticOnNhd isOpen_compl_singleton) z hz",
"+",
" /-- F is analytic on the closed unit disc (\u03b6 is analytic on B(s\u2080, 5/2),",
" which avoids the pole at 1 since |t| \u2265 10 \u27f9 |im| \u2265 15/2). -/",
" theorem scaledZeta_analytic {t : \u211d} (ht : 10 \u2264 |t|) :"
]
},
{
"oldStart": 126,
"oldLines": 54,
"newStart": 131,
"newLines": 37,
"lines": [
" intro w hw",
" rw [Metric.mem_closedBall, dist_zero_right] at hw",
" have hw' : \u2016(5 / 2 : \u2102) * w\u2016 \u2264 5 / 2 := by",
"- rw [norm_mul]",
"- calc \u2016(5 / 2 : \u2102)\u2016 * \u2016w\u2016 \u2264 (5 / 2) * 1 := by",
"- apply mul_le_mul _ hw (norm_nonneg _) (by norm_num)",
"- \u00b7 rw [norm_div, norm_one]; norm_num",
"- _ = 5 / 2 := by norm_num",
"- have hmem : discCenter t + (5 / 2 : \u2102) * w \u2208 Metric.closedBall (discCenter t) (5 / 2) := by",
"- rw [Metric.mem_closedBall, Complex.dist_eq]",
"- rw [add_sub_cancel_left]",
"- exact hw'",
"- -- the point is not 1 (its imaginary part is \u2265 15/2 in absolute value)",
"+ rw [norm_mul, show \u2016(5 / 2 : \u2102)\u2016 = 5 / 2 by norm_num [Complex.norm_ofNat, Complex.norm_two]]",
"+ exact mul_le_mul_of_nonneg_left hw (by norm_num)",
"+ -- the evaluation point is not 1 (its imaginary part is large)",
" have hne : discCenter t + (5 / 2 : \u2102) * w \u2260 1 := by",
" intro h",
"+ have hwim : |w.im| \u2264 1 := (abs_im_le_norm _).trans hw",
" have him : (discCenter t + (5 / 2 : \u2102) * w).im = t + (5 / 2) * w.im := by",
"- simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, mul_re]",
"- have h1 : |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im| \u2264 5 / 2 := by",
"- calc |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im|",
"- \u2264 \u2016discCenter t + (5 / 2 : \u2102) * w - discCenter t\u2016 := abs_im_le_norm _",
"- _ \u2264 5 / 2 := by rw [add_sub_cancel_left]; exact hw'",
"- rw [show (discCenter t + (5 / 2 : \u2102) * w - discCenter t) = (5 / 2 : \u2102) * w by ring] at h1",
"- rw [h] at him",
"- simp at him -- him : (1:\u2102).im = t + (5/2)*w.im; (1:\u2102).im = 0",
"- -- |t + (5/2) w.im| \u2265 |t| \u2212 (5/2)|w.im| \u2265 10 \u2212 5/2 = 15/2 > 0",
"- have hwim : |w.im| \u2264 1 := (abs_im_le_norm _).trans hw",
"- have : |t + (5 / 2) * w.im| \u2265 15 / 2 := by",
"- have h2 : |t + (5 / 2) * w.im| \u2265 |t| - |(5 / 2) * w.im| := by",
"- have h3 : |t| \u2264 |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by",
"- calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf",
"- _ \u2264 |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _",
"- _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]",
"- linarith [h3]",
"+ simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]",
"+ have hbig : 15 / 2 \u2264 |t + (5 / 2) * w.im| := by",
"+ have h2 : |t| \u2264 |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by",
"+ calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf",
"+ _ \u2264 |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _",
"+ _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]",
" have h4 : |(5 / 2) * w.im| \u2264 5 / 2 := by",
"- rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5/2)]",
"- calc (5 / 2) * |w.im| \u2264 (5 / 2) * 1 := by",
"- apply mul_le_mul_of_nonneg_left hwim (by norm_num)",
"+ rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5 / 2)]",
"+ calc (5 / 2) * |w.im| \u2264 (5 / 2) * 1 :=",
"+ mul_le_mul_of_nonneg_left hwim (by norm_num)",
" _ = 5 / 2 := by norm_num",
" linarith [h2, h4, ht]",
"- rw [him] at this",
"- norm_num at this",
"- -- \u03b6 analytic at the point",
"- have h\u03b6 : AnalyticAt \u2102 riemannZeta (discCenter t + (5 / 2 : \u2102) * w) := by",
"- have hd := differentiableAt_riemannZeta hne",
"- -- DifferentiableAt at a point doesn't give AnalyticAt directly; use the",
"- -- neighborhood differentiability on {z \u2260 1}.",
"- have hU : {z : \u2102 | z \u2260 1} \u2208 \ud835\udcdd (discCenter t + (5 / 2 : \u2102) * w) :=",
"- isOpen_compl_singleton.mem_nhds hne",
"- exact ((HolomorphicOn_riemannZeta.mono (Set.subset_univ _) |>.analyticOnNhd",
"- isOpen_compl_singleton) _ hU ... )",
"- sorry",
"+ rw [h] at him",
"+ rw [Complex.one_im] at him",
"+ rw [him] at hbig",
"+ norm_num at hbig",
"+ have haff : AnalyticAt \u2102 (fun w : \u2102 => discCenter t + (5 / 2 : \u2102) * w) w :=",
"+ analyticAt_const.add (analyticAt_const.mul analyticAt_id)",
"+ exact ((analyticAt_riemannZeta_of_ne_one hne).comp haff).div analyticAt_const",
"+ (by",
"+ intro h0",
"+ have h := RvM.zeta_lower_bound_two t",
"+ rw [h0, norm_zero] at h",
"+ norm_num at h)",
" ",
" end NguyenRH1",
" "
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"I left a sorry and an incomplete expression in scaledZeta_analytic. The issue: getting AnalyticAt ζ at a point from DifferentiableAt. The clean route: ζ is DifferentiableOn {z ≠ 1} (open set) ⟹ AnalyticOnNhd on {z ≠ 1} via DifferentiableOn.analyticOnNhd — wait — HolomorphicOn_riemannZeta : HolomorphicOn ζ {s ≠ 1} — HolomorphicOn is DifferentiableOn — so `(HolomorphicOn_riemannZeta).analyticOnNhd isOpen_compl_singleton : AnalyticOnNhd ℂ riemannZeta {z | z ≠ 1}` ✓. Then at our point: `(that) _ (hU-membership)` — AnalyticOnNhd f s = ∀ x ∈ s, AnalyticAt f x — so `that _ (hne : point ∈ {z ≠ 1})`. Fix:\n\n```lean\n have hζ : AnalyticAt ℂ riemannZeta (discCenter t + (5 / 2 : ℂ) * w) :=\n (HolomorphicOn_riemannZeta.analyticOnNhd isOpen_compl_singleton) _ hne\n```\nWait — HolomorphicOn_riemannZeta : HolomorphicOn ζ {s | s ≠ 1} — HolomorphicOn ℂ f s is DifferentiableOn ℂ f s? In current Mathlib, HolomorphicOn is a def for DifferentiableOn ℂ. So HolomorphicOn_riemannZeta.analyticOnNhd (isOpen_compl_singleton : IsOpen {z | z ≠ 1})... the set in the lemma is {s : ℂ | s ≠ 1} — isOpen_compl_singleton : IsOpen ({1}ᶜ) — {s | s ≠ 1} = {1}ᶜ ✓ defeq. Then membership hne : point ∈ {z | z ≠ 1} — hne : point ≠ 1 ✓ defeq.\n\nHmm — does `DifferentiableOn.analyticOnNhd` accept HolomorphicOn (they're the same def)? HolomorphicOn = DifferentiableOn ℂ ✓ defeq ✓.\n\nThen the full analyticity of scaledZeta: F(w) = ζ(g w)/ζ(s₀) with g w = s₀ + (5/2)w analytic everywhere: AnalyticAt via comp:\n```lean\n have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w :=\n (analyticAt_const.mul analyticAt_id).const_add _ -- hmm forms\n```\nanalyticAt_id.const_mul? `AnalyticAt.const_mul`? there's `analyticAt_const.mul analyticAt_id` for (fun w => c * w) ✓ then .const_add for + s₀: `AnalyticAt.add analyticAt_const that`... the function is s₀ + (5/2)·w: (analyticAt_const).add ((analyticAt_const).mul analyticAt_id)?? analyticAt_const : AnalyticAt ℂ (fun _ => c) w ✓; .add : AnalyticAt (f + g)... pointwise — the lambda fun w => s₀ + (5/2)*w — matches (fun w => s₀) + (fun w => (5/2)*w) via Pi.add_apply ✓ defeq for exact? Use:\n```lean\n have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w :=\n analyticAt_const.add (analyticAt_const.mul analyticAt_id)\n```\nthe unification: fun w => s₀ + (5/2)*w vs (fun w => s₀) + (fun w => (5/2)*w)?? AnalyticAt.add hf hg : AnalyticAt (fun x => f x + g x) — hmm — AnalyticAt.add (hf : AnalyticAt f) (hg : AnalyticAt g) : AnalyticAt (f + g)? or (fun x => f x + g x)? In current Mathlib: `AnalyticAt.add (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (f + g) z` — the Pi.add form (f + g)(x) = f x + g x by Pi.add_apply — the lambda fun w => s₀ + (5/2)*w — Lean needs to see (f + g) w = s₀ + (5/2)*w — with f = const s₀, g = (5/2)·id: (f+g) w = s₀ + (5/2)*w ✓ via Pi.add_apply — the exact/unification should handle (defeq).\n\nThen:\n```lean\n exact (hζ.comp haff).div_const _ -- ζ(g w)/ζ(s₀): AnalyticAt.div_const? or .div analyticAt_const (ζ(s₀) ≠ 0)\n```\nscaledZeta t w = riemannZeta (...) / riemannZeta (...) = fun w => ζ(g w) / const: AnalyticAt.div (hζ.comp haff) analyticAt_const (by norm_num? no — ζ(s₀) ≠ 0 from the lower bound): `AnalyticAt.div (hf) (hg : AnalyticAt g) (hg0 : g w ≠ 0)`: g = const ζ(s₀): hg0 : ζ(s₀) ≠ 0 ✓ from zeta_lower_bound_two (1/3 ≤ ‖ζ‖ ⟹ ≠ 0).\n\nHmm — but my goal in scaledZeta_analytic is AnalyticOnNhd ℂ (scaledZeta t) (closedBall 0 1) — intro w hw gave AnalyticAt at w with hw : w ∈ closedBall 0 1. The hne argument used hw (the disc membership for the im-lower-bound). So the full proof: per point w in the closed unit ball: the evaluation point is in the 5/2-disc, ≠ 1, ζ analytic there, F analytic via comp/div. ✓.\n\nAlso — I realize my §1 theorem zeroDisc_isNontrivial's h2 hypothesis usage: fine.\n\nLet me rewrite the whole scaledZeta_analytic cleanly, and continue with the rest of §2 (finiteness + ZerosBound + gap). Let me rewrite the current broken block first.","signature":""},{"type":"text","text":"Restructuring `scaledZeta_analytic` cleanly (the HolomorphicOn→AnalyticOnNhd route)."},{"type":"tool_use","id":"Edit_351","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean","old_string":"/-- F is analytic on the closed unit disc (ζ is analytic on B(s₀, 5/2),\nwhich avoids the pole at 1 since |t| ≥ 10 ⟹ |im| ≥ 15/2). -/\ntheorem scaledZeta_analytic {t : ℝ} (ht : 10 ≤ |t|) :\n AnalyticOnNhd ℂ (scaledZeta t) (Metric.closedBall 0 1) := by\n intro w hw\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n have hw' : ‖(5 / 2 : ℂ) * w‖ ≤ 5 / 2 := by\n rw [norm_mul]\n calc ‖(5 / 2 : ℂ)‖ * ‖w‖ ≤ (5 / 2) * 1 := by\n apply mul_le_mul _ hw (norm_nonneg _) (by norm_num)\n · rw [norm_div, norm_one]; norm_num\n _ = 5 / 2 := by norm_num\n have hmem : discCenter t + (5 / 2 : ℂ) * w ∈ Metric.closedBall (discCenter t) (5 / 2) := by\n rw [Metric.mem_closedBall, Complex.dist_eq]\n rw [add_sub_cancel_left]\n exact hw'\n -- the point is not 1 (its imaginary part is ≥ 15/2 in absolute value)\n have hne : discCenter t + (5 / 2 : ℂ) * w ≠ 1 := by\n intro h\n have him : (discCenter t + (5 / 2 : ℂ) * w).im = t + (5 / 2) * w.im := by\n simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, mul_re]\n have h1 : |(discCenter t + (5 / 2 : ℂ) * w - discCenter t).im| ≤ 5 / 2 := by\n calc |(discCenter t + (5 / 2 : ℂ) * w - discCenter t).im|\n ≤ ‖discCenter t + (5 / 2 : ℂ) * w - discCenter t‖ := abs_im_le_norm _\n _ ≤ 5 / 2 := by rw [add_sub_cancel_left]; exact hw'\n rw [show (discCenter t + (5 / 2 : ℂ) * w - discCenter t) = (5 / 2 : ℂ) * w by ring] at h1\n rw [h] at him\n simp at him -- him : (1:ℂ).im = t + (5/2)*w.im; (1:ℂ).im = 0\n -- |t + (5/2) w.im| ≥ |t| − (5/2)|w.im| ≥ 10 − 5/2 = 15/2 > 0\n have hwim : |w.im| ≤ 1 := (abs_im_le_norm _).trans hw\n have : |t + (5 / 2) * w.im| ≥ 15 / 2 := by\n have h2 : |t + (5 / 2) * w.im| ≥ |t| - |(5 / 2) * w.im| := by\n have h3 : |t| ≤ |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by\n calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf\n _ ≤ |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _\n _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]\n linarith [h3]\n have h4 : |(5 / 2) * w.im| ≤ 5 / 2 := by\n rw [abs_mul, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5/2)]\n calc (5 / 2) * |w.im| ≤ (5 / 2) * 1 := by\n apply mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h2, h4, ht]\n rw [him] at this\n norm_num at this\n -- ζ analytic at the point\n have hζ : AnalyticAt ℂ riemannZeta (discCenter t + (5 / 2 : ℂ) * w) := by\n have hd := differentiableAt_riemannZeta hne\n -- DifferentiableAt at a point doesn't give AnalyticAt directly; use the\n -- neighborhood differentiability on {z ≠ 1}.\n have hU : {z : ℂ | z ≠ 1} ∈ 𝓝 (discCenter t + (5 / 2 : ℂ) * w) :=\n isOpen_compl_singleton.mem_nhds hne\n exact ((HolomorphicOn_riemannZeta.mono (Set.subset_univ _) |>.analyticOnNhd\n isOpen_compl_singleton) _ hU ... )\n sorry\n\nend NguyenRH1\n\nend","new_string":"/-- ζ is analytic on neighborhoods of every point ≠ 1. -/\ntheorem analyticAt_riemannZeta_of_ne_one {z : ℂ} (hz : z ≠ 1) :\n AnalyticAt ℂ riemannZeta z :=\n (HolomorphicOn_riemannZeta.analyticOnNhd isOpen_compl_singleton) z hz\n\n/-- F is analytic on the closed unit disc (ζ is analytic on B(s₀, 5/2),\nwhich avoids the pole at 1 since |t| ≥ 10 ⟹ |im| ≥ 15/2). -/\ntheorem scaledZeta_analytic {t : ℝ} (ht : 10 ≤ |t|) :\n AnalyticOnNhd ℂ (scaledZeta t) (Metric.closedBall 0 1) := by\n intro w hw\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n have hw' : ‖(5 / 2 : ℂ) * w‖ ≤ 5 / 2 := by\n rw [norm_mul, show ‖(5 / 2 : ℂ)‖ = 5 / 2 by norm_num [Complex.norm_ofNat, Complex.norm_two]]\n exact mul_le_mul_of_nonneg_left hw (by norm_num)\n -- the evaluation point is not 1 (its imaginary part is large)\n have hne : discCenter t + (5 / 2 : ℂ) * w ≠ 1 := by\n intro h\n have hwim : |w.im| ≤ 1 := (abs_im_le_norm _).trans hw\n have him : (discCenter t + (5 / 2 : ℂ) * w).im = t + (5 / 2) * w.im := by\n simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]\n have hbig : 15 / 2 ≤ |t + (5 / 2) * w.im| := by\n have h2 : |t| ≤ |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by\n calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf\n _ ≤ |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _\n _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]\n have h4 : |(5 / 2) * w.im| ≤ 5 / 2 := by\n rw [abs_mul, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]\n calc (5 / 2) * |w.im| ≤ (5 / 2) * 1 :=\n mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h2, h4, ht]\n rw [h] at him\n rw [Complex.one_im] at him\n rw [him] at hbig\n norm_num at hbig\n have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w :=\n analyticAt_const.add (analyticAt_const.mul analyticAt_id)\n exact ((analyticAt_riemannZeta_of_ne_one hne).comp haff).div analyticAt_const\n (by\n intro h0\n have h := RvM.zeta_lower_bound_two t\n rw [h0, norm_zero] at h\n norm_num at h)\n\nend NguyenRH1\n\nend"},"extra_content":null}]