← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (2549 chars)
I left a sorry at the end of scaledZeta_jensen_count. The ZerosBound conclusion: Σ ≤ 1/log(R/r)·log B with r = 24/25, R = 99/100: 1/log((99/100)/(24/25))·log((9/4)|t|²) = 1/log(99/96)·log(...) = 1/log(33/32)·log(...) — wait (99/100)/(24/25) = (99/100)·(25/24) = 99/(4·24) = 99/96 = 33/32 ✓. So h : Σ ≤ (1/log(33/32))·log((9/4)|t|²). My target: Σ ≤ log((9/4)|t|²)/log(33/32) — same thing (div vs 1/· mul): `one_div` form. The exact form of ZerosBound's conclusion: `1 / Real.log (R / r) * Real.log B` — my target `Real.log B / Real.log (33/32)` — with R/r = (99/100)/(24/25) = 33/32 ✓. So the final step: 1/log(R/r)·log B = log B/log(33/32): need R/r = 33/32: norm_num: (99/100)/(24/25) = 33/32 ✓. So:
```lean
refine h.trans_eq ?_
rw [one_div, inv_mul_eq_div] -- 1/log(R/r)·log B = log B / log(R/r)
congr 2 -- log B = log B ✓; log(R/r) = log(33/32)
· -- (9/4)|t|² = (9/4)|t|² ✓ rfl — hmm the congr structure
· norm_num -- (99/100)/(24/25) = 33/32
```
Hmm — `trans_eq` : a ≤ b → b = c → a ≤ c — `h.trans_eq ?_`?? the name for LE: `LE.le.trans_eq (h : a ≤ b) (h' : b = c) : a ≤ c` ✓. Then goal: 1/log(R/r)·log B = log((9/4)|t|²)/log(33/32) — with B = (9/4)|t|², R = 99/100, r = 24/25 as the implicits — need them to match: the ZerosBound call's B was inferred from hB : ∀ z, ‖z‖ ≤ R → ‖f z‖ ≤ B — B := (9/4)*|t|² ✓ and R := 99/100 ✓ r := 24/25 ✓. So h : Σ ≤ 1/Real.log(99/100/(24/25))·Real.log((9/4)*|t|²). Then:
```lean
refine h.trans_eq ?_
rw [one_div, inv_mul_eq_div]
norm_num -- (99/100)/(24/25) = 33/32: the log argument
```
Hmm — rw [one_div, inv_mul_eq_div]: target RHS: log B/log(33/32): after rw: 1/log((99/100)/(24/25))·log B = log B/log(33/32): one_div : 1/x = x⁻¹: then inv_mul_eq_div : x⁻¹·y = x/y ✓: becomes log B / log((99/100)/(24/25)) = log B / log(33/32): then congr on the log args: (99/100)/(24/25) = 33/32 by norm_num:
```lean
rw [one_div, inv_mul_eq_div]
congr 2
· rfl? -- the log B parts... hmm
```
The equality: Real.log B / Real.log ((99/100)/(24/25)) = Real.log B / Real.log (33/32): congr 1 gives Real.log((99/100)/(24/25)) = Real.log(33/32): congr 1 again: (99/100)/(24/25) = 33/32: norm_num ✓. So `rw [one_div, inv_mul_eq_div]; congr 2; norm_num`? congr 2 on A/X = B/Y gives A = B and X = Y: A = B is log B = log B ✓ rfl (congr auto-closes rfl?) and X = Y: log(...) = log(33/32): then need another congr... use `congr 1` twice? Let me just:
```lean
refine h.trans_eq ?_
rw [one_div, inv_mul_eq_div]
have hratio : (99 / 100 : ℝ) / (24 / 25) = 33 / 32 := by norm_num
rw [hratio]
```
✓ clean.
Completing the Jensen count's final step (the ratio normalization).
tool: Edit ok
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
"old_string": " have h := ZerosBound (f := scaledZeta t) (r := 24 / 25) (R := 99 / 100)\n (by norm_num) (by norm_num) (by norm_num) (by norm_num)\n (scaledZeta_analytic ht) (scaledZeta_zero t) scaledZeta_zeros_finite hB\n refine h.trans ?_\n rw [one_div, inv_mul_eq_div]\n apply div_le_div_of_nonneg_right _ ... \n sorry\n\nend NguyenRH1\n\nend",
"new_string": " have h := ZerosBound (f := scaledZeta t) (r := 24 / 25) (R := 99 / 100)\n (by norm_num) (by norm_num) (by norm_num) (by norm_num)\n (scaledZeta_analytic ht) (scaledZeta_zero t) scaledZeta_zeros_finite hB\n refine h.trans_eq ?_\n rw [one_div, inv_mul_eq_div]\n have hratio : (99 / 100 : \u211d) / (24 / 25) = 33 / 32 := by norm_num\n rw [hratio]\n\nend NguyenRH1\n\nend"
}
result 2026-08-22 20:21:04Z → 2026-08-23 10:24:16Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
"oldString": " tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ\n (summable_digamma_majorant hwre)",
"newString": " Summable.tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ\n (summable_digamma_majorant hwre)",
"originalFile": "/-\nNguyenRH1/LiDigammaLeft.lean \u2014 tier ii\u2032 sub-stage 5e-ii (D-068 \u00a71 C2):\nthe two digamma bounds feeding the circle estimate of ii\u2032-5e-v.\n\n* \u00a71 `tsum_one_div_sub_telescope`: \u2211'\u2099 (1/(n+N) \u2212 1/(n+N+1)) = 1/N\n (partial-sum telescope + squeeze).\n* \u00a72 `norm_digamma_le_of_two_le_re`: \u2016\u03c8(w)\u2016 \u2264 20\u00b7log(2+\u2016w\u2016) for\n re w \u2265 2, |im w| \u2264 5 \u2014 the Weierstrass-series route (Zeta23\n `DigammaSeries.digamma_series`): \u03a3'_n w/((n+1)(w+n+1)) split at\n N = \u2308re w\u2309\u208a (head via the harmonic bound `harmonic_le_one_add_log`,\n tail via \u00a71's telescope); the positive-integer case via `digamma_one`\n + the recurrence (`digamma_natCast_eq`).\n* \u00a73 (C): `digamma_recip_sum_le` \u2014 the separated reciprocal sum bound\n \u03a3_{j<m} \u2016w+j\u2016\u207b\u00b9 \u2264 2/c + 2 + 2\u00b7log m for dist(w, \u2212\u2115) \u2265 c (V-split).\n* \u00a74 (A): `norm_digamma_le_of_dist_nat` \u2014 the near-axis left-plane bound\n for re w \u2264 2, dist(w,\u2212\u2115) \u2265 c (recurrence `digamma_add_natCast` + \u00a73 +\n the landing-zone bound via \u00a72 or StirlingVert).\n* \u00a75 (G): `logDeriv_Gamma\u211d_eq` \u2014 logDeriv \u0393R s = \u2212(log \u03c0)/2 + \u00bd\u03c8(s/2)\n for im s \u2260 0 (the m-fold shift: `gamma_mul_prod` + the EventuallyEq\n machinery of 5d).\n\nArchive references: D-068 \u00a71 (C2) + \u00a77, journal-025/026.\n-/\nimport Mathlib\nimport Zeta23.GammaFacts.Series\nimport Zeta23.GammaFacts.StirlingVert\nimport NguyenRH1.LiReflect\nimport NguyenRH1.LiTrivialZeros\n\nopen Zeta23 Complex Filter Topology MeasureTheory\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The telescoping tail -/\n\n/-- The partial sums of the telescoping series. -/\ntheorem sum_range_one_div_sub (N M : \u2115) :\n \u2211 n \u2208 Finset.range M, ((1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1))\n = 1 / (N : \u211d) - 1 / ((M : \u211d) + N) := by\n have h := Finset.sum_range_sub' (fun n : \u2115 => (1 : \u211d) / ((n : \u211d) + N)) M\n rw [Nat.cast_zero, zero_add] at h\n rw [\u2190 h]\n apply Finset.sum_congr rfl\n intro n _\n push_cast\n ring_nf\n\n/-- **The telescoping tail, HasSum form**. -/\ntheorem hasSum_one_div_sub_telescope (N : \u2115) (hN : 1 \u2264 N) :\n HasSum (fun n : \u2115 => (1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1))\n (1 / (N : \u211d)) := by\n have hNR : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN\n have hnonneg : \u2200 n : \u2115, (0 : \u211d) \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1) := by\n intro n\n have h1 : (0 : \u211d) < (n : \u211d) + N := by\n have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hNR, h2]\n have h3 : 1 / ((n : \u211d) + N + 1) \u2264 1 / ((n : \u211d) + N) :=\n one_div_le_one_div_of_le h1 (by linarith)\n linarith [h3]\n have hlim0 : Tendsto (fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + N)) atTop (\ud835\udcdd 0) := by\n have h1 : Tendsto (fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + 1)) atTop (\ud835\udcdd 0) :=\n tendsto_one_div_add_atTop_nhds_zero_nat\n refine squeeze_zero (f := fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + N))\n (g := fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + 1)) ?_ ?_ h1\n \u00b7 intro M\n positivity\n \u00b7 intro M\n apply one_div_le_one_div_of_le (by positivity)\n have hN1R : (1 : \u211d) \u2264 (N : \u211d) := by exact_mod_cast hN\n linarith [hN1R]\n have hlim : Tendsto (fun M : \u2115 => (1 : \u211d) / (N : \u211d) - 1 / ((M : \u211d) + N)) atTop\n (\ud835\udcdd (1 / (N : \u211d))) := by\n have h := hlim0.const_sub (1 / (N : \u211d))\n rwa [sub_zero] at h\n rw [hasSum_iff_tendsto_nat_of_nonneg hnonneg]\n convert hlim using 1\n ext M\n exact sum_range_one_div_sub N M\n\n/-- **The telescoping tail**: \u2211'\u2099 (1/(n+N) \u2212 1/(n+N+1)) = 1/N for N \u2265 1. -/\ntheorem tsum_one_div_sub_telescope (N : \u2115) (hN : 1 \u2264 N) :\n \u2211' n : \u2115, ((1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)) = 1 / (N : \u211d) :=\n (hasSum_one_div_sub_telescope N hN).tsum_eq\n\n/-! ## 2. The right-half-plane bound (B) -/\n\n/-- \u03c8 at positive integers: \u03c8(n) = \u2212\u03b3 + H_{n\u22121} for n \u2265 1. -/\ntheorem digamma_natCast_eq (n : \u2115) (hn : 1 \u2264 n) :\n Complex.digamma (n : \u2102)\n = -(Real.eulerMascheroniConstant : \u2102) + ((harmonic (n - 1) : \u211a) : \u2102) := by\n induction n with\n | zero => omega\n | succ k ih =>\n rcases eq_or_ne k 0 with hk | hk\n \u00b7 subst hk\n simp [Complex.digamma_one, harmonic]\n \u00b7 have hk1 : 1 \u2264 k := Nat.one_le_iff_ne_zero.mpr hk\n have h1 := ih hk1\n have hside : \u2200 m : \u2115, (k : \u2102) \u2260 -(m : \u2102) := by\n intro m h\n have hre := congrArg Complex.re h\n simp [Complex.neg_re, Complex.natCast_re] at hre\n have hmk : (1 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk1\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := by positivity\n linarith\n have h2 := Complex.digamma_apply_add_one (k : \u2102) hside\n rw [show ((k + 1 : \u2115) : \u2102) = (k : \u2102) + 1 by push_cast; ring, h2, h1]\n have hharm : ((harmonic (k + 1 - 1) : \u211a) : \u2102)\n = ((harmonic (k - 1) : \u211a) : \u2102) + ((k : \u211d) : \u2102)\u207b\u00b9 := by\n have h3 : k + 1 - 1 = k := by omega\n rw [h3]\n have h4 : harmonic k = harmonic (k - 1) + ((k : \u211a))\u207b\u00b9 := by\n conv_lhs => rw [show k = (k - 1) + 1 by omega]\n rw [harmonic, Finset.sum_range_succ]\n have h5 : k - 1 + 1 = k := by omega\n rw [h5]\n rw [harmonic]\n rw [h4]\n push_cast\n ring\n rw [hharm]\n push_cast\n ring\n\n/-- The digamma-series majorant g n = \u2016w\u2016/((n+1)(re w+n+1)) is summable\n(dominated by \u2016w\u2016/(n+1)\u00b2) for re w \u2265 2. -/\ntheorem summable_digamma_majorant {w : \u2102} (hwre : 2 \u2264 w.re) :\n Summable (fun n : \u2115 => \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1))) := by\n have h1 : Summable (fun n : \u2115 => (((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by\n have h2 : Summable (fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9) := by\n have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : \u211d) < 2)\n have heq : (fun n : \u2115 => ((n : \u211d) ^ (2 : \u211d))\u207b\u00b9) = fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9 := by\n funext n\n rw [show ((2 : \u211d)) = ((2 : \u2115) : \u211d) by norm_num, Real.rpow_natCast]\n rwa [heq] at h3\n have h4 := (summable_nat_add_iff 1).mpr h2\n simpa [add_comm] using h4\n refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ (h1.mul_left \u2016w\u2016)\n intro n\n have hstep : ((n : \u211d) + 1) ^ 2 \u2264 ((n : \u211d) + 1) * (w.re + (n : \u211d) + 1) := by\n rw [sq]\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hwre, h2]\n calc \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1))\n \u2264 \u2016w\u2016 / (((n : \u211d) + 1) ^ 2) := by\n apply div_le_div_of_nonneg_left (norm_nonneg _)\n (show (0 : \u211d) < ((n : \u211d) + 1) ^ 2 by positivity) hstep\n _ = \u2016w\u2016 * ((((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by rw [div_eq_mul_inv]\n\n/-- The per-term bound: \u20161/(n+1) \u2212 1/(w+n+1)\u2016 \u2264 \u2016w\u2016/((n+1)(re w+n+1)). -/\ntheorem norm_digamma_term_le {w : \u2102} (hwre : 2 \u2264 w.re) (n : \u2115) :\n \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016\n \u2264 \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1)) := by\n have hwn1 : w + (n : \u2102) + 1 \u2260 0 := by\n intro h\n have h2 := congrArg Complex.re h\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re] at h2\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hwre, h3, h2]\n have hident : 1 / ((n : \u2102) + 1) - 1 / (w + n + 1)\n = w / (((n : \u2102) + 1) * (w + n + 1)) := by\n field_simp [Nat.cast_add_one_ne_zero n, hwn1]\n ring\n have hrew : (w + (n : \u2102) + 1).re = w.re + (n : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have hle : w.re + (n : \u211d) + 1 \u2264 \u2016w + (n : \u2102) + 1\u2016 := by\n have hpos : (0 : \u211d) \u2264 (w + (n : \u2102) + 1).re := by\n rw [hrew]\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hwre, h3]\n have h2 := Complex.abs_re_le_norm (w + (n : \u2102) + 1)\n rwa [abs_of_nonneg hpos, hrew] at h2\n rw [hident, norm_div, norm_mul, DigammaSeries.norm_natCast_add_one]\n apply div_le_div_of_nonneg_left (norm_nonneg _)\n \u00b7 apply mul_pos (by positivity)\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hwre, h3]\n \u00b7 apply mul_le_mul_of_nonneg_left hle (by positivity)\n\n/-- The harmonic-sum form used in the head split. -/\ntheorem sum_one_div_le_one_add_log (N : \u2115) :\n \u2211 n \u2208 Finset.range N, (1 : \u211d) / ((n : \u211d) + 1) \u2264 1 + Real.log N := by\n have h1 : (\u2211 n \u2208 Finset.range N, (1 : \u211d) / ((n : \u211d) + 1)) = (harmonic N : \u211d) := by\n rw [harmonic, Rat.cast_sum]\n apply Finset.sum_congr rfl\n intro i _\n rw [Rat.cast_inv, Rat.cast_natCast, Nat.cast_add_one, one_div]\n rw [h1]\n exact harmonic_le_one_add_log N\n/-- **The right-half-plane digamma bound (B)**: for re w \u2265 2, |im w| \u2264 5,\n\u2016\u03c8(w)\u2016 \u2264 20\u00b7log(2+\u2016w\u2016). Weierstrass series + split at N = \u2308re w\u2309\u208a;\npositive integers via the harmonic identity. -/\ntheorem norm_digamma_le_of_two_le_re {w : \u2102} (hwre : 2 \u2264 w.re) (hwim : |w.im| \u2264 5) :\n \u2016Complex.digamma w\u2016 \u2264 20 * Real.log (2 + \u2016w\u2016) := by\n have hw_norm_ge : 2 \u2264 \u2016w\u2016 := by\n have h1 := Complex.abs_re_le_norm w\n rw [abs_of_nonneg (by linarith [hwre])] at h1\n linarith [hwre, h1]\n have h1log4 : Real.log 4 \u2264 Real.log (2 + \u2016w\u2016) :=\n Real.log_le_log (by norm_num) (by linarith [hw_norm_ge])\n have hlog4gt : (1 : \u211d) < Real.log 4 := by\n have h4 := Real.log_two_gt_d9.le\n have h5 : Real.log 4 = 2 * Real.log 2 := by\n rw [show (4 : \u211d) = 2 ^ 2 by norm_num, Real.log_pow]\n push_cast\n ring\n linarith [h4, h5]\n have hlog4 : (5 : \u211d) / 3 \u2264 19 * Real.log (2 + \u2016w\u2016) := by nlinarith [h1log4, hlog4gt]\n by_cases hwint : \u2203 m : \u2124, (m : \u2102) = w\n \u00b7 -- the positive-integer case: w = \u2191n, n \u2265 2\n obtain \u27e8m, hm\u27e9 := hwint\n have hmre : w.re = (m : \u211d) := by rw [\u2190 hm]; simp\n have hm2 : 2 \u2264 m := by\n by_contra h\n push Not at h\n have h1 : (m : \u211d) \u2264 1 := by exact_mod_cast (show m \u2264 1 by omega)\n linarith [hwre, hmre, h1]\n have hn2 : 2 \u2264 m.toNat := by\n have h1 : (m : \u2124) = ((m.toNat : \u2115) : \u2124) := (Int.toNat_of_nonneg (by omega)).symm\n rw [h1] at hm2\n exact_mod_cast hm2\n set n := m.toNat with hn_def\n have hwn : w = (n : \u2102) := by\n rw [\u2190 hm, hn_def]\n exact_mod_cast (Int.toNat_of_nonneg (by omega : (0 : \u2124) \u2264 m)).symm\n rw [hwn, digamma_natCast_eq n (by omega)]\n have h\u03b30 : (0 : \u211d) \u2264 Real.eulerMascheroniConstant :=\n (by norm_num : (0 : \u211d) \u2264 1 / 2).trans Real.one_half_lt_eulerMascheroniConstant.le\n have hreal : |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : \u211a) : \u211d)|\n \u2264 Real.eulerMascheroniConstant + (1 + Real.log ((n : \u211d) - 1)) := by\n have hH0\u211a : (0 : \u211a) \u2264 harmonic (n - 1) :=\n Finset.sum_nonneg (fun i _ => by positivity)\n have hH0 : (0 : \u211d) \u2264 ((harmonic (n - 1) : \u211a) : \u211d) := by exact_mod_cast hH0\u211a\n have hcast2 : ((n - 1 : \u2115) : \u211d) = (n : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 n)]\n push_cast\n ring\n have hHbound : ((harmonic (n - 1) : \u211a) : \u211d) \u2264 1 + Real.log ((n : \u211d) - 1) := by\n have h := harmonic_le_one_add_log (n - 1)\n rw [hcast2] at h\n exact h\n have hlog0 : (0 : \u211d) \u2264 Real.log ((n : \u211d) - 1) := by\n apply Real.log_nonneg\n have h1 : (1 : \u211d) \u2264 ((n - 1 : \u2115) : \u211d) := by exact_mod_cast (by omega : 1 \u2264 n - 1)\n linarith [h1, hcast2]\n apply abs_le.mpr\n constructor <;> linarith [h\u03b30, hH0, hHbound, hlog0]\n have hnrm : \u2016-(Real.eulerMascheroniConstant : \u2102) + ((harmonic (n - 1) : \u211a) : \u2102)\u2016\n = |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : \u211a) : \u211d)| := by\n rw [\u2190 Complex.ofReal_ratCast, \u2190 Complex.ofReal_neg, \u2190 Complex.ofReal_add,\n Complex.norm_real, Real.norm_eq_abs]\n rw [hnrm]\n have hlogn1 : Real.log ((n : \u211d) - 1) \u2264 Real.log (2 + \u2016w\u2016) := by\n have h2 : ((n - 1 : \u2115) : \u211d) = (n : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 n)]\n push_cast\n ring\n have hpos : (0 : \u211d) < (n : \u211d) - 1 := by\n have h1 : (1 : \u211d) \u2264 ((n - 1 : \u2115) : \u211d) := by exact_mod_cast (by omega : 1 \u2264 n - 1)\n linarith [h1, h2]\n apply Real.log_le_log hpos\n have hwnorm : \u2016w\u2016 = (n : \u211d) := by rw [hwn, RCLike.norm_natCast]\n rw [hwnorm]\n linarith [h2]\n have h\u03b31 : Real.eulerMascheroniConstant \u2264 1 :=\n Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)\n rw [hwn] at hlogn1 h1log4\n have hlogbig : (2 : \u211d) \u2264 19 * Real.log (2 + \u2016(n : \u2102)\u2016) := by nlinarith [h1log4, hlog4gt]\n linarith [hreal, h\u03b31, hlogn1, hlogbig]\n \u00b7 -- the series case: w off the integers\n have hcomp : w \u2208 Complex.integerComplement := hwint\n rw [DigammaSeries.digamma_series hcomp]\n set A := w.re with hA_def\n set N := \u2308w.re\u2309\u208a with hN_def\n have hA0 : (0 : \u211d) < A := by linarith [hwre]\n have hNA : A \u2264 (N : \u211d) := by rw [hN_def]; exact Nat.le_ceil _\n have hNA1 : (N : \u211d) \u2264 A + 1 := by\n have h := Nat.ceil_lt_add_one (show (0 : \u211d) \u2264 w.re by linarith [hwre])\n have h2 : ((\u2308w.re\u2309\u208a : \u2115) : \u211d) < w.re + 1 := by exact_mod_cast h\n rw [hN_def]\n linarith [h2]\n have hN1 : 1 \u2264 N := by\n have h1 : (2 : \u2115) \u2264 N := by\n rw [hN_def]\n have h2 := Nat.ceil_mono hwre\n rwa [Nat.ceil_ofNat] at h2\n omega\n have hterm_summ : Summable (fun n : \u2115 => \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016) :=\n Summable.of_nonneg_of_le (fun n => norm_nonneg _) (fun n => norm_digamma_term_le hwre n)\n (summable_digamma_majorant hwre)\n -- the kernel: summable + the split bound\n have hker_summ : Summable (fun n : \u2115 => (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9) := by\n have h1 : Summable (fun n : \u2115 => (((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by\n have h2 : Summable (fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9) := by\n have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : \u211d) < 2)\n have heq : (fun n : \u2115 => ((n : \u211d) ^ (2 : \u211d))\u207b\u00b9)\n = fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9 := by\n funext n\n rw [show ((2 : \u211d)) = ((2 : \u2115) : \u211d) by norm_num, Real.rpow_natCast]\n rwa [heq] at h3\n have h4 := (summable_nat_add_iff 1).mpr h2\n simpa [add_comm] using h4\n refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ h1\n intro n\n apply (inv_le_inv\u2080 (by positivity) (by positivity)).mpr\n rw [sq]\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hA0, h2]\n have hsplit : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)\n = \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n + \u2211' n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N) := by\n exact (hker_summ.sum_add_tsum_nat_add N).symm\n -- the head bound\n have hhead : \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n \u2264 (1 + Real.log (N : \u211d)) / A := by\n have hper : \u2200 n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n \u2264 ((n : \u211d) + 1)\u207b\u00b9 * A\u207b\u00b9 := by\n intro n\n have h1 : (0 : \u211d) < ((n : \u211d) + 1) * A := mul_pos (by positivity) hA0\n have h2 : (0 : \u211d) < ((n : \u211d) + 1) * (A + (n : \u211d) + 1) := by\n apply mul_pos (by positivity)\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hA0, h3]\n rw [\u2190 mul_inv]\n apply (inv_le_inv\u2080 h2 h1).mpr\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n linarith [hA0, h3]\n have hS' : (\u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9) \u2264 1 + Real.log (N : \u211d) := by\n have h := sum_one_div_le_one_add_log N\n simpa [one_div] using h\n calc \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n \u2264 \u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9 * A\u207b\u00b9 :=\n Finset.sum_le_sum fun n _ => hper n\n _ = (\u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9) * A\u207b\u00b9 := by rw [\u2190 Finset.sum_mul]\n _ \u2264 (1 + Real.log (N : \u211d)) * A\u207b\u00b9 :=\n mul_le_mul_of_nonneg_right hS' (inv_nonneg.mpr hA0.le)\n _ = (1 + Real.log (N : \u211d)) / A := by rw [div_eq_mul_inv]\n -- the tail bound\n have htail : (\u2211' n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N))\n \u2264 1 / (N : \u211d) := by\n have h1 : Summable (fun n : \u2115 => (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9)\n (n + N)) :=\n (summable_nat_add_iff N).mpr hker_summ\n have hterm : \u2200 n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N)\n \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1) := by\n intro n\n show ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9\n \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)\n have hN0 : (0 : \u211d) < (n : \u211d) + N := by\n have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n have h3 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n linarith [h2, h3]\n have htele : (1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)\n = (((n : \u211d) + N) * ((n : \u211d) + N + 1))\u207b\u00b9 := by\n rw [div_sub_div _ _ hN0.ne' (by positivity)]\n rw [div_eq_iff (by positivity : ((n : \u211d) + N) * ((n : \u211d) + N + 1) \u2260 0)]\n rw [inv_mul_cancel\u2080 (by positivity : ((n : \u211d) + N) * ((n : \u211d) + N + 1) \u2260 0)]\n ring\n rw [htele]\n have h2 : (0 : \u211d) < ((n : \u211d) + N) * ((n : \u211d) + N + 1) := by positivity\n have h3 : (0 : \u211d) < (((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1) := by\n apply mul_pos\n \u00b7 push_cast\n have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n have h5 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n positivity\n \u00b7 push_cast\n have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n have h5 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n linarith [hA0, h4, h5]\n apply (inv_le_inv\u2080 h3 h2).mpr\n push_cast\n have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n nlinarith [hA0, h4, hN0]\n calc (\u2211' n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N))\n \u2264 \u2211' n : \u2115, (1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)) :=\n Summable.tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable\n _ = 1 / (N : \u211d) := (hasSum_one_div_sub_telescope N hN1).tsum_eq\n -- the kernel bound\n have hN0R : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n have hkernel_bound : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)\n \u2264 (2 + Real.log (A + 1)) / A := by\n rw [hsplit]\n have h1 : (1 + Real.log (N : \u211d)) / A \u2264 (1 + Real.log (A + 1)) / A := by\n apply div_le_div_of_nonneg_left _ hA0\n have h2 : Real.log (N : \u211d) \u2264 Real.log (A + 1) := Real.log_le_log hN0R hNA1\n linarith [h2]\n have h2 : (1 : \u211d) / (N : \u211d) \u2264 1 / A := one_div_le_one_div_of_le hA0 hNA\n linarith [h1, h2, hhead, htail]\n -- the norm of the series\n have hser : \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n \u2264 (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by\n calc \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n \u2264 \u2211' n : \u2115, \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016 :=\n norm_tsum_le_tsum_norm hterm_summ\n _ \u2264 \u2211' n : \u2115, \u2016w\u2016 / (((n : \u211d) + 1) * (A + (n : \u211d) + 1)) :=\n tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ\n (summable_digamma_majorant hwre)\n _ = \u2016w\u2016 * \u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9 := by\n rw [tsum_mul_left]\n apply tsum_congr\n intro n\n rw [div_eq_mul_inv]\n _ \u2264 \u2016w\u2016 * ((2 + Real.log (A + 1)) / A) :=\n mul_le_mul_of_nonneg_left hkernel_bound (norm_nonneg _)\n _ = (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by ring\n -- the ratio \u2016w\u2016/A \u2264 3\n have hratio : \u2016w\u2016 / A \u2264 3 := by\n have h1 : \u2016w\u2016 \u2264 3 * A := by\n have hnormsq : \u2016w\u2016 ^ 2 = w.re ^ 2 + w.im ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n ring\n have him5 : w.im ^ 2 \u2264 25 := by\n calc w.im ^ 2 = |w.im| ^ 2 := by rw [sq_abs]\n _ \u2264 5 ^ 2 := pow_le_pow_left\u2080 (abs_nonneg _) hwim _\n _ = 25 := by norm_num\n have h2 : \u2016w\u2016 ^ 2 \u2264 (3 * A) ^ 2 := by\n rw [hnormsq]\n have hA2 : 2 \u2264 A := hwre\n nlinarith [him5, hA2]\n exact le_of_pow_le_pow_left\u2080 (two_ne_zero) (by positivity) h2\n rw [div_le_iff\u2080 hA0]\n linarith [h1]\n have hlogA : Real.log (A + 1) \u2264 Real.log (\u2016w\u2016 + 1) := by\n apply Real.log_le_log (by linarith [hA0])\n have h1 : w.re \u2264 \u2016w\u2016 := by\n have h2 := Complex.abs_re_le_norm w\n rwa [abs_of_nonneg (by linarith [hwre])] at h2\n linarith [h1]\n -- the final assembly\n have h\u03b31 : Real.eulerMascheroniConstant \u2264 1 :=\n Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)\n have h1w : \u2016(1 : \u2102) / w\u2016 \u2264 1 := by\n rw [norm_div, norm_one]\n rw [div_le_one (by linarith [hw_norm_ge] : (0 : \u211d) < \u2016w\u2016)]\n exact hw_norm_ge\n calc \u2016-(Real.eulerMascheroniConstant : \u2102) - 1 / w\n + \u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n \u2264 Real.eulerMascheroniConstant + \u2016(1 : \u2102) / w\u2016\n + \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016 := by\n refine (norm_add_le _ _).trans ?_\n refine add_le_add_right ?_ _\n refine (norm_sub_le _ _).trans ?_\n rw [norm_neg]\n refine add_le_add_right ?_ _\n rw [show (Real.eulerMascheroniConstant : \u2102)\n = ((Real.eulerMascheroniConstant : \u211d) : \u2102) from rfl, Complex.norm_real,\n Real.norm_eq_abs,\n abs_of_nonneg (Real.one_half_lt_eulerMascheroniConstant.le.trans (by norm_num))]\n _ \u2264 1 + 1 + (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by\n gcongr\n \u00b7 exact h\u03b31\n \u00b7 exact h1w\n \u00b7 exact hser\n _ \u2264 20 * Real.log (2 + \u2016w\u2016) := by\n have h2 : (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) \u2264 3 * (2 + Real.log (\u2016w\u2016 + 1)) := by\n apply mul_le_mul hratio (by linarith [hlogA]) (by positivity) (by positivity)\n have h3 : Real.log (\u2016w\u2016 + 1) \u2264 Real.log (2 + \u2016w\u2016) :=\n Real.log_le_log (by positivity) (by linarith)\n have hlognonneg : (0 : \u211d) \u2264 Real.log (2 + \u2016w\u2016) :=\n Real.log_nonneg (by linarith [hw_norm_ge])\n nlinarith [h2, h3, hlog4, hlognonneg]\n\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 401,
"oldLines": 7,
"newStart": 401,
"newLines": 7,
"lines": [
" \u2264 \u2211' n : \u2115, \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016 :=",
" norm_tsum_le_tsum_norm hterm_summ",
" _ \u2264 \u2211' n : \u2115, \u2016w\u2016 / (((n : \u211d) + 1) * (A + (n : \u211d) + 1)) :=",
"- tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ",
"+ Summable.tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ",
" (summable_digamma_majorant hwre)",
" _ = \u2016w\u2016 * \u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9 := by",
" rw [tsum_mul_left]"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"I left a sorry at the end of scaledZeta_jensen_count. The ZerosBound conclusion: Σ ≤ 1/log(R/r)·log B with r = 24/25, R = 99/100: 1/log((99/100)/(24/25))·log((9/4)|t|²) = 1/log(99/96)·log(...) = 1/log(33/32)·log(...) — wait (99/100)/(24/25) = (99/100)·(25/24) = 99/(4·24) = 99/96 = 33/32 ✓. So h : Σ ≤ (1/log(33/32))·log((9/4)|t|²). My target: Σ ≤ log((9/4)|t|²)/log(33/32) — same thing (div vs 1/· mul): `one_div` form. The exact form of ZerosBound's conclusion: `1 / Real.log (R / r) * Real.log B` — my target `Real.log B / Real.log (33/32)` — with R/r = (99/100)/(24/25) = 33/32 ✓. So the final step: 1/log(R/r)·log B = log B/log(33/32): need R/r = 33/32: norm_num: (99/100)/(24/25) = 33/32 ✓. So:\n```lean\n refine h.trans_eq ?_\n rw [one_div, inv_mul_eq_div] -- 1/log(R/r)·log B = log B / log(R/r)\n congr 2 -- log B = log B ✓; log(R/r) = log(33/32)\n · -- (9/4)|t|² = (9/4)|t|² ✓ rfl — hmm the congr structure\n · norm_num -- (99/100)/(24/25) = 33/32\n```\nHmm — `trans_eq` : a ≤ b → b = c → a ≤ c — `h.trans_eq ?_`?? the name for LE: `LE.le.trans_eq (h : a ≤ b) (h' : b = c) : a ≤ c` ✓. Then goal: 1/log(R/r)·log B = log((9/4)|t|²)/log(33/32) — with B = (9/4)|t|², R = 99/100, r = 24/25 as the implicits — need them to match: the ZerosBound call's B was inferred from hB : ∀ z, ‖z‖ ≤ R → ‖f z‖ ≤ B — B := (9/4)*|t|² ✓ and R := 99/100 ✓ r := 24/25 ✓. So h : Σ ≤ 1/Real.log(99/100/(24/25))·Real.log((9/4)*|t|²). Then:\n```lean\n refine h.trans_eq ?_\n rw [one_div, inv_mul_eq_div]\n norm_num -- (99/100)/(24/25) = 33/32: the log argument\n```\nHmm — rw [one_div, inv_mul_eq_div]: target RHS: log B/log(33/32): after rw: 1/log((99/100)/(24/25))·log B = log B/log(33/32): one_div : 1/x = x⁻¹: then inv_mul_eq_div : x⁻¹·y = x/y ✓: becomes log B / log((99/100)/(24/25)) = log B / log(33/32): then congr on the log args: (99/100)/(24/25) = 33/32 by norm_num:\n```lean\n rw [one_div, inv_mul_eq_div]\n congr 2\n · rfl? -- the log B parts... hmm\n```\nThe equality: Real.log B / Real.log ((99/100)/(24/25)) = Real.log B / Real.log (33/32): congr 1 gives Real.log((99/100)/(24/25)) = Real.log(33/32): congr 1 again: (99/100)/(24/25) = 33/32: norm_num ✓. So `rw [one_div, inv_mul_eq_div]; congr 2; norm_num`? congr 2 on A/X = B/Y gives A = B and X = Y: A = B is log B = log B ✓ rfl (congr auto-closes rfl?) and X = Y: log(...) = log(33/32): then need another congr... use `congr 1` twice? Let me just:\n```lean\n refine h.trans_eq ?_\n rw [one_div, inv_mul_eq_div]\n have hratio : (99 / 100 : ℝ) / (24 / 25) = 33 / 32 := by norm_num\n rw [hratio]\n```\n✓ clean.","signature":""},{"type":"text","text":"Completing the Jensen count's final step (the ratio normalization)."},{"type":"tool_use","id":"Edit_374","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean","old_string":" have h := ZerosBound (f := scaledZeta t) (r := 24 / 25) (R := 99 / 100)\n (by norm_num) (by norm_num) (by norm_num) (by norm_num)\n (scaledZeta_analytic ht) (scaledZeta_zero t) scaledZeta_zeros_finite hB\n refine h.trans ?_\n rw [one_div, inv_mul_eq_div]\n apply div_le_div_of_nonneg_right _ ... \n sorry\n\nend NguyenRH1\n\nend","new_string":" have h := ZerosBound (f := scaledZeta t) (r := 24 / 25) (R := 99 / 100)\n (by norm_num) (by norm_num) (by norm_num) (by norm_num)\n (scaledZeta_analytic ht) (scaledZeta_zero t) scaledZeta_zeros_finite hB\n refine h.trans_eq ?_\n rw [one_div, inv_mul_eq_div]\n have hratio : (99 / 100 : ℝ) / (24 / 25) = 33 / 32 := by norm_num\n rw [hratio]\n\nend NguyenRH1\n\nend"},"extra_content":null}]