← Session 14 — Phase 5 kickoff: paper draft + honesty audit
thinking (4064 chars)
`Multipliable.subtype (hf : Multipliable f) (p : β → Prop)` → additive: `Summable.subtype (hf : Summable f) (p : β → Prop) : Summable (fun x : {x // p x} => f x)` presumably (or on Set.subtype). It takes a predicate p : β → Prop — our subtype is {m : ℕ // Odd m ∧ 3 ≤ m} = {m // (fun m => Odd m ∧ 3 ≤ m) m} ✓.
Note: `Summable.subtype` may require DecidablePred p? It might produce `Summable (f ∘ Subtype.val : Subtype p → α)`. Our tsum in SInfty is `tsum fun m : {m // Odd m ∧ 3 ≤ m} => ((1 - 1/(m:ℝ))^n − 1 + n/(m:ℝ))` — that's exactly fun x : subtype => f x with coercion. Fine.
Summability comparison: base summable: fun m : ℕ => C/(m:ℝ)² — from summable_one_div_nat_pow (p=2) .mul_left C. But m = 0 term: 1/0² = 0 in Lean (division by zero = 0) — fine, summable_one_div_nat_pow handles it (junk value at 0).
Then on subtype: (that).subtype p : Summable (fun m : {m // Odd m ∧ 3≤m} => C/(m:ℝ)²).
Comparison: Summable.of_nonneg_of_le (hg : ∀ x, 0 ≤ g x) (hfg : ∀ x, g x ≤ f x) (hf : Summable f) — check exact name/signature: `Summable.of_nonneg_of_le (hg : ∀ b, 0 ≤ g b) (h : ∀ b, g b ≤ f b) (hf : Summable f) : Summable g` ✓ (in Order.lean).
Bernoulli upper lemma proof detail (L_bern_upper): for m ≥ 1, x := 1/m ∈ (0,1].
1 − (1−x)ⁿ = (1−x)⁰·... use geom_sum_eq with y = 1−x: Σ_{j∈range n} y^j = (yⁿ − 1)/(y − 1) = (1 − yⁿ)/x (since y−1 = −x). So 1 − yⁿ = x·Σ yʲ — requires x ≠ 0 for the division form; alternatively use the ring identity directly: (1 − y) * Σ_{j∈range n} y^j = 1 − yⁿ — Mathlib: `geom_sum_mul`? There's `geom_sum_mul : (x − 1) * Σ x^i = x^n − 1` (in a ring, no division!) — check name: `geom_sum_mul (x : α) (n : ℕ) [Ring α] : (∑ i in range n, x^i) * (x − 1) = x^n − 1` or (x−1)*sum. With that: (1−y)·Σ yʲ = 1 − yⁿ directly ✓ no division.
Then Σ_{j<n} yʲ ≥ Σ_{j<n} (1 − jx) by Bernoulli per term (one_add_mul_le_pow with a = −x: 1 + j(−x) ≤ (1−x)ʲ needs −2 ≤ −x ⟸ x ≤ 2 ✓).
Σ_{j<n} (1 − jx) = n − x·Σ_{j<n} j = n − x·(n(n−1)/2).
So 1 − yⁿ ≥ x·(n − C(n,2)·x) where C(n,2) as real = n(n−1)/2.
h⁺(m) = yⁿ − 1 + nx = nx − (1 − yⁿ) ≤ nx − x(n − C(n,2)x) = C(n,2)x² = C(n,2)/m² ✓.
In ℝ: C(n,2) real = n*(n−1)/2 — I'll state with (n*(n−1)/2 : ℝ) form? Cleaner: use (n.choose 2 : ℝ) with Nat.choose_two_right + Nat.cast... choose_two_right : n.choose 2 = n * (n − 1) / 2 (nat division) — casting nat division to real needs n*(n−1) even — Nat.even_mul_pred_self ✓ (n*(n−1) even). Might be simpler to state the lemma with (n : ℝ)*(n−1)/2 directly, avoiding choose. Yes: L_bern_upper conclusion: ... ≤ (n : ℝ)*(n−1)/(2*m^2). The summability comparison then uses C := n(n−1)/2 as a real constant. Cleaner.
For the finite sum Σ_{j<n} j over ℝ: cast: Σ_{j∈range n} (j:ℝ) = n(n−1)/2 via Finset.sum_range_id... there's `Finset.sum_range_id : Σ i in range n, i = n * (n - 1) / 2` (ℕ) — cast with same evenness issue. Better: `Finset.sum_range_id_mul_two` in ℕ then cast? Or find real version: there is a known lemma `Finset.sum_range_id_div_two`? Alternatively compute directly: Σ_{j∈range n} (j:ℝ) — Mathlib has `Finset.sum_range_id (n : ℕ) : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2` — for ℕ. Hmm, there's also `sum_range_geometric`... Let me just handle: (Σ_{j∈range n} (j : ℝ)) = (n:ℝ)*(n−1)/2. Prove: 2 * Σ = n(n−1): from sum_range_id_mul_two cast: cast both sides. (Nat.cast_inj). Doable:
```lean
have hsum : ∑ j ∈ Finset.range n, (j : ℝ) = n * (n - 1) / 2 := by
have h := Finset.sum_range_id_mul_two n
-- h : (Σ i in range n, i) * 2 = n * (n - 1) in ℕ
have h2 : ((∑ i ∈ Finset.range n, i : ℕ) : ℝ) * 2 = n * (n - 1) := by exact_mod_cast h
-- then divide
...
```
Careful with casts (n−1 : ℕ) vs (n:ℝ)−1: Nat.cast_sub needs 1 ≤ n. Since we need n ≥ 1 anyway (actually n ≥ 20 in main theorem; but lemma can assume 1 ≤ n), fine.
OK. Also for L_bern_nonneg: one_add_mul_le_pow (H : -2 ≤ a) n : 1 + n*a ≤ (1+a)^n with a = −1/m: −2 ≤ −1/m ⟺ 1/m ≤ 2 ⟸ m ≥ 1 (1/m ≤ 1 ≤ 2 ✓). Then 0 ≤ (1−1/m)ⁿ − 1 + n/m ⟸ 1 − n/m ≤ (1−1/m)ⁿ ✓ = 1 + n·(−1/m) ✓ ring-normalize.
Write both lemmas in Scratch now. I'll write them with full context and iterate.
All names verified. Writing the two Bernoulli lemmas in the scratch file.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean",
"old_string": "end Scratch",
"new_string": "/-- h\u207a(m) \u2265 0 for m \u2265 1: first-order Bernoulli, (1\u22121/m)\u207f \u2265 1 \u2212 n/m. -/\ntheorem bern_term_nonneg (n : \u2115) (m : \u2115) (hm : 1 \u2264 m) :\n 0 \u2264 (1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / m := by\n have hm0 : (m : \u211d) \u2260 0 := by positivity\n have h1 : (1 : \u211d) + n * (-1 / m) \u2264 (1 + -1 / (m : \u211d)) ^ n := by\n apply one_add_mul_le_pow\n have : (1 : \u211d) / m \u2264 1 := by\n rw [div_le_one (by positivity)]; exact_mod_cast hm\n linarith\n have h2 : (1 : \u211d) - n / m \u2264 (1 - 1 / m) ^ n := by\n have : (1 : \u211d) + n * (-1 / m) = 1 - n / m := by field_simp; ring\n rwa [this, show (1 : \u211d) + -1 / m = 1 - 1 / m by ring] at h1\n linarith\n\n/-- h\u207a(m) \u2264 (n choose 2)/m\u00b2 for m \u2265 1: geometric factorization\n1 \u2212 (1\u2212x)\u207f = x\u00b7\u03a3_{j<n} (1\u2212x)\u02b2 \u2265 x\u00b7(n \u2212 x\u00b7\u03a3j) plus Bernoulli per term. -/\ntheorem bern_term_upper (n : \u2115) (m : \u2115) (hm : 1 \u2264 m) :\n (1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / m \u2264 (n : \u211d) * (n - 1) / (2 * m ^ 2) := by\n have hm0 : (m : \u211d) \u2260 0 := by positivity\n set x := (1 : \u211d) / m with hxdef\n have hx1 : x \u2264 1 := by\n rw [hxdef, div_le_one (by positivity)]; exact_mod_cast hm\n have hx0 : 0 \u2264 x := by positivity\n -- per-term Bernoulli: (1 \u2212 x)\u02b2 \u2265 1 \u2212 jx\n have hterm : \u2200 j : \u2115, 1 - j * x \u2264 (1 - x) ^ j := by\n intro j\n have := one_add_mul_le_pow (a := -x) (by linarith : (-2 : \u211d) \u2264 -x) j\n rwa [show (1 : \u211d) + j * (-x) = 1 - j * x by ring,\n show (1 : \u211d) + -x = 1 - x by ring] at this\n -- sum of j over range n, as a real identity\n have hsum : \u2211 j \u2208 Finset.range n, (j : \u211d) = (n : \u211d) * (n - 1) / 2 := by\n have h := Finset.sum_range_id_mul_two n\n have h2 : ((\u2211 i \u2208 Finset.range n, i : \u2115) : \u211d) * 2 = (n : \u211d) * ((n : \u211d) - 1) := by\n have hcast : ((\u2211 i \u2208 Finset.range n, i : \u2115) : \u211d) * 2 = ((n * (n - 1) : \u2115) : \u211d) := by\n exact_mod_cast h\n rw [hcast]\n rcases Nat.eq_zero_or_pos n with hn0 | hnpos\n \u00b7 simp [hn0]\n \u00b7 rw [Nat.cast_sub hnpos.one_le]; push_cast; ring\n have h3 : (\u2211 j \u2208 Finset.range n, (j : \u211d)) * 2 = (n : \u211d) * ((n : \u211d) - 1) := by\n rw [\u2190 h2]; push_cast [Finset.sum]; simp [Nat.cast_sum]\n linarith\n -- geometric factorization: 1 \u2212 (1\u2212x)\u207f = x \u00b7 \u03a3_{j<n} (1\u2212x)\u02b2\n have hgeom : (1 - (1 - x) ^ n) = x * \u2211 j \u2208 Finset.range n, (1 - x) ^ j := by\n have h := geom_sum_mul (1 - x) n\n -- h : (\u2211 i in range n, (1\u2212x)^i) * ((1\u2212x) \u2212 1) = (1\u2212x)^n \u2212 1\n have hx0' : x \u2260 0 \u2228 x = 0 := ne_or_eq x 0\n rcases hx0' with hx0' | rfl\n \u00b7 have hx1' : (1 - x) - 1 = -x := by ring\n rw [hx1'] at h\n have : \u2211 j \u2208 Finset.range n, (1 - x) ^ j = ((1 - x) ^ n - 1) / (-x) := by\n field_simp; linarith [h]\n rw [this]; field_simp; ring\n \u00b7 simp\n -- assemble\n have hmain : (1 - x) ^ n - 1 + (n : \u211d) * x \u2264 (n : \u211d) * (n - 1) / 2 * x ^ 2 := by\n have h4 : (n : \u211d) * x - (n * (n - 1) / 2) * x ^ 2 \u2264 1 - (1 - x) ^ n := by\n rw [hgeom]\n have h5 : (n : \u211d) - x * ((n : \u211d) * (n - 1) / 2) \u2264\n \u2211 j \u2208 Finset.range n, (1 - x) ^ j := by\n have h6 : \u2211 j \u2208 Finset.range n, (1 - (j : \u211d) * x) =\n (n : \u211d) - x * \u2211 j \u2208 Finset.range n, (j : \u211d) := by\n rw [Finset.mul_sum, Finset.sum_sub_distrib]\n simp [Finset.sum_const, Finset.card_range, nsmul_eq_mul]\n rw [hsum] at h6\n rw [\u2190 h6]\n exact Finset.sum_le_sum fun j _ => hterm j\n calc (n : \u211d) * x - (n * (n - 1) / 2) * x ^ 2\n = x * ((n : \u211d) - x * (n * (n - 1) / 2)) := by ring\n _ \u2264 x * \u2211 j \u2208 Finset.range n, (1 - x) ^ j :=\n mul_le_mul_of_nonneg_left h5 hx0\n linarith\n -- convert back to the m-form\n have hx2 : x ^ 2 = 1 / m ^ 2 := by rw [hxdef]; ring\n have hdiv : (n : \u211d) / m = n * x := by rw [hxdef]; ring\n rw [hdiv]\n have h7 : (1 - 1 / (m : \u211d)) ^ n = (1 - x) ^ n := by rw [hxdef]\n rw [h7]\n calc (1 - x) ^ n - 1 + (n : \u211d) * x\n \u2264 (n : \u211d) * (n - 1) / 2 * x ^ 2 := hmain\n _ = (n : \u211d) * (n - 1) / (2 * m ^ 2) := by rw [hx2]; ring\n\nend Scratch"
}
result 2026-08-20 03:42:59Z → 2026-08-23 16:25:46Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean",
"oldString": " rw [e, neg_div, one_div_div]\n ring\n linear_combination h1\n\nend NguyenRH1\n\nend",
"newString": " rw [e, neg_div, one_div_div]\n ring\n linear_combination h1",
"originalFile": "/-\nNguyenRH1/LiFEntire.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-iv (D-068 \u00a74):\nthe partial-fraction difference function\n\n Fexpr s := logDeriv \u03b6 s \u2212 seriesFun s + 1/s + 1/(s\u22121) \u2212 (log \u03c0)/2 + \u03c8(s/2)/2\n\nis ENTIRE. The excluded set is\n\n badPoint s := IsNontrivialZero s \u2228 s = 0 \u2228 s = 1 \u2228 \u2203 n \u2265 1, s = \u22122n;\n\nat each bad point the principal parts cancel exactly (D-068 \u00a70's residue\nbookkeeping: +m vs +m at nontrivial zeros; \u22121 vs \u22121 at 1; 0 = \u22121+1 at 0;\n+1 vs +1 at \u22122n). Since Mathlib lacks a general removable-singularity\ntheorem, entirety is packaged via the punctured-limit extension\n\n Gentire s := limUnder (\ud835\udcdd[\u2260] s) Fexpr:\n\nat GOOD points Fexpr is analytic (hence the punctured limit is the\nvalue), at each BAD point an explicit analytic witness agrees with Fexpr\non a punctured neighbourhood (the principal-part splits), so Gentire is\neverywhere analytic and agrees with Fexpr at every good point\n(`gentire_analyticAt`, `gentire_eq_Fexpr`).\n\nThe witnesses:\n* nontrivial zero \u03c1\u2080: [logDeriv \u03b6 \u2212 m/(s\u2212\u03c1\u2080)] analytic by the order\n normal form (`logDeriv_zeta_sub_mult_div_eventually`, the LiSides NF\n block) + [seriesFun \u2212 m/(s\u2212\u03c1\u2080)] analytic by 5e-iii's\n `seriesFun_sub_polar_analyticAt`; the elementary terms analytic since\n re \u03c1\u2080 \u2208 (0, 1) avoids 0, 1, \u22122n.\n* s = 1: logDeriv \u03b6 + 1/(s\u22121) = logDeriv zetaA punctured (zetaA\n analytic, zetaA 1 = 1 \u2014 ii\u2032-1b).\n* s = 0: \u03c8(s/2)/2 + 1/s = \u2212\u03b3/2 + \u00bd\u00b7digammaSeriesPart(s/2) punctured\n (the digamma series, Zeta23 `DigammaSeries.digamma_series`; the series\n part analytic on ball(0, 1/2) by the M-test); logDeriv \u03b6 analytic at\n 0 (\u03b6(0) = \u22121/2 \u2260 0).\n* s = \u22122n: logDeriv \u03b6 \u2212 1/(s+2n) analytic (NF + `zeroMult_neg_two_mul`,\n session 026); \u03c8(s/2)/2 + 1/(s+2n) = \u00bd\u00b7H_n(s/2) punctured where H_n is\n the digamma series with the j = n\u22121 term dropped (analytic on\n ball(\u2212n, 1/2) by the eventually M-test).\n\nAlso proved: `zeta_zero_classification` (every zero of \u03b6 is nontrivial,\n0, or \u22122n \u2014 from Zeta23's `completedRiemannZeta_eq_zero_iff` +\n`Gamma\u211d_eq_zero_iff`) and `analyticAt_digamma` (\u03c8 analytic off\n{0} \u222a \u2212\u2115).\n\nArchive references: D-068 \u00a74, journal-028 (the series machinery),\njournal-017 (the NF block), journal-026 (zeroMult(\u22122n)).\n-/\nimport Mathlib\nimport Zeta23.Statement\nimport Zeta23.RvM.CountByIntegral\nimport Zeta23.GammaFacts.Series\nimport NguyenRH1.LiSeries\nimport NguyenRH1.LiTrivialZeros\nimport NguyenRH1.LiDigamma\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. The difference function and the excluded set -/\n\n/-- The partial-fraction difference function (D-068 \u00a70):\n\u03b6\u2032/\u03b6 \u2212 series + 1/s + 1/(s\u22121) \u2212 \u00bdlog \u03c0 + \u00bd\u03c8(s/2); entire after the\npunctured-limit extension (`Gentire`). -/\ndef Fexpr (s : \u2102) : \u2102 :=\n logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n\n/-- The excluded set of the partial-fraction identity: the nontrivial\nzeros, 0, 1, and the trivial zeros \u22122n (n \u2265 1). -/\ndef badPoint (s : \u2102) : Prop :=\n IsNontrivialZero s \u2228 s = 0 \u2228 s = 1 \u2228 \u2203 n : \u2115, 1 \u2264 n \u2227 s = -2 * (n : \u2102)\n\n/-! ## 1. Digamma is analytic off {0} \u222a \u2212\u2115 -/\n\n/-- \u03c8 = logDeriv \u0393 is analytic at any w \u2209 {0} \u222a \u2212\u2115 (the finite-min ball\navoiding the poles; \u0393 analytic + nonzero there). -/\nlemma analyticAt_digamma {w : \u2102} (hw : \u2200 m : \u2115, w \u2260 -(m : \u2102)) :\n AnalyticAt \u2102 Complex.digamma w := by\n set M : \u2115 := \u2308\u2016w\u2016\u2309\u208a with hM\n have hMle : \u2016w\u2016 \u2264 M := Nat.le_ceil _\n set d : Finset \u211d := (Finset.range (M + 2)).image (fun m : \u2115 => \u2016w + (m : \u2102)\u2016) with hd\n have hdne : d.Nonempty := by\n refine \u27e8\u2016w\u2016, ?_\u27e9\n rw [hd]\n refine Finset.mem_image.mpr \u27e80, Finset.mem_range.mpr (by omega), ?_\u27e9\n simp\n have hdpos : \u2200 x \u2208 d, 0 < x := by\n intro x hx\n rw [hd] at hx\n obtain \u27e8m, -, rfl\u27e9 := Finset.mem_image.mp hx\n rw [norm_pos_iff]\n intro hz\n exact hw m (eq_neg_of_add_eq_zero_left hz)\n have hmin0 : 0 < d.min' hdne := hdpos _ (Finset.min'_mem _ _)\n set \u03b4 : \u211d := min (1 / 2) (d.min' hdne / 2) with h\u03b4\n have h\u03b40 : 0 < \u03b4 := lt_min (by norm_num) (half_pos hmin0)\n have h\u03b41 : \u03b4 \u2264 1 / 2 := min_le_left _ _\n have h\u03b42 : \u03b4 \u2264 d.min' hdne / 2 := min_le_right _ _\n -- every point of ball(w, \u03b4) avoids the poles\n have hball : \u2200 y \u2208 Metric.ball w \u03b4, \u2200 m : \u2115, y \u2260 -(m : \u2102) := by\n intro y hy m hye\n have hdist : \u2016y - w\u2016 < \u03b4 := by\n have := Metric.mem_ball.mp hy\n rwa [dist_eq_norm] at this\n by_cases hm : m < M + 2\n \u00b7 have hmem : \u2016w + (m : \u2102)\u2016 \u2208 d := by\n rw [hd]\n exact Finset.mem_image.mpr \u27e8m, Finset.mem_range.mpr hm, rfl\u27e9\n have hle : d.min' hdne \u2264 \u2016w + (m : \u2102)\u2016 := Finset.min'_le _ _ hmem\n have hnm : \u2016y + (m : \u2102)\u2016 = 0 := by rw [hye]; simp\n have hnorm : \u2016w + (m : \u2102)\u2016 \u2264 \u2016y + (m : \u2102)\u2016 + \u2016y - w\u2016 := by\n calc \u2016w + (m : \u2102)\u2016 = \u2016(y + (m : \u2102)) - (y - w)\u2016 := by congr 1; ring\n _ \u2264 \u2016y + (m : \u2102)\u2016 + \u2016y - w\u2016 := norm_sub_le _ _\n rw [hnm] at hnorm\n simp at hnorm\n linarith\n \u00b7 push Not at hm\n have hnm : y + (m : \u2102) = 0 := by rw [hye]; simp\n have hnorm : (m : \u211d) \u2264 \u2016y + (m : \u2102)\u2016 + \u2016y\u2016 := by\n calc (m : \u211d) = \u2016(m : \u2102)\u2016 := (RCLike.norm_natCast m).symm\n _ = \u2016(y + (m : \u2102)) - y\u2016 := by congr 1; ring\n _ \u2264 \u2016y + (m : \u2102)\u2016 + \u2016y\u2016 := norm_sub_le _ _\n rw [hnm] at hnorm\n simp at hnorm\n have hyw : \u2016y\u2016 \u2264 \u2016y - w\u2016 + \u2016w\u2016 := by\n calc \u2016y\u2016 = \u2016(y - w) + w\u2016 := by congr 1; ring\n _ \u2264 \u2016y - w\u2016 + \u2016w\u2016 := norm_add_le _ _\n have hmM : M + 2 \u2264 m := by omega\n have hmre : (M : \u211d) + 2 \u2264 (m : \u211d) := by exact_mod_cast hmM\n linarith [hMle, hdist, h\u03b41]\n -- \u0393 analytic on the ball\n have hGammaOn : DifferentiableOn \u2102 Complex.Gamma (Metric.ball w \u03b4) := by\n intro y hy\n exact Complex.differentiableAt_Gamma y (hball y hy) |>.differentiableWithinAt\n have hGammaAn : AnalyticOnNhd \u2102 Complex.Gamma (Metric.ball w \u03b4) :=\n hGammaOn.analyticOnNhd Metric.isOpen_ball\n have hAn : AnalyticOnNhd \u2102 (fun z => deriv Complex.Gamma z / Complex.Gamma z)\n (Metric.ball w \u03b4) := by\n intro y hy\n exact ((hGammaAn y hy).deriv).div (hGammaAn y hy)\n (Complex.Gamma_ne_zero (hball y hy))\n have heq : Complex.digamma = fun z => deriv Complex.Gamma z / Complex.Gamma z := by\n funext z\n rw [digamma_def, logDeriv_apply]\n rw [heq]\n exact hAn w (Metric.mem_ball_self h\u03b40)\n\n/-- \u03c8(s/2)/2 is analytic wherever s/2 avoids the poles. -/\nlemma analyticAt_digamma_div_two {s : \u2102} (h : \u2200 m : \u2115, s / 2 \u2260 -(m : \u2102)) :\n AnalyticAt \u2102 (fun s => Complex.digamma (s / 2) / 2) s := by\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s / 2) s := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n have h2 : AnalyticAt \u2102 (Complex.digamma \u2218 fun s : \u2102 => s / 2) s :=\n AnalyticAt.comp (f := fun s : \u2102 => s / 2) (analyticAt_digamma h) h1\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : \u2102) \u2260 0)\n exact h2\n\n/-! ## 2. The zero classification -/\n\n/-- Every zero of \u03b6 is a nontrivial zero, 0, or a trivial zero \u22122n\n(from Zeta23's `completedRiemannZeta_eq_zero_iff` via the \u0393R-pole case\nsplit; `riemannZeta_ne_zero_of_one_le_re` excludes re \u2265 1). -/\nlemma zeta_zero_classification {s : \u2102} (hs : riemannZeta s = 0) :\n IsNontrivialZero s \u2228 s = 0 \u2228 \u2203 n : \u2115, 1 \u2264 n \u2227 s = -2 * (n : \u2102) := by\n by_cases h1 : 1 \u2264 s.re\n \u00b7 exact absurd hs (riemannZeta_ne_zero_of_one_le_re h1)\n \u00b7 push Not at h1\n by_cases h0 : 0 < s.re\n \u00b7 exact Or.inl \u27e8hs, h0, h1\u27e9\n \u00b7 push Not at h0\n by_cases hs0 : s = 0\n \u00b7 exact Or.inr (Or.inl hs0)\n \u00b7 by_cases hG : Complex.Gamma\u211d s = 0\n \u00b7 rw [Complex.Gamma\u211d_eq_zero_iff] at hG\n obtain \u27e8n, hn\u27e9 := hG\n rcases Nat.eq_zero_or_pos n with hn0 | hnpos\n \u00b7 subst hn0\n simp at hn\n exact absurd hn hs0\n \u00b7 exact Or.inr (Or.inr \u27e8n, hnpos, by rw [hn]; ring\u27e9)\n \u00b7 have h\u039b : completedRiemannZeta s = 0 := by\n rw [RvM.completedRiemannZeta_eq_Gamma\u211d_mul hs0 hG, hs, mul_zero]\n have hpos := (RvM.completedRiemannZeta_eq_zero_iff.mp h\u039b).2.1\n linarith\n\n/-! ## 3. The logDeriv normal-form witness at a zero -/\n\n/-- At a zero \u03c1\u2080 \u2260 1 of \u03b6, the subtraction of the polar term\nmult(\u03c1\u2080)/(s\u2212\u03c1\u2080) from logDeriv \u03b6 agrees punctured with an analytic\nfunction (the logDeriv of the NF factor h). Unified witness for the\nnontrivial and the trivial zeros (the LiSides NF block). -/\nlemma logDeriv_zeta_sub_mult_div_eventually {\u03c1\u2080 : \u2102} (_h\u03b6 : riemannZeta \u03c1\u2080 = 0)\n (h\u03c11 : \u03c1\u2080 \u2260 1) :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W \u03c1\u2080 \u2227\n \u2200\u1da0 s in \ud835\udcdd[\u2260] \u03c1\u2080, logDeriv riemannZeta s - (zeroMult \u03c1\u2080 : \u2102) / (s - \u03c1\u2080) = W s := by\n have h\u03c1\u03b1 : AnalyticAt \u2102 riemannZeta \u03c1\u2080 := analyticAt_riemannZeta h\u03c11\n obtain \u27e8h, hh, hh0, hfh\u27e9 := h\u03c1\u03b1.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne h\u03c11)\n refine \u27e8logDeriv h, hh.deriv.div hh hh0, ?_\u27e9\n filter_upwards [self_mem_nhdsWithin,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hs\u03c1 hfhs hhs hhas\n have hfhs' : riemannZeta =\u1da0[\ud835\udcdd s]\n (fun z => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080 \u2022 h z) := hfhs\n have hs\u03c1' : s - \u03c1\u2080 \u2260 0 := sub_ne_zero.mpr hs\u03c1\n have hld : logDeriv riemannZeta s =\n (analyticOrderNatAt riemannZeta \u03c1\u2080 : \u2102) / (s - \u03c1\u2080) + logDeriv h s := by\n have e1 : logDeriv riemannZeta s =\n logDeriv (fun z => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080 * h z) s := by\n simp only [logDeriv_apply, hfhs'.deriv_eq, hfhs'.self_of_nhds, smul_eq_mul]\n rw [e1, logDeriv_mul (f := fun z : \u2102 => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080)\n (g := h) s (pow_ne_zero _ hs\u03c1') hhs (by fun_prop) hhas.differentiableAt]\n have e2 : logDeriv (fun z : \u2102 => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080) s\n = (analyticOrderNatAt riemannZeta \u03c1\u2080 : \u2102) / (s - \u03c1\u2080) := by\n rw [show (fun z : \u2102 => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080)\n = (fun x : \u2102 => x ^ analyticOrderNatAt riemannZeta \u03c1\u2080) \u2218 (fun z => z - \u03c1\u2080)\n from rfl,\n logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]\n simp\n rw [e2]\n have hmz : (zeroMult \u03c1\u2080 : \u2102) = (analyticOrderNatAt riemannZeta \u03c1\u2080 : \u2102) := rfl\n rw [hld, hmz]\n ring\n\n/-! ## 4. The witness at s = 1 -/\n\n/-- Near s = 1 (punctured): logDeriv \u03b6 s = logDeriv zetaA s \u2212 1/(s\u22121). -/\nlemma logDeriv_zeta_eq_logDeriv_zetaA_sub :\n \u2200\u1da0 s in \ud835\udcdd[\u2260] (1 : \u2102),\n logDeriv riemannZeta s = logDeriv zetaA s - 1 / (s - 1) := by\n filter_upwards [self_mem_nhdsWithin,\n mem_nhdsWithin_of_mem_nhds zetaA_ne_zero_near_one] with s hs1 hZA\n have hs1' : s - 1 \u2260 0 := sub_ne_zero.mpr hs1\n have h\u03b6 : riemannZeta s \u2260 0 := by\n have e := zetaA_apply hs1\n intro hz\n rw [hz, mul_zero] at e\n exact hZA e\n have hcong : zetaA =\u1da0[\ud835\udcdd s] (fun w : \u2102 => (w - 1) * riemannZeta w) := by\n filter_upwards [eventually_ne_nhds hs1] with z hz using zetaA_apply hz\n have hld : logDeriv zetaA s = 1 / (s - 1) + logDeriv riemannZeta s := by\n have e1 : logDeriv zetaA s = logDeriv (fun w : \u2102 => (w - 1) * riemannZeta w) s := by\n simp only [logDeriv_apply, hcong.deriv_eq, hcong.self_of_nhds]\n rw [e1, logDeriv_mul (f := fun w : \u2102 => w - 1) (g := riemannZeta) s hs1' h\u03b6\n (differentiableAt_id.sub (differentiableAt_const 1))\n (analyticAt_riemannZeta hs1).differentiableAt]\n have e2 : logDeriv (fun w : \u2102 => w - 1) s = 1 / (s - 1) := by\n have hd : deriv (fun w : \u2102 => w - 1) s = 1 :=\n ((hasDerivAt_id s).sub_const (1 : \u2102)).deriv\n rw [logDeriv_apply, hd]\n rw [e2]\n rw [hld]\n ring\n\n/-- The witness at s = 1: Fexpr agrees punctured with\nlogDeriv zetaA \u2212 seriesFun + 1/s \u2212 (log \u03c0)/2 + \u03c8(s/2)/2, analytic at 1. -/\nlemma Fexpr_eventually_one :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W 1 \u2227 \u2200\u1da0 s in \ud835\udcdd[\u2260] (1 : \u2102), Fexpr s = W s := by\n have h1dig : \u2200 m : \u2115, (1 : \u2102) / 2 \u2260 -(m : \u2102) := by\n intro m h\n have hre := congrArg Complex.re h\n simp at hre\n have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n refine \u27e8fun s => logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : \u2102) / 2\n + Complex.digamma (s / 2) / 2, ?_, ?_\u27e9\n \u00b7 have hA : AnalyticAt \u2102 (logDeriv zetaA) 1 :=\n (zetaA_analyticAt_one.deriv).div zetaA_analyticAt_one (by rw [zetaA_one]; norm_num)\n have hB : AnalyticAt \u2102 seriesFun 1 := seriesFun_analyticAt (by\n intro h\n have hlt := h.2.2\n rw [Complex.one_re] at hlt\n exact lt_irrefl 1 hlt)\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / s) 1 :=\n analyticAt_const.div analyticAt_id (by norm_num)\n have hD : AnalyticAt \u2102 (fun s : \u2102 => (Real.log Real.pi : \u2102) / 2) 1 := analyticAt_const\n have hE : AnalyticAt \u2102 (fun s => Complex.digamma (s / 2) / 2) 1 :=\n analyticAt_digamma_div_two h1dig\n exact ((((hA.sub hB).add hC).sub hD).add hE)\n \u00b7 filter_upwards [logDeriv_zeta_eq_logDeriv_zetaA_sub] with s hs\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n = logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : \u2102) / 2\n + Complex.digamma (s / 2) / 2\n rw [hs]\n ring\n\n/-! ## 5. The digamma series part and the witness at s = 0 -/\n\n/-- The series part of the digamma partial-fraction expansion\n\u03a3'_j (1/(j+1) \u2212 1/(w+j+1)); analytic on ball(0, 1/2). -/\ndef digammaSeriesPart (w : \u2102) : \u2102 :=\n \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))\n\n/-- A point of ball(\u2212n, 1/2) other than \u2212n is not an integer\n(the integer lattice is 1-separated). -/\nlemma integerComplement_of_mem_ball_neg_natCast {n : \u2115} {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) (hwn : w \u2260 -(n : \u2102)) :\n w \u2208 Complex.integerComplement := by\n intro hk\n obtain \u27e8k, rfl\u27e9 := hk\n have h2 : dist (k : \u2102) (-(n : \u2102)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [Complex.dist_eq] at h2\n by_cases hk0 : k = -(n : \u2124)\n \u00b7 exact hwn (by rw [hk0]; push_cast; ring)\n \u00b7 have h1 : (1 : \u2124) \u2264 |k + (n : \u2124)| := Int.one_le_abs (by\n intro hh\n exact hk0 (eq_neg_of_add_eq_zero_left hh))\n have h3 : (k : \u2102) - -(n : \u2102) = (k : \u2102) + ((n : \u2124) : \u2102) := by push_cast; ring\n rw [h3] at h2\n have h4 : (1 : \u211d) \u2264 \u2016(k : \u2102) + ((n : \u2124) : \u2102)\u2016 := by\n have h6 : |((k : \u2102) + ((n : \u2124) : \u2102)).re| \u2264 \u2016(k : \u2102) + ((n : \u2124) : \u2102)\u2016 :=\n Complex.abs_re_le_norm _\n have hre : ((k : \u2102) + ((n : \u2124) : \u2102)).re = (k : \u211d) + (n : \u211d) := by\n simp [Complex.add_re]\n rw [hre] at h6\n have h5 : (1 : \u211d) \u2264 |(k : \u211d) + (n : \u211d)| := by\n have e : |(k : \u211d) + (n : \u211d)| = ((|k + (n : \u2124)| : \u2124) : \u211d) := by\n rw [show (k : \u211d) + (n : \u211d) = (((k + (n : \u2124)) : \u2124) : \u211d) by push_cast; ring,\n Int.cast_abs]\n rw [e]\n exact_mod_cast h1\n exact h5.trans h6\n linarith\n\n/-- Pole avoidance on ball(0, 1/2): w + j + 1 \u2260 0. -/\nlemma add_nat_add_one_ne_zero_of_mem_ball {w : \u2102} (hw : w \u2208 Metric.ball 0 (1 / 2)) (j : \u2115) :\n w + (j : \u2102) + 1 \u2260 0 := by\n have hwn : \u2016w\u2016 < 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rwa [dist_zero_right] at h\n intro h\n have h1 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n rw [h] at h1\n simp at h1\n have h2 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n have hj0 : (0 : \u211d) \u2264 (j : \u211d) := Nat.cast_nonneg j\n linarith\n\n/-- The digamma series part is analytic on ball(0, 1/2) (M-test,\n\u03a3 1/(j+1)\u00b2 majorant). -/\nlemma digammaSeriesPart_analyticOn :\n AnalyticOnNhd \u2102 digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n have hsum : Summable (fun j : \u2115 => (1 : \u211d) / ((j : \u211d) + 1) ^ 2) :=\n summable_div_add_one_sq 1\n have hu : HasSumUniformlyOn (fun (j : \u2115) => fun w : \u2102 => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1))\n (fun w => \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n (Metric.ball 0 (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable hsum\n intro j w hw\n have hwn : \u2016w\u2016 < 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rwa [dist_zero_right] at h\n have hj1 : (0 : \u211d) < (j : \u211d) + 1 := by positivity\n have hwj : w + (j : \u2102) + 1 \u2260 0 := add_nat_add_one_ne_zero_of_mem_ball hw j\n have hj0 : ((j : \u2102) + 1) \u2260 0 := Nat.cast_add_one_ne_zero j\n have halg : 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)\n = w / (((j : \u2102) + 1) * (w + j + 1)) := by\n field_simp\n ring\n have hnorm1 : \u2016((j : \u2102) + 1)\u2016 = (j : \u211d) + 1 := by\n have e : ((j : \u2102) + 1) = ((j + 1 : \u2115) : \u2102) := by push_cast; ring\n rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]\n have hnorm2 : ((j : \u211d) + 1) / 2 \u2264 \u2016w + (j : \u2102) + 1\u2016 := by\n have h2 : (w + (j : \u2102) + 1).re \u2264 \u2016w + (j : \u2102) + 1\u2016 := Complex.re_le_norm _\n have h3 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have h4 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n linarith\n rw [halg, norm_div, norm_mul, hnorm1]\n have hA2 : (0 : \u211d) < ((j : \u211d) + 1) ^ 2 := by positivity\n have hden0 : (0 : \u211d) < ((j : \u211d) + 1) * \u2016w + (j : \u2102) + 1\u2016 :=\n mul_pos hj1 (by linarith [hnorm2, hj1])\n rw [div_le_div_iff\u2080 hden0 hA2]\n nlinarith [hwn.le, hnorm2, hj1.le, sq_nonneg ((j : \u211d) + 1)]\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset \u2115 => fun w => \u2211 j \u2208 t, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n (fun w => \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n atTop (Metric.ball 0 (1 / 2)) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)\n have hdiff : DifferentiableOn \u2102 (fun w => \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n (Metric.ball 0 (1 / 2)) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t w hw\n rw [show (fun w => \u2211 j \u2208 t, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n = \u2211 j \u2208 t, (fun w => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) from by\n funext w; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro j _\n have hwj : w + (j : \u2102) + 1 \u2260 0 := add_nat_add_one_ne_zero_of_mem_ball hw j\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => 1 / (w + (j : \u2102) + 1)) w :=\n (differentiableAt_const (1 : \u2102)).div\n ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))\n hwj\n exact (differentiableAt_const _).sub h2\n have hdiff2 : DifferentiableOn \u2102 digammaSeriesPart (Metric.ball 0 (1 / 2)) := hdiff\n exact hdiff2.analyticOnNhd Metric.isOpen_ball\n\n/-- The digamma series evaluation near 0 (punctured): for\nw \u2208 ball(0, 1/2), w \u2260 0. -/\nlemma digamma_eq_seriesPart_near_zero {w : \u2102}\n (hw : w \u2208 Metric.ball 0 (1 / 2)) (hw0 : w \u2260 0) :\n Complex.digamma w = -(Real.eulerMascheroniConstant : \u2102) - 1 / w + digammaSeriesPart w := by\n have hZ : w \u2208 Complex.integerComplement :=\n integerComplement_of_mem_ball_neg_natCast (n := 0) (by simpa using hw) (by simpa using hw0)\n have h := Zeta23.DigammaSeries.digamma_series hZ\n rw [h]\n rfl\n\n/-- The witness at s = 0: Fexpr agrees punctured with\nlogDeriv \u03b6 \u2212 seriesFun + 1/(s\u22121) \u2212 (log \u03c0)/2 + (\u2212\u03b3 + digammaSeriesPart(s/2))/2,\nanalytic at 0. -/\nlemma Fexpr_eventually_zero :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W 0 \u2227 \u2200\u1da0 s in \ud835\udcdd[\u2260] (0 : \u2102), Fexpr s = W s := by\n have hA : AnalyticAt \u2102 (logDeriv riemannZeta) 0 := by\n have hz : riemannZeta 0 \u2260 0 := by rw [riemannZeta_zero]; norm_num\n exact ((analyticAt_riemannZeta (by norm_num)).deriv).div\n (analyticAt_riemannZeta (by norm_num)) hz\n have hB : AnalyticAt \u2102 seriesFun 0 := seriesFun_analyticAt (by\n intro h\n have hpos := h.2.1\n rw [Complex.zero_re] at hpos\n exact lt_irrefl 0 hpos)\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s - 1)) 0 := by\n apply AnalyticAt.div analyticAt_const (g := fun s : \u2102 => s - 1) _ (by norm_num)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => (Real.log Real.pi : \u2102) / 2) 0 := analyticAt_const\n have hE : AnalyticAt \u2102\n (fun s => (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2) 0 := by\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : \u2102) \u2260 0)\n apply AnalyticAt.add analyticAt_const\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s / 2) 0 := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n have hdsp0 : AnalyticAt \u2102 digammaSeriesPart ((0 : \u2102) / 2) := by\n rw [zero_div]\n exact digammaSeriesPart_analyticOn 0 (Metric.mem_ball_self (by norm_num))\n exact AnalyticAt.comp (f := fun s : \u2102 => s / 2) hdsp0 h1\n refine \u27e8fun s => logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2\n + (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2, ?_, ?_\u27e9\n \u00b7 exact ((((hA.sub hB).add hC).sub hD).add hE)\n \u00b7 -- punctured agreement on ball(0, 1/2)\n rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball]\n refine \u27e81 / 2, by norm_num, fun s hsball hsne => ?_\u27e9\n have hs0 : s \u2260 0 := hsne\n have hs2ball : s / 2 \u2208 Metric.ball 0 (1 / 2) := by\n rw [Metric.mem_ball, dist_zero_right] at hsball \u22a2\n rw [norm_div, RCLike.norm_ofNat]\n linarith\n have hs20 : s / 2 \u2260 0 := by\n intro h\n exact hs0 (by linear_combination 2 * h)\n have hdig := digamma_eq_seriesPart_near_zero hs2ball hs20\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n = logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2\n + (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2\n rw [hdig]\n ring\n\n/-! ## 6. The digamma series minus a pole term, and the witness at s = \u22122n -/\n\n/-- \u03b6(\u22122n) = 0 for n \u2265 1 (from `zeroMult_neg_two_mul`: the order is 1). -/\nlemma riemannZeta_neg_two_mul {n : \u2115} (hn : 1 \u2264 n) :\n riemannZeta (-2 * (n : \u2102)) = 0 := by\n by_contra h\n have hord := zeroMult_neg_two_mul n hn\n have hne1 : (-2 * (n : \u2102)) \u2260 1 := by\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith\n have h0 : analyticOrderAt riemannZeta (-2 * (n : \u2102)) = 0 :=\n (analyticAt_riemannZeta hne1).analyticOrderAt_eq_zero.mpr h\n have hmz : zeroMult (-2 * (n : \u2102)) = analyticOrderNatAt riemannZeta (-2 * (n : \u2102)) := rfl\n rw [hmz] at hord\n simp only [analyticOrderNatAt] at hord\n rw [h0] at hord\n simp at hord\n\n/-- Pole avoidance on ball(\u2212n, 1/2) for j \u2260 n\u22121: w + j + 1 \u2260 0. -/\nlemma add_nat_add_one_ne_zero_of_mem_ball_neg {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) {j : \u2115} (hj : j \u2260 n - 1) :\n w + (j : \u2102) + 1 \u2260 0 := by\n intro h\n have h1 : w = -((j : \u2102) + 1) := by linear_combination h\n have h2 : dist w (-(n : \u2102)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [h1, Complex.dist_eq] at h2\n have h3 : -((j : \u2102) + 1) - -(n : \u2102) = ((n : \u2102) - ((j : \u2102) + 1)) := by ring\n rw [h3] at h2\n have hne : n \u2260 j + 1 := by\n intro hc\n apply hj\n omega\n have h5 : (1 : \u211d) \u2264 |(n : \u211d) - ((j : \u211d) + 1)| := by\n rcases lt_or_gt_of_ne hne with hlt | hgt\n \u00b7 have h6 : (n : \u211d) + 1 \u2264 (j : \u211d) + 1 := by\n exact_mod_cast Nat.succ_le_of_lt hlt\n rw [abs_of_neg (by linarith : (n : \u211d) - ((j : \u211d) + 1) < 0)]\n linarith\n \u00b7 have h6 : (j : \u211d) + 1 + 1 \u2264 (n : \u211d) := by\n exact_mod_cast Nat.succ_le_of_lt hgt\n rw [abs_of_pos (by linarith : 0 < (n : \u211d) - ((j : \u211d) + 1))]\n linarith\n have h6 : |((n : \u2102) - ((j : \u2102) + 1)).re| \u2264 \u2016(n : \u2102) - ((j : \u2102) + 1)\u2016 :=\n Complex.abs_re_le_norm _\n have hre : ((n : \u2102) - ((j : \u2102) + 1)).re = (n : \u211d) - ((j : \u211d) + 1) := by\n simp [Complex.sub_re, Complex.add_re, Complex.natCast_re, Complex.one_re]\n rw [hre] at h6\n linarith [h2, h5, h6]\n\n/-- The digamma series with the j = n\u22121 term dropped; analytic on\nball(\u2212n, 1/2). -/\ndef digammaSeriesPartSub (n : \u2115) (w : \u2102) : \u2102 :=\n \u2211' j : \u2115, (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n\n/-- The dropped-term series is analytic on ball(\u2212n, 1/2) (the eventually\nM-test with majorant (2n+1)/(j+1)\u00b2 for j \u2265 2n+1). -/\nlemma digammaSeriesPartSub_analyticOn {n : \u2115} (hn : 1 \u2264 n) :\n AnalyticOnNhd \u2102 (digammaSeriesPartSub n) (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n have hsum : Summable (fun j : \u2115 => (2 * (n : \u211d) + 1) / ((j : \u211d) + 1) ^ 2) :=\n summable_div_add_one_sq _\n have hu : HasSumUniformlyOn\n (fun (j : \u2115) => fun w : \u2102 =>\n (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (fun w => \u2211' j : \u2115, (if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum\n rw [eventually_cofinite]\n apply (Set.finite_Iio (2 * n + 1)).subset\n intro j hj\n show j < 2 * n + 1\n by_contra hj2\n push Not at hj2\n apply hj\n intro w hw\n have hwn : \u2016w\u2016 < (n : \u211d) + 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rw [Complex.dist_eq] at h\n have htri : \u2016w\u2016 \u2264 \u2016w - -(n : \u2102)\u2016 + \u2016-(n : \u2102)\u2016 := by\n calc \u2016w\u2016 = \u2016(w - -(n : \u2102)) + -(n : \u2102)\u2016 := by congr 1; ring\n _ \u2264 _ := norm_add_le _ _\n have hnnorm : \u2016(-(n : \u2102))\u2016 = (n : \u211d) := by\n rw [norm_neg, RCLike.norm_natCast]\n linarith\n have hjne : j \u2260 n - 1 := by omega\n rw [if_neg hjne]\n have hwj : w + (j : \u2102) + 1 \u2260 0 :=\n add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hjne\n have hj0 : ((j : \u2102) + 1) \u2260 0 := Nat.cast_add_one_ne_zero j\n have halg : 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)\n = w / (((j : \u2102) + 1) * (w + j + 1)) := by\n field_simp\n ring\n have hnorm1 : \u2016((j : \u2102) + 1)\u2016 = (j : \u211d) + 1 := by\n have e : ((j : \u2102) + 1) = ((j + 1 : \u2115) : \u2102) := by push_cast; ring\n rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]\n have hj1 : (0 : \u211d) < (j : \u211d) + 1 := by positivity\n -- for j \u2265 2n+1: \u2016w + j + 1\u2016 \u2265 (j+1)/2\n have hnorm2 : ((j : \u211d) + 1) / 2 \u2264 \u2016w + (j : \u2102) + 1\u2016 := by\n have h2 : (w + (j : \u2102) + 1).re \u2264 \u2016w + (j : \u2102) + 1\u2016 := Complex.re_le_norm _\n have h3 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have h4 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n have hj2' : 2 * ((n : \u211d) + 1) \u2264 (j : \u211d) + 1 := by\n have h5 : 2 * n + 2 \u2264 j + 1 := by omega\n have h6 : (2 * n + 2 : \u2115) \u2264 j + 1 := h5\n have h7 : ((2 * n + 2 : \u2115) : \u211d) \u2264 ((j + 1 : \u2115) : \u211d) := by exact_mod_cast h6\n push_cast at h7\n linarith\n nlinarith [hwn]\n rw [halg, norm_div, norm_mul, hnorm1]\n have hA2 : (0 : \u211d) < ((j : \u211d) + 1) ^ 2 := by positivity\n have hden0 : (0 : \u211d) < ((j : \u211d) + 1) * \u2016w + (j : \u2102) + 1\u2016 :=\n mul_pos hj1 (by linarith [hnorm2, hj1])\n rw [div_le_div_iff\u2080 hden0 hA2]\n have hn0 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n have h21 : (0 : \u211d) \u2264 2 * (n : \u211d) + 1 := by linarith\n have hstep1 : ((j : \u211d) + 1) ^ 2 / 2 \u2264 ((j : \u211d) + 1) * \u2016w + (j : \u2102) + 1\u2016 := by\n have h := mul_le_mul_of_nonneg_left hnorm2 hj1.le\n nlinarith [h]\n have hstep2 : (2 * (n : \u211d) + 1) * (((j : \u211d) + 1) ^ 2 / 2)\n \u2264 (2 * (n : \u211d) + 1) * (((j : \u211d) + 1) * \u2016w + (j : \u2102) + 1\u2016) :=\n mul_le_mul_of_nonneg_left hstep1 h21\n have hstep3 : \u2016w\u2016 * ((j : \u211d) + 1) ^ 2 \u2264 ((n : \u211d) + 1 / 2) * ((j : \u211d) + 1) ^ 2 :=\n mul_le_mul_of_nonneg_right hwn.le (sq_nonneg _)\n linarith [hstep2, hstep3]\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset \u2115 => fun w =>\n \u2211 j \u2208 t, (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (fun w => \u2211' j : \u2115, (if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n atTop (Metric.ball (-(n : \u2102)) (1 / 2)) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)\n have hdiff : DifferentiableOn \u2102 (fun w => \u2211' j : \u2115, (if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t w hw\n rw [show (fun w => \u2211 j \u2208 t, (if j = n - 1 then 0\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n = \u2211 j \u2208 t, (fun w => if j = n - 1 then 0\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) from by\n funext w; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro j _\n by_cases hj : j = n - 1\n \u00b7 show DifferentiableAt \u2102 (fun w => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) w\n simp only [if_pos hj]\n exact differentiableAt_const 0\n \u00b7 have hwj : w + (j : \u2102) + 1 \u2260 0 :=\n add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hj\n show DifferentiableAt \u2102 (fun w => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) w\n simp only [if_neg hj]\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => 1 / (w + (j : \u2102) + 1)) w :=\n (differentiableAt_const (1 : \u2102)).div\n ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))\n hwj\n exact (differentiableAt_const _).sub h2\n have hdiff2 : DifferentiableOn \u2102 (digammaSeriesPartSub n)\n (Metric.ball (-(n : \u2102)) (1 / 2)) := hdiff\n exact hdiff2.analyticOnNhd Metric.isOpen_ball\n\n/-- The single-term split: for w \u2208 ball(\u2212n, 1/2), w \u2260 \u2212n,\ndigammaSeriesPart w = digammaSeriesPartSub n w + (1/n \u2212 1/(w+n)). -/\nlemma digammaSeriesPart_eq_sub_add_single {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) (hwn : w \u2260 -(n : \u2102)) :\n digammaSeriesPart w\n = digammaSeriesPartSub n w + (1 / (n : \u2102) - 1 / (w + (n : \u2102))) := by\n have hZ : w \u2208 Complex.integerComplement :=\n integerComplement_of_mem_ball_neg_natCast hw hwn\n have hfull : Summable (fun j : \u2115 => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) :=\n Zeta23.DigammaSeries.summable_digamma_series hZ\n have hsub : Summable (fun j : \u2115 => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) := by\n apply Summable.of_norm_bounded hfull.norm\n intro j\n by_cases hjj : j = n - 1 <;> simp [hjj]\n have hsingle : Summable (fun j : \u2115 => if j = n - 1\n then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102)) := by\n apply summable_of_hasFiniteSupport ((Set.finite_singleton (n - 1)).subset ?_)\n intro j hj\n rw [Function.mem_support, ne_eq] at hj\n by_contra h\n apply hj\n rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]\n have htsum : \u2211' j, (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102))\n = 1 / (n : \u2102) - 1 / (w + (n : \u2102)) := by\n rw [tsum_eq_single (n - 1) (fun j hj => if_neg hj)]\n rw [if_pos rfl]\n congr 1\n \u00b7 rw [Nat.cast_sub hn, Nat.cast_one]\n ring\n \u00b7 congr 1\n rw [Nat.cast_sub hn, Nat.cast_one]\n ring\n calc digammaSeriesPart w\n = \u2211' (j : \u2115), (1 / ((j : \u2102) + 1) - 1 / (w + (j : \u2102) + 1)) := rfl\n _ = \u2211' (j : \u2115), ((if j = n - 1 then (0 : \u2102) else (1 / ((j : \u2102) + 1) - 1 / (w + (j : \u2102) + 1)))\n + (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + (j : \u2102) + 1)) else (0 : \u2102))) := by\n apply tsum_congr\n intro j\n by_cases hjj : j = n - 1 <;> simp [hjj]\n _ = digammaSeriesPartSub n w\n + \u2211' j, (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102)) :=\n Summable.tsum_add hsub hsingle\n _ = digammaSeriesPartSub n w + (1 / (n : \u2102) - 1 / (w + (n : \u2102))) := by rw [htsum]\n\n/-- H_n: digamma plus its pole term at \u2212n, minus the pole \u2014 analytic on\nball(\u2212n, 1/2). -/\ndef Hsub (n : \u2115) (w : \u2102) : \u2102 :=\n -(Real.eulerMascheroniConstant : \u2102) - 1 / w + digammaSeriesPartSub n w + 1 / (n : \u2102)\n\n/-- The punctured digamma split at \u2212n: digamma w = \u22121/(w+n) + H_n w. -/\nlemma digamma_eq_neg_inv_add_Hsub {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) (hwn : w \u2260 -(n : \u2102)) :\n Complex.digamma w = -1 / (w + (n : \u2102)) + Hsub n w := by\n have hZ : w \u2208 Complex.integerComplement :=\n integerComplement_of_mem_ball_neg_natCast hw hwn\n have hdig := Zeta23.DigammaSeries.digamma_series hZ\n have hsplit := digammaSeriesPart_eq_sub_add_single hn hw hwn\n rw [hdig]\n show -(Real.eulerMascheroniConstant : \u2102) - 1 / w + digammaSeriesPart w\n = -1 / (w + (n : \u2102)) + (-(Real.eulerMascheroniConstant : \u2102) - 1 / w\n + digammaSeriesPartSub n w + 1 / (n : \u2102))\n rw [hsplit]\n ring\n\n/-- H_n is analytic at \u2212n. -/\nlemma Hsub_analyticAt {n : \u2115} (hn : 1 \u2264 n) :\n AnalyticAt \u2102 (Hsub n) (-(n : \u2102)) := by\n have hA : AnalyticAt \u2102 (fun _ : \u2102 => -(Real.eulerMascheroniConstant : \u2102)) (-(n : \u2102)) :=\n analyticAt_const\n have hB : AnalyticAt \u2102 (fun w : \u2102 => 1 / w) (-(n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const analyticAt_id (show (-(n : \u2102)) \u2260 0 by\n simp only [ne_eq, neg_eq_zero, Nat.cast_eq_zero]\n omega)\n have hC : AnalyticAt \u2102 (digammaSeriesPartSub n) (-(n : \u2102)) :=\n digammaSeriesPartSub_analyticOn hn (-(n : \u2102)) (Metric.mem_ball_self (by norm_num))\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => 1 / (n : \u2102)) (-(n : \u2102)) := analyticAt_const\n show AnalyticAt \u2102 (fun w => -(Real.eulerMascheroniConstant : \u2102) - 1 / w\n + digammaSeriesPartSub n w + 1 / (n : \u2102)) (-(n : \u2102))\n exact (((hA.sub hB).add hC).add hD)\n\n/-- The witness at s = \u22122n (n \u2265 1): Fexpr agrees punctured with\nWtriv \u2212 seriesFun + 1/s + 1/(s\u22121) \u2212 (log \u03c0)/2 + H_n(s/2)/2. -/\nlemma Fexpr_eventually_neg_two_mul {n : \u2115} (hn : 1 \u2264 n) :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W (-2 * (n : \u2102)) \u2227\n \u2200\u1da0 s in \ud835\udcdd[\u2260] (-2 * (n : \u2102)), Fexpr s = W s := by\n have h\u03b6 := riemannZeta_neg_two_mul hn\n have hne1 : (-2 * (n : \u2102)) \u2260 1 := by\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith\n obtain \u27e8Wtriv, hWtriv, hWtrivEq\u27e9 := logDeriv_zeta_sub_mult_div_eventually h\u03b6 hne1\n rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball] at hWtrivEq\n obtain \u27e8\u03b5, h\u03b5, hWtrivEq\u27e9 := hWtrivEq\n have hmult : zeroMult (-2 * (n : \u2102)) = 1 := zeroMult_neg_two_mul n hn\n -- the pieces\n have hB : AnalyticAt \u2102 seriesFun (-2 * (n : \u2102)) := seriesFun_analyticAt (by\n intro h\n have hpos := h.2.1\n have hre : (-2 * (n : \u2102)).re = -2 * (n : \u211d) := by simp\n rw [hre] at hpos\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith)\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / s) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const analyticAt_id (by\n have hn0 : (n : \u2102) \u2260 0 := Nat.cast_ne_zero.mpr (by omega)\n exact mul_ne_zero (by norm_num) hn0)\n have hC1 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s - 1)) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const (g := fun s : \u2102 => s - 1) _ (by\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n linarith)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => (Real.log Real.pi : \u2102) / 2) (-2 * (n : \u2102)) :=\n analyticAt_const\n have hE : AnalyticAt \u2102 (fun s => Hsub n (s / 2) / 2) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : \u2102) \u2260 0)\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s / 2) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n have hg : AnalyticAt \u2102 (Hsub n) ((-2 * (n : \u2102)) / 2) := by\n rw [show (-2 * (n : \u2102)) / 2 = -(n : \u2102) by ring]\n exact Hsub_analyticAt hn\n exact AnalyticAt.comp (f := fun s : \u2102 => s / 2) hg h1\n refine \u27e8fun s => Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Hsub n (s / 2) / 2, ?_, ?_\u27e9\n \u00b7 exact ((((hWtriv.sub hB).add hC).add hC1).sub hD).add hE\n \u00b7 -- punctured agreement on ball(\u22122n, min 1 \u03b5) (then s/2 \u2208 ball(\u2212n, 1/2))\n rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball]\n refine \u27e8min 1 \u03b5, lt_min (by norm_num) h\u03b5, fun s hsball hsne => ?_\u27e9\n have hs0 : s \u2260 -2 * (n : \u2102) := hsne\n have hsdist : dist s (-2 * (n : \u2102)) < 1 \u2227 dist s (-2 * (n : \u2102)) < \u03b5 := by\n have h := Metric.mem_ball.mp hsball\n constructor <;> linarith [h, min_le_left 1 \u03b5, min_le_right 1 \u03b5]\n have hs2ball : s / 2 \u2208 Metric.ball (-(n : \u2102)) (1 / 2) := by\n rw [Metric.mem_ball, Complex.dist_eq]\n have e : s / 2 - -(n : \u2102) = (s - -2 * (n : \u2102)) / 2 := by ring\n rw [e, norm_div, RCLike.norm_ofNat]\n have h := Metric.mem_ball.mp hsball\n rw [Complex.dist_eq] at h\n linarith [h, min_le_left 1 \u03b5]\n have hs20 : s / 2 \u2260 -(n : \u2102) := by\n intro h\n exact hs0 (by linear_combination 2 * h)\n have hdig := digamma_eq_neg_inv_add_Hsub hn hs2ball hs20\n -- logDeriv split: logDeriv \u03b6 s = Wtriv s + 1/(s + 2n)\n have hlog : logDeriv riemannZeta s = Wtriv s + 1 / (s + 2 * (n : \u2102)) := by\n have h3 := hWtrivEq s (Metric.mem_ball.mpr hsdist.2) hsne\n rw [hmult, Nat.cast_one] at h3\n have e : s - -2 * (n : \u2102) = s + 2 * (n : \u2102) := by ring\n rw [e] at h3\n linear_combination h3\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n = Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Hsub n (s / 2) / 2\n rw [hlog, hdig]\n have h1 : -1 / (s / 2 + (n : \u2102)) / 2 = -1 / (s + 2 * (n : \u2102)) := by\n have e : s / 2 + (n : \u2102) = (s + 2 * (n : \u2102)) / 2 := by ring\n rw [e, neg_div, one_div_div]\n ring\n linear_combination h1\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 803,
"oldLines": 7,
"newStart": 803,
"newLines": 3,
"lines": [
" ring",
" linear_combination h1",
" ",
"-end NguyenRH1",
"-",
"-end",
"-"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"`Multipliable.subtype (hf : Multipliable f) (p : β → Prop)` → additive: `Summable.subtype (hf : Summable f) (p : β → Prop) : Summable (fun x : {x // p x} => f x)` presumably (or on Set.subtype). It takes a predicate p : β → Prop — our subtype is {m : ℕ // Odd m ∧ 3 ≤ m} = {m // (fun m => Odd m ∧ 3 ≤ m) m} ✓.\n\nNote: `Summable.subtype` may require DecidablePred p? It might produce `Summable (f ∘ Subtype.val : Subtype p → α)`. Our tsum in SInfty is `tsum fun m : {m // Odd m ∧ 3 ≤ m} => ((1 - 1/(m:ℝ))^n − 1 + n/(m:ℝ))` — that's exactly fun x : subtype => f x with coercion. Fine.\n\nSummability comparison: base summable: fun m : ℕ => C/(m:ℝ)² — from summable_one_div_nat_pow (p=2) .mul_left C. But m = 0 term: 1/0² = 0 in Lean (division by zero = 0) — fine, summable_one_div_nat_pow handles it (junk value at 0).\n\nThen on subtype: (that).subtype p : Summable (fun m : {m // Odd m ∧ 3≤m} => C/(m:ℝ)²).\n\nComparison: Summable.of_nonneg_of_le (hg : ∀ x, 0 ≤ g x) (hfg : ∀ x, g x ≤ f x) (hf : Summable f) — check exact name/signature: `Summable.of_nonneg_of_le (hg : ∀ b, 0 ≤ g b) (h : ∀ b, g b ≤ f b) (hf : Summable f) : Summable g` ✓ (in Order.lean).\n\nBernoulli upper lemma proof detail (L_bern_upper): for m ≥ 1, x := 1/m ∈ (0,1].\n1 − (1−x)ⁿ = (1−x)⁰·... use geom_sum_eq with y = 1−x: Σ_{j∈range n} y^j = (yⁿ − 1)/(y − 1) = (1 − yⁿ)/x (since y−1 = −x). So 1 − yⁿ = x·Σ yʲ — requires x ≠ 0 for the division form; alternatively use the ring identity directly: (1 − y) * Σ_{j∈range n} y^j = 1 − yⁿ — Mathlib: `geom_sum_mul`? There's `geom_sum_mul : (x − 1) * Σ x^i = x^n − 1` (in a ring, no division!) — check name: `geom_sum_mul (x : α) (n : ℕ) [Ring α] : (∑ i in range n, x^i) * (x − 1) = x^n − 1` or (x−1)*sum. With that: (1−y)·Σ yʲ = 1 − yⁿ directly ✓ no division.\n\nThen Σ_{j<n} yʲ ≥ Σ_{j<n} (1 − jx) by Bernoulli per term (one_add_mul_le_pow with a = −x: 1 + j(−x) ≤ (1−x)ʲ needs −2 ≤ −x ⟸ x ≤ 2 ✓).\nΣ_{j<n} (1 − jx) = n − x·Σ_{j<n} j = n − x·(n(n−1)/2).\nSo 1 − yⁿ ≥ x·(n − C(n,2)·x) where C(n,2) as real = n(n−1)/2.\nh⁺(m) = yⁿ − 1 + nx = nx − (1 − yⁿ) ≤ nx − x(n − C(n,2)x) = C(n,2)x² = C(n,2)/m² ✓.\n\nIn ℝ: C(n,2) real = n*(n−1)/2 — I'll state with (n*(n−1)/2 : ℝ) form? Cleaner: use (n.choose 2 : ℝ) with Nat.choose_two_right + Nat.cast... choose_two_right : n.choose 2 = n * (n − 1) / 2 (nat division) — casting nat division to real needs n*(n−1) even — Nat.even_mul_pred_self ✓ (n*(n−1) even). Might be simpler to state the lemma with (n : ℝ)*(n−1)/2 directly, avoiding choose. Yes: L_bern_upper conclusion: ... ≤ (n : ℝ)*(n−1)/(2*m^2). The summability comparison then uses C := n(n−1)/2 as a real constant. Cleaner.\n\nFor the finite sum Σ_{j<n} j over ℝ: cast: Σ_{j∈range n} (j:ℝ) = n(n−1)/2 via Finset.sum_range_id... there's `Finset.sum_range_id : Σ i in range n, i = n * (n - 1) / 2` (ℕ) — cast with same evenness issue. Better: `Finset.sum_range_id_mul_two` in ℕ then cast? Or find real version: there is a known lemma `Finset.sum_range_id_div_two`? Alternatively compute directly: Σ_{j∈range n} (j:ℝ) — Mathlib has `Finset.sum_range_id (n : ℕ) : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2` — for ℕ. Hmm, there's also `sum_range_geometric`... Let me just handle: (Σ_{j∈range n} (j : ℝ)) = (n:ℝ)*(n−1)/2. Prove: 2 * Σ = n(n−1): from sum_range_id_mul_two cast: cast both sides. (Nat.cast_inj). Doable:\n```lean\nhave hsum : ∑ j ∈ Finset.range n, (j : ℝ) = n * (n - 1) / 2 := by\n have h := Finset.sum_range_id_mul_two n\n -- h : (Σ i in range n, i) * 2 = n * (n - 1) in ℕ\n have h2 : ((∑ i ∈ Finset.range n, i : ℕ) : ℝ) * 2 = n * (n - 1) := by exact_mod_cast h\n -- then divide\n ...\n```\nCareful with casts (n−1 : ℕ) vs (n:ℝ)−1: Nat.cast_sub needs 1 ≤ n. Since we need n ≥ 1 anyway (actually n ≥ 20 in main theorem; but lemma can assume 1 ≤ n), fine.\n\nOK. Also for L_bern_nonneg: one_add_mul_le_pow (H : -2 ≤ a) n : 1 + n*a ≤ (1+a)^n with a = −1/m: −2 ≤ −1/m ⟺ 1/m ≤ 2 ⟸ m ≥ 1 (1/m ≤ 1 ≤ 2 ✓). Then 0 ≤ (1−1/m)ⁿ − 1 + n/m ⟸ 1 − n/m ≤ (1−1/m)ⁿ ✓ = 1 + n·(−1/m) ✓ ring-normalize.\n\nWrite both lemmas in Scratch now. I'll write them with full context and iterate.","signature":""},{"type":"text","text":"All names verified. Writing the two Bernoulli lemmas in the scratch file."},{"type":"tool_use","id":"Edit_196","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean","old_string":"end Scratch","new_string":"/-- h⁺(m) ≥ 0 for m ≥ 1: first-order Bernoulli, (1−1/m)ⁿ ≥ 1 − n/m. -/\ntheorem bern_term_nonneg (n : ℕ) (m : ℕ) (hm : 1 ≤ m) :\n 0 ≤ (1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / m := by\n have hm0 : (m : ℝ) ≠ 0 := by positivity\n have h1 : (1 : ℝ) + n * (-1 / m) ≤ (1 + -1 / (m : ℝ)) ^ n := by\n apply one_add_mul_le_pow\n have : (1 : ℝ) / m ≤ 1 := by\n rw [div_le_one (by positivity)]; exact_mod_cast hm\n linarith\n have h2 : (1 : ℝ) - n / m ≤ (1 - 1 / m) ^ n := by\n have : (1 : ℝ) + n * (-1 / m) = 1 - n / m := by field_simp; ring\n rwa [this, show (1 : ℝ) + -1 / m = 1 - 1 / m by ring] at h1\n linarith\n\n/-- h⁺(m) ≤ (n choose 2)/m² for m ≥ 1: geometric factorization\n1 − (1−x)ⁿ = x·Σ_{j<n} (1−x)ʲ ≥ x·(n − x·Σj) plus Bernoulli per term. -/\ntheorem bern_term_upper (n : ℕ) (m : ℕ) (hm : 1 ≤ m) :\n (1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / m ≤ (n : ℝ) * (n - 1) / (2 * m ^ 2) := by\n have hm0 : (m : ℝ) ≠ 0 := by positivity\n set x := (1 : ℝ) / m with hxdef\n have hx1 : x ≤ 1 := by\n rw [hxdef, div_le_one (by positivity)]; exact_mod_cast hm\n have hx0 : 0 ≤ x := by positivity\n -- per-term Bernoulli: (1 − x)ʲ ≥ 1 − jx\n have hterm : ∀ j : ℕ, 1 - j * x ≤ (1 - x) ^ j := by\n intro j\n have := one_add_mul_le_pow (a := -x) (by linarith : (-2 : ℝ) ≤ -x) j\n rwa [show (1 : ℝ) + j * (-x) = 1 - j * x by ring,\n show (1 : ℝ) + -x = 1 - x by ring] at this\n -- sum of j over range n, as a real identity\n have hsum : ∑ j ∈ Finset.range n, (j : ℝ) = (n : ℝ) * (n - 1) / 2 := by\n have h := Finset.sum_range_id_mul_two n\n have h2 : ((∑ i ∈ Finset.range n, i : ℕ) : ℝ) * 2 = (n : ℝ) * ((n : ℝ) - 1) := by\n have hcast : ((∑ i ∈ Finset.range n, i : ℕ) : ℝ) * 2 = ((n * (n - 1) : ℕ) : ℝ) := by\n exact_mod_cast h\n rw [hcast]\n rcases Nat.eq_zero_or_pos n with hn0 | hnpos\n · simp [hn0]\n · rw [Nat.cast_sub hnpos.one_le]; push_cast; ring\n have h3 : (∑ j ∈ Finset.range n, (j : ℝ)) * 2 = (n : ℝ) * ((n : ℝ) - 1) := by\n rw [← h2]; push_cast [Finset.sum]; simp [Nat.cast_sum]\n linarith\n -- geometric factorization: 1 − (1−x)ⁿ = x · Σ_{j<n} (1−x)ʲ\n have hgeom : (1 - (1 - x) ^ n) = x * ∑ j ∈ Finset.range n, (1 - x) ^ j := by\n have h := geom_sum_mul (1 - x) n\n -- h : (∑ i in range n, (1−x)^i) * ((1−x) − 1) = (1−x)^n − 1\n have hx0' : x ≠ 0 ∨ x = 0 := ne_or_eq x 0\n rcases hx0' with hx0' | rfl\n · have hx1' : (1 - x) - 1 = -x := by ring\n rw [hx1'] at h\n have : ∑ j ∈ Finset.range n, (1 - x) ^ j = ((1 - x) ^ n - 1) / (-x) := by\n field_simp; linarith [h]\n rw [this]; field_simp; ring\n · simp\n -- assemble\n have hmain : (1 - x) ^ n - 1 + (n : ℝ) * x ≤ (n : ℝ) * (n - 1) / 2 * x ^ 2 := by\n have h4 : (n : ℝ) * x - (n * (n - 1) / 2) * x ^ 2 ≤ 1 - (1 - x) ^ n := by\n rw [hgeom]\n have h5 : (n : ℝ) - x * ((n : ℝ) * (n - 1) / 2) ≤\n ∑ j ∈ Finset.range n, (1 - x) ^ j := by\n have h6 : ∑ j ∈ Finset.range n, (1 - (j : ℝ) * x) =\n (n : ℝ) - x * ∑ j ∈ Finset.range n, (j : ℝ) := by\n rw [Finset.mul_sum, Finset.sum_sub_distrib]\n simp [Finset.sum_const, Finset.card_range, nsmul_eq_mul]\n rw [hsum] at h6\n rw [← h6]\n exact Finset.sum_le_sum fun j _ => hterm j\n calc (n : ℝ) * x - (n * (n - 1) / 2) * x ^ 2\n = x * ((n : ℝ) - x * (n * (n - 1) / 2)) := by ring\n _ ≤ x * ∑ j ∈ Finset.range n, (1 - x) ^ j :=\n mul_le_mul_of_nonneg_left h5 hx0\n linarith\n -- convert back to the m-form\n have hx2 : x ^ 2 = 1 / m ^ 2 := by rw [hxdef]; ring\n have hdiv : (n : ℝ) / m = n * x := by rw [hxdef]; ring\n rw [hdiv]\n have h7 : (1 - 1 / (m : ℝ)) ^ n = (1 - x) ^ n := by rw [hxdef]\n rw [h7]\n calc (1 - x) ^ n - 1 + (n : ℝ) * x\n ≤ (n : ℝ) * (n - 1) / 2 * x ^ 2 := hmain\n _ = (n : ℝ) * (n - 1) / (2 * m ^ 2) := by rw [hx2]; ring\n\nend Scratch"},"extra_content":null}]