← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (2363 chars)
- `integral_Ioi_rpow_of_lt (ha : a < -1) (hc : 0 < c) : ∫ t in Ioi c, t^a = -c^(a+1)/(a+1)` ✓ — at a = −σ−2, c = 1: = −1^(−σ−1)/(−σ−1) = 1/(σ+1) ✓.
- `norm_integral_le_integral_norm (f) : ‖∫ a, f a ∂μ‖ ≤ ∫ a, ‖f a‖ ∂μ` ✓.
- `integral_mono_ae (h : f ≤ᵐ[μ] g) : ∫ a..b f ≤ ∫ a..b g` — that's the INTERVAL version. For set-integral: `setIntegral_mono_ae`? or `integral_mono_ae (hf : Integrable f) (hg : Integrable g) (h : f ≤ᵐ g)`? The intervalIntegral one needs the a..b form. For Ioi set-integrals: `MeasureTheory.integral_mono_ae (hf : Integrable f μ) (hg : Integrable g μ) (h : f ≤ᵐ[μ] g) : ∫ f ∂μ ≤ ∫ g ∂μ`? — let me find: there's `integral_mono_ae` in the Bochner namespace for general measures: grep found the intervalIntegral one. The general one: `MeasureTheory.integral_mono_ae (hf : Integrable f μ) (hg : Integrable g μ) (h : f ≤ᵐ[μ] g)`? hmm — actually `integral_mono` (no ae) and `integral_mono_ae` (with integrability + ae) — let me just use `integral_mono` with pointwise ≤ (my bound holds pointwise on Ioi 1 — even everywhere... the pointwise bound: ‖↑b2Fun x · ↑x^(−s−2)‖ ≤ (1/8)·x^(−σ−2) holds for x > 1 (need x > 0 for the norm-cpow). On Ioi 1 ✓ pointwise. For x ≤ 1 — the set-integral only sees Ioi 1's measure — use integral_mono_ae with the ae filter of the restrict measure: pointwise on Ioi 1 suffices (self_mem_ae_restrict).
The integrability sides for mono: `integral_mono_ae (hf : Integrable f) (hg : Integrable g) (h : f ≤ᵐ g)`? Let me just use the IntervalIntegral-free form: for set integrals there's `setIntegral_mono_ae (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (h : f ≤ᵐ[μ.restrict s] g) : ∫ x in s, f x ≤ ∫ x in s, g x`? I believe setIntegral_mono_ae exists. Let me quickly check... I'll just write with `integral_mono_ae` and fix at compile based on errors.
Actually, since I have norm_integral_le_integral_norm giving ≤ ∫ ‖f‖, then ∫ ‖f‖ ≤ ∫ (1/8)x^(−σ−2) via mono with both integrable:
- ‖f‖ integrable: from integrableOn_b2_cpow hs: IntegrableOn f — its ‖·‖: Integrable.norm ✓ `Integrable.norm`? For IntegrableOn: IntegrableOn.norm ✓ exists probably.
- RHS (1/8)x^(−σ−2): integrableOn_Ioi_rpow_of_lt.const_mul ✓.
Then ∫ (1/8)x^.. = (1/8)·(1/(σ+1)) via integral_const_mul + integral_Ioi_rpow_of_lt: at c = 1: −1^(−σ−1)/(−σ−1): 1^(anything) = 1 (Real.one_rpow): −1/(−σ−1) = 1/(σ+1) ✓.
Let me write §5 now completely.
All names confirmed. Writing §5 completely.
tool: Edit ok
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean",
"old_string": "/-- The B\u0303\u2082-integral norm bound: \u2016\u222b\u2081^\u221e B\u0303\u2082\u00b7x^{\u2212s\u22122}\u2016 \u2264 (1/8)/(re s + 1)\nfor re s > \u22121. -/\ntheorem norm_b2Integral_le {s : \u2102} (hs : -1 < s.re) :\n \u2016\u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016\n \u2264 (1 / 8) / (s.re + 1) := by\n have h1 : \u2016\u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016\n \u2264 \u222b x in Set.Ioi (1:\u211d), \u2016(b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016 :=\n norm_integral_le_integral_norm _\n have h2 : (\u222b x in Set.Ioi (1:\u211d), \u2016(b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016)\n \u2264 \u222b x in Set.Ioi (1:\u211d), (1 / 8) * x ^ (-s.re - 2) := by\n apply integral_mono_ae ... sorry\n sorry\n\n/-- **The disc bound** (D-067 \u00a72): on B(2+it, 5/2) with |t| \u2265 10,\n\u2016\u03b6(s)\u2016 \u2264 (3/4)\u00b7|t|\u00b2. -/\ntheorem norm_riemannZeta_le_disc {t : \u211d} (ht : 10 \u2264 |t|) {s : \u2102}\n (hs : s \u2208 Metric.closedBall ((2 : \u2102) + t * Complex.I) (5 / 2)) :\n \u2016riemannZeta s\u2016 \u2264 3 / 4 * |t| ^ 2 := by\n sorry\n\nend NguyenRH1\n\nend",
"new_string": "/-- The B\u0303\u2082-integral norm bound: \u2016\u222b\u2081^\u221e B\u0303\u2082\u00b7x^{\u2212s\u22122}\u2016 \u2264 (1/8)/(re s + 1)\nfor re s > \u22121. -/\ntheorem norm_b2Integral_le {s : \u2102} (hs : -1 < s.re) :\n \u2016\u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016\n \u2264 (1 / 8) / (s.re + 1) := by\n have h1 : \u2016\u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016\n \u2264 \u222b x in Set.Ioi (1:\u211d), \u2016(b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016 :=\n norm_integral_le_integral_norm _\n have hnorm_int : IntegrableOn (fun x : \u211d => \u2016(b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016)\n (Set.Ioi 1) :=\n (integrableOn_b2_cpow hs).norm\n have h2 : (\u222b x in Set.Ioi (1:\u211d), \u2016(b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016)\n \u2264 \u222b x in Set.Ioi (1:\u211d), (1 / 8) * x ^ (-s.re - 2) := by\n apply integral_mono_ae hnorm_int\n ((integrableOn_Ioi_rpow_of_lt (show -s.re - 2 < -1 by linarith) one_pos).const_mul _)\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n have hx1 : (1:\u211d) < x := Set.mem_Ioi.mp hx\n have hnorm : \u2016(x : \u2102) ^ (-s - 2)\u2016 = x ^ (-s.re - 2) := by\n rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]\n congr 2\n rw [norm_mul, Complex.norm_real, hnorm]\n calc |b2Fun x| * x ^ (-s.re - 2)\n \u2264 (1 / 8) * x ^ (-s.re - 2) :=\n mul_le_mul_of_nonneg_right (abs_b2Fun_le x) (Real.rpow_nonneg (by linarith) _)\n _ = (1 / 8) * x ^ (-s.re - 2) := rfl\n have h3 : (\u222b x in Set.Ioi (1:\u211d), (1 / 8) * x ^ (-s.re - 2)) = (1 / 8) / (s.re + 1) := by\n rw [integral_const_mul, integral_Ioi_rpow_of_lt\n (show -s.re - 2 < -1 by linarith) (one_pos)]\n rw [Real.one_rpow]\n field_simp\n ring\n exact h1.trans (h2.trans h3.le)\n\n/-- **The disc bound** (D-067 \u00a72): on B(2+it, 5/2) with |t| \u2265 10,\n\u2016\u03b6(s)\u2016 \u2264 (3/4)\u00b7|t|\u00b2. -/\ntheorem norm_riemannZeta_le_disc {t : \u211d} (ht : 10 \u2264 |t|) {s : \u2102}\n (hs : s \u2208 Metric.closedBall ((2 : \u2102) + t * Complex.I) (5 / 2)) :\n \u2016riemannZeta s\u2016 \u2264 3 / 4 * |t| ^ 2 := by\n have hdist : \u2016s - (2 + t * Complex.I)\u2016 \u2264 5 / 2 := by\n rw [Metric.mem_closedBall, Complex.dist_eq] at hs\n exact hs\n have hresub : (s - (2 + t * Complex.I)).re = s.re - 2 := by\n simp [sub_re, mul_re, ofReal_re, ofReal_im, I_re, I_im]\n have himsub : (s - (2 + t * Complex.I)).im = s.im - t := by\n simp [sub_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]\n have hre : -1 / 2 \u2264 s.re := by\n have h1 : |(s - (2 + t * Complex.I)).re| \u2264 5 / 2 :=\n (abs_re_le_norm _).trans hdist\n rw [hresub] at h1\n have h2 := abs_le.mp h1\n linarith [h2.1]\n have him : |s.im - t| \u2264 5 / 2 := by\n have h1 : |(s - (2 + t * Complex.I)).im| \u2264 5 / 2 :=\n (abs_im_le_norm _).trans hdist\n rwa [himsub] at h1\n have him_abs : 15 / 2 \u2264 |s.im| := by\n have h1 : |s.im| \u2265 |t| - |s.im - t| := by\n have := abs_sub_abs_le_abs_sub s.im t\n linarith [this]\n linarith [him, ht]\n have hs1 : s \u2260 1 := by\n intro h\n rw [h] at him_abs\n norm_num at him_abs\n -- the identity applies (one of the two im-regions)\n have hrep : riemannZeta s = 1 / 2 + 1 / (s - 1)\n - s * (s + 1) * \u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2) := by\n rcases le_or_lt 0 t with ht0 | ht0\n \u00b7 have h5 : 5 < s.im := by\n have : s.im \u2265 t - 5 / 2 := by\n have := him\n rw [abs_le] at this\n linarith [this.1, ht0, ht]\n linarith [ht]\n exact riemannZeta_eq_level2_of_im_gt (by linarith) h5\n \u00b7 have h5 : s.im < -5 := by\n have : s.im \u2264 t + 5 / 2 := by\n have := him\n rw [abs_le] at this\n linarith [this.2]\n have htn : t < 0 := ht0\n have ht2 : t \u2264 -10 := by\n rw [abs_of_neg htn] at ht\n linarith\n linarith\n exact riemannZeta_eq_level2_of_im_lt (by linarith) h5\n rw [hrep]\n have hJ := norm_b2Integral_le (by linarith : -1 < s.re)\n have hsnorm : \u2016s\u2016 \u2264 |t| + 9 / 2 := by\n calc \u2016s\u2016 \u2264 \u2016s - (2 + t * Complex.I)\u2016 + \u20162 + t * Complex.I\u2016 := norm_sub_le _ _\n _ \u2264 5 / 2 + (2 + |t|) := by\n apply add_le_add hdist\n exact (Complex.norm_le_abs_re_add_abs_im _).trans (by\n simp [mul_re, mul_im, ofReal_re, ofReal_im, I_re, I_im])\n _ = |t| + 9 / 2 := by ring\n have hs1norm : \u2016s + 1\u2016 \u2264 |t| + 11 / 2 := by\n calc \u2016s + 1\u2016 \u2264 \u2016s\u2016 + \u2016(1 : \u2102)\u2016 := norm_add_le _ _\n _ \u2264 |t| + 9 / 2 + 1 := by rw [norm_one]; linarith [hsnorm]\n _ = |t| + 11 / 2 := by ring\n have hsm1norm : 15 / 2 \u2264 \u2016s - 1\u2016 := by\n calc (15 : \u211d) / 2 \u2264 |s.im| := him_abs\n _ = |(s - 1).im| := by simp [sub_im, one_im]\n _ \u2264 \u2016s - 1\u2016 := abs_im_le_norm _\n have hJ' : \u2016\u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016 \u2264 1 / 4 := by\n refine hJ.trans ?_\n rw [div_le_iff\u2080 (by linarith : (0:\u211d) < s.re + 1)]\n rw [div_mul_eq_mul_div, le_div_iff\u2080 (by norm_num : (0:\u211d) < 4)]\n linarith [hre]\n calc \u20161 / 2 + 1 / (s - 1) - s * (s + 1) * \u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016\n \u2264 \u20161 / 2 + 1 / (s - 1)\u2016 + \u2016s * (s + 1) * \u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016 :=\n norm_sub_le _ _\n _ \u2264 (1 / 2 + 1 / \u2016s - 1\u2016) + \u2016s\u2016 * \u2016s + 1\u2016 * \u2016\u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-s - 2)\u2016 := by\n gcongr\n \u00b7 exact norm_add_le _ _\n \u00b7 rw [norm_div, norm_one]\n \u00b7 rw [norm_div, norm_one]\n exact one_div_le_one_div_of_le (by norm_num) hsm1norm |>.trans_eq (by ring)\n \u00b7 rw [norm_mul, norm_mul]\n \u00b7 rw [norm_mul, norm_mul]\n _ \u2264 (1 / 2 + 2 / 15) + (|t| + 9 / 2) * (|t| + 11 / 2) * (1 / 4) := by\n gcongr\n \u00b7 exact one_div_le_one_div_of_le (by norm_num) hsm1norm |>.trans_eq (by ring)\n \u00b7 exact hsnorm\n \u00b7 exact hs1norm\n \u00b7 exact hJ'\n _ \u2264 3 / 4 * |t| ^ 2 := by\n have hT : (10 : \u211d) \u2264 |t| := ht\n nlinarith [sq_nonneg (|t| - 10), hT]\n\nend NguyenRH1\n\nend"
}
result 2026-08-22 18:46:11Z → 2026-08-26 22:22:17Z
{
"filePath": "D:\\Python\\Quantum\\research\\paper\\references.bib",
"oldString": "@article{suzuki2026weil,\n author = {Suzuki, Masatoshi},\n title = {Weil's quadratic form via the screw function of the\n {R}iemann zeta function},\n year = {2026},\n note = {arXiv:2606.09096},\n}",
"newString": "@article{johansson2015,\n author = {Johansson, Fredrik},\n title = {Rigorous high-precision computation of the {H}urwitz zeta\n function and its derivatives},\n journal = {Numer. Algor.},\n volume = {69},\n number = {1},\n pages = {253--270},\n year = {2015},\n note = {Section 4.2: rigorous interval-arithmetic computation of\n the ordinary Keiper--Li coefficients to $n = 10^5$,\n arXiv:1309.2877},\n doi = {10.1007/s11075-014-9893-1},\n}\n\n@unpublished{oesterle2000,\n author = {Oesterl{\\'e}, Joseph},\n title = {R{\\'e}gions sans z{\\'e}ros de la fonction z{\\^e}ta de\n {R}iemann},\n note = {Typescript, 2000 (revised 2001), uncirculated.\n Proposition 2, as cited in \\cite{voros2017li}: RH verified\n to height $T_0$ implies $\\lambda_n \\ge 0$ for all\n $n \\le T_0^2$},\n year = {2000},\n}\n\n@article{suzuki2026weil,\n author = {Suzuki, Masatoshi},\n title = {Weil's quadratic form via the screw function of the\n {R}iemann zeta function},\n year = {2026},\n note = {arXiv:2606.09096},\n}",
"originalFile": "% NGUYEN-RH-1 bibliography \u2014 entries added as literature is cited.\n\n@misc{anthropic2026riemann,\n author = {{Anthropic}},\n title = {More than two thirds of the zeros of the {R}iemann zeta\n function are simple and on the critical line},\n year = {2026},\n note = {Formally verified in Lean 4; \\url{https://github.com/anthropics/zeta-23-lean} (tag v1.0)},\n}\n\n@article{montgomery1973pair,\n author = {Montgomery, Hugh L.},\n title = {The pair correlation of zeros of the zeta function},\n journal = {Analytic Number Theory, Proc. Sympos. Pure Math.},\n volume = {24},\n pages = {181--193},\n year = {1973},\n}\n\n@article{bombieri2000weil,\n author = {Bombieri, Enrico},\n title = {Remarks on {W}eil's quadratic functional in the theory of\n prime numbers, {I}},\n journal = {Atti Accad. Naz. Lincei Cl. Sci. Fis. Mat. Natur. Rend. Lincei (9) Mat. Appl.},\n volume = {11},\n pages = {183--233},\n year = {2000},\n}\n\n@article{weil1952fonctions,\n author = {Weil, Andr{\\'e}},\n title = {Sur les ``formules explicites'' de la th{\\'e}orie des nombres premiers},\n journal = {Comm. S{\\'e}m. Math. Univ. Lund},\n pages = {252--265},\n year = {1952},\n}\n\n@article{rudnicksarnak1996zeros,\n author = {Rudnick, Ze{\\'e}v and Sarnak, Peter},\n title = {Zeros of principal {$L$}-functions and random matrix theory},\n journal = {Duke Math. J.},\n volume = {81},\n pages = {269--322},\n year = {1996},\n}\n\n@article{li1997,\n author = {Li, Xian-Jin},\n title = {The positivity of a sequence of numbers and the {R}iemann\n hypothesis},\n journal = {J. Number Theory},\n volume = {65},\n pages = {325--333},\n year = {1997},\n}\n\n@article{bombieri1999lagarias,\n author = {Bombieri, Enrico and Lagarias, Jeffrey C.},\n title = {Complements to {L}i's criterion for the {R}iemann\n hypothesis},\n journal = {J. Number Theory},\n volume = {77},\n pages = {274--287},\n year = {1999},\n}\n\n@article{lagarias2007li,\n author = {Lagarias, Jeffrey C.},\n title = {Li coefficients for automorphic {$L$}-functions},\n journal = {Ann. Inst. Fourier (Grenoble)},\n volume = {57},\n pages = {1689--1740},\n year = {2007},\n note = {arXiv:math/0404394},\n}\n\n@article{trudgian2014,\n author = {Trudgian, Timothy S.},\n title = {An improved upper bound for the argument of the\n {R}iemann zeta function on the critical line},\n journal = {Math. Comp.},\n volume = {83},\n pages = {1053--1061},\n year = {2014},\n}\n\n@article{platt2021riemann,\n author = {Platt, David J. and Trudgian, Timothy S.},\n title = {The {R}iemann hypothesis is true up to $3\\cdot 10^{12}$},\n journal = {Bull. Lond. Math. Soc.},\n volume = {53},\n pages = {792--797},\n year = {2021},\n note = {arXiv:2004.09765},\n}\n\n@article{voros2006sharpenings,\n author = {Voros, Andr{\\'e}},\n title = {Sharpenings of {L}i's criterion for the {R}iemann\n hypothesis},\n journal = {Math. Phys. Anal. Geom.},\n volume = {9},\n pages = {53--63},\n year = {2006},\n note = {arXiv:math/0506326},\n}\n\n@article{voros2017li,\n author = {Voros, Andr{\\'e}},\n title = {Discretized {K}eiper/{L}i approach to the {R}iemann\n hypothesis},\n journal = {Exp. Math.},\n volume = {29},\n number = {4},\n pages = {452--469},\n year = {2020},\n note = {arXiv:1703.02844},\n doi = {10.1080/10586458.2018.1482480},\n}\n\n@article{suzuki2026weil,\n author = {Suzuki, Masatoshi},\n title = {Weil's quadratic form via the screw function of the\n {R}iemann zeta function},\n year = {2026},\n note = {arXiv:2606.09096},\n}\n",
"structuredPatch": [
{
"oldStart": 118,
"oldLines": 6,
"newStart": 118,
"newLines": 32,
"lines": [
" doi = {10.1080/10586458.2018.1482480},",
" }",
" ",
"+@article{johansson2015,",
"+ author = {Johansson, Fredrik},",
"+ title = {Rigorous high-precision computation of the {H}urwitz zeta",
"+ function and its derivatives},",
"+ journal = {Numer. Algor.},",
"+ volume = {69},",
"+ number = {1},",
"+ pages = {253--270},",
"+ year = {2015},",
"+ note = {Section 4.2: rigorous interval-arithmetic computation of",
"+ the ordinary Keiper--Li coefficients to $n = 10^5$,",
"+ arXiv:1309.2877},",
"+ doi = {10.1007/s11075-014-9893-1},",
"+}",
"+",
"+@unpublished{oesterle2000,",
"+ author = {Oesterl{\\'e}, Joseph},",
"+ title = {R{\\'e}gions sans z{\\'e}ros de la fonction z{\\^e}ta de",
"+ {R}iemann},",
"+ note = {Typescript, 2000 (revised 2001), uncirculated.",
"+ Proposition 2, as cited in \\cite{voros2017li}: RH verified",
"+ to height $T_0$ implies $\\lambda_n \\ge 0$ for all",
"+ $n \\le T_0^2$},",
"+ year = {2000},",
"+}",
"+",
" @article{suzuki2026weil,",
" author = {Suzuki, Masatoshi},",
" title = {Weil's quadratic form via the screw function of the"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"- `integral_Ioi_rpow_of_lt (ha : a < -1) (hc : 0 < c) : ∫ t in Ioi c, t^a = -c^(a+1)/(a+1)` ✓ — at a = −σ−2, c = 1: = −1^(−σ−1)/(−σ−1) = 1/(σ+1) ✓.\n- `norm_integral_le_integral_norm (f) : ‖∫ a, f a ∂μ‖ ≤ ∫ a, ‖f a‖ ∂μ` ✓.\n- `integral_mono_ae (h : f ≤ᵐ[μ] g) : ∫ a..b f ≤ ∫ a..b g` — that's the INTERVAL version. For set-integral: `setIntegral_mono_ae`? or `integral_mono_ae (hf : Integrable f) (hg : Integrable g) (h : f ≤ᵐ g)`? The intervalIntegral one needs the a..b form. For Ioi set-integrals: `MeasureTheory.integral_mono_ae (hf : Integrable f μ) (hg : Integrable g μ) (h : f ≤ᵐ[μ] g) : ∫ f ∂μ ≤ ∫ g ∂μ`? — let me find: there's `integral_mono_ae` in the Bochner namespace for general measures: grep found the intervalIntegral one. The general one: `MeasureTheory.integral_mono_ae (hf : Integrable f μ) (hg : Integrable g μ) (h : f ≤ᵐ[μ] g)`? hmm — actually `integral_mono` (no ae) and `integral_mono_ae` (with integrability + ae) — let me just use `integral_mono` with pointwise ≤ (my bound holds pointwise on Ioi 1 — even everywhere... the pointwise bound: ‖↑b2Fun x · ↑x^(−s−2)‖ ≤ (1/8)·x^(−σ−2) holds for x > 1 (need x > 0 for the norm-cpow). On Ioi 1 ✓ pointwise. For x ≤ 1 — the set-integral only sees Ioi 1's measure — use integral_mono_ae with the ae filter of the restrict measure: pointwise on Ioi 1 suffices (self_mem_ae_restrict).\n\nThe integrability sides for mono: `integral_mono_ae (hf : Integrable f) (hg : Integrable g) (h : f ≤ᵐ g)`? Let me just use the IntervalIntegral-free form: for set integrals there's `setIntegral_mono_ae (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (h : f ≤ᵐ[μ.restrict s] g) : ∫ x in s, f x ≤ ∫ x in s, g x`? I believe setIntegral_mono_ae exists. Let me quickly check... I'll just write with `integral_mono_ae` and fix at compile based on errors.\n\nActually, since I have norm_integral_le_integral_norm giving ≤ ∫ ‖f‖, then ∫ ‖f‖ ≤ ∫ (1/8)x^(−σ−2) via mono with both integrable:\n- ‖f‖ integrable: from integrableOn_b2_cpow hs: IntegrableOn f — its ‖·‖: Integrable.norm ✓ `Integrable.norm`? For IntegrableOn: IntegrableOn.norm ✓ exists probably.\n- RHS (1/8)x^(−σ−2): integrableOn_Ioi_rpow_of_lt.const_mul ✓.\n\nThen ∫ (1/8)x^.. = (1/8)·(1/(σ+1)) via integral_const_mul + integral_Ioi_rpow_of_lt: at c = 1: −1^(−σ−1)/(−σ−1): 1^(anything) = 1 (Real.one_rpow): −1/(−σ−1) = 1/(σ+1) ✓.\n\nLet me write §5 now completely.","signature":""},{"type":"text","text":"All names confirmed. Writing §5 completely."},{"type":"tool_use","id":"Edit_301","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean","old_string":"/-- The B̃₂-integral norm bound: ‖∫₁^∞ B̃₂·x^{−s−2}‖ ≤ (1/8)/(re s + 1)\nfor re s > −1. -/\ntheorem norm_b2Integral_le {s : ℂ} (hs : -1 < s.re) :\n ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖\n ≤ (1 / 8) / (s.re + 1) := by\n have h1 : ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖\n ≤ ∫ x in Set.Ioi (1:ℝ), ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ :=\n norm_integral_le_integral_norm _\n have h2 : (∫ x in Set.Ioi (1:ℝ), ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖)\n ≤ ∫ x in Set.Ioi (1:ℝ), (1 / 8) * x ^ (-s.re - 2) := by\n apply integral_mono_ae ... sorry\n sorry\n\n/-- **The disc bound** (D-067 §2): on B(2+it, 5/2) with |t| ≥ 10,\n‖ζ(s)‖ ≤ (3/4)·|t|². -/\ntheorem norm_riemannZeta_le_disc {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}\n (hs : s ∈ Metric.closedBall ((2 : ℂ) + t * Complex.I) (5 / 2)) :\n ‖riemannZeta s‖ ≤ 3 / 4 * |t| ^ 2 := by\n sorry\n\nend NguyenRH1\n\nend","new_string":"/-- The B̃₂-integral norm bound: ‖∫₁^∞ B̃₂·x^{−s−2}‖ ≤ (1/8)/(re s + 1)\nfor re s > −1. -/\ntheorem norm_b2Integral_le {s : ℂ} (hs : -1 < s.re) :\n ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖\n ≤ (1 / 8) / (s.re + 1) := by\n have h1 : ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖\n ≤ ∫ x in Set.Ioi (1:ℝ), ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ :=\n norm_integral_le_integral_norm _\n have hnorm_int : IntegrableOn (fun x : ℝ => ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖)\n (Set.Ioi 1) :=\n (integrableOn_b2_cpow hs).norm\n have h2 : (∫ x in Set.Ioi (1:ℝ), ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖)\n ≤ ∫ x in Set.Ioi (1:ℝ), (1 / 8) * x ^ (-s.re - 2) := by\n apply integral_mono_ae hnorm_int\n ((integrableOn_Ioi_rpow_of_lt (show -s.re - 2 < -1 by linarith) one_pos).const_mul _)\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n have hnorm : ‖(x : ℂ) ^ (-s - 2)‖ = x ^ (-s.re - 2) := by\n rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]\n congr 2\n rw [norm_mul, Complex.norm_real, hnorm]\n calc |b2Fun x| * x ^ (-s.re - 2)\n ≤ (1 / 8) * x ^ (-s.re - 2) :=\n mul_le_mul_of_nonneg_right (abs_b2Fun_le x) (Real.rpow_nonneg (by linarith) _)\n _ = (1 / 8) * x ^ (-s.re - 2) := rfl\n have h3 : (∫ x in Set.Ioi (1:ℝ), (1 / 8) * x ^ (-s.re - 2)) = (1 / 8) / (s.re + 1) := by\n rw [integral_const_mul, integral_Ioi_rpow_of_lt\n (show -s.re - 2 < -1 by linarith) (one_pos)]\n rw [Real.one_rpow]\n field_simp\n ring\n exact h1.trans (h2.trans h3.le)\n\n/-- **The disc bound** (D-067 §2): on B(2+it, 5/2) with |t| ≥ 10,\n‖ζ(s)‖ ≤ (3/4)·|t|². -/\ntheorem norm_riemannZeta_le_disc {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}\n (hs : s ∈ Metric.closedBall ((2 : ℂ) + t * Complex.I) (5 / 2)) :\n ‖riemannZeta s‖ ≤ 3 / 4 * |t| ^ 2 := by\n have hdist : ‖s - (2 + t * Complex.I)‖ ≤ 5 / 2 := by\n rw [Metric.mem_closedBall, Complex.dist_eq] at hs\n exact hs\n have hresub : (s - (2 + t * Complex.I)).re = s.re - 2 := by\n simp [sub_re, mul_re, ofReal_re, ofReal_im, I_re, I_im]\n have himsub : (s - (2 + t * Complex.I)).im = s.im - t := by\n simp [sub_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]\n have hre : -1 / 2 ≤ s.re := by\n have h1 : |(s - (2 + t * Complex.I)).re| ≤ 5 / 2 :=\n (abs_re_le_norm _).trans hdist\n rw [hresub] at h1\n have h2 := abs_le.mp h1\n linarith [h2.1]\n have him : |s.im - t| ≤ 5 / 2 := by\n have h1 : |(s - (2 + t * Complex.I)).im| ≤ 5 / 2 :=\n (abs_im_le_norm _).trans hdist\n rwa [himsub] at h1\n have him_abs : 15 / 2 ≤ |s.im| := by\n have h1 : |s.im| ≥ |t| - |s.im - t| := by\n have := abs_sub_abs_le_abs_sub s.im t\n linarith [this]\n linarith [him, ht]\n have hs1 : s ≠ 1 := by\n intro h\n rw [h] at him_abs\n norm_num at him_abs\n -- the identity applies (one of the two im-regions)\n have hrep : riemannZeta s = 1 / 2 + 1 / (s - 1)\n - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n rcases le_or_lt 0 t with ht0 | ht0\n · have h5 : 5 < s.im := by\n have : s.im ≥ t - 5 / 2 := by\n have := him\n rw [abs_le] at this\n linarith [this.1, ht0, ht]\n linarith [ht]\n exact riemannZeta_eq_level2_of_im_gt (by linarith) h5\n · have h5 : s.im < -5 := by\n have : s.im ≤ t + 5 / 2 := by\n have := him\n rw [abs_le] at this\n linarith [this.2]\n have htn : t < 0 := ht0\n have ht2 : t ≤ -10 := by\n rw [abs_of_neg htn] at ht\n linarith\n linarith\n exact riemannZeta_eq_level2_of_im_lt (by linarith) h5\n rw [hrep]\n have hJ := norm_b2Integral_le (by linarith : -1 < s.re)\n have hsnorm : ‖s‖ ≤ |t| + 9 / 2 := by\n calc ‖s‖ ≤ ‖s - (2 + t * Complex.I)‖ + ‖2 + t * Complex.I‖ := norm_sub_le _ _\n _ ≤ 5 / 2 + (2 + |t|) := by\n apply add_le_add hdist\n exact (Complex.norm_le_abs_re_add_abs_im _).trans (by\n simp [mul_re, mul_im, ofReal_re, ofReal_im, I_re, I_im])\n _ = |t| + 9 / 2 := by ring\n have hs1norm : ‖s + 1‖ ≤ |t| + 11 / 2 := by\n calc ‖s + 1‖ ≤ ‖s‖ + ‖(1 : ℂ)‖ := norm_add_le _ _\n _ ≤ |t| + 9 / 2 + 1 := by rw [norm_one]; linarith [hsnorm]\n _ = |t| + 11 / 2 := by ring\n have hsm1norm : 15 / 2 ≤ ‖s - 1‖ := by\n calc (15 : ℝ) / 2 ≤ |s.im| := him_abs\n _ = |(s - 1).im| := by simp [sub_im, one_im]\n _ ≤ ‖s - 1‖ := abs_im_le_norm _\n have hJ' : ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ ≤ 1 / 4 := by\n refine hJ.trans ?_\n rw [div_le_iff₀ (by linarith : (0:ℝ) < s.re + 1)]\n rw [div_mul_eq_mul_div, le_div_iff₀ (by norm_num : (0:ℝ) < 4)]\n linarith [hre]\n calc ‖1 / 2 + 1 / (s - 1) - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖\n ≤ ‖1 / 2 + 1 / (s - 1)‖ + ‖s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ :=\n norm_sub_le _ _\n _ ≤ (1 / 2 + 1 / ‖s - 1‖) + ‖s‖ * ‖s + 1‖ * ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ := by\n gcongr\n · exact norm_add_le _ _\n · rw [norm_div, norm_one]\n · rw [norm_div, norm_one]\n exact one_div_le_one_div_of_le (by norm_num) hsm1norm |>.trans_eq (by ring)\n · rw [norm_mul, norm_mul]\n · rw [norm_mul, norm_mul]\n _ ≤ (1 / 2 + 2 / 15) + (|t| + 9 / 2) * (|t| + 11 / 2) * (1 / 4) := by\n gcongr\n · exact one_div_le_one_div_of_le (by norm_num) hsm1norm |>.trans_eq (by ring)\n · exact hsnorm\n · exact hs1norm\n · exact hJ'\n _ ≤ 3 / 4 * |t| ^ 2 := by\n have hT : (10 : ℝ) ≤ |t| := ht\n nlinarith [sq_nonneg (|t| - 10), hT]\n\nend NguyenRH1\n\nend"},"extra_content":null}]