← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (2294 chars)
- `AnalyticAt.iteratedDeriv` — NOT found. But `AnalyticAt.deriv` exists (used in LiResidue: ha.deriv ✓). For iteratedDeriv j F: iteratedDeriv j F = deriv^j F — hmm — actually there's `AnalyticAt.iteratedFDeriv`? or I can use: AnalyticAt F x → AnalyticAt (iteratedDeriv n F) x — let me check for iteratedFDeriv... Actually — simpler: I'll do a tiny induction: `AnalyticAt.iteratedDeriv_aux : AnalyticAt ℂ F x → AnalyticAt ℂ (iteratedDeriv n F) x := Nat.rec h (fun n ih => ih.deriv)`? — but iteratedDeriv (n+1) F = deriv (iteratedDeriv n F) [succ] or iteratedDeriv n (deriv F) [succ'] — for the induction with .deriv I need the succ form: iteratedDeriv (n+1) F = deriv (iteratedDeriv n F) ✓ `iteratedDeriv_succ` — so:
```lean
lemma AnalyticAt.iteratedDeriv_aux {F : ℂ → ℂ} {x : ℂ} (hF : AnalyticAt ℂ F x) (n : ℕ) :
AnalyticAt ℂ (iteratedDeriv n F) x := by
induction n with
| zero => simpa [iteratedDeriv_zero] using hF
| succ n ih =>
rw [iteratedDeriv_succ]
exact ih.deriv
```
✓.
- `EventuallyEq.deriv_eq` — grep found nothing?! But LiResidue used `h3.deriv_eq` (line 122: `rw [← h3.deriv_eq, h1, h2, one_mul]`) — where h3 : (fun z => (z−1)*ζ z) =ᶠ[𝓝 w] zetaA — so EventuallyEq.deriv_eq EXISTS (maybe via a different grep-able name — `Filter.EventuallyEq.deriv_eq`? my grep pattern missed it). Fine — it exists (used in LiResidue ✓).
- `interior_mem_nhds : interior s ∈ 𝓝 x ↔ s ∈ 𝓝 x` ✓.
Now let me write Section 5 in one big chunk. This is the final stretch of piece (A). Let me be very careful with the details. The pieces:
1. eventuallyEq_deriv + eventuallyEq_iteratedDeriv + iteratedDeriv_congr_of_eventuallyEq.
2. The zpow iterated derivative: iteratedDeriv_neg_zpow_add (k) (c) (s+c ≠ 0) : iteratedDeriv k (fun s => −((s+c)^(−1:ℤ))) s = −(−1)^k·k!·(s+c)^(−(k+1):ℤ).
3. The series iterated values: iteratedDeriv j DinfC (1/2) = (−1)^{j+1} j! Σ_{m≥0} (↑m+1/2)^{−(j+1)} via iteratedDerivWithin_tsum.
4. The identity principle: digamma = DinfC on dpsiDomain.
5. iteratedDeriv j digamma (1/2) = (−1)^{j+1} j! Σ ... via the congruence helper.
6. The reindexing to lagariasA.
7. The affine comp + final assembly (in LiArchimedean.lean or here).
This is ~300+ lines. Given the hour (~00:00), let me write it carefully but efficiently, in 2 chunks. Chunk 1: items 1-2 (helpers).
Now Section 5 — the congruence helpers and the zpow iterated derivative.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
"old_string": " rw [Complex.digamma_def, logDeriv_apply, hderiv, hGx]\n rw [\u2190 Complex.ofReal_div]\n congr 1\n exact psiReal_eq_DinfR hx0\n\nend NguyenRH1",
"new_string": " rw [Complex.digamma_def, logDeriv_apply, hderiv, hGx]\n rw [\u2190 Complex.ofReal_div]\n congr 1\n exact psiReal_eq_DinfR hx0\n\n/-! ## 5. Congruence helpers and the inverse-power iterated derivative -/\n\n/-- If f = g on a nbd of x, then deriv f = deriv g on a (smaller) nbd of x. -/\nlemma eventuallyEq_deriv {f g : \u2102 \u2192 \u2102} {x : \u2102} (h : f =\u1da0[\ud835\udcdd x] g) :\n deriv f =\u1da0[\ud835\udcdd x] deriv g := by\n have hS : {y | f y = g y} \u2208 \ud835\udcdd x := h\n have hxint : x \u2208 interior {y | f y = g y} := by\n rw [mem_interior_iff_mem_nhds]\n exact hS\n filter_upwards [IsOpen.mem_nhds isOpen_interior hxint] with y hy\n have h3 : f =\u1da0[\ud835\udcdd y] g := by\n apply Filter.eventually_of_mem (IsOpen.mem_nhds isOpen_interior hy)\n intro z hz\n exact interior_subset hz\n exact h3.deriv_eq\n\nlemma eventuallyEq_iteratedDeriv {f g : \u2102 \u2192 \u2102} {x : \u2102} (h : f =\u1da0[\ud835\udcdd x] g) (n : \u2115) :\n iteratedDeriv n f =\u1da0[\ud835\udcdd x] iteratedDeriv n g := by\n induction n with\n | zero => simpa [iteratedDeriv_zero] using h\n | succ n ih =>\n rw [iteratedDeriv_succ, iteratedDeriv_succ]\n exact eventuallyEq_deriv ih\n\n/-- Pointwise congruence of iteratedDeriv under eventual equality. -/\nlemma iteratedDeriv_congr_of_eventuallyEq {f g : \u2102 \u2192 \u2102} {x : \u2102} (h : f =\u1da0[\ud835\udcdd x] g) (n : \u2115) :\n iteratedDeriv n f x = iteratedDeriv n g x :=\n (eventuallyEq_iteratedDeriv h n).self_of_nhds\n\n/-- The iterated derivative of s \u21a6 \u2212(s+c)\u207b\u00b9:\n(d/ds)^k [\u2212(s+c)\u207b\u00b9] = \u2212(\u22121)^k\u00b7k!\u00b7(s+c)^{\u2212(k+1)}. -/\nlemma iteratedDeriv_neg_zpow_neg_one_add (k : \u2115) (c : \u2102) {s : \u2102} (hs : s + c \u2260 0) :\n iteratedDeriv k (fun s : \u2102 => -((s + c) ^ (-1 : \u2124))) s =\n -((-1 : \u2102)) ^ k * (k ! : \u2102) * (s + c) ^ (-(k : \u2124) - 1) := by\n induction k generalizing s with\n | zero =>\n simp\n | succ k ih =>\n rw [iteratedDeriv_succ']\n -- replace iteratedDeriv k F by its closed form on a nbd of s\n have hopen : IsOpen {t : \u2102 | t + c \u2260 0} := by\n have hcont : Continuous (fun t : \u2102 => t + c) := continuous_id.add continuous_const\n exact isOpen_compl_singleton.preimage hcont\n have hev : (fun t => iteratedDeriv k (fun u : \u2102 => -((u + c) ^ (-1 : \u2124))) t) =\u1da0[\ud835\udcdd s]\n (fun t => -((-1 : \u2102)) ^ k * (k ! : \u2102) * (t + c) ^ (-(k : \u2124) - 1)) := by\n filter_upwards [hopen.mem_nhds hs] with t ht\n exact ih ht\n rw [hev.deriv_eq]\n -- compute deriv of the closed form at s\n have h1 : HasDerivAt (fun t : \u2102 => (t + c) ^ (-(k : \u2124) - 1))\n (((-(k : \u2124) - 1 : \u2124) : \u2102) * (s + c) ^ (-(k : \u2124) - 2)) s := by\n have h2 : HasDerivAt (fun t : \u2102 => t + c) 1 s := by\n simpa using (hasDerivAt_id s).add_const c\n have h3 := (hasDerivAt_zpow (-(k : \u2124) - 1) (s + c) (Or.inl hs)).comp s h2\n rw [mul_one] at h3\n have heq : ((fun x : \u2102 => x ^ (-(k : \u2124) - 1)) \u2218 fun t : \u2102 => t + c) =\n fun t => (t + c) ^ (-(k : \u2124) - 1) := rfl\n rw [heq] at h3\n exact h3\n have h4 : deriv (fun t : \u2102 => -((-1 : \u2102)) ^ k * (k ! : \u2102) * (t + c) ^ (-(k : \u2124) - 1)) s =\n -((-1 : \u2102)) ^ k * (k ! : \u2102) * (((-(k : \u2124) - 1 : \u2124) : \u2102) * (s + c) ^ (-(k : \u2124) - 2)) := by\n rw [deriv_const_mul]\n \u00b7 exact h1.deriv\n \u00b7 exact h1.differentiableAt\n rw [h4]\n -- algebra: the constants and the exponent\n have hfact : ((k + 1 : \u2115) ! : \u2102) = (k + 1) * (k ! : \u2102) := by\n rw [Nat.factorial_succ]\n push_cast\n ring\n have hexp : (-(k : \u2124) - 1 - 1 : \u2124) = (-((k + 1 : \u2115) : \u2124) - 1 : \u2124) := by\n push_cast\n ring\n have hsign : -((-1 : \u2102)) ^ (k + 1) = -((-1 : \u2102)) ^ k * -((-(k : \u2124) - 1 : \u2124) : \u2102) := by\n rw [pow_succ]\n push_cast\n ring\n rw [hexp, hfact]\n rw [hsign]\n ring_nf\n -- reconcile -(\u22121)^k\u00b7k!\u00b7((\u2212(k+1))\u00b7X) with the two forms\n have h5 : (((-(k : \u2124) - 1 : \u2124) : \u2102)) = -((k : \u2102) + 1) := by push_cast; ring\n rw [h5]\n ring\n\nend NguyenRH1"
}
result 2026-08-22 08:16:46Z → 2026-08-23 19:43:22Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
"oldString": " have hdisj : Disjoint hW1.toFinset hW2.toFinset := by\n rw [Finset.disjoint_left]\n intro z hz1 hz2\n rw [Set.Finite.mem_toFinset] at hz1 hz2\n have h1 : (2 : \u211d) ^ j * X - 1 < z.im := hz1.2.1\n have h2 : z.im \u2264 -((2 : \u211d) ^ j * X) := hz2.2.2\n linarith",
"newString": " have hdisj : Disjoint hW1.toFinset hW2.toFinset := by\n rw [Finset.disjoint_left]\n intro z hz1 hz2\n rw [Set.Finite.mem_toFinset] at hz1 hz2\n have h1 : (2 : \u211d) ^ j * X - 1 < z.im := hz1.2.1\n have h2 : z.im \u2264 -((2 : \u211d) ^ j * X) := hz2.2.2\n have hge : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1le : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1le, hX]\n linarith",
"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 rw [one_div_pow]\n field_simp\n ring\n rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.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.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\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 have h6 : (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a * X :=\n mul_le_mul_of_nonneg_right h3 hX.le\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 < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) :=\n (Nat.lt_floor_add_one _).trans_le h3\n rw [div_lt_iff\u2080 hX] at h6\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 : \u2102).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 : \u2102).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) := by\n rw [Real.norm_eq_abs, abs_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, norm_zero]\n have hnn := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n exact mul_nonneg (by norm_num) (div_nonneg (Nat.cast_nonneg _) (by linarith))\n\n/-- The dyadic log series is summable. -/\nlemma dyadicLog_summable (X : \u211d) :\n Summable (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j) := by\n have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\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 rw [one_div_pow]\n field_simp\n ring\n rw [hsplit]\n exact (hlinH.summable.mul_left _).add (summable_geometric_two.mul_left _)\n\n/-- The dyadic fiber {dyadClass X \u03c1 = j} is finite. -/\nlemma dyadClass_fiber_finite {X : \u211d} (hX : 0 < X) (j : \u2115) :\n {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im|}.Finite := by\n apply (finite_subtype_norm_lt (1 + (2 : \u211d) ^ (j + 1) * X + 1)).subset\n intro \u03c1 h\u03c1\n have h\u03c1j : dyadClass X \u03c1 = j := h\u03c1.1\n have hup := dyadClass_upper hX \u03c1\n rw [h\u03c1j] at hup\n have hnorm : \u2016(\u03c1 : \u2102)\u2016 \u2264 |(\u03c1 : \u2102).re| + |(\u03c1 : \u2102).im| :=\n Complex.norm_le_abs_re_add_abs_im _\n have hre : |(\u03c1 : \u2102).re| \u2264 1 := by\n rw [abs_le]\n exact \u27e8by linarith [\u03c1.2.2.1], by linarith [\u03c1.2.2.2]\u27e9\n have h2pow : (0 : \u211d) \u2264 (2 : \u211d) ^ (j + 1) * X := by positivity\n show \u2016(\u03c1 : \u2102)\u2016 < 1 + (2 : \u211d) ^ (j + 1) * X + 1\n linarith\n\n/-- The fiber count: the zeros in the dyadic fiber with X < |\u03b3| have\nmultiplicity-sum \u2264 A\u2080\u00b7(2^{j+1}X+3)\u00b7log(3\u00b72^{j+1}X+5). -/\nlemma fiber_mult_count {X : \u211d} (hX : 200 \u2264 X) (j : \u2115) :\n \u2211 \u03c1 \u2208 (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).toFinset,\n (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n classical\n have hX0 : (0 : \u211d) < X := by linarith\n have h2jX : (0 : \u211d) < (2 : \u211d) ^ j * X := by positivity\n have h2j1X : (0 : \u211d) < (2 : \u211d) ^ (j + 1) * X := by positivity\n set FS := (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).toFinset with hFS\n have hmemFS : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n \u03c1 \u2208 FS \u2194 dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im| := by\n intro \u03c1\n rw [hFS, Set.Finite.mem_toFinset]\n exact Iff.rfl\n have hW1 : (Zeta23.zerosIn ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X)).Finite :=\n Zeta23.zerosIn_finite _ _\n have hW2 : (Zeta23.zerosIn (-(2 : \u211d) ^ (j + 1) * X) (-((2 : \u211d) ^ j * X))).Finite :=\n Zeta23.zerosIn_finite _ _\n have himg : FS.image (Subtype.val) \u2286 hW1.toFinset \u222a hW2.toFinset := by\n intro z hz\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hz\n rw [hmemFS] at h\u03c1\n obtain \u27e8h\u03c1j, hgt\u27e9 := h\u03c1\n have hup : |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (j + 1) * X := by\n have h := dyadClass_upper hX0 \u03c1\n rw [h\u03c1j] at h\n exact h\n have hlo : (2 : \u211d) ^ j * X \u2264 |(\u03c1 : \u2102).im| := by\n have h := dyadClass_lower hX0 (show X \u2264 |(\u03c1 : \u2102).im| from hgt.le)\n rw [h\u03c1j] at h\n exact h\n rcases le_or_gt 0 (\u03c1 : \u2102).im with him | him\n \u00b7 apply Finset.mem_union_left\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_nonneg him] at hlo\n linarith\n \u00b7 rw [abs_of_nonneg him] at hup\n linarith\n \u00b7 apply Finset.mem_union_right\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_neg him] at hup\n linarith\n \u00b7 rw [abs_of_neg him] at hlo\n linarith\n have hsum_img : \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.val_injective h)]\n have hdisj : Disjoint hW1.toFinset hW2.toFinset := by\n rw [Finset.disjoint_left]\n intro z hz1 hz2\n rw [Set.Finite.mem_toFinset] at hz1 hz2\n have h1 : (2 : \u211d) ^ j * X - 1 < z.im := hz1.2.1\n have h2 : z.im \u2264 -((2 : \u211d) ^ j * X) := hz2.2.2\n linarith\n calc \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := hsum_img\n _ \u2264 \u2211 z \u2208 hW1.toFinset \u222a hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg himg (fun z _ _ => Nat.cast_nonneg _)\n _ = \u2211 z \u2208 hW1.toFinset, (zeroMult z : \u211d) + \u2211 z \u2208 hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_union hdisj\n _ = (Zeta23.Ncount ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X) : \u211d)\n + (Zeta23.Ncount (-(2 : \u211d) ^ (j + 1) * X) (-((2 : \u211d) ^ j * X)) : \u211d) := by\n rw [Zeta23.Ncount, Zeta23.Ncount, finsum_mem_eq_finite_toFinset_sum _ hW1,\n finsum_mem_eq_finite_toFinset_sum _ hW2, Nat.cast_sum, Nat.cast_sum]\n _ \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n have h2jX1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1, hX]\n have hpowX : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by\n rw [pow_succ']; ring\n have hlogpos : (0 : \u211d) \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_nonneg\n linarith [h2j1X]\n have h1 := Ncount_le_of_interval_gen (a := (2 : \u211d) ^ j * X - 1)\n (b := (2 : \u211d) ^ (j + 1) * X) (by linarith [hpowX, h2jX1])\n have h2 := Ncount_le_of_interval_gen (a := -(2 : \u211d) ^ (j + 1) * X)\n (b := -(2 : \u211d) ^ j * X) (by linarith [hpowX, h2jX1])\n -- the log arguments match L = log(3\u00b72^{j+1}X + 5)\n have hlog1 : Real.log (3 * max |(2 : \u211d) ^ j * X - 1| |(2 : \u211d) ^ (j + 1) * X| + 5)\n \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_le_log (by positivity)\n have hmax : max |(2 : \u211d) ^ j * X - 1| |(2 : \u211d) ^ (j + 1) * X|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_of_nonneg (by linarith [h2jX1])]\n nlinarith [h2jX, h2j1X]\n \u00b7 rw [abs_of_nonneg h2j1X.le]\n linarith [hmax]\n have hlog2 : Real.log (3 * max |-(2 : \u211d) ^ (j + 1) * X| |-(2 : \u211d) ^ j * X| + 5)\n \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_le_log (by positivity)\n have hmax : max |-(2 : \u211d) ^ (j + 1) * X| |-(2 : \u211d) ^ j * X|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_neg, abs_of_nonneg h2j1X.le]\n \u00b7 rw [abs_neg, abs_of_nonneg h2jX.le]\n nlinarith [h2jX, h2j1X]\n linarith [hmax]\n -- the lengths: b\u2212a+1 = 2^jX + 2 and 2^jX + 1\n have hlen1 : (2 : \u211d) ^ (j + 1) * X - ((2 : \u211d) ^ j * X - 1) + 1\n = (2 : \u211d) ^ j * X + 2 := by\n have hpow : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']; ring\n rw [hpow]\n ring\n have hlen2 : -(2 : \u211d) ^ j * X - (-(2 : \u211d) ^ (j + 1) * X) + 1\n = (2 : \u211d) ^ j * X + 1 := by\n have hpow : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']; ring\n rw [hpow]\n ring\n rw [hlen1] at h1\n rw [hlen2] at h2\n -- assemble: A\u2080(2^jX+2)L + A\u2080(2^jX+1)L = A\u2080(2^{j+1}X+3)L\n have hA0 := A0count_pos.le\n have h1' : (Zeta23.Ncount ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ j * X + 2) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) :=\n h1.trans (mul_le_mul_of_nonneg_left hlog1 (by positivity))\n have h2' : (Zeta23.Ncount (-(2 : \u211d) ^ (j + 1) * X) (-((2 : \u211d) ^ j * X)) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ j * X + 1) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) :=\n h2.trans (mul_le_mul_of_nonneg_left hlog2 (by positivity))\n have hpow : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by rw [pow_succ']; ring\n linarith [h1', h2', hA0, hlogpos, hpow]\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 569,
"oldLines": 6,
"newStart": 569,
"newLines": 9,
"lines": [
" rw [Set.Finite.mem_toFinset] at hz1 hz2",
" have h1 : (2 : \u211d) ^ j * X - 1 < z.im := hz1.2.1",
" have h2 : z.im \u2264 -((2 : \u211d) ^ j * X) := hz2.2.2",
"+ have hge : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by",
"+ have h1le : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow",
"+ nlinarith [h1le, hX]",
" linarith",
" calc \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)",
" = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := hsum_img"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"- `AnalyticAt.iteratedDeriv` — NOT found. But `AnalyticAt.deriv` exists (used in LiResidue: ha.deriv ✓). For iteratedDeriv j F: iteratedDeriv j F = deriv^j F — hmm — actually there's `AnalyticAt.iteratedFDeriv`? or I can use: AnalyticAt F x → AnalyticAt (iteratedDeriv n F) x — let me check for iteratedFDeriv... Actually — simpler: I'll do a tiny induction: `AnalyticAt.iteratedDeriv_aux : AnalyticAt ℂ F x → AnalyticAt ℂ (iteratedDeriv n F) x := Nat.rec h (fun n ih => ih.deriv)`? — but iteratedDeriv (n+1) F = deriv (iteratedDeriv n F) [succ] or iteratedDeriv n (deriv F) [succ'] — for the induction with .deriv I need the succ form: iteratedDeriv (n+1) F = deriv (iteratedDeriv n F) ✓ `iteratedDeriv_succ` — so:\n```lean\nlemma AnalyticAt.iteratedDeriv_aux {F : ℂ → ℂ} {x : ℂ} (hF : AnalyticAt ℂ F x) (n : ℕ) :\n AnalyticAt ℂ (iteratedDeriv n F) x := by\n induction n with\n | zero => simpa [iteratedDeriv_zero] using hF\n | succ n ih =>\n rw [iteratedDeriv_succ]\n exact ih.deriv\n```\n✓.\n- `EventuallyEq.deriv_eq` — grep found nothing?! But LiResidue used `h3.deriv_eq` (line 122: `rw [← h3.deriv_eq, h1, h2, one_mul]`) — where h3 : (fun z => (z−1)*ζ z) =ᶠ[𝓝 w] zetaA — so EventuallyEq.deriv_eq EXISTS (maybe via a different grep-able name — `Filter.EventuallyEq.deriv_eq`? my grep pattern missed it). Fine — it exists (used in LiResidue ✓).\n- `interior_mem_nhds : interior s ∈ 𝓝 x ↔ s ∈ 𝓝 x` ✓.\n\nNow let me write Section 5 in one big chunk. This is the final stretch of piece (A). Let me be very careful with the details. The pieces:\n\n1. eventuallyEq_deriv + eventuallyEq_iteratedDeriv + iteratedDeriv_congr_of_eventuallyEq.\n2. The zpow iterated derivative: iteratedDeriv_neg_zpow_add (k) (c) (s+c ≠ 0) : iteratedDeriv k (fun s => −((s+c)^(−1:ℤ))) s = −(−1)^k·k!·(s+c)^(−(k+1):ℤ).\n3. The series iterated values: iteratedDeriv j DinfC (1/2) = (−1)^{j+1} j! Σ_{m≥0} (↑m+1/2)^{−(j+1)} via iteratedDerivWithin_tsum.\n4. The identity principle: digamma = DinfC on dpsiDomain.\n5. iteratedDeriv j digamma (1/2) = (−1)^{j+1} j! Σ ... via the congruence helper.\n6. The reindexing to lagariasA.\n7. The affine comp + final assembly (in LiArchimedean.lean or here).\n\nThis is ~300+ lines. Given the hour (~00:00), let me write it carefully but efficiently, in 2 chunks. Chunk 1: items 1-2 (helpers).","signature":""},{"type":"text","text":"Now Section 5 — the congruence helpers and the zpow iterated derivative."},{"type":"tool_use","id":"Edit_396","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean","old_string":" rw [Complex.digamma_def, logDeriv_apply, hderiv, hGx]\n rw [← Complex.ofReal_div]\n congr 1\n exact psiReal_eq_DinfR hx0\n\nend NguyenRH1","new_string":" rw [Complex.digamma_def, logDeriv_apply, hderiv, hGx]\n rw [← Complex.ofReal_div]\n congr 1\n exact psiReal_eq_DinfR hx0\n\n/-! ## 5. Congruence helpers and the inverse-power iterated derivative -/\n\n/-- If f = g on a nbd of x, then deriv f = deriv g on a (smaller) nbd of x. -/\nlemma eventuallyEq_deriv {f g : ℂ → ℂ} {x : ℂ} (h : f =ᶠ[𝓝 x] g) :\n deriv f =ᶠ[𝓝 x] deriv g := by\n have hS : {y | f y = g y} ∈ 𝓝 x := h\n have hxint : x ∈ interior {y | f y = g y} := by\n rw [mem_interior_iff_mem_nhds]\n exact hS\n filter_upwards [IsOpen.mem_nhds isOpen_interior hxint] with y hy\n have h3 : f =ᶠ[𝓝 y] g := by\n apply Filter.eventually_of_mem (IsOpen.mem_nhds isOpen_interior hy)\n intro z hz\n exact interior_subset hz\n exact h3.deriv_eq\n\nlemma eventuallyEq_iteratedDeriv {f g : ℂ → ℂ} {x : ℂ} (h : f =ᶠ[𝓝 x] g) (n : ℕ) :\n iteratedDeriv n f =ᶠ[𝓝 x] iteratedDeriv n g := by\n induction n with\n | zero => simpa [iteratedDeriv_zero] using h\n | succ n ih =>\n rw [iteratedDeriv_succ, iteratedDeriv_succ]\n exact eventuallyEq_deriv ih\n\n/-- Pointwise congruence of iteratedDeriv under eventual equality. -/\nlemma iteratedDeriv_congr_of_eventuallyEq {f g : ℂ → ℂ} {x : ℂ} (h : f =ᶠ[𝓝 x] g) (n : ℕ) :\n iteratedDeriv n f x = iteratedDeriv n g x :=\n (eventuallyEq_iteratedDeriv h n).self_of_nhds\n\n/-- The iterated derivative of s ↦ −(s+c)⁻¹:\n(d/ds)^k [−(s+c)⁻¹] = −(−1)^k·k!·(s+c)^{−(k+1)}. -/\nlemma iteratedDeriv_neg_zpow_neg_one_add (k : ℕ) (c : ℂ) {s : ℂ} (hs : s + c ≠ 0) :\n iteratedDeriv k (fun s : ℂ => -((s + c) ^ (-1 : ℤ))) s =\n -((-1 : ℂ)) ^ k * (k ! : ℂ) * (s + c) ^ (-(k : ℤ) - 1) := by\n induction k generalizing s with\n | zero =>\n simp\n | succ k ih =>\n rw [iteratedDeriv_succ']\n -- replace iteratedDeriv k F by its closed form on a nbd of s\n have hopen : IsOpen {t : ℂ | t + c ≠ 0} := by\n have hcont : Continuous (fun t : ℂ => t + c) := continuous_id.add continuous_const\n exact isOpen_compl_singleton.preimage hcont\n have hev : (fun t => iteratedDeriv k (fun u : ℂ => -((u + c) ^ (-1 : ℤ))) t) =ᶠ[𝓝 s]\n (fun t => -((-1 : ℂ)) ^ k * (k ! : ℂ) * (t + c) ^ (-(k : ℤ) - 1)) := by\n filter_upwards [hopen.mem_nhds hs] with t ht\n exact ih ht\n rw [hev.deriv_eq]\n -- compute deriv of the closed form at s\n have h1 : HasDerivAt (fun t : ℂ => (t + c) ^ (-(k : ℤ) - 1))\n (((-(k : ℤ) - 1 : ℤ) : ℂ) * (s + c) ^ (-(k : ℤ) - 2)) s := by\n have h2 : HasDerivAt (fun t : ℂ => t + c) 1 s := by\n simpa using (hasDerivAt_id s).add_const c\n have h3 := (hasDerivAt_zpow (-(k : ℤ) - 1) (s + c) (Or.inl hs)).comp s h2\n rw [mul_one] at h3\n have heq : ((fun x : ℂ => x ^ (-(k : ℤ) - 1)) ∘ fun t : ℂ => t + c) =\n fun t => (t + c) ^ (-(k : ℤ) - 1) := rfl\n rw [heq] at h3\n exact h3\n have h4 : deriv (fun t : ℂ => -((-1 : ℂ)) ^ k * (k ! : ℂ) * (t + c) ^ (-(k : ℤ) - 1)) s =\n -((-1 : ℂ)) ^ k * (k ! : ℂ) * (((-(k : ℤ) - 1 : ℤ) : ℂ) * (s + c) ^ (-(k : ℤ) - 2)) := by\n rw [deriv_const_mul]\n · exact h1.deriv\n · exact h1.differentiableAt\n rw [h4]\n -- algebra: the constants and the exponent\n have hfact : ((k + 1 : ℕ) ! : ℂ) = (k + 1) * (k ! : ℂ) := by\n rw [Nat.factorial_succ]\n push_cast\n ring\n have hexp : (-(k : ℤ) - 1 - 1 : ℤ) = (-((k + 1 : ℕ) : ℤ) - 1 : ℤ) := by\n push_cast\n ring\n have hsign : -((-1 : ℂ)) ^ (k + 1) = -((-1 : ℂ)) ^ k * -((-(k : ℤ) - 1 : ℤ) : ℂ) := by\n rw [pow_succ]\n push_cast\n ring\n rw [hexp, hfact]\n rw [hsign]\n ring_nf\n -- reconcile -(−1)^k·k!·((−(k+1))·X) with the two forms\n have h5 : (((-(k : ℤ) - 1 : ℤ) : ℂ)) = -((k : ℂ) + 1) := by push_cast; ring\n rw [h5]\n ring\n\nend NguyenRH1"},"extra_content":null}]