LiReflect.lean
993 lines · 26 declarations · 0 sorries · updated 08-23-2026
Declarations
| Kind | Name | Line |
|---|---|---|
| theorem | norm_le_abs_re_add_abs_im' | 39 |
| theorem | im_div_two | 46 |
| theorem | re_div_two | 50 |
| theorem | Gammaℝ_ne_zero_of_im_ne_zero' | 54 |
| theorem | differentiableAt_Gammaℝ_of_im_ne_zero' | 64 |
| theorem | logDeriv_congr | 84 |
| theorem | gammaR_shift_four | 92 |
| theorem | gammaR_shift | 130 |
| theorem | logDeriv_Gammaℝ_shift | 161 |
| theorem | completedZeta_eventuallyEq | 233 |
| theorem | logDeriv_completedZeta_eq_add | 242 |
| theorem | logDeriv_completedZeta_neg_one_sub | 251 |
| theorem | riemannZeta_one_sub_ne_zero | 271 |
| theorem | logDeriv_zeta_fe | 283 |
| theorem | riemannZeta_one_sub_eq_zero_of_nontrivial | 300 |
| theorem | one_sub_mem_nearZeros_neg | 318 |
| theorem | mem_nearZeros_of_one_sub_mem_neg | 368 |
| theorem | nearZeros_neg_eq_image | 374 |
| theorem | zeroMult_one_sub | 388 |
| theorem | sum_nearZeros_neg_reflect | 395 |
| theorem | norm_log_le_of_one_le | 415 |
| theorem | norm_digamma_le_log_of | 425 |
| theorem | gammaR_bracket_norm_le | 466 |
| theorem | digamma_add_natCast | 614 |
| theorem | norm_digamma_sub_log_le_of_two_le_abs_im | 640 |
| theorem | logDeriv_riemannZeta_sub_nearZeros_le_left | 928 |
Source
/-
NguyenRH1/LiReflect.lean — tier ii′ sub-stage ii′-5d (D-067 §3 left half +
§6): the FE-reflection of the loose Davenport-disc R-bound (ii′-5c) to
σ ∈ [−5/2, 1/2], |t| ≥ 10, plus the left-plane uniform digamma bound
‖ψ(w) − log w‖ ≤ 3 for |im w| ≥ 2 (an ii′-5e input).
Route (D-067 §3):
* Λ = ΓR·ζ and Λ(1−s) = Λ(s) give the pointwise log-derivative FE
logDeriv ζ s = −logDeriv ζ (1−s) − [logDeriv ΓR s + logDeriv ΓR (1−s)];
* the near-zero sums at t and −t CANCEL EXACTLY under ρ ↦ 1−ρ
(Zeta23 `analyticOrderAt_zeta_one_sub` for the multiplicities);
* the ΓR-bracket is −log π + ½ψ((1−s)/2) + ½ψ((s+4)/2) − 2(s+1)/(s(s+2))
(the s-side shifted by +4 via the ΓR recurrence so both digamma arguments
sit in re > 0), each piece O(log|t|) by Zeta23
`StirlingVert.digamma_stirling`.
Constants are deliberately loose (D-067 §6): only the ii′-5e identity
passes tight constants to ii′-5f.
Archive references: D-067 §3/§6, journal-024.
-/
import Mathlib
import Zeta23.RvM.GammaSide
import Zeta23.RvM.CountByIntegral
import Zeta23.GammaFacts.StirlingVert
import Zeta23.ZetaReflect
import Zeta23.FromPNTPlus.EulerMaclaurin
import NguyenRH1.LiDisc
open Zeta23 Complex Filter Topology MeasureTheory
open scoped Nat
noncomputable section
namespace NguyenRH1
/-! ## 0. Small complex helpers -/
/-- `‖z‖ ≤ |re z| + |im z|` (triangle on the re/im decomposition). -/
theorem norm_le_abs_re_add_abs_im' (z : ℂ) : ‖z‖ ≤ |z.re| + |z.im| := by
have hb : (0 : ℝ) ≤ |z.re| + |z.im| := add_nonneg (abs_nonneg _) (abs_nonneg _)
refine le_of_pow_le_pow_left₀ (two_ne_zero) hb ?_
rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]
nlinarith [sq_abs z.re, sq_abs z.im, mul_nonneg (abs_nonneg z.re) (abs_nonneg z.im)]
/-- `(s/2).im = s.im/2`. -/
theorem im_div_two (s : ℂ) : (s / 2).im = s.im / 2 := by
simp [Complex.div_ofNat_im]
/-- `(s/2).re = s.re/2`. -/
theorem re_div_two (s : ℂ) : (s / 2).re = s.re / 2 := by
simp [Complex.div_ofNat_re]
/-- ΓR is nonzero off the real line (its zeros are the real points −2n). -/
theorem Gammaℝ_ne_zero_of_im_ne_zero' {s : ℂ} (hs : s.im ≠ 0) : Complex.Gammaℝ s ≠ 0 := by
intro h
rw [Complex.Gammaℝ_eq_zero_iff] at h
obtain ⟨n, hn⟩ := h
apply hs
rw [hn]
simp
/-- ΓR is complex-differentiable off the real line (local copy of the
Zeta23 XiPrime lemma, kept here to avoid the heavy import). -/
theorem differentiableAt_Gammaℝ_of_im_ne_zero' {s : ℂ} (hs : s.im ≠ 0) :
DifferentiableAt ℂ Complex.Gammaℝ s := by
have hhalf : ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := by
intro m h
apply hs
have h2 : s = -2 * (m : ℂ) := by
have := congrArg (· * (2 : ℂ)) h
rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at this
rw [this]; ring
rw [h2]; simp
have h1 : DifferentiableAt ℂ (fun z : ℂ => (Real.pi : ℂ) ^ (-z / 2)) s := by
refine DifferentiableAt.const_cpow ?_ (Or.inl (by exact_mod_cast Real.pi_ne_zero))
exact (differentiableAt_id.neg).div_const 2
have h2 : DifferentiableAt ℂ (fun z : ℂ => Complex.Gamma (z / 2)) s :=
(Complex.differentiableAt_Gamma _ hhalf).comp s (differentiableAt_id.div_const 2)
have hdef : Complex.Gammaℝ = fun z : ℂ => (Real.pi : ℂ) ^ (-z / 2) * Complex.Gamma (z / 2) :=
funext Complex.Gammaℝ_def
rw [hdef]; exact h1.mul h2
/-- logDeriv transfers across an eventually-equal pair. -/
theorem logDeriv_congr {f g : ℂ → ℂ} {s : ℂ} (h : f =ᶠ[𝓝 s] g) :
logDeriv f s = logDeriv g s := by
simp only [logDeriv_apply, h.deriv_eq, h.eq_of_nhds]
/-! ## 1. The ΓR shift by +4 -/
/-- The ΓR recurrence in ratio form: ΓR(s+4) = π⁻²·(s/2)(s/2+1)·ΓR(s),
valid off the real line. -/
theorem gammaR_shift_four {s : ℂ} (hs : s.im ≠ 0) :
Complex.Gammaℝ (s + 4)
= (((Real.pi ^ 2 : ℝ)⁻¹ : ℝ) : ℂ) * ((s / 2) * (s / 2 + 1)) * Complex.Gammaℝ s := by
have hs0 : s ≠ 0 := fun h => hs (by rw [h]; simp)
have hs2 : s / 2 ≠ 0 := div_ne_zero hs0 (two_ne_zero : (2 : ℂ) ≠ 0)
have hs21 : s / 2 + 1 ≠ 0 := by
intro h
have h1 : s / 2 = -1 := eq_neg_of_add_eq_zero_left h
have h2 : s = -2 := by
have := congrArg (· * (2 : ℂ)) h1
rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at this
rw [this]; ring
exact hs (by rw [h2]; simp)
have hGamma : Complex.Gamma (s / 2 + 2)
= (s / 2 + 1) * (s / 2) * Complex.Gamma (s / 2) := by
rw [show s / 2 + 2 = s / 2 + 1 + 1 by ring,
Complex.Gamma_add_one _ hs21, Complex.Gamma_add_one _ hs2]
ring
have hexp2 : Real.exp (-2 * Real.log Real.pi) = (Real.pi ^ 2)⁻¹ := by
have h1 : (-2 : ℝ) * Real.log Real.pi = Real.log ((Real.pi ^ 2)⁻¹) := by
rw [Real.log_inv, Real.log_pow]; push_cast; ring
rw [h1, Real.exp_log (by positivity)]
have hpi : (Real.pi : ℂ) ^ (-(s + 4) / 2)
= (Real.pi : ℂ) ^ (-s / 2) * (((Real.pi ^ 2 : ℝ)⁻¹ : ℝ) : ℂ) := by
have hlog : Complex.log (Real.pi : ℂ) = (Real.log Real.pi : ℂ) :=
(Complex.ofReal_log Real.pi_nonneg).symm
rw [Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero : (Real.pi : ℂ) ≠ 0) _,
Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero : (Real.pi : ℂ) ≠ 0) _,
hlog]
have harg : (Real.log Real.pi : ℂ) * (-(s + 4) / 2)
= (Real.log Real.pi : ℂ) * (-s / 2) + ((-2 * Real.log Real.pi : ℝ) : ℂ) := by
push_cast; ring
rw [harg, Complex.exp_add, ← Complex.ofReal_exp, hexp2]
rw [Complex.Gammaℝ_def, Complex.Gammaℝ_def, show (s + 4) / 2 = s / 2 + 2 by ring,
hGamma, hpi]
ring
/-- The pointwise shift identity in solved form. -/
theorem gammaR_shift {s : ℂ} (hs : s.im ≠ 0) :
Complex.Gammaℝ s
= (Real.pi : ℂ) ^ 2 * Complex.Gammaℝ (s + 4) / ((s / 2) * (s / 2 + 1)) := by
have hs0 : s ≠ 0 := fun h => hs (by rw [h]; simp)
have hs2 : s / 2 ≠ 0 := div_ne_zero hs0 (two_ne_zero : (2 : ℂ) ≠ 0)
have hs21 : s / 2 + 1 ≠ 0 := by
intro h
have h1 : s / 2 = -1 := eq_neg_of_add_eq_zero_left h
have h2 : s = -2 := by
have := congrArg (· * (2 : ℂ)) h1
rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at this
rw [this]; ring
exact hs (by rw [h2]; simp)
have hP : (s / 2) * (s / 2 + 1) ≠ 0 := mul_ne_zero hs2 hs21
have hC : ((((Real.pi ^ 2 : ℝ)⁻¹ : ℝ) : ℂ)) ≠ 0 := by
exact_mod_cast inv_ne_zero (pow_ne_zero 2 Real.pi_ne_zero)
have hpi2 : (Real.pi : ℂ) ^ 2 * (((Real.pi ^ 2 : ℝ)⁻¹ : ℝ) : ℂ) = 1 := by
push_cast
rw [mul_inv_cancel₀
(pow_ne_zero 2 (show (Real.pi : ℂ) ≠ 0 by exact_mod_cast Real.pi_ne_zero))]
rw [eq_div_iff hP, gammaR_shift_four hs]
calc Complex.Gammaℝ s * ((s / 2) * (s / 2 + 1))
= ((Real.pi : ℂ) ^ 2 * (((Real.pi ^ 2 : ℝ)⁻¹ : ℝ) : ℂ))
* (Complex.Gammaℝ s * ((s / 2) * (s / 2 + 1))) := by
rw [hpi2, one_mul]
_ = (Real.pi : ℂ) ^ 2
* ((((Real.pi ^ 2 : ℝ)⁻¹ : ℝ) : ℂ) * ((s / 2) * (s / 2 + 1)) * Complex.Gammaℝ s) := by
ring
/-- logDeriv of ΓR at a non-real point, shifted to re > 0:
logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)). -/
theorem logDeriv_Gammaℝ_shift {s : ℂ} (hs : s.im ≠ 0) :
logDeriv Complex.Gammaℝ s
= logDeriv Complex.Gammaℝ (s + 4) - 2 * (s + 1) / (s * (s + 2)) := by
have hU : IsOpen {z : ℂ | z.im ≠ 0} := isOpen_ne_fun Complex.continuous_im continuous_const
have hs0 : s ≠ 0 := fun h => hs (by rw [h]; simp)
have hs2 : s / 2 ≠ 0 := div_ne_zero hs0 (two_ne_zero : (2 : ℂ) ≠ 0)
have hs21 : s / 2 + 1 ≠ 0 := by
intro h
have h1 : s / 2 = -1 := eq_neg_of_add_eq_zero_left h
have h2 : s = -2 := by
have := congrArg (· * (2 : ℂ)) h1
rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at this
rw [this]; ring
exact hs (by rw [h2]; simp)
have hs22 : s + 2 ≠ 0 := by
intro h
have h2 : s = -2 := by
have h' := congrArg (· - 2) h
rw [add_sub_cancel_right] at h'
exact h'.trans (zero_sub 2)
exact hs (by rw [h2]; simp)
have hEv : Complex.Gammaℝ =ᶠ[𝓝 s]
fun z => (Real.pi : ℂ) ^ 2 * Complex.Gammaℝ (z + 4) / ((z / 2) * (z / 2 + 1)) := by
filter_upwards [hU.mem_nhds hs] with z hz using gammaR_shift hz
have hG4 : Complex.Gammaℝ (s + 4) ≠ 0 :=
Gammaℝ_ne_zero_of_im_ne_zero' (by simp [Complex.add_im]; exact hs)
have hP : (s / 2) * (s / 2 + 1) ≠ 0 := mul_ne_zero hs2 hs21
have hdG4 : DifferentiableAt ℂ (fun z : ℂ => Complex.Gammaℝ (z + 4)) s :=
(differentiableAt_Gammaℝ_of_im_ne_zero' (by simp [Complex.add_im]; exact hs)).comp s
(differentiableAt_id.add_const 4)
have hpi_ne : (Real.pi : ℂ) ≠ 0 := by exact_mod_cast Real.pi_ne_zero
have hnum_ne : (Real.pi : ℂ) ^ 2 * Complex.Gammaℝ (s + 4) ≠ 0 :=
mul_ne_zero (pow_ne_zero 2 hpi_ne) hG4
have hnum_diff : DifferentiableAt ℂ
(fun z => (Real.pi : ℂ) ^ 2 * Complex.Gammaℝ (z + 4)) s :=
(differentiableAt_const _).mul hdG4
have hden_diff : DifferentiableAt ℂ (fun z : ℂ => (z / 2) * (z / 2 + 1)) s :=
(differentiableAt_id.div_const 2).mul ((differentiableAt_id.div_const 2).add_const 1)
have hstep1 : logDeriv (fun z => (Real.pi : ℂ) ^ 2 * Complex.Gammaℝ (z + 4)
/ ((z / 2) * (z / 2 + 1))) s
= logDeriv (fun z => (Real.pi : ℂ) ^ 2 * Complex.Gammaℝ (z + 4)) s
- logDeriv (fun z => (z / 2) * (z / 2 + 1)) s :=
logDeriv_div s hnum_ne hP hnum_diff hden_diff
have hstep2 : logDeriv (fun z => (Real.pi : ℂ) ^ 2 * Complex.Gammaℝ (z + 4)) s
= logDeriv (fun z => Complex.Gammaℝ (z + 4)) s :=
logDeriv_const_mul s _ (pow_ne_zero 2 hpi_ne)
rw [logDeriv_congr hEv, hstep1, hstep2]
-- logDeriv (ΓR(·+4)) s = logDeriv ΓR (s+4)
have hder : deriv (fun z : ℂ => Complex.Gammaℝ (z + 4)) s = deriv Complex.Gammaℝ (s + 4) := by
have h1 := ((differentiableAt_Gammaℝ_of_im_ne_zero'
(by simp [Complex.add_im]; exact hs)).hasDerivAt).comp s ((hasDerivAt_id' s).add_const 4)
have h2 : deriv (fun z : ℂ => Complex.Gammaℝ (z + 4)) s = deriv Complex.Gammaℝ (s + 4) * 1 :=
h1.deriv
rw [h2, mul_one]
have hld : logDeriv (fun z : ℂ => Complex.Gammaℝ (z + 4)) s = logDeriv Complex.Gammaℝ (s + 4) := by
simp only [logDeriv_apply, hder]
rw [hld]
-- the polynomial logDeriv
have hpoly : logDeriv (fun z : ℂ => (z / 2) * (z / 2 + 1)) s = 2 * (s + 1) / (s * (s + 2)) := by
have hd1 : HasDerivAt (fun z : ℂ => z / 2) (1 / 2 : ℂ) s := (hasDerivAt_id' s).div_const 2
have hd2 : HasDerivAt (fun z : ℂ => z / 2 + 1) (1 / 2 : ℂ) s := hd1.add_const 1
have hdm := hd1.mul hd2
have hdeq : deriv (fun z : ℂ => (z / 2) * (z / 2 + 1)) s
= (1 / 2 : ℂ) * (s / 2 + 1) + s / 2 * (1 / 2) := hdm.deriv
rw [logDeriv_apply, hdeq]
field_simp [hs2, hs21, hs0, hs22]
ring
rw [hpoly]
/-! ## 2. The log-derivative functional equation -/
/-- Λ agrees with ΓR·ζ near any nonzero non-pole point. -/
theorem completedZeta_eventuallyEq {s : ℂ} (hs0 : s ≠ 0) (hG : Complex.Gammaℝ s ≠ 0)
(hd : DifferentiableAt ℂ Complex.Gammaℝ s) :
completedRiemannZeta =ᶠ[𝓝 s] fun z => Complex.Gammaℝ z * riemannZeta z := by
have h1 : ∀ᶠ z in 𝓝 s, z ≠ 0 := isOpen_compl_singleton.mem_nhds hs0
have h2 : ∀ᶠ z in 𝓝 s, Complex.Gammaℝ z ≠ 0 := hd.continuousAt.eventually_ne hG
filter_upwards [h1, h2] with z hz0 hzG
exact RvM.completedRiemannZeta_eq_Gammaℝ_mul hz0 hzG
/-- logDeriv Λ = logDeriv ΓR + logDeriv ζ at good points. -/
theorem logDeriv_completedZeta_eq_add {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1)
(hG : Complex.Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0)
(hd : DifferentiableAt ℂ Complex.Gammaℝ s) :
logDeriv completedRiemannZeta s
= logDeriv Complex.Gammaℝ s + logDeriv riemannZeta s := by
rw [logDeriv_congr (completedZeta_eventuallyEq hs0 hG hd)]
exact logDeriv_mul s hG hζ hd (differentiableAt_riemannZeta hs1)
/-- logDeriv Λ s = −logDeriv Λ (1−s) (the FE derivative). -/
theorem logDeriv_completedZeta_neg_one_sub {s : ℂ} (h1s0 : 1 - s ≠ 0) (h1s1 : 1 - s ≠ 1) :
logDeriv completedRiemannZeta s = - logDeriv completedRiemannZeta (1 - s) := by
have hfe : (fun z : ℂ => completedRiemannZeta (1 - z)) = completedRiemannZeta :=
funext fun z => completedRiemannZeta_one_sub z
have hd1 : DifferentiableAt ℂ completedRiemannZeta (1 - s) :=
differentiableAt_completedZeta h1s0 h1s1
have hder : deriv (fun z : ℂ => completedRiemannZeta (1 - z)) s
= - deriv completedRiemannZeta (1 - s) := by
have h1 : HasDerivAt (fun z : ℂ => 1 - z) (-1 : ℂ) s := by
simpa using (hasDerivAt_id' s).const_sub (1 : ℂ)
have h2 := hd1.hasDerivAt.comp s h1
have h3 : deriv (fun z : ℂ => completedRiemannZeta (1 - z)) s
= deriv completedRiemannZeta (1 - s) * -1 := h2.deriv
rw [h3, mul_neg_one]
have h3 : logDeriv completedRiemannZeta s
= logDeriv (fun z : ℂ => completedRiemannZeta (1 - z)) s := by
rw [hfe]
rw [h3, logDeriv_apply, logDeriv_apply, hder, neg_div]
/-- ζ(1−s) ≠ 0 from ζ(s) ≠ 0 (via Λ). -/
theorem riemannZeta_one_sub_ne_zero {s : ℂ} (hs0 : s ≠ 0) (hG : Complex.Gammaℝ s ≠ 0)
(hζ : riemannZeta s ≠ 0) (h1s0 : 1 - s ≠ 0) (hG1 : Complex.Gammaℝ (1 - s) ≠ 0) :
riemannZeta (1 - s) ≠ 0 := by
intro h
have hΛ : completedRiemannZeta (1 - s) = 0 := by
rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul h1s0 hG1, h, mul_zero]
rw [completedRiemannZeta_one_sub] at hΛ
rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul hs0 hG] at hΛ
exact mul_ne_zero hG hζ hΛ
/-- **The log-derivative functional equation** at good points:
logDeriv ζ s = −logDeriv ζ (1−s) − [logDeriv ΓR s + logDeriv ΓR (1−s)]. -/
theorem logDeriv_zeta_fe {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1)
(hG : Complex.Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0)
(hd : DifferentiableAt ℂ Complex.Gammaℝ s)
(h1s0 : 1 - s ≠ 0) (h1s1 : 1 - s ≠ 1)
(hG1 : Complex.Gammaℝ (1 - s) ≠ 0) (hζ1 : riemannZeta (1 - s) ≠ 0)
(hd1 : DifferentiableAt ℂ Complex.Gammaℝ (1 - s)) :
logDeriv riemannZeta s
= - logDeriv riemannZeta (1 - s)
- (logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s)) := by
have h1 := logDeriv_completedZeta_eq_add hs0 hs1 hG hζ hd
have h2 := logDeriv_completedZeta_eq_add h1s0 h1s1 hG1 hζ1 hd1
have h3 := logDeriv_completedZeta_neg_one_sub h1s0 h1s1
linear_combination -h1 - h2 + h3
/-! ## 3. The exact zero-sum cancellation under ρ ↦ 1 − ρ -/
/-- Reflection of nontrivial zeros: ζ(1−ρ) = 0. -/
theorem riemannZeta_one_sub_eq_zero_of_nontrivial {ρ : ℂ} (hρ : IsNontrivialZero ρ) :
riemannZeta (1 - ρ) = 0 := by
have h0 : ρ ≠ 0 := fun h => hρ.2.1.ne' (by rw [h]; exact Complex.zero_re)
have hG : Complex.Gammaℝ ρ ≠ 0 := Complex.Gammaℝ_ne_zero_of_re_pos hρ.2.1
have h1ρre : (1 - ρ).re = 1 - ρ.re := by simp [Complex.sub_re, Complex.one_re]
have h1ρ0 : (1 : ℂ) - ρ ≠ 0 := fun h => by
have hre0 : (1 - ρ).re = 0 := by rw [h]; simp
rw [h1ρre] at hre0
linarith [hρ.2.2]
have hG1 : Complex.Gammaℝ (1 - ρ) ≠ 0 :=
Complex.Gammaℝ_ne_zero_of_re_pos (by rw [h1ρre]; linarith [hρ.2.2])
have hΛ1 : completedRiemannZeta (1 - ρ) = 0 := by
rw [completedRiemannZeta_one_sub, RvM.completedRiemannZeta_eq_Gammaℝ_mul h0 hG,
hρ.1, mul_zero]
rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul h1ρ0 hG1] at hΛ1
exact (mul_eq_zero.mp hΛ1).resolve_left hG1
/-- The reflected near-zero lies in the reflected window. -/
theorem one_sub_mem_nearZeros_neg {t : ℝ} {ρ : ℂ} (hρ : ρ ∈ nearZeros t) :
1 - ρ ∈ nearZeros (-t) := by
rw [mem_nearZeros] at hρ
obtain ⟨hρdisc, hρim⟩ := hρ
have hρnt : IsNontrivialZero ρ := zeroDisc_isNontrivial hρdisc
rw [mem_nearZeros]
refine ⟨mem_zeroDiscFinset.mpr ⟨?_, riemannZeta_one_sub_eq_zero_of_nontrivial hρnt⟩, ?_⟩
· -- ball membership: ‖(1−ρ) − (2 − it)‖² = (1 + ρ.re)² + (ρ.im − t)² ≤ 5 ≤ (5/2)²
rw [Metric.mem_closedBall, Complex.dist_eq]
have hnorm1 : ‖(1 - ρ) - discCenter (-t)‖ ≤ Real.sqrt 5 := by
have hsq : Complex.normSq ((1 - ρ) - discCenter (-t)) ≤ 5 := by
rw [Complex.normSq_apply]
have hre : ((1 - ρ) - discCenter (-t)).re = -(1 + ρ.re) := by
simp [discCenter, sub_re, add_re, mul_re, ofReal_re, ofReal_im, I_re, I_im, neg_re]
ring
have him : ((1 - ρ) - discCenter (-t)).im = -(ρ.im - t) := by
simp [discCenter, sub_im, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, neg_im]
ring
have h1 : (1 + ρ.re) ^ 2 ≤ 4 := by
have hb : |1 + ρ.re| ≤ 2 := by
rw [abs_le]
constructor <;> linarith [hρnt.2.1, hρnt.2.2]
calc (1 + ρ.re) ^ 2 = |1 + ρ.re| ^ 2 := by rw [sq_abs]
_ ≤ 2 ^ 2 := pow_le_pow_left₀ (abs_nonneg _) hb _
_ = 4 := by norm_num
have h2 : (ρ.im - t) ^ 2 ≤ 1 := by
have h3 : |ρ.im - t| ≤ 1 := hρim.le
calc (ρ.im - t) ^ 2 = |ρ.im - t| ^ 2 := by rw [sq_abs]
_ ≤ 1 ^ 2 := pow_le_pow_left₀ (abs_nonneg _) h3 2
_ = 1 := by norm_num
rw [hre, him]
nlinarith [h1, h2]
have h4 : ‖(1 - ρ) - discCenter (-t)‖ ^ 2 ≤ 5 := by
rw [← Complex.normSq_eq_norm_sq]; exact hsq
calc ‖(1 - ρ) - discCenter (-t)‖ = Real.sqrt (‖(1 - ρ) - discCenter (-t)‖ ^ 2) :=
(Real.sqrt_sq (norm_nonneg _)).symm
_ ≤ Real.sqrt 5 := Real.sqrt_le_sqrt h4
have h52 : Real.sqrt 5 ≤ 5 / 2 := by
have h1 : Real.sqrt 5 ≤ Real.sqrt ((5 / 2) ^ 2) := Real.sqrt_le_sqrt (by norm_num)
rwa [Real.sqrt_sq (by norm_num)] at h1
exact hnorm1.trans h52
· -- the ordinate window
show |(1 - ρ).im - -t| < 1
have : (1 - ρ).im = -ρ.im := by simp [Complex.sub_im, Complex.one_im]
rw [this]
have h2 : -ρ.im - -t = -(ρ.im - t) := by ring
rw [h2, abs_neg]
exact hρim
/-- The reverse direction (same lemma at −t). -/
theorem mem_nearZeros_of_one_sub_mem_neg {t : ℝ} {ρ' : ℂ} (h : ρ' ∈ nearZeros (-t)) :
1 - ρ' ∈ nearZeros t := by
have h2 := one_sub_mem_nearZeros_neg (t := -t) h
rwa [neg_neg] at h2
/-- The reflected near-zero finset is the image under ρ ↦ 1 − ρ. -/
theorem nearZeros_neg_eq_image (t : ℝ) :
nearZeros (-t) = (nearZeros t).image (fun ρ => 1 - ρ) := by
classical
ext ρ'
constructor
· intro h
rw [Finset.mem_image]
exact ⟨1 - ρ', mem_nearZeros_of_one_sub_mem_neg h, by ring⟩
· intro h
rw [Finset.mem_image] at h
obtain ⟨ρ, hρ, rfl⟩ := h
exact one_sub_mem_nearZeros_neg hρ
/-- Multiplicity invariance under ρ ↦ 1 − ρ (Zeta23 order transport). -/
theorem zeroMult_one_sub {ρ : ℂ} (h0 : 0 < ρ.re) (h1 : ρ.re < 1) :
zeroMult (1 - ρ) = zeroMult ρ := by
show ((analyticOrderAt riemannZeta (1 - ρ)).toNat) = (analyticOrderAt riemannZeta ρ).toNat
rw [analyticOrderAt_zeta_one_sub h0 h1]
/-- **The exact cancellation**: the near-zero sum at −t evaluated at 1−s is
minus the near-zero sum at t evaluated at s. -/
theorem sum_nearZeros_neg_reflect (t : ℝ) (s : ℂ) :
∑ ρ' ∈ nearZeros (-t), (zeroMult ρ' : ℂ) / (1 - s - ρ')
= - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ) := by
classical
have hinj : Set.InjOn (fun ρ : ℂ => 1 - ρ) (↑(nearZeros t)) := by
intro a _ b _ hab
have h1 : (1 : ℂ) - a = 1 - b := hab
exact sub_right_inj.mp h1
rw [nearZeros_neg_eq_image, Finset.sum_image hinj]
rw [← Finset.sum_neg_distrib]
apply Finset.sum_congr rfl
intro ρ hρ
have hnt := zeroDisc_isNontrivial ((mem_nearZeros.mp hρ).1)
rw [zeroMult_one_sub hnt.2.1 hnt.2.2]
have hden : (1 : ℂ) - s - (1 - ρ) = -(s - ρ) := by ring
rw [hden, div_neg]
/-! ## 4. The ΓR-bracket bound -/
/-- `‖log w‖ ≤ log ‖w‖ + π` for `‖w‖ ≥ 1`. -/
theorem norm_log_le_of_one_le {w : ℂ} (hw : 1 ≤ ‖w‖) :
‖Complex.log w‖ ≤ Real.log ‖w‖ + Real.pi := by
calc ‖Complex.log w‖ ≤ |(Complex.log w).re| + |(Complex.log w).im| :=
norm_le_abs_re_add_abs_im' _
_ = |Real.log ‖w‖| + |Complex.arg w| := by rw [Complex.log_re, Complex.log_im]
_ = Real.log ‖w‖ + |Complex.arg w| := by rw [abs_of_nonneg (Real.log_nonneg hw)]
_ ≤ Real.log ‖w‖ + Real.pi := add_le_add_right (Complex.abs_arg_le_pi w) _
/-- Stirling-flavoured digamma bound on the vertical strip:
`‖ψ(w)‖ ≤ log|t| + 5` when `|im w| = |t|/2`, `re w > 0`, `‖w‖ ≤ 2|t|`. -/
theorem norm_digamma_le_log_of {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
(hwre : 0 < w.re) (hwim : |w.im| = |t| / 2) (hwn : ‖w‖ ≤ 2 * |t|) :
‖Complex.digamma w‖ ≤ Real.log |t| + 5 := by
have ht0 : (0 : ℝ) < |t| := lt_of_lt_of_le (by norm_num) ht
have hwim5 : 5 ≤ |w.im| := by rw [hwim]; linarith [ht]
have hwnorm5 : 5 ≤ ‖w‖ := hwim5.trans (Complex.abs_im_le_norm w)
have hst := StirlingVert.digamma_stirling hwre (by rw [hwim]; linarith [ht])
have hlogpi : Real.pi ≤ 7 / 2 := Real.pi_lt_d2.le.trans (by norm_num)
have hlog2 : Real.log 2 ≤ 1 := Real.log_two_lt_d9.le.trans (by norm_num)
have hnorm12 : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by
rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 2)]
calc ‖Complex.digamma w‖
= ‖(Complex.digamma w - Complex.log w + (1 / 2 : ℂ) / w) + Complex.log w
- (1 / 2 : ℂ) / w‖ := by
congr 1; ring
_ ≤ ‖Complex.digamma w - Complex.log w + (1 / 2 : ℂ) / w‖ + ‖Complex.log w‖
+ ‖(1 / 2 : ℂ) / w‖ := by
refine (norm_sub_le _ _).trans ?_
exact add_le_add_left (norm_add_le _ _) _
_ ≤ 3 / w.im ^ 2 + (Real.log ‖w‖ + Real.pi) + (1 / 2) / ‖w‖ := by
refine add_le_add (add_le_add hst (norm_log_le_of_one_le (by linarith [hwnorm5]))) ?_
rw [norm_div, hnorm12]
_ ≤ Real.log |t| + 5 := by
have h1 : 3 / w.im ^ 2 ≤ 1 / 4 := by
have hsq : (25 : ℝ) ≤ w.im ^ 2 := by
calc (25 : ℝ) = 5 ^ 2 := by norm_num
_ ≤ |w.im| ^ 2 := pow_le_pow_left₀ (by norm_num) hwim5 _
_ = w.im ^ 2 := by rw [sq_abs]
rw [div_le_iff₀ (by linarith [hsq] : (0 : ℝ) < w.im ^ 2)]
nlinarith [hsq]
have h2 : Real.log ‖w‖ ≤ Real.log |t| + 1 := by
have h3 := Real.log_le_log (by linarith [hwnorm5] : (0 : ℝ) < ‖w‖) hwn
rw [Real.log_mul (two_ne_zero) (ne_of_gt ht0)] at h3
linarith [h3, hlog2]
have h4 : (1 / 2 : ℝ) / ‖w‖ ≤ 1 / 4 := by
rw [div_le_iff₀ (by linarith [hwnorm5] : (0 : ℝ) < ‖w‖)]
nlinarith [hwnorm5]
linarith [h1, h2, h4, hlogpi]
/-- The ΓR-bracket bound: `‖logDeriv ΓR (1−s) + logDeriv ΓR s‖ ≤ 4(log|t|)²`. -/
theorem gammaR_bracket_norm_le {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}
(hsim : s.im = t) (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 1 / 2) :
‖logDeriv Complex.Gammaℝ (1 - s) + logDeriv Complex.Gammaℝ s‖
≤ 4 * (Real.log |t|) ^ 2 := by
have ht0 : (0 : ℝ) < |t| := lt_of_lt_of_le (by norm_num) ht
have htim : s.im ≠ 0 := by
rw [hsim]
intro h
rw [h, abs_zero] at ht
norm_num at ht
have hsnorm : ‖s‖ ≤ 5 / 2 + |t| := by
refine (norm_le_abs_re_add_abs_im' s).trans ?_
have hsre : |s.re| ≤ 5 / 2 := abs_le.mpr ⟨by linarith [hσlo], by linarith [hσhi]⟩
rw [hsim]
linarith [hsre]
-- the (1−s)/2 point
have hw1re : 0 < ((1 - s) / 2).re := by
rw [re_div_two]
have : (1 - s).re = 1 - s.re := by simp [Complex.sub_re, Complex.one_re]
linarith [hσhi]
have hw1im : |((1 - s) / 2).im| = |t| / 2 := by
rw [im_div_two]
have : (1 - s).im = -t := by simp [Complex.sub_im, Complex.one_im, hsim]
rw [this, abs_div, abs_neg]
norm_num
have hw1n : ‖(1 - s) / 2‖ ≤ 2 * |t| := by
have h2 : ‖((2 : ℂ))‖ = 2 := by
rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by norm_num, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)]
rw [norm_div, h2]
have h1s : ‖1 - s‖ ≤ 1 + (5 / 2 + |t|) :=
(norm_sub_le 1 s).trans (by rw [norm_one]; linarith [hsnorm])
rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)]
nlinarith [h1s, ht]
-- the (s+4)/2 point
have hw2re : 0 < ((s + 4) / 2).re := by
rw [re_div_two]
have : (s + 4).re = s.re + 4 := by simp [Complex.add_re]
linarith [hσlo]
have hw2im : |((s + 4) / 2).im| = |t| / 2 := by
rw [im_div_two]
have : (s + 4).im = t := by simp [Complex.add_im, hsim]
rw [this, abs_div]
norm_num
have hw2n : ‖(s + 4) / 2‖ ≤ 2 * |t| := by
have h2 : ‖((2 : ℂ))‖ = 2 := by
rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by norm_num, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)]
rw [norm_div, h2]
have h4s : ‖s + 4‖ ≤ (5 / 2 + |t|) + 4 :=
(norm_add_le s 4).trans (by
have : ‖(4 : ℂ)‖ = 4 := by
rw [show (4 : ℂ) = ((4 : ℝ) : ℂ) by norm_num, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 4)]
linarith [hsnorm, this])
rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)]
nlinarith [h4s, ht]
have hd1 := norm_digamma_le_log_of ht hw1re hw1im hw1n
have hd2 := norm_digamma_le_log_of ht hw2re hw2im hw2n
-- the logDeriv evaluations
have hev1 : logDeriv Complex.Gammaℝ (1 - s)
= -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2) :=
RvM.logDeriv_Gammaℝ (by
have : (1 - s).re = 1 - s.re := by simp [Complex.sub_re, Complex.one_re]
linarith [hσhi])
have hev2 : logDeriv Complex.Gammaℝ (s + 4)
= -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma ((s + 4) / 2) :=
RvM.logDeriv_Gammaℝ (by
have : (s + 4).re = s.re + 4 := by simp [Complex.add_re]
linarith [hσlo])
have hshift := logDeriv_Gammaℝ_shift htim
have hbr : logDeriv Complex.Gammaℝ (1 - s) + logDeriv Complex.Gammaℝ s
= -(Real.log Real.pi : ℂ) + (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2)
+ (1 / 2 : ℂ) * Complex.digamma ((s + 4) / 2) - 2 * (s + 1) / (s * (s + 2)) := by
rw [hshift, hev1, hev2]
ring
rw [hbr]
-- the rational term
have hsnorm_pos : (0 : ℝ) < ‖s‖ := by
have : |t| ≤ ‖s‖ := by
have h := Complex.abs_im_le_norm s
rw [hsim] at h
exact h
linarith [ht0, this]
have hsnorm2_pos : (0 : ℝ) < ‖s + 2‖ := by
have h : |(s + 2).im| ≤ ‖s + 2‖ := Complex.abs_im_le_norm _
have him : (s + 2).im = t := by simp [Complex.add_im, hsim]
rw [him] at h
linarith [ht0, h]
have hrat : ‖2 * (s + 1) / (s * (s + 2))‖ ≤ 1 := by
rw [norm_div, norm_mul, norm_mul]
have h2 : ‖((2 : ℂ))‖ = 2 := by
rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by norm_num, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)]
have hs1n : ‖s + 1‖ ≤ 5 / 2 + |t| + 1 := by
have := norm_add_le s 1
rw [norm_one] at this
linarith [hsnorm, this]
have hsnorm_ge : |t| ≤ ‖s‖ := by
have h := Complex.abs_im_le_norm s
rw [hsim] at h
exact h
have hs2norm_ge : |t| ≤ ‖s + 2‖ := by
have h := Complex.abs_im_le_norm (s + 2)
have him : (s + 2).im = t := by simp [Complex.add_im, hsim]
rw [him] at h
exact h
rw [h2, div_le_one (mul_pos hsnorm_pos hsnorm2_pos)]
nlinarith [hs1n, hsnorm_ge, hs2norm_ge, ht]
-- log π ≤ 2
have hlogpi : Real.log Real.pi ≤ 2 := by
have he2 : Real.pi ≤ Real.exp 2 := by
have h1 := Real.exp_one_gt_d9
have h2 : Real.exp 2 = Real.exp 1 * Real.exp 1 := by
rw [← Real.exp_add]; norm_num
rw [h2]
nlinarith [h1, Real.pi_lt_d2, Real.exp_pos 1]
calc Real.log Real.pi ≤ Real.log (Real.exp 2) := Real.log_le_log Real.pi_pos he2
_ = 2 := Real.log_exp 2
-- the norm of the constant term
have hnormlogpi : ‖-(Real.log Real.pi : ℂ)‖ = Real.log Real.pi := by
rw [norm_neg, show ((Real.log Real.pi : ℂ)) = ((Real.log Real.pi : ℝ) : ℂ) from rfl,
Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (Real.log_nonneg ((by norm_num : (1 : ℝ) ≤ 3).trans Real.pi_gt_three.le))]
calc ‖-(Real.log Real.pi : ℂ) + (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2)
+ (1 / 2 : ℂ) * Complex.digamma ((s + 4) / 2) - 2 * (s + 1) / (s * (s + 2))‖
≤ ‖-(Real.log Real.pi : ℂ)‖ + ‖(1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2)‖
+ ‖(1 / 2 : ℂ) * Complex.digamma ((s + 4) / 2)‖ + ‖2 * (s + 1) / (s * (s + 2))‖ := by
refine (norm_sub_le _ _).trans ?_
refine add_le_add_left ?_ _
refine (norm_add_le _ _).trans ?_
exact add_le_add_left (norm_add_le _ _) _
_ ≤ Real.log Real.pi + (1 / 2) * (Real.log |t| + 5) + (1 / 2) * (Real.log |t| + 5) + 1 := by
have hnorm12 : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by
rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 2)]
rw [hnormlogpi, norm_mul, norm_mul, hnorm12]
linarith [hd1, hd2, hrat, hlogpi]
_ = Real.log |t| + 6 + Real.log Real.pi := by ring
_ ≤ Real.log |t| + 8 := by linarith [hlogpi]
_ ≤ 4 * (Real.log |t|) ^ 2 := by
have hL := two_le_log_abs_t ht
nlinarith [hL, sq_nonneg (Real.log |t| - 2)]
/-! ## 5. The digamma recurrence over a natural shift -/
/-- ψ(w + n) = ψ(w) + Σ_{j<n} (w + j)⁻¹ (iterated `digamma_apply_add_one`;
the off-real hypothesis keeps every step away from the poles). -/
theorem digamma_add_natCast {w : ℂ} (hw : w.im ≠ 0) (n : ℕ) :
Complex.digamma (w + n) = Complex.digamma w + ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ := by
have hne : ∀ j : ℕ, ∀ m : ℕ, w + (j : ℂ) ≠ -(m : ℂ) := by
intro j m h
apply hw
have h2 : (w + (j : ℂ)).im = 0 := by rw [h]; simp
rw [Complex.add_im, Complex.natCast_im, add_zero] at h2
exact h2
induction n with
| zero => simp
| succ k ih =>
have h1 := Complex.digamma_apply_add_one (w + (k : ℂ)) (hne k)
rw [show w + ((k + 1 : ℕ) : ℂ) = (w + (k : ℂ)) + 1 by push_cast; ring, h1, ih,
Finset.sum_range_succ]
ring
/-! ## 6. The left-plane uniform digamma bound (ii′-5e input) -/
/-- **The left-plane uniform digamma bound**: for `2 ≤ |im w|` (away from the
poles), `‖ψ(w) − log w‖ ≤ 3`. Route (D-067 §6): shift `w` by
`n = ⌈|re w|⌉₊ + 2` into the right half-plane (StirlingVert there), and
compare the reciprocal sum with the log difference by first-order
Euler–Maclaurin (`sum_eq_integral_add_integral_deriv`); the B̃₁ remainder is
bounded by the arctan integral `∫ dx/((x+a)²+c²) ≤ π/c ≤ π/2`. The constants
are uniform in the chain length — this is what makes the bound usable on the
γ-gap circles of ii′-5e. -/
theorem norm_digamma_sub_log_le_of_two_le_abs_im {w : ℂ} (hw : 2 ≤ |w.im|) :
‖Complex.digamma w - Complex.log w‖ ≤ 3 := by
-- setup
have him : w.im ≠ 0 := by
intro h
rw [h, abs_zero] at hw
norm_num at hw
have hc0 : (0 : ℝ) < |w.im| := by linarith [hw]
set n := ⌈|w.re|⌉₊ + 2 with hn
set v := w + (n : ℂ) with hv
have hnv : (0 : ℝ) < w.re + (n : ℝ) := by
have h1 : (n : ℝ) = (⌈|w.re|⌉₊ : ℝ) + 2 := by rw [hn]; push_cast; ring
have h2 : |w.re| ≤ (⌈|w.re|⌉₊ : ℝ) := Nat.le_ceil _
have h3 : 0 ≤ w.re + |w.re| := by linarith [neg_abs_le w.re]
nlinarith [h1, h2, h3]
have hvre : 0 < v.re := by
rw [hv]
simp [Complex.add_re, Complex.natCast_re]
exact hnv
have hvim : v.im = w.im := by
rw [hv]
simp [Complex.add_im, Complex.natCast_im]
have hvnorm : 2 ≤ ‖v‖ := by
have h := Complex.abs_im_le_norm v
rw [hvim] at h
linarith [hw, h]
have hwnorm : 2 ≤ ‖w‖ := hw.trans (Complex.abs_im_le_norm w)
have hne_all : ∀ x : ℝ, w + (x : ℂ) ≠ 0 := by
intro x h
apply him
have h2 : (w + (x : ℂ)).im = 0 := by rw [h]; simp
rw [Complex.add_im, Complex.ofReal_im, add_zero] at h2
exact h2
-- the derivative family of f y = (w + ↑y)⁻¹
have hder : ∀ x : ℝ, HasDerivAt (fun y : ℝ => (w + (y : ℂ))⁻¹) (-(((w + (x : ℂ)) ^ 2)⁻¹)) x := by
intro x
have hne := hne_all x
have h1 : HasDerivAt (fun z : ℂ => (w + z)⁻¹) (-(((w + (x : ℂ)) ^ 2)⁻¹)) (x : ℂ) := by
have h2 := (hasDerivAt_inv hne).comp (x : ℂ) ((hasDerivAt_id' (x : ℂ)).const_add w)
simpa [Function.comp_def] using h2
exact h1.comp_ofReal
have hderiv_eq : deriv (fun y : ℝ => (w + (y : ℂ))⁻¹)
= fun x : ℝ => -(((w + (x : ℂ)) ^ 2)⁻¹) := funext fun x => (hder x).deriv
have hcont : ContinuousOn (deriv (fun y : ℝ => (w + (y : ℂ))⁻¹)) (Set.uIcc 0 (n : ℝ)) := by
rw [hderiv_eq]
apply Continuous.continuousOn
apply Continuous.neg
apply Continuous.inv₀ _ (fun x => pow_ne_zero 2 (hne_all x))
exact (continuous_const.add Complex.continuous_ofReal).pow 2
-- Euler–Maclaurin
have hEM := sum_eq_integral_add_integral_deriv (f := fun y : ℝ => (w + (y : ℂ))⁻¹)
(a := 0) (b := (n : ℝ)) le_rfl (Nat.cast_nonneg _)
(fun t _ => (hder t).differentiableAt) hcont
rw [Nat.floor_zero, Nat.floor_natCast] at hEM
have hB10 : B1 0 = -1 / 2 := by
show (0 : ℝ) - ⌊(0 : ℝ)⌋₊ - 1 / 2 = -1 / 2
rw [Nat.floor_zero]
norm_num
have hB1n : B1 (n : ℝ) = -1 / 2 := by
show (n : ℝ) - ⌊(n : ℝ)⌋₊ - 1 / 2 = -1 / 2
rw [Nat.floor_natCast]
norm_num
rw [hB10, hB1n] at hEM
push_cast at hEM
simp only [add_zero] at hEM
have hIoc : Finset.Ioc 0 n = (Finset.range (n + 1)).erase 0 := by
ext x
simp only [Finset.mem_Ioc, Finset.mem_erase, Finset.mem_range]
omega
have hconv : ∑ k ∈ Finset.Ioc 0 n, (w + (k : ℂ))⁻¹
= ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ - w⁻¹ + (w + (n : ℂ))⁻¹ := by
rw [hIoc]
have h0mem : 0 ∈ Finset.range (n + 1) := Finset.mem_range.mpr (Nat.succ_pos n)
have h1 := Finset.add_sum_erase (Finset.range (n + 1)) (fun k => (w + (k : ℂ))⁻¹) h0mem
rw [Finset.sum_range_succ] at h1
simp only [Nat.cast_zero, add_zero] at h1
linear_combination h1
have hsum : ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹
= (∫ x in (0 : ℝ)..(n : ℝ), (w + (x : ℂ))⁻¹)
+ (w⁻¹ - (w + (n : ℂ))⁻¹) / 2
+ ∫ x in (0 : ℝ)..(n : ℝ),
deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ) := by
linear_combination hEM - hconv
-- the log FTC
have hanti : ∀ x ∈ Set.uIcc 0 (n : ℝ),
HasDerivAt (fun y : ℝ => Complex.log (w + (y : ℂ))) ((w + (x : ℂ))⁻¹) x := by
intro x _
have hne := hne_all x
have hslit : w + (x : ℂ) ∈ Complex.slitPlane := by
rw [Complex.mem_slitPlane_iff]
right
rw [Complex.add_im, Complex.ofReal_im, add_zero]
exact him
have h1 : HasDerivAt (fun z : ℂ => Complex.log (w + z)) ((w + (x : ℂ))⁻¹) (x : ℂ) := by
have h2 := (Complex.hasDerivAt_log hslit).comp (x : ℂ)
((hasDerivAt_id' (x : ℂ)).const_add w)
simpa [Function.comp_def] using h2
exact h1.comp_ofReal
have hconti : IntervalIntegrable (fun y : ℝ => (w + (y : ℂ))⁻¹) volume 0 (n : ℝ) := by
apply ContinuousOn.intervalIntegrable
apply Continuous.continuousOn
apply Continuous.inv₀ _ hne_all
exact continuous_const.add Complex.continuous_ofReal
have hint : ∫ x in (0 : ℝ)..(n : ℝ), (w + (x : ℂ))⁻¹ = Complex.log v - Complex.log w := by
rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti hconti]
simp [hv]
-- the arctan comparison integral
have hanti2 : ∀ x ∈ Set.uIcc 0 (n : ℝ),
HasDerivAt (fun y : ℝ => (1 / |w.im|) * Real.arctan ((y + w.re) / |w.im|))
(((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) x := by
intro x _
have h1 : HasDerivAt (fun y : ℝ => (y + w.re) / |w.im|) (1 / |w.im|) x :=
((hasDerivAt_id x).add_const w.re).div_const |w.im|
have h2 := h1.arctan
have h3 := h2.const_mul (1 / |w.im|)
refine h3.congr_deriv ?_
field_simp [hc0.ne']
ring
have hconti2 : IntervalIntegrable (fun x : ℝ => ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹)
volume 0 (n : ℝ) := by
apply ContinuousOn.intervalIntegrable
apply Continuous.continuousOn
apply Continuous.inv₀ _ (fun x => by
have h1 : (0 : ℝ) < (x + w.re) ^ 2 + |w.im| ^ 2 := by
nlinarith [sq_nonneg (x + w.re), hc0]
exact ne_of_gt h1)
exact (continuous_id.add continuous_const).pow 2 |>.add continuous_const
have harctan : ∫ x in (0 : ℝ)..(n : ℝ), ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹
≤ Real.pi / |w.im| := by
rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti2 hconti2]
have h1 : Real.arctan (((n : ℝ) + w.re) / |w.im|)
- Real.arctan ((0 + w.re) / |w.im|) ≤ Real.pi := by
have hu := Real.arctan_lt_pi_div_two (((n : ℝ) + w.re) / |w.im|)
have hv2 := Real.arctan_lt_pi_div_two (-((0 + w.re) / |w.im|))
rw [Real.arctan_neg] at hv2
linarith [Real.pi_pos, hv2]
calc (1 / |w.im|) * Real.arctan (((n : ℝ) + w.re) / |w.im|)
- (1 / |w.im|) * Real.arctan ((0 + w.re) / |w.im|)
= (1 / |w.im|) * (Real.arctan (((n : ℝ) + w.re) / |w.im|)
- Real.arctan ((0 + w.re) / |w.im|)) := by ring
_ ≤ (1 / |w.im|) * Real.pi :=
mul_le_mul_of_nonneg_left h1 (by positivity)
_ = Real.pi / |w.im| := by ring
-- the B̃₁ remainder bound
have hderiv_eq2 : ∀ x : ℝ, deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x
= -(((w + (x : ℂ)) ^ 2)⁻¹) := fun x => (hder x).deriv
have hn1 : ∀ x : ℝ, ‖-(((w + (x : ℂ)) ^ 2)⁻¹)‖ = ‖(w + (x : ℂ))⁻¹‖ ^ 2 := by
intro x
simp only [norm_neg, norm_inv, norm_pow, inv_pow]
have hnorm_eq : (fun x : ℝ => ‖deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖)
= fun x : ℝ => ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖ := by
funext x
rw [hderiv_eq2 x, norm_mul, Complex.norm_real, hn1 x]
have hnsq : ∀ x : ℝ, ‖w + (x : ℂ)‖ ^ 2 = (x + w.re) ^ 2 + |w.im| ^ 2 := by
intro x
rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]
have h1 : (w + (x : ℂ)).re = w.re + x := by simp [Complex.add_re, Complex.ofReal_re]
have h2 : (w + (x : ℂ)).im = w.im := by simp [Complex.add_im, Complex.ofReal_im]
rw [h1, h2]
rw [sq_abs]
ring
have hnsq_inv : ∀ x : ℝ, ‖(w + (x : ℂ))⁻¹‖ ^ 2 = ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹ := by
intro x
rw [norm_inv, inv_pow, hnsq x]
have hgnorm_cont : Continuous fun x : ℝ => ‖(w + (x : ℂ))⁻¹‖ ^ 2 :=
((Continuous.inv₀ (continuous_const.add Complex.continuous_ofReal) hne_all).norm).pow 2
have hB1int : IntervalIntegrable (fun x : ℝ => ‖B1 x‖) volume 0 (n : ℝ) := by
rw [intervalIntegrable_iff']
apply MeasureTheory.Measure.integrableOn_of_bounded (by simp)
aestronglyMeasurable_B1.norm (M := 1 / 2)
filter_upwards [self_mem_ae_restrict (by measurability)] with x hx
rw [Set.uIcc_of_le (Nat.cast_nonneg n), Set.mem_Icc] at hx
rw [Real.norm_of_nonneg (norm_nonneg _), Real.norm_eq_abs]
exact abs_B1_le_half hx.1
have hrem_integrable : IntervalIntegrable
(fun x : ℝ => ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖) volume 0 (n : ℝ) :=
hB1int.continuousOn_mul hgnorm_cont.continuousOn
have hmono : ∫ x in (0 : ℝ)..(n : ℝ), ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖
≤ ∫ x in (0 : ℝ)..(n : ℝ), (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) := by
refine intervalIntegral.integral_mono_on (Nat.cast_nonneg n) hrem_integrable
(hconti2.const_mul _) ?_
intro x hx
rw [Set.mem_Icc] at hx
show ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖ ≤ (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹)
rw [hnsq_inv x, Real.norm_eq_abs]
have hB : |B1 x| ≤ 1 / 2 := abs_B1_le_half hx.1
have hpos : (0 : ℝ) ≤ ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹ := inv_nonneg.mpr (by positivity)
calc (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) * |B1 x|
≤ (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) * (1 / 2) :=
mul_le_mul_of_nonneg_left hB hpos
_ = (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) := by ring
have hrem : ‖∫ x in (0 : ℝ)..(n : ℝ),
deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖
≤ (1 / 2) * (Real.pi / |w.im|) := by
refine (intervalIntegral.norm_integral_le_integral_norm (Nat.cast_nonneg n)).trans ?_
calc ∫ x in (0 : ℝ)..(n : ℝ), ‖deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖
= ∫ x in (0 : ℝ)..(n : ℝ), ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖ := by
rw [hnorm_eq]
_ ≤ ∫ x in (0 : ℝ)..(n : ℝ), (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) := hmono
_ = (1 / 2) * ∫ x in (0 : ℝ)..(n : ℝ), ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹ := by
rw [intervalIntegral.integral_const_mul]
_ ≤ (1 / 2) * (Real.pi / |w.im|) :=
mul_le_mul_of_nonneg_left harctan (by norm_num)
-- the boundary term
have hboundary : ‖(w⁻¹ - (w + (n : ℂ))⁻¹) / 2‖ ≤ 1 / 2 := by
have h1 : ‖w⁻¹‖ ≤ 1 / 2 := by
rw [norm_inv, show (1 / 2 : ℝ) = (2 : ℝ)⁻¹ by norm_num]
exact (inv_le_inv₀ (by linarith [hwnorm] : (0 : ℝ) < ‖w‖)
(by norm_num : (0 : ℝ) < 2)).mpr hwnorm
have h2 : ‖(w + (n : ℂ))⁻¹‖ ≤ 1 / 2 := by
have hvn : (w : ℂ) + (n : ℂ) = v := hv.symm
rw [hvn, norm_inv, show (1 / 2 : ℝ) = (2 : ℝ)⁻¹ by norm_num]
exact (inv_le_inv₀ (by linarith [hvnorm] : (0 : ℝ) < ‖v‖)
(by norm_num : (0 : ℝ) < 2)).mpr hvnorm
have h2c : ‖((2 : ℂ))‖ = 2 := by
rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by norm_num, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)]
have hsum12 : ‖w⁻¹ - (w + (n : ℂ))⁻¹‖ ≤ 1 :=
(norm_sub_le _ _).trans (by linarith [h1, h2])
calc ‖(w⁻¹ - (w + (n : ℂ))⁻¹) / 2‖
= ‖w⁻¹ - (w + (n : ℂ))⁻¹‖ / 2 := by rw [norm_div, h2c]
_ ≤ 1 / 2 := by
rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)]
nlinarith [hsum12]
-- the middle piece: sum minus log-difference
have hmid : ‖(∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹)
- (Complex.log v - Complex.log w)‖
≤ 1 / 2 + (1 / 2) * (Real.pi / |w.im|) := by
have halg : (∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹) - (Complex.log v - Complex.log w)
= (w⁻¹ - (w + (n : ℂ))⁻¹) / 2
+ ∫ x in (0 : ℝ)..(n : ℝ), deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ) := by
rw [hsum, hint]
ring
rw [halg]
exact (norm_add_le _ _).trans (add_le_add hboundary hrem)
-- StirlingVert at v = w + n
have hv1 : ‖Complex.digamma v - Complex.log v‖ ≤ 1 := by
have hst := StirlingVert.digamma_stirling hvre (by rw [hvim]; linarith [hw])
have hnorm12 : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by
rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 2)]
have hsq : (4 : ℝ) ≤ v.im ^ 2 := by
rw [hvim]
calc (4 : ℝ) = 2 ^ 2 := by norm_num
_ ≤ |w.im| ^ 2 := pow_le_pow_left₀ (by norm_num) hw _
_ = w.im ^ 2 := by rw [sq_abs]
calc ‖Complex.digamma v - Complex.log v‖
= ‖(Complex.digamma v - Complex.log v + (1 / 2 : ℂ) / v) - (1 / 2 : ℂ) / v‖ := by
congr 1; ring
_ ≤ ‖Complex.digamma v - Complex.log v + (1 / 2 : ℂ) / v‖ + ‖(1 / 2 : ℂ) / v‖ :=
norm_sub_le _ _
_ ≤ 3 / v.im ^ 2 + 1 / 4 := by
apply add_le_add hst
rw [norm_div, hnorm12, div_le_iff₀ (by linarith [hvnorm] : (0 : ℝ) < ‖v‖)]
nlinarith [hvnorm]
_ ≤ 3 / 4 + 1 / 4 := by
apply add_le_add_left
rw [div_le_div_iff₀ (by linarith [hsq] : (0 : ℝ) < v.im ^ 2) (by norm_num)]
nlinarith [hsq]
_ ≤ 1 := by norm_num
-- final assembly
have hshift' : Complex.digamma v
= Complex.digamma w + ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ := by
rw [hv]
exact digamma_add_natCast him n
calc ‖Complex.digamma w - Complex.log w‖
= ‖(Complex.digamma v - Complex.log v)
- ((∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹)
- (Complex.log v - Complex.log w))‖ := by
congr 1
rw [hshift']
ring
_ ≤ ‖Complex.digamma v - Complex.log v‖
+ ‖(∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹)
- (Complex.log v - Complex.log w)‖ :=
norm_sub_le _ _
_ ≤ 1 + (1 / 2 + (1 / 2) * (Real.pi / |w.im|)) := add_le_add hv1 hmid
_ ≤ 3 := by
have hpc : Real.pi / |w.im| ≤ Real.pi / 2 :=
div_le_div_of_nonneg_left Real.pi_nonneg (by norm_num) hw
nlinarith [hpc, Real.pi_lt_d2.le]
/-! ## 7. The left-half loose R-bound (ii′-5d capstone) -/
/-- **The loose R-bound on the left half-strip** (ii′-5d, D-067 §3/§6): on
σ ∈ [−5/2, 1/2], |t| ≥ 10, the log-derivative of ζ minus its near-zero sum
is O((log|t|)²) — the FE-reflection of the ii′-5c disc bound. Deliberately
loose; only the ii′-5e identity passes tight constants to ii′-5f. -/
theorem logDeriv_riemannZeta_sub_nearZeros_le_left {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}
(hsim : s.im = t) (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 1 / 2)
(hs0 : riemannZeta s ≠ 0) :
‖logDeriv riemannZeta s - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖
≤ 200000 * (Real.log |t|) ^ 2 := by
have ht0 : (0 : ℝ) < |t| := lt_of_lt_of_le (by norm_num) ht
have htim : s.im ≠ 0 := by
rw [hsim]
intro h
rw [h, abs_zero] at ht
norm_num at ht
have hne0 : s ≠ 0 := fun h => by rw [h] at htim; simp at htim
have hne1 : s ≠ 1 := fun h => by rw [h] at htim; simp at htim
have hG : Complex.Gammaℝ s ≠ 0 := Gammaℝ_ne_zero_of_im_ne_zero' htim
have hd : DifferentiableAt ℂ Complex.Gammaℝ s := differentiableAt_Gammaℝ_of_im_ne_zero' htim
have h1sre : (1 - s).re = 1 - s.re := by simp [Complex.sub_re, Complex.one_re]
have h1s0 : (1 : ℂ) - s ≠ 0 := fun h => by
have := congrArg Complex.re h
simp [Complex.sub_re, Complex.one_re] at this
linarith [hσhi]
have h1s1 : (1 : ℂ) - s ≠ 1 := fun h => by
have := congrArg Complex.im h
simp [Complex.sub_im, Complex.one_im, hsim] at this
rw [this, abs_zero] at ht
norm_num at ht
have hG1 : Complex.Gammaℝ (1 - s) ≠ 0 :=
Complex.Gammaℝ_ne_zero_of_re_pos (by rw [h1sre]; linarith [hσhi])
have hζ1 : riemannZeta (1 - s) ≠ 0 :=
riemannZeta_one_sub_ne_zero hne0 hG hs0 h1s0 hG1
have htne : t ≠ 0 := by
intro h
rw [h, abs_zero] at ht
norm_num at ht
have hd1 : DifferentiableAt ℂ Complex.Gammaℝ (1 - s) :=
differentiableAt_Gammaℝ_of_im_ne_zero' (by
have h1 : (1 - s).im = -t := by simp [Complex.sub_im, Complex.one_im, hsim]
rw [h1]
exact neg_ne_zero.mpr htne)
-- the reflected ii′-5c bound
have h5c := logDeriv_riemannZeta_sub_nearZeros_le (t := -t) (by simpa using ht) (s := 1 - s)
(by simp [Complex.sub_im, Complex.one_im, hsim])
(by rw [h1sre]; linarith [hσhi])
(by rw [h1sre]; linarith [hσlo])
hζ1
rw [abs_neg] at h5c
-- the FE identity and the sum reflection
have hfe := logDeriv_zeta_fe hne0 hne1 hG hs0 hd h1s0 h1s1 hG1 hζ1 hd1
have hrefl := sum_nearZeros_neg_reflect t s
have hbr := gammaR_bracket_norm_le ht hsim hσlo hσhi
have hkey : logDeriv riemannZeta s - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)
= -(logDeriv riemannZeta (1 - s)
- ∑ ρ' ∈ nearZeros (-t), (zeroMult ρ' : ℂ) / (1 - s - ρ'))
- (logDeriv Complex.Gammaℝ (1 - s) + logDeriv Complex.Gammaℝ s) := by
rw [hfe, hrefl]
ring
rw [hkey]
refine (norm_sub_le _ _).trans ?_
rw [norm_neg]
refine (add_le_add h5c hbr).trans ?_
have hL := two_le_log_abs_t ht
nlinarith [sq_nonneg (Real.log |t|)]
end NguyenRH1
end