← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (5694 chars)
There's `analyticOrderAt_smul` (order additive under scalar mul) and `analyticOrderAt_mul_eq_top_of_left` at 490 — so there's likely `analyticOrderAt_mul` nearby. For the constant multiple: analyticOrderAt (c * f) = analyticOrderAt (const c) + analyticOrderAt f = 0 + order f (const nonzero ⟹ order 0 via analyticOrderAt_eq_zero: `analyticOrderAt_eq_zero : analyticOrderAt f z₀ = 0 ↔ f z₀ ≠ 0`? something like that).
And for the affine comp — no direct lemma. So per-point: analyticOrderAt (fun w => ζ(aff w)) w₀ = analyticOrderAt ζ (aff w₀) via the normal form. Let me just build it via `AnalyticAt.analyticOrderAt_eq_natCast` (the characterization: order = n ⟺ ∃ g analytic, g(z₀) ≠ 0, f =ᶠ (z−z₀)^n • g):
Forward: given ζ =ᶠ[𝓝 z₀'] (z − z₀')^m • h with h analytic, h z₀' ≠ 0 (from the ζ-side factorization): then ζ(aff w) = (aff w − z₀')^m • h(aff w) with aff w₀ = z₀' (z₀' := aff w₀ = s₀ + (5/2)w₀): aff w − aff w₀ = (5/2)(w − w₀): so ζ(aff w) = ((5/2)(w−w₀))^m · h(aff w) = (w−w₀)^m • [(5/2)^m · h(aff w)] near w₀: the cofactor g'(w) := (5/2)^m · h(aff w) analytic at w₀ (h analytic at aff w₀ + aff) and g'(w₀) = (5/2)^m·h(z₀') ≠ 0 ✓ (5/2 ≠ 0). So analyticOrderAt (ζ∘aff) w₀ = analyticOrderAt ζ (aff w₀) — both equal m... wait the characterization gives order = m from the existence ✓. And the reverse direction isn't needed (I have the ζ-side order m from its factorization; the F-side order equals m by exhibiting the factorization).
Formally:
```lean
theorem analyticOrderAt_riemannZeta_affine {t : ℝ} (w₀ : ℂ) :
analyticOrderAt (fun w => riemannZeta (discCenter t + (5/2 : ℂ) * w)) w₀
= analyticOrderAt riemannZeta (discCenter t + (5/2 : ℂ) * w₀) := by
by_cases htop : analyticOrderAt riemannZeta (discCenter t + (5/2:ℂ)*w₀) = ⊤
· -- both ⊤: the comp order is ⊤ iff... (if ζ locally zero at the point then ζ∘aff locally zero)
sorry
· obtain ⟨h', h1, h2, h3⟩ := (analyticAt_riemannZeta_of_ne_one ?_).analyticOrderAt_ne_top.mp htop
-- h3 : ζ =ᶠ[𝓝 z₀'] fun z => (z − z₀')^m • h' z with m = analyticOrderNatAt ζ z₀'
...
```
Hmm wait — analyticOrderAt = ⊤ means ζ locally identically zero — impossible for ζ (not identically zero; analyticity + identity principle). So the ⊤ case is excluded: analyticOrderAt ζ z ≠ ⊤ for all z ≠ 1 (LiSides' zeta_order_ne_top_of_ne ✓ EXISTS — from ii′-1b!). So the order is always finite. Good:
```lean
theorem analyticOrderNatAt_riemannZeta_affine {t : ℝ} (w₀ : ℂ) :
analyticOrderNatAt (fun w => riemannZeta (discCenter t + (5/2 : ℂ) * w)) w₀
= analyticOrderNatAt riemannZeta (discCenter t + (5/2 : ℂ) * w₀) := by
set z₀ := discCenter t + (5/2 : ℂ) * w₀
-- ζ ≠ 1-point? z₀ could be 1?? — z₀ = s₀ + (5/2)w₀ — for general w₀, z₀ could be 1! The affine invariance only needed for w₀ in the unit ball — where z₀ is in the 5/2-disc, ≠ 1 ✓ (from hne-style argument with ht). Add hypothesis.
```
Right — need (ht : 10 ≤ |t|) and ‖w₀‖ ≤ 1 (so z₀ ≠ 1). Let me include those.
The proof via analyticOrderNatAt: use `Nat.cast_analyticOrderNatAt (hf' : analyticOrderAt f z₀ ≠ ⊤)`?? from the smul proof: `Nat.cast_analyticOrderNatAt hf' : (analyticOrderNatAt f z₀ : ℕ∞) = analyticOrderAt f z₀`? — so it suffices to show the analyticOrderAt versions equal as ℕ∞, via the natCast characterization on both sides with the same m and transferred cofactor:
```lean
-- from the ζ-side: ζ =ᶠ[𝓝 z₀] (z − z₀)^m • h' with h' analytic, h' z₀ ≠ 0, m = analyticOrderNatAt ζ z₀
obtain ⟨h', h1, h2, h3⟩ := (analyticAt_riemannZeta_of_ne_one hz₀ne).analyticOrderAt_ne_top.mp
(zeta_order_ne_top_of_ne hz₀ne) -- from LiSides ✓
-- transfer to w-side:
have hF : (fun w => riemannZeta (discCenter t + (5/2 : ℂ) * w)) =ᶠ[𝓝 w₀]
fun w => (w - w₀) ^ analyticOrderNatAt riemannZeta z₀ • (((5/2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) * h' (discCenter t + (5/2 : ℂ) * w)) := by
-- from h3 via the affine map's tendsto: eventuallyEq pullback
...
-- then analyticOrderAt F w₀ = m via the natCast characterization, with the cofactor analytic and nonvanishing
...
```
The eventuallyEq pullback: h3 : ζ =ᶠ[𝓝 z₀] (fun z => (z−z₀)^m • h' z) — I need ζ∘aff =ᶠ[𝓝 w₀] ((·−w₀)^m • g') — via `Filter.EventuallyEq.comp_tendsto`? — there's `EventuallyEq.comp_tendsto (h : f =ᶠ[l'] g) (ht : Tendsto φ l l') : f ∘ φ =ᶠ[l] g ∘ φ`? something like `Filter.EventuallyEq.comp_tendsto` ✓ exists. With φ = aff, Tendsto aff (𝓝 w₀) (𝓝 z₀) ✓ (aff continuous). Then the pointwise: (aff w − aff w₀)^m • h'(aff w) = ((5/2)(w−w₀))^m • h'(aff w) = (w−w₀)^m • ((5/2)^m·h'(aff w)) via smul algebra (mul_pow, smul_smul) — the congr of eventuallyEq with the pointwise identity ✓.
Then the cofactor g'(w) = (5/2)^m · h'(aff w): analytic at w₀ (h1 : AnalyticAt h' z₀, aff analytic, comp_of_eq); g'(w₀) = (5/2)^m · h'(z₀) ≠ 0 ✓ (pow_ne_zero + h2).
Then analyticOrderAt F w₀ = ↑m via (hF_an.analyticOrderAt_eq_natCast).mpr ⟨g', g'_an, g'_ne, hF-transferred⟩ and the ζ-side = ↑m via Nat.cast_analyticOrderNatAt — concluding analyticOrderNatAt F w₀ = analyticOrderNatAt ζ z₀ via ENat.natCast_inj.
This is all standard-but-fiddly. OK — I'm now deep into a long build. Let me continue writing §2's remainder. But first — given how long this is getting, let me reconsider scope for the current work session. The user is engaged and wants progress. The sub-stage rule says commit at clean boundaries. §1 committed. §2 partial (scaledZeta_analytic + scaledZeta_zero green). Let me finish §2's count+gap and commit, which is a natural boundary. The order-invariance lemma is part of the count.
Let me write the remainder of §2 now — the finiteness, the affine order invariance, the ZerosBound application, the R-gap. This is a big chunk; write it and iterate.
The API is clear (`analyticOrderAt_smul`, the natCast characterization, LiSides' `zeta_order_ne_top_of_ne`). Writing the rest of §2: order-invariance under the affine map, finiteness, the Jensen count, and the R-gap.
tool: Edit ok
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
"old_string": "end NguyenRH1\n\nend",
"new_string": "/-- The order of \u03b6 is invariant under the affine change of variable\nw \u21a6 s\u2080 + (5/2)\u00b7w (nonzero slope), valid for \u2016w\u2080\u2016 \u2264 1 (so the target\navoids the pole at 1). -/\ntheorem analyticOrderNatAt_riemannZeta_affine {t : \u211d} (ht : 10 \u2264 |t|) {w\u2080 : \u2102}\n (hw\u2080 : \u2016w\u2080\u2016 \u2264 1) :\n analyticOrderNatAt (fun w => riemannZeta (discCenter t + (5 / 2 : \u2102) * w)) w\u2080\n = analyticOrderNatAt riemannZeta (discCenter t + (5 / 2 : \u2102) * w\u2080) := by\n set z\u2080 := discCenter t + (5 / 2 : \u2102) * w\u2080 with hz\u2080\n -- z\u2080 avoids 1 (its imaginary part is large)\n have hz\u2080ne : z\u2080 \u2260 1 := by\n intro h\n have hwim : |w\u2080.im| \u2264 1 := (abs_im_le_norm _).trans hw\u2080\n have him : z\u2080.im = t + (5 / 2) * w\u2080.im := by\n simp [hz\u2080, discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]\n have hbig : 15 / 2 \u2264 |t + (5 / 2) * w\u2080.im| := by\n have h3 := abs_add_le (t + (5 / 2) * w\u2080.im) (-((5 / 2) * w\u2080.im))\n rw [abs_neg, add_neg_cancel_right] at h3\n have h4 : |(5 / 2) * w\u2080.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\u2080.im| \u2264 (5 / 2) * 1 :=\n mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h3, h4, ht]\n rw [h] at him\n rw [Complex.one_im] at him\n rw [\u2190 him] at hbig\n norm_num at hbig\n obtain \u27e8h', h1, h2, h3\u27e9 := (analyticAt_riemannZeta_of_ne_one hz\u2080ne).analyticOrderAt_ne_top.mp\n (zeta_order_ne_top_of_ne hz\u2080ne)\n -- transfer the factorization to the w-side\n have haff : AnalyticAt \u2102 (fun w : \u2102 => discCenter t + (5 / 2 : \u2102) * w) w\u2080 :=\n analyticAt_const.add (analyticAt_const.mul analyticAt_id)\n have haffT : Tendsto (fun w : \u2102 => discCenter t + (5 / 2 : \u2102) * w) (\ud835\udcdd w\u2080) (\ud835\udcdd z\u2080) :=\n haff.continuousAt\n have h3' := h3.comp_tendsto haffT\n -- h3' : (fun z => (z \u2212 z\u2080)^m \u2022 h' z) \u2218 aff =\u1da0 \u03b6 \u2218 aff; massage the form\n have hF : (fun w => riemannZeta (discCenter t + (5 / 2 : \u2102) * w)) =\u1da0[\ud835\udcdd w\u2080]\n fun w => (w - w\u2080) ^ analyticOrderNatAt riemannZeta z\u2080 \u2022\n (((5 / 2 : \u2102) ^ analyticOrderNatAt riemannZeta z\u2080) *\n h' (discCenter t + (5 / 2 : \u2102) * w)) := by\n apply h3'.congr'\n filter_upwards with w\n simp only [Function.comp_apply]\n rw [show discCenter t + (5 / 2 : \u2102) * w - z\u2080 = (5 / 2 : \u2102) * (w - w\u2080) by rw [hz\u2080]; ring]\n rw [mul_pow, smul_eq_mul, smul_eq_mul]\n ring\n have hcof : AnalyticAt \u2102 (fun w => ((5 / 2 : \u2102) ^ analyticOrderNatAt riemannZeta z\u2080) *\n h' (discCenter t + (5 / 2 : \u2102) * w)) w\u2080 :=\n (analyticAt_const.mul (h1.comp_of_eq haff rfl)) -- hmm h1 is AnalyticAt h' z\u2080\n have hcof_ne : ((5 / 2 : \u2102) ^ analyticOrderNatAt riemannZeta z\u2080) * h' z\u2080 \u2260 0 :=\n mul_ne_zero (pow_ne_zero _ (by norm_num)) h2\n have hF_an : AnalyticAt \u2102 (fun w => riemannZeta (discCenter t + (5 / 2 : \u2102) * w)) w\u2080 :=\n analyticAt_riemannZeta_of_ne_one hz\u2080ne |>.comp_of_eq haff rfl\n have horder : analyticOrderAt (fun w => riemannZeta (discCenter t + (5 / 2 : \u2102) * w)) w\u2080\n = (analyticOrderNatAt riemannZeta z\u2080 : \u2115\u221e) :=\n (hF_an.analyticOrderAt_eq_natCast).mpr \u27e8_, hcof, hcof_ne, hF\u27e9\n rw [\u2190 Nat.cast_inj (R := \u2115\u221e), Nat.cast_analyticOrderNatAt\n (zeta_order_ne_top_of_ne hz\u2080ne), horder]\n\n/-! ## 3. The Jensen count and the R-gap -/\n\n/-- Zeros of the scaled function F in the closed unit ball are finite. -/\ntheorem scaledZeta_zeros_finite {t : \u211d} (ht : 10 \u2264 |t|) :\n (SetOfZeros 1 (scaledZeta t)).Finite := by\n have hz0 : riemannZeta (discCenter t) \u2260 0 := by\n have h := RvM.zeta_lower_bound_two t\n intro h0\n rw [\u2190 show discCenter t = 2 + t * Complex.I from rfl, h0, norm_zero] at h\n norm_num at h\n -- SetOfZeros 1 F = the affine preimage of the \u03b6-zeros in the 5/2-disc\n have hsub : SetOfZeros 1 (scaledZeta t) \u2286\n (fun w => discCenter t + (5 / 2 : \u2102) * w) \u207b\u00b9'\n (Metric.closedBall (discCenter t) (5 / 2) \u2229 riemannZetaZeros) := by\n intro w hw\n simp only [SetOfZeros, Set.mem_setOf_eq] at hw\n have hFw : riemannZeta (discCenter t + (5 / 2 : \u2102) * w) = 0 := by\n have := hw.2\n unfold scaledZeta at this\n exact (div_eq_zero_iff.mp this).1 -- hmm div_eq_zero_iff : a/b = 0 \u2194 a = 0 \u2228 b = 0; need a = 0 from b \u2260 0\n constructor\n \u00b7 rw [Metric.mem_closedBall, Complex.dist_eq]\n rw [add_sub_cancel_left]\n calc \u2016(5 / 2 : \u2102) * w\u2016 \u2264 (5 / 2) * \u2016w\u2016 := by\n rw [norm_mul]\n have hn : \u2016(5 / 2 : \u2102)\u2016 = 5 / 2 := by\n rw [show (5 / 2 : \u2102) = ((5 / 2 : \u211d) : \u2102) by norm_num, Complex.norm_real,\n Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5 / 2)]\n rw [hn]\n _ \u2264 (5 / 2) * 1 := mul_le_mul_of_nonneg_left hw.1 (by norm_num)\n _ = 5 / 2 := by norm_num\n \u00b7 exact mem_riemannZetaZeros.mpr hFw\n exact ((isCompact_closedBall _ _).inter_riemannZetaZeros_finite).subset\n ... -- hmm need preimage-finite\n sorry\n\nend NguyenRH1\n\nend"
}
result 2026-08-22 20:08:41Z → 2026-08-23 19:06:15Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
"oldString": " have h2 := Real.exp_one_lt_d9.le\n have h3 : (Real.exp 1) ^ 5 \u2264 (2.718281829 : \u211d) ^ 5 :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5\n have h4 : (2.718281829 : \u211d) ^ 5 \u2264 200 := by norm_num\n linarith [h1, h3, h4]\n have hlog2 := log_two_le_one\n have hA0 : (0 : \u211d) \u2264 4 * A0count / X := by positivity",
"newString": " have h2 := Real.exp_one_lt_d9.le\n have h3 : (Real.exp 1) ^ 5 \u2264 (2.7182818286 : \u211d) ^ 5 :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5\n have h4 : (2.7182818286 : \u211d) ^ 5 \u2264 200 := by norm_num\n linarith [h1, h3, h4]\n have hlog2 := log_two_le_one\n have hA0 : (0 : \u211d) \u2264 4 * A0count / X :=\n div_nonneg (mul_nonneg (by norm_num) A0count_pos.le) hX0.le",
"originalFile": "/-\nNguyenRH1/LiCircleBound.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-v (D-068 \u00a75):\nthe circle bound for the partial-fraction difference and the squeeze to\nthe capstone identity.\n\n\u00a70: conjugate symmetry of the nontrivial zeros (for the lower-half\n circle arcs).\n\u00a71: the mult-weighted ordinate-window count bridges from Zeta23's RvM\n local count (`zeta_local_zero_count`: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3)\n with multiplicity, ALL t \u2014 no perimeter): `A0count` + the dyadic\n interval count `Ncount_le_of_interval`.\n\u00a72: the Dirichlet bound `norm_logDeriv_zeta_le_dirichlet` (\u2016\u03b6\u2032/\u03b6 s\u2016 \u2264\n dirichletC2 for re s \u2265 2; \u2212\u03b6\u2032/\u03b6 = LSeries \u039b, termwise \u2264 the s = 2\n majorant) \u2014 the right near-axis arc input.\n\u00a73+: (this file, subsequent sub-stages) the series bound, the logDeriv\n assembly, the Fexpr circle bound, the Schwarz squeeze, and the\n capstone `partialFraction_identity`.\n\nArchive references: D-068 \u00a75, journal-029.\n-/\nimport Mathlib\nimport Zeta23.RvM.LocalCount\nimport NguyenRH1.LiFEntire\nimport NguyenRH1.LiGapCircles\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. Conjugate symmetry -/\n\n/-- The conjugate of a nontrivial zero is a nontrivial zero. -/\nlemma isNontrivialZero_conj {\u03c1 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1) :\n IsNontrivialZero ((starRingEnd \u2102) \u03c1) := by\n refine \u27e8?_, ?_, ?_\u27e9\n \u00b7 rw [_root_.riemannZeta_conj, h\u03c1.1, map_zero]\n \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.1\n \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.2\n\n/-! ## 1. The mult-weighted window count bridges -/\n\n/-- The local-count constant: from Zeta23's RvM local count\n(`zeta_local_zero_count`, [Tit86 Thm 9.2] \u2014 mult-weighted, two-sided,\nall t, PROVED unconditionally in Zeta23). -/\ndef A0count : \u211d := Classical.choose Zeta23.RvM.zeta_local_zero_count\n\nlemma A0count_ge_one : (1 : \u211d) \u2264 A0count :=\n (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).1\n\nlemma A0count_pos : (0 : \u211d) < A0count := lt_of_lt_of_le one_pos A0count_ge_one\n\n/-- The unit-window bound: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3). -/\nlemma Ncount_window_le (t : \u211d) :\n (Zeta23.Ncount t (t + 1) : \u211d) \u2264 A0count * Real.log (|t| + 3) :=\n (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).2 t\n\n/-- Window additivity: Ncount(a, c] = Ncount(a, b] + Ncount(b, c] for\na \u2264 b \u2264 c (the disjoint union of the ordinate windows). -/\nlemma Ncount_add_of_le {a b c : \u211d} (hab : a \u2264 b) (hbc : b \u2264 c) :\n Zeta23.Ncount a c = Zeta23.Ncount a b + Zeta23.Ncount b c := by\n have hunion : Zeta23.zerosIn a c = Zeta23.zerosIn a b \u222a Zeta23.zerosIn b c := by\n ext \u03c1\n constructor\n \u00b7 intro h\u03c1c\n obtain \u27e8h\u03c1, ha, hc\u27e9 := h\u03c1c\n rcases le_or_gt \u03c1.im b with h | h\n \u00b7 exact Set.mem_union_left _ \u27e8h\u03c1, ha, h\u27e9\n \u00b7 exact Set.mem_union_right _ \u27e8h\u03c1, h, hc\u27e9\n \u00b7 intro h\n rcases h with h\u03c1b | h\u03c1c\n \u00b7 obtain \u27e8h\u03c1, ha, hb\u27e9 := h\u03c1b\n exact \u27e8h\u03c1, ha, hb.trans hbc\u27e9\n \u00b7 obtain \u27e8h\u03c1, hb, hc\u27e9 := h\u03c1c\n exact \u27e8h\u03c1, hab.trans_lt hb, hc\u27e9\n have hdisj : Disjoint (Zeta23.zerosIn a b) (Zeta23.zerosIn b c) := by\n rw [Set.disjoint_iff]\n intro \u03c1 \u27e8h1, h2\u27e9\n exact absurd (h1.2.2.trans_lt h2.2.1) (lt_irrefl \u03c1.im)\n rw [Zeta23.Ncount, Zeta23.Ncount, Zeta23.Ncount, hunion]\n exact_mod_cast finsum_mem_union hdisj (Zeta23.zerosIn_finite a b)\n (Zeta23.zerosIn_finite b c)\n\n/-- The N-step unit-window chain: Ncount(a, a+N] \u2264 A\u2080\u00b7N\u00b7log(|a|+N+3). -/\nlemma Ncount_chain_le (a : \u211d) (N : \u2115) :\n (Zeta23.Ncount a (a + (N : \u211d)) : \u211d)\n \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := by\n induction N with\n | zero =>\n simp only [Nat.cast_zero, add_zero]\n have h0 : Zeta23.zerosIn a a = \u2205 := by\n ext \u03c1\n constructor\n \u00b7 intro h\n obtain \u27e8-, h1, h2\u27e9 := h\n exact absurd (h2.trans_lt h1) (lt_irrefl _)\n \u00b7 intro h\n simp at h\n have hz : Zeta23.Ncount a a = 0 := by\n simp only [Zeta23.Ncount, h0, finsum_mem_empty]\n rw [hz, Nat.cast_zero]\n simp\n | succ N ih =>\n have hN0 : (0 : \u211d) \u2264 (N : \u211d) := Nat.cast_nonneg N\n have hsplit : Zeta23.Ncount a (a + (N : \u211d) + 1)\n = Zeta23.Ncount a (a + (N : \u211d)) + Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1) :=\n Ncount_add_of_le (a := a) (b := a + (N : \u211d)) (c := a + (N : \u211d) + 1)\n (by linarith) (by linarith)\n have hcast : a + ((N + 1 : \u2115) : \u211d) = a + (N : \u211d) + 1 := by push_cast; ring\n rw [hcast, hsplit]\n have hwin := Ncount_window_le (a + (N : \u211d))\n have hlog : Real.log (|a + (N : \u211d)| + 3) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n apply Real.log_le_log (by positivity)\n have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n linarith\n have hlogpos : (0 : \u211d) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n apply Real.log_nonneg\n have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n linarith [hN0]\n have hlogpos' : (0 : \u211d) \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n apply Real.log_nonneg\n have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n linarith [hN0]\n push_cast\n -- goal: \u2191(Ncount a (a+\u2191N)) + \u2191(Ncount (a+\u2191N) (a+\u2191N+1)) \u2264 A\u2080(\u2191N+1)\u00b7log(|a|+(\u2191N+1)+3)\n have hlogC : Real.log (|a| + (N : \u211d) + 3)\n \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n Real.log_le_log (by positivity) (by linarith)\n have hle1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n mul_le_mul_of_nonneg_left hlogC (mul_nonneg A0count_pos.le hN0)\n have hle2 : A0count * Real.log (|a + (N : \u211d)| + 3)\n \u2264 A0count * Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n apply mul_le_mul_of_nonneg_left _ A0count_pos.le\n apply Real.log_le_log (by positivity)\n have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n linarith\n have hsum : \u2191(Zeta23.Ncount a (a + (N : \u211d))) + \u2191(Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1))\n \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n + A0count * Real.log (|a + (N : \u211d)| + 3) :=\n add_le_add ih hwin\n linarith [hsum, hle1, hle2]\n\n/-- The dyadic-interval count: Ncount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(b+4) for\n0 \u2264 a \u2264 b (the unit-window chain + the ceil cover). -/\nlemma Ncount_le_of_interval {a b : \u211d} (ha : 0 \u2264 a) (hab : a \u2264 b) :\n (Zeta23.Ncount a b : \u211d) \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n set N : \u2115 := \u2308b - a\u2309\u208a with hN\n have hNb : b \u2264 a + (N : \u211d) := by\n have h := Nat.le_ceil (b - a)\n rw [\u2190 hN] at h\n have h2 : (b - a : \u211d) \u2264 (N : \u211d) := h\n linarith\n have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, h\u03c1.2.1, ?_\u27e9\n exact h\u03c1.2.2.trans hNb\n have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n rw [Zeta23.Ncount, Zeta23.Ncount]\n rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n apply Finset.sum_le_sum_of_subset_of_nonneg\n \u00b7 intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n exact hsub h\u03c1\n \u00b7 intro \u03c1 _ _\n exact Nat.cast_nonneg _\n have hchain := Ncount_chain_le a N\n have hNle : (N : \u211d) \u2264 b - a + 1 := by\n have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n rw [\u2190 hN] at h\n have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n linarith\n have hlogle : Real.log (|a| + (N : \u211d) + 3) \u2264 Real.log (b + 4) := by\n apply Real.log_le_log (by positivity)\n rw [abs_of_nonneg ha]\n linarith\n calc (Zeta23.Ncount a b : \u211d)\n \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n _ \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n have hlogpos : (0 : \u211d) \u2264 Real.log (b + 4) := by\n apply Real.log_nonneg; linarith\n have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (b + 4) :=\n mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n have h2 : A0count * (N : \u211d) * Real.log (b + 4)\n \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n apply mul_le_mul_of_nonneg_right _ hlogpos\n nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n exact h1.trans h2\n\n/-! ## 2. The Dirichlet bound -/\n\n/-- The Dirichlet majorant constant: the absolute sum of the von\nMangoldt L-series terms at s = 2 (summable since 2 > 1). -/\ndef dirichletC2 : \u211d :=\n \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 C\u2082 for re s \u2265 2 (the Dirichlet-series majorant:\n\u2212\u03b6\u2032/\u03b6 = LSeries \u039b for re > 1, termwise \u2264 the s = 2 sum). -/\nlemma norm_logDeriv_zeta_le_dirichlet {s : \u2102} (hs : 2 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC2 := by\n have hs1 : (1 : \u211d) < s.re := by linarith\n have h1 : -logDeriv riemannZeta s\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n \u2264 dirichletC2 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n simp\n exact hs) n) hsumS hsum2\n _ = dirichletC2 := rfl\n calc \u2016logDeriv riemannZeta s\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 dirichletC2 := hle\n\n/-! ## 3. The tsum split + the generalized interval count + the low-zero\nconstant -/\n\n/-- Splitting a summable real tsum over a finset:\n\u2211' f = \u2211_{i \u2208 s} f i + \u2211' (if i \u2208 s then 0 else f i). -/\nlemma tsum_split_finset {\u03b9 : Type*} [DecidableEq \u03b9] {f : \u03b9 \u2192 \u211d} (hf : Summable f)\n (s : Finset \u03b9) :\n \u2211' i, f i = \u2211 i \u2208 s, f i + \u2211' i, (if i \u2208 s then 0 else f i) := by\n classical\n have h1 : Summable (fun i => if i \u2208 s then f i else 0) := by\n apply Summable.of_norm_bounded hf.norm\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n have h2 : Summable (fun i => if i \u2208 s then 0 else f i) := by\n apply Summable.of_norm_bounded hf.norm\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n have h3 : \u2211' i, f i\n = \u2211' i, ((if i \u2208 s then f i else 0) + (if i \u2208 s then 0 else f i)) := by\n apply tsum_congr\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n rw [h3, Summable.tsum_add h1 h2]\n congr 1\n rw [tsum_eq_sum (s := s) (fun b hb => if_neg hb)]\n exact Finset.sum_congr rfl (fun b hb => if_pos hb)\n\n/-- The generalized dyadic-interval count (both signs):\nNcount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(3\u00b7max|a||b| + 5). -/\nlemma Ncount_le_of_interval_gen {a b : \u211d} (hab : a \u2264 b) :\n (Zeta23.Ncount a b : \u211d)\n \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n set N : \u2115 := \u2308b - a\u2309\u208a with hN\n have hNb : b \u2264 a + (N : \u211d) := by\n have h := Nat.le_ceil (b - a)\n rw [\u2190 hN] at h\n linarith\n have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n intro \u03c1 h\u03c1\n exact \u27e8h\u03c1.1, h\u03c1.2.1, h\u03c1.2.2.trans hNb\u27e9\n have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n rw [Zeta23.Ncount, Zeta23.Ncount]\n rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n apply Finset.sum_le_sum_of_subset_of_nonneg\n \u00b7 intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n exact hsub h\u03c1\n \u00b7 intro \u03c1 _ _\n exact Nat.cast_nonneg _\n have hchain := Ncount_chain_le a N\n have hNle : (N : \u211d) \u2264 b - a + 1 := by\n have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n rw [\u2190 hN] at h\n have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n linarith\n have hlogle : Real.log (|a| + (N : \u211d) + 3)\n \u2264 Real.log (3 * max |a| |b| + 5) := by\n apply Real.log_le_log (by positivity)\n have hM1 : |a| \u2264 max |a| |b| := le_max_left _ _\n have hM2 : |b| \u2264 max |a| |b| := le_max_right _ _\n have hba : b - a \u2264 |b| + |a| := by\n have h1 := le_abs_self b\n have h2 : -a \u2264 |a| := by rw [\u2190 abs_neg a]; exact le_abs_self (-a)\n linarith\n nlinarith [hNle, hM1, hM2, hba, abs_nonneg a, abs_nonneg b]\n have hlogpos : (0 : \u211d) \u2264 Real.log (3 * max |a| |b| + 5) := by\n apply Real.log_nonneg\n have h1 : (0 : \u211d) \u2264 max |a| |b| := le_trans (abs_nonneg a) (le_max_left _ _)\n linarith\n calc (Zeta23.Ncount a b : \u211d)\n \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n _ \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5) :=\n mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n have h2 : A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5)\n \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n apply mul_le_mul_of_nonneg_right _ hlogpos\n nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n exact h1.trans h2\n\n/-- The low-zero finset: nontrivial zeros with \u2016\u03c1\u2016 \u2264 3. -/\ndef lowZeros : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} :=\n (show {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | \u2016(\u03c1 : \u2102)\u2016 \u2264 3}.Finite from\n (finite_subtype_norm_lt 4).subset\n (fun \u03c1 h\u03c1 => lt_of_le_of_lt (show \u2016(\u03c1 : \u2102)\u2016 \u2264 3 from h\u03c1) (by norm_num))).toFinset\n\n/-- The low-zero symbolic constant (a fixed finite sum of fixed positive\nreals; \u2016\u03c1\u2016 > 0 for nontrivial \u03c1 since re \u03c1 > 0). -/\ndef lowZeroConst : \u211d :=\n \u2211 \u03c1 \u2208 lowZeros, (zeroMult (\u03c1 : \u2102) : \u211d) * (1 + 1 / \u2016(\u03c1 : \u2102)\u2016)\n\nlemma lowZeroConst_nonneg : 0 \u2264 lowZeroConst :=\n Finset.sum_nonneg fun _\u03c1 _ => mul_nonneg (Nat.cast_nonneg _)\n (add_nonneg one_pos.le (div_nonneg one_pos.le (norm_nonneg _)))\n\n/-! ## 4. The far-tail bound -/\n\n/-- The dyadic log series closed form:\n\u2211' j, ((j+4)\u00b7log 2 + log X)/2^j = 10\u00b7log 2 + 2\u00b7log X. -/\nlemma tsum_dyadic_log (X : \u211d) :\n \u2211' j : \u2115, ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j\n = 10 * Real.log 2 + 2 * Real.log X := by\n have hgeom2H : Summable (fun j : \u2115 => ((1 : \u211d) / 2) ^ j) := summable_geometric_two\n have hgeom2 : \u2211' j : \u2115, ((1 : \u211d) / 2) ^ j = 2 := tsum_geometric_two\n have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\n have hlin : \u2211' j : \u2115, (j : \u211d) * ((1 : \u211d) / 2) ^ j = 2 := by\n have h := hlinH.tsum_eq\n norm_num at h\n exact h\n have hsplit : (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n = fun j : \u2115 => Real.log 2 * ((j : \u211d) * ((1 : \u211d) / 2) ^ j)\n + (4 * Real.log 2 + Real.log X) * ((1 : \u211d) / 2) ^ j := by\n funext j\n have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n field_simp\n ring\n rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.summable.mul_left _)]\n rw [tsum_mul_left, tsum_mul_left, hlin, hgeom2]\n ring\n\n/-- log 2 \u2264 1 (since 2 \u2264 e). -/\nlemma log_two_le_one : Real.log 2 \u2264 1 := by\n rw [show (1 : \u211d) = Real.log (Real.exp 1) by rw [Real.log_exp]]\n apply Real.log_le_log (by norm_num)\n have h := Real.exp_one_gt_d9\n linarith\n\n/-- For X \u2265 200: (4A\u2080/X)\u00b7(10\u00b7log 2 + 2\u00b7log X) \u2264 16\u00b7A\u2080\u00b7log X / X. -/\nlemma dyadic_tail_constant {X : \u211d} (hX : 200 \u2264 X) :\n (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n \u2264 16 * A0count * Real.log X / X := by\n have hX0 : (0 : \u211d) < X := by linarith\n have hlogX : 5 \u2264 Real.log X := by\n rw [show (5 : \u211d) = Real.log (Real.exp 5) by rw [Real.log_exp]]\n apply Real.log_le_log (Real.exp_pos _)\n have h1 : Real.exp 5 = (Real.exp 1) ^ 5 := by\n rw [\u2190 Real.exp_nat_mul]\n norm_num\n have h2 := Real.exp_one_lt_d9.le\n have h3 : (Real.exp 1) ^ 5 \u2264 (2.718281829 : \u211d) ^ 5 :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5\n have h4 : (2.718281829 : \u211d) ^ 5 \u2264 200 := by norm_num\n linarith [h1, h3, h4]\n have hlog2 := log_two_le_one\n have hA0 : (0 : \u211d) \u2264 4 * A0count / X := by positivity\n have h1 : 10 * Real.log 2 + 2 * Real.log X \u2264 4 * Real.log X := by linarith\n calc (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n \u2264 (4 * A0count / X) * (4 * Real.log X) := mul_le_mul_of_nonneg_left h1 hA0\n _ = 16 * A0count * Real.log X / X := by ring\n\n/-- The dyadic class of a zero relative to scale X:\nNat.log 2 \u230a|im \u03c1|/X\u230b\u208a, so 2^j\u00b7X \u2264 |im \u03c1| < 2^{j+1}\u00b7X when |im \u03c1| \u2265 X. -/\ndef dyadClass (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2115 :=\n Nat.log 2 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a\n\nlemma dyadClass_lower {X : \u211d} (hX : 0 < X) {\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}}\n (h\u03c1 : X \u2264 |(\u03c1 : \u2102).im|) :\n (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 |(\u03c1 : \u2102).im| := by\n have hfl : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a \u2260 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n have h1 : (1 : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := (le_div_iff\u2080 hX).mpr (by linarith)\n linarith\n have h2 := Nat.pow_log_le_self 2 hfl\n have h3 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a := by exact_mod_cast h2\n have h4 : (\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := Nat.floor_le (by positivity)\n have h5 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) = (2 : \u211d) ^ dyadClass X \u03c1 := by push_cast; ring\n rw [h5] at h3\n rw [le_div_iff\u2080 hX] at h4\n linarith\n\nlemma dyadClass_upper {X : \u211d} (hX : 0 < X) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) * X := by\n have h2 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a < 2 ^ (dyadClass X \u03c1 + 1) :=\n Nat.lt_pow_succ_log_self (by norm_num) _\n have h3 : ((\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) + 1) \u2264 (2 : \u211d) ^ (dyadClass X \u03c1 + 1) := by\n have h4 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 \u2264 2 ^ (dyadClass X \u03c1 + 1) := h2\n have h5 : ((\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 : \u2115) : \u211d) \u2264 ((2 ^ (dyadClass X \u03c1 + 1) : \u2115) : \u211d) := by\n exact_mod_cast h4\n push_cast at h5\n linarith\n have h6 : |(\u03c1 : \u2102).im| / X < \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 := Nat.lt_floor_add_one _\n have h7 : ((2 ^ (dyadClass X \u03c1 + 1) : \u2115) : \u211d) = (2 : \u211d) ^ (dyadClass X \u03c1 + 1) := by\n push_cast; ring\n rw [h7] at h3\n have h8 := (div_lt_iff\u2080 hX).mpr ((Nat.lt_floor_add_one _).trans_le h3)\n linarith\n\n/-- The tail summand (if-form on the zero subtype). -/\ndef tailTerm (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u211d :=\n if X < |(\u03c1 : \u2102).im| then (zeroMult \u03c1 : \u211d) / (1 + \u03c1.im ^ 2) else 0\n\nlemma tailTerm_nonneg {X : \u211d} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n 0 \u2264 tailTerm X \u03c1 := by\n by_cases h : X < |(\u03c1 : \u2102).im| <;>\n simp [tailTerm, h, div_nonneg (Nat.cast_nonneg _)\n (by positivity : (0 : \u211d) \u2264 1 + \u03c1.im ^ 2)]\n\n/-- The tail summand is summable (dominated by 2\u00b7m/(1+\u2016\u03b3\u2016\u00b2) via\n1 + \u2016\u03b3\u2016\u00b2 \u2264 2(1 + im\u00b2)). -/\nlemma tailTerm_summable (X : \u211d) :\n Summable (tailTerm X) := by\n have hbase : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))) :=\n (WeilEF.zero_sum_inv_sq zetaSeam).mul_left 2\n apply Summable.of_norm_bounded hbase\n intro \u03c1\n rw [tailTerm]\n by_cases h : X < |(\u03c1 : \u2102).im|\n \u00b7 rw [if_pos h]\n have hgam : Complex.normSq (gammaOf (\u03c1 : \u2102))\n = (\u03c1 : \u2102).im ^ 2 + (1 / 2 - (\u03c1 : \u2102).re) ^ 2 := by\n rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n ring\n have hcmp : 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) \u2264 2 * (1 + (\u03c1 : \u2102).im ^ 2) := by\n rw [hgam]\n have hre : ((\u03c1 : \u2102).re - 1 / 2) ^ 2 \u2264 1 / 4 := by\n have h0 := \u03c1.2.2.1\n have h1 := \u03c1.2.2.2\n nlinarith [sq_nonneg ((\u03c1 : \u2102).re - 1 / 2)]\n nlinarith [sq_nonneg (\u03c1 : \u2102).im]\n have hpos1 : (0 : \u211d) < 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n have h := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102)); linarith\n have hpos2 : (0 : \u211d) < 1 + (\u03c1 : \u2102).im ^ 2 := by positivity\n have hfrac : 1 / (1 + (\u03c1 : \u2102).im ^ 2) \u2264 2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n rw [div_le_div_iff\u2080 hpos2 hpos1]\n nlinarith [hcmp]\n have hm : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) := Nat.cast_nonneg _\n calc \u2016(zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\u2016\n = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) :=\n norm_of_nonneg (div_nonneg (Nat.cast_nonneg _) hpos2.le)\n _ \u2264 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by\n rw [show (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\n = (zeroMult \u03c1 : \u211d) * (1 / (1 + (\u03c1 : \u2102).im ^ 2)) from by ring]\n rw [show 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))\n = (zeroMult \u03c1 : \u211d) * (2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) from by ring]\n exact mul_le_mul_of_nonneg_left hfrac hm\n \u00b7 rw [if_neg h]\n positivity\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 376,
"oldLines": 12,
"newStart": 376,
"newLines": 13,
"lines": [
" rw [\u2190 Real.exp_nat_mul]",
" norm_num",
" have h2 := Real.exp_one_lt_d9.le",
"- have h3 : (Real.exp 1) ^ 5 \u2264 (2.718281829 : \u211d) ^ 5 :=",
"+ have h3 : (Real.exp 1) ^ 5 \u2264 (2.7182818286 : \u211d) ^ 5 :=",
" pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5",
"- have h4 : (2.718281829 : \u211d) ^ 5 \u2264 200 := by norm_num",
"+ have h4 : (2.7182818286 : \u211d) ^ 5 \u2264 200 := by norm_num",
" linarith [h1, h3, h4]",
" have hlog2 := log_two_le_one",
"- have hA0 : (0 : \u211d) \u2264 4 * A0count / X := by positivity",
"+ have hA0 : (0 : \u211d) \u2264 4 * A0count / X :=",
"+ div_nonneg (mul_nonneg (by norm_num) A0count_pos.le) hX0.le",
" have h1 : 10 * Real.log 2 + 2 * Real.log X \u2264 4 * Real.log X := by linarith",
" calc (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)",
" \u2264 (4 * A0count / X) * (4 * Real.log X) := mul_le_mul_of_nonneg_left h1 hA0"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"There's `analyticOrderAt_smul` (order additive under scalar mul) and `analyticOrderAt_mul_eq_top_of_left` at 490 — so there's likely `analyticOrderAt_mul` nearby. For the constant multiple: analyticOrderAt (c * f) = analyticOrderAt (const c) + analyticOrderAt f = 0 + order f (const nonzero ⟹ order 0 via analyticOrderAt_eq_zero: `analyticOrderAt_eq_zero : analyticOrderAt f z₀ = 0 ↔ f z₀ ≠ 0`? something like that).\n\nAnd for the affine comp — no direct lemma. So per-point: analyticOrderAt (fun w => ζ(aff w)) w₀ = analyticOrderAt ζ (aff w₀) via the normal form. Let me just build it via `AnalyticAt.analyticOrderAt_eq_natCast` (the characterization: order = n ⟺ ∃ g analytic, g(z₀) ≠ 0, f =ᶠ (z−z₀)^n • g):\n\nForward: given ζ =ᶠ[𝓝 z₀'] (z − z₀')^m • h with h analytic, h z₀' ≠ 0 (from the ζ-side factorization): then ζ(aff w) = (aff w − z₀')^m • h(aff w) with aff w₀ = z₀' (z₀' := aff w₀ = s₀ + (5/2)w₀): aff w − aff w₀ = (5/2)(w − w₀): so ζ(aff w) = ((5/2)(w−w₀))^m · h(aff w) = (w−w₀)^m • [(5/2)^m · h(aff w)] near w₀: the cofactor g'(w) := (5/2)^m · h(aff w) analytic at w₀ (h analytic at aff w₀ + aff) and g'(w₀) = (5/2)^m·h(z₀') ≠ 0 ✓ (5/2 ≠ 0). So analyticOrderAt (ζ∘aff) w₀ = analyticOrderAt ζ (aff w₀) — both equal m... wait the characterization gives order = m from the existence ✓. And the reverse direction isn't needed (I have the ζ-side order m from its factorization; the F-side order equals m by exhibiting the factorization).\n\nFormally:\n```lean\ntheorem analyticOrderAt_riemannZeta_affine {t : ℝ} (w₀ : ℂ) :\n analyticOrderAt (fun w => riemannZeta (discCenter t + (5/2 : ℂ) * w)) w₀\n = analyticOrderAt riemannZeta (discCenter t + (5/2 : ℂ) * w₀) := by\n by_cases htop : analyticOrderAt riemannZeta (discCenter t + (5/2:ℂ)*w₀) = ⊤\n · -- both ⊤: the comp order is ⊤ iff... (if ζ locally zero at the point then ζ∘aff locally zero)\n sorry\n · obtain ⟨h', h1, h2, h3⟩ := (analyticAt_riemannZeta_of_ne_one ?_).analyticOrderAt_ne_top.mp htop\n -- h3 : ζ =ᶠ[𝓝 z₀'] fun z => (z − z₀')^m • h' z with m = analyticOrderNatAt ζ z₀'\n ...\n```\nHmm wait — analyticOrderAt = ⊤ means ζ locally identically zero — impossible for ζ (not identically zero; analyticity + identity principle). So the ⊤ case is excluded: analyticOrderAt ζ z ≠ ⊤ for all z ≠ 1 (LiSides' zeta_order_ne_top_of_ne ✓ EXISTS — from ii′-1b!). So the order is always finite. Good:\n\n```lean\ntheorem analyticOrderNatAt_riemannZeta_affine {t : ℝ} (w₀ : ℂ) :\n analyticOrderNatAt (fun w => riemannZeta (discCenter t + (5/2 : ℂ) * w)) w₀\n = analyticOrderNatAt riemannZeta (discCenter t + (5/2 : ℂ) * w₀) := by\n set z₀ := discCenter t + (5/2 : ℂ) * w₀\n -- ζ ≠ 1-point? z₀ could be 1?? — z₀ = s₀ + (5/2)w₀ — for general w₀, z₀ could be 1! The affine invariance only needed for w₀ in the unit ball — where z₀ is in the 5/2-disc, ≠ 1 ✓ (from hne-style argument with ht). Add hypothesis.\n```\nRight — need (ht : 10 ≤ |t|) and ‖w₀‖ ≤ 1 (so z₀ ≠ 1). Let me include those.\n\nThe proof via analyticOrderNatAt: use `Nat.cast_analyticOrderNatAt (hf' : analyticOrderAt f z₀ ≠ ⊤)`?? from the smul proof: `Nat.cast_analyticOrderNatAt hf' : (analyticOrderNatAt f z₀ : ℕ∞) = analyticOrderAt f z₀`? — so it suffices to show the analyticOrderAt versions equal as ℕ∞, via the natCast characterization on both sides with the same m and transferred cofactor:\n\n```lean\n -- from the ζ-side: ζ =ᶠ[𝓝 z₀] (z − z₀)^m • h' with h' analytic, h' z₀ ≠ 0, m = analyticOrderNatAt ζ z₀\n obtain ⟨h', h1, h2, h3⟩ := (analyticAt_riemannZeta_of_ne_one hz₀ne).analyticOrderAt_ne_top.mp\n (zeta_order_ne_top_of_ne hz₀ne) -- from LiSides ✓\n -- transfer to w-side:\n have hF : (fun w => riemannZeta (discCenter t + (5/2 : ℂ) * w)) =ᶠ[𝓝 w₀]\n fun w => (w - w₀) ^ analyticOrderNatAt riemannZeta z₀ • (((5/2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) * h' (discCenter t + (5/2 : ℂ) * w)) := by\n -- from h3 via the affine map's tendsto: eventuallyEq pullback\n ...\n -- then analyticOrderAt F w₀ = m via the natCast characterization, with the cofactor analytic and nonvanishing\n ...\n```\n\nThe eventuallyEq pullback: h3 : ζ =ᶠ[𝓝 z₀] (fun z => (z−z₀)^m • h' z) — I need ζ∘aff =ᶠ[𝓝 w₀] ((·−w₀)^m • g') — via `Filter.EventuallyEq.comp_tendsto`? — there's `EventuallyEq.comp_tendsto (h : f =ᶠ[l'] g) (ht : Tendsto φ l l') : f ∘ φ =ᶠ[l] g ∘ φ`? something like `Filter.EventuallyEq.comp_tendsto` ✓ exists. With φ = aff, Tendsto aff (𝓝 w₀) (𝓝 z₀) ✓ (aff continuous). Then the pointwise: (aff w − aff w₀)^m • h'(aff w) = ((5/2)(w−w₀))^m • h'(aff w) = (w−w₀)^m • ((5/2)^m·h'(aff w)) via smul algebra (mul_pow, smul_smul) — the congr of eventuallyEq with the pointwise identity ✓.\n\nThen the cofactor g'(w) = (5/2)^m · h'(aff w): analytic at w₀ (h1 : AnalyticAt h' z₀, aff analytic, comp_of_eq); g'(w₀) = (5/2)^m · h'(z₀) ≠ 0 ✓ (pow_ne_zero + h2).\n\nThen analyticOrderAt F w₀ = ↑m via (hF_an.analyticOrderAt_eq_natCast).mpr ⟨g', g'_an, g'_ne, hF-transferred⟩ and the ζ-side = ↑m via Nat.cast_analyticOrderNatAt — concluding analyticOrderNatAt F w₀ = analyticOrderNatAt ζ z₀ via ENat.natCast_inj.\n\nThis is all standard-but-fiddly. OK — I'm now deep into a long build. Let me continue writing §2's remainder. But first — given how long this is getting, let me reconsider scope for the current work session. The user is engaged and wants progress. The sub-stage rule says commit at clean boundaries. §1 committed. §2 partial (scaledZeta_analytic + scaledZeta_zero green). Let me finish §2's count+gap and commit, which is a natural boundary. The order-invariance lemma is part of the count.\n\nLet me write the remainder of §2 now — the finiteness, the affine order invariance, the ZerosBound application, the R-gap. This is a big chunk; write it and iterate.","signature":""},{"type":"text","text":"The API is clear (`analyticOrderAt_smul`, the natCast characterization, LiSides' `zeta_order_ne_top_of_ne`). Writing the rest of §2: order-invariance under the affine map, finiteness, the Jensen count, and the R-gap."},{"type":"tool_use","id":"Edit_362","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-- The order of ζ is invariant under the affine change of variable\nw ↦ s₀ + (5/2)·w (nonzero slope), valid for ‖w₀‖ ≤ 1 (so the target\navoids the pole at 1). -/\ntheorem analyticOrderNatAt_riemannZeta_affine {t : ℝ} (ht : 10 ≤ |t|) {w₀ : ℂ}\n (hw₀ : ‖w₀‖ ≤ 1) :\n analyticOrderNatAt (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀\n = analyticOrderNatAt riemannZeta (discCenter t + (5 / 2 : ℂ) * w₀) := by\n set z₀ := discCenter t + (5 / 2 : ℂ) * w₀ with hz₀\n -- z₀ avoids 1 (its imaginary part is large)\n have hz₀ne : z₀ ≠ 1 := by\n intro h\n have hwim : |w₀.im| ≤ 1 := (abs_im_le_norm _).trans hw₀\n have him : z₀.im = t + (5 / 2) * w₀.im := by\n simp [hz₀, 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 h3 := abs_add_le (t + (5 / 2) * w₀.im) (-((5 / 2) * w₀.im))\n rw [abs_neg, add_neg_cancel_right] at 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 :=\n mul_le_mul_of_nonneg_left hwim (by norm_num)\n _ = 5 / 2 := by norm_num\n linarith [h3, 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 obtain ⟨h', h1, h2, h3⟩ := (analyticAt_riemannZeta_of_ne_one hz₀ne).analyticOrderAt_ne_top.mp\n (zeta_order_ne_top_of_ne hz₀ne)\n -- transfer the factorization to the w-side\n have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w₀ :=\n analyticAt_const.add (analyticAt_const.mul analyticAt_id)\n have haffT : Tendsto (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) (𝓝 w₀) (𝓝 z₀) :=\n haff.continuousAt\n have h3' := h3.comp_tendsto haffT\n -- h3' : (fun z => (z − z₀)^m • h' z) ∘ aff =ᶠ ζ ∘ aff; massage the form\n have hF : (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) =ᶠ[𝓝 w₀]\n fun w => (w - w₀) ^ analyticOrderNatAt riemannZeta z₀ •\n (((5 / 2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) *\n h' (discCenter t + (5 / 2 : ℂ) * w)) := by\n apply h3'.congr'\n filter_upwards with w\n simp only [Function.comp_apply]\n rw [show discCenter t + (5 / 2 : ℂ) * w - z₀ = (5 / 2 : ℂ) * (w - w₀) by rw [hz₀]; ring]\n rw [mul_pow, smul_eq_mul, smul_eq_mul]\n ring\n have hcof : AnalyticAt ℂ (fun w => ((5 / 2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) *\n h' (discCenter t + (5 / 2 : ℂ) * w)) w₀ :=\n (analyticAt_const.mul (h1.comp_of_eq haff rfl)) -- hmm h1 is AnalyticAt h' z₀\n have hcof_ne : ((5 / 2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) * h' z₀ ≠ 0 :=\n mul_ne_zero (pow_ne_zero _ (by norm_num)) h2\n have hF_an : AnalyticAt ℂ (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀ :=\n analyticAt_riemannZeta_of_ne_one hz₀ne |>.comp_of_eq haff rfl\n have horder : analyticOrderAt (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀\n = (analyticOrderNatAt riemannZeta z₀ : ℕ∞) :=\n (hF_an.analyticOrderAt_eq_natCast).mpr ⟨_, hcof, hcof_ne, hF⟩\n rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_analyticOrderNatAt\n (zeta_order_ne_top_of_ne hz₀ne), horder]\n\n/-! ## 3. The Jensen count and the R-gap -/\n\n/-- Zeros of the scaled function F in the closed unit ball are finite. -/\ntheorem scaledZeta_zeros_finite {t : ℝ} (ht : 10 ≤ |t|) :\n (SetOfZeros 1 (scaledZeta t)).Finite := by\n have hz0 : riemannZeta (discCenter t) ≠ 0 := by\n have h := RvM.zeta_lower_bound_two t\n intro h0\n rw [← show discCenter t = 2 + t * Complex.I from rfl, h0, norm_zero] at h\n norm_num at h\n -- SetOfZeros 1 F = the affine preimage of the ζ-zeros in the 5/2-disc\n have hsub : SetOfZeros 1 (scaledZeta t) ⊆\n (fun w => discCenter t + (5 / 2 : ℂ) * w) ⁻¹'\n (Metric.closedBall (discCenter t) (5 / 2) ∩ riemannZetaZeros) := by\n intro w hw\n simp only [SetOfZeros, Set.mem_setOf_eq] at hw\n have hFw : riemannZeta (discCenter t + (5 / 2 : ℂ) * w) = 0 := by\n have := hw.2\n unfold scaledZeta at this\n exact (div_eq_zero_iff.mp this).1 -- hmm div_eq_zero_iff : a/b = 0 ↔ a = 0 ∨ b = 0; need a = 0 from b ≠ 0\n constructor\n · rw [Metric.mem_closedBall, Complex.dist_eq]\n rw [add_sub_cancel_left]\n calc ‖(5 / 2 : ℂ) * w‖ ≤ (5 / 2) * ‖w‖ := by\n rw [norm_mul]\n have hn : ‖(5 / 2 : ℂ)‖ = 5 / 2 := by\n rw [show (5 / 2 : ℂ) = ((5 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,\n Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]\n rw [hn]\n _ ≤ (5 / 2) * 1 := mul_le_mul_of_nonneg_left hw.1 (by norm_num)\n _ = 5 / 2 := by norm_num\n · exact mem_riemannZetaZeros.mpr hFw\n exact ((isCompact_closedBall _ _).inter_riemannZetaZeros_finite).subset\n ... -- hmm need preimage-finite\n sorry\n\nend NguyenRH1\n\nend"},"extra_content":null}]