LiSideBounds.lean
1731 lines · 27 declarations · 0 sorries · updated 08-26-2026
Declarations
| Kind | Name | Line |
|---|---|---|
| theorem | Z2hat_mono | 35 |
| theorem | nearZerosSub_mult_sum_le | 53 |
| theorem | continuousAt_logDeriv_zeta | 78 |
| theorem | continuousOn_logDeriv_zeta | 87 |
| theorem | Jlag_norm_eq | 94 |
| theorem | zeta_ne_zero_left_vertical | 101 |
| theorem | zeta_ne_zero_horizontal | 129 |
| theorem | rectangleIntegral_Jlag_eq | 162 |
| theorem | VIntegral_norm | 173 |
| theorem | HIntegral_split | 180 |
| theorem | jlag_left_vertical_norm_even | 191 |
| theorem | Z2hat_nonneg | 208 |
| theorem | vIntegral_Jlag_left_norm_le | 222 |
| theorem | kFun_right_vertical_norm_le_exp_sqrt_add_third | 416 |
| theorem | vIntegral_Jlag_right_le_exp_third_IIMaj | 495 |
| theorem | integral_one_div_sqrt_sq_add_sq | 609 |
| theorem | arcsinh_right_endpoint_le | 661 |
| theorem | arcsinh_left_endpoint_le | 679 |
| theorem | per_zero_integral_le_two_log | 731 |
| theorem | hIntegral_Jlag_mid_norm_le | 767 |
| theorem | hIntegral_Jlag_mid_neg_norm_le | 1145 |
| theorem | hIntegral_Jlag_full_norm_le | 1183 |
| theorem | hIntegral_Jlag_full_neg_norm_le | 1272 |
| theorem | hIntegral_Jlag_full_two_sides | 1308 |
| theorem | C0hat_le_self | 1335 |
| theorem | pinch_horizontal | 1363 |
| theorem | sfBoundProp | 1452 |
Source
/-
LiSideBounds.lean — tier ii′-6-c: the four side bounds of the L0
assembly (D-071 §4.4 with the D-074 dog-leg horizontal and the F-E
I_I repair, D-074 §9).
§1 scaffolding: Z2hat_mono, the nearZerosSub mult-count bridge,
logDeriv continuity on the paths, the Jlag norm factorization, the
rectangle side decomposition, HIntegral/VIntegral norm machinery,
the left-vertical even symmetry, and the two zero-freeness lemmas
(left vertical by classification, horizontal by the wide pigeonhole).
§2 (6-c-ii) DONE: I_III — the left vertical σ = −5/2.
§3 (6-c-iii) DONE: I_I — the right vertical σ₁ = 2√n (F-E form: ≤ e^{1/3}·IIMaj).
§4 (6-c-iv) DONE: the mid-horizontal segment machine [−5/2, 3].
§5 (6-c-v) DONE: the full horizontal assembly (mid + DL-5 tails, both sides).
§6 (6-d) DONE: the fold — `sfBoundProp : SfBoundProp` (six perimeter hyps).
Perimeter used: ZeroCountProp2 (near-count bridge), MZeroProp (I_III
short piece), the 5f tight R-bound hypotheses hZC/hZC2/hNLZ.
-/
import Mathlib
import NguyenRH1.LiAssembly
import NguyenRH1.LiDogLeg
open Zeta23 Complex Filter Topology
open scoped Nat
noncomputable section
namespace NguyenRH1
/-! ## 1. Scaffolding -/
/-- Z₂ is monotone for t ≥ 1 (clone of `C0hat_mono`, LiGapCircles). -/
theorem Z2hat_mono {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) : Z2hat a ≤ Z2hat b := by
have hapos : (0 : ℝ) < a + 2 := by linarith
have h1 : Real.log (a + 2) ≤ Real.log (b + 2) := Real.log_le_log hapos (by linarith)
have hlog1 : (1 : ℝ) ≤ Real.log (a + 2) := by
rw [Real.le_log_iff_exp_le hapos]
have he := Real.exp_one_lt_d9.le
linarith
have h2 : Real.log (Real.log (a + 2)) ≤ Real.log (Real.log (b + 2)) :=
Real.log_le_log (by linarith) h1
unfold Z2hat
have h3 : (0 : ℝ) ≤ (0.886 : ℝ) := by norm_num
have h4 : (0 : ℝ) ≤ (0.6 : ℝ) := by norm_num
nlinarith [h1, h2, h3, h4]
/-- **The nearZerosSub mult-count bridge** (cloned from
`near_sum_refPoint_le`, LiTightR §5): the multiplicity-weighted count
of nearZerosSub t is ≤ Z₂(t) via the image/subset bridge and the
perimeter `ZeroCountProp2`. -/
theorem nearZerosSub_mult_sum_le (hZC2 : ZeroCountProp2) {t : ℝ} (ht : 10 ≤ t) :
∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ) ≤ Z2hat t := by
classical
have hbridge : ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ)
= ∑ ρ ∈ (nearZerosSub t).image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := by
rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]
have hsub : (nearZerosSub t).image (fun ρ => ρ.1)
⊆ (zeroAbsWindow_finite t).toFinset := by
intro ρ hρ
rw [Finset.mem_image] at hρ
obtain ⟨ρ', hρ'mem, hρ'eq⟩ := hρ
have hnear := mem_nearZerosSub.mp hρ'mem
rw [Set.Finite.mem_toFinset]
show IsNontrivialZero ρ ∧ |ρ.im - t| ≤ 1
rw [← hρ'eq]
exact ⟨ρ'.2, hnear.le⟩
calc ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ)
= ∑ ρ ∈ (nearZerosSub t).image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := hbridge
_ ≤ ∑ ρ ∈ (zeroAbsWindow_finite t).toFinset, (zeroMult ρ : ℝ) :=
Finset.sum_le_sum_of_subset_of_nonneg hsub (fun ρ _ _ => Nat.cast_nonneg _)
_ = (((zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ) := rfl
_ ≤ Z2hat t := hZC2 t ht
/-- logDeriv ζ is continuous at any point off the pole and off the
zero set (analyticity of ζ + the quotient). -/
theorem continuousAt_logDeriv_zeta {s : ℂ} (h1 : s ≠ 1) (hζ : riemannZeta s ≠ 0) :
ContinuousAt (logDeriv riemannZeta) s := by
have hA : AnalyticAt ℂ (fun z => deriv riemannZeta z / riemannZeta z) s :=
((analyticAt_riemannZeta h1).deriv).div (analyticAt_riemannZeta h1) hζ
have heq : logDeriv riemannZeta = fun z => deriv riemannZeta z / riemannZeta z := rfl
rw [heq]
exact hA.continuousAt
/-- logDeriv ζ is continuous on a set avoiding the pole and the zeros. -/
theorem continuousOn_logDeriv_zeta {S : Set ℂ} (h1 : ∀ s ∈ S, s ≠ 1)
(hζ : ∀ s ∈ S, riemannZeta s ≠ 0) :
ContinuousOn (logDeriv riemannZeta) S :=
fun s hs => (continuousAt_logDeriv_zeta (h1 s hs) (hζ s hs)).continuousWithinAt
/-- **The Jlag norm factorization**: Jlag = kFun · (−logDeriv ζ), so
the norm splits (logDeriv unfolds to deriv/ζ definitionally). -/
theorem Jlag_norm_eq (n : ℕ) (s : ℂ) :
‖Jlag n s‖ = ‖kFun n s‖ * ‖logDeriv riemannZeta s‖ := by
unfold Jlag logDeriv
rw [Pi.div_apply, norm_mul, norm_neg]
/-- **Zero-freeness on the left vertical** σ = −5/2 (classification:
nontrivial zeros have re ∈ (0,1), the others are 0 and −2n). -/
theorem zeta_ne_zero_left_vertical (t : ℝ) :
riemannZeta ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I) ≠ 0 := by
intro hζ
have hre : (((-5 / 2 : ℝ) : ℂ) + (t : ℝ) * Complex.I).re = -5 / 2 := by simp
have him : (((-5 / 2 : ℝ) : ℂ) + (t : ℝ) * Complex.I).im = t := by simp
rcases zeta_zero_classification hζ with hnt | h0 | hn2
· have h21 : (0 : ℝ) < -5 / 2 := hre ▸ hnt.2.1
norm_num at h21
· rw [h0] at hre
norm_num at hre
· obtain ⟨m, hm1, hs⟩ := hn2
have hre2 : ((-2 : ℂ) * (m : ℂ)).re = -2 * (m : ℝ) := by
simp [Complex.mul_re]
rw [hs] at hre
rw [hre2] at hre
have hm : (m : ℝ) = 5 / 4 := by linarith
have h12 : (1 : ℝ) ≤ (m : ℝ) := by exact_mod_cast hm1
have h2 : (m : ℝ) < 2 := by linarith
have hm2 : m = 1 := by
have : m < 2 := by exact_mod_cast h2
exact le_antisymm (Nat.lt_succ_iff.mp this) hm1
rw [hm2] at hm
norm_num at hm
/-- **Zero-freeness on the horizontal at height T** (T the wide
zero-avoiding ordinate): a zero on the path would be a nontrivial
zero with γ = T inside the clearance window — contradiction.
(The trivial zeros have im = 0 ≠ T.) -/
theorem zeta_ne_zero_horizontal {n : ℕ} {T : ℝ} {σ : ℝ}
(hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im →
ρ.im < Real.sqrt n + 2 → 1 / (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|)
(hn : 1 ≤ n) (hTn : Real.sqrt n ≤ T) (hTn1 : T ≤ Real.sqrt n + 1) :
riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 0 := by
intro hζ
have hre : (((σ : ℝ) : ℂ) + (T : ℝ) * Complex.I).re = σ := by simp
have him : (((σ : ℝ) : ℂ) + (T : ℝ) * Complex.I).im = T := by simp
have hT0 : (0 : ℝ) < T := by
have h1 : (1 : ℝ) ≤ Real.sqrt n := Real.one_le_sqrt.mpr (by exact_mod_cast hn)
linarith
rcases zeta_zero_classification hζ with hnt | h0 | hn2
· -- nontrivial with im = T: inside the clearance window
have hγ1 : Real.sqrt n - 1 < T := by linarith [Real.sqrt_nonneg (n : ℝ)]
have hγ2 : T < Real.sqrt n + 2 := by linarith
have hc := hTwide _ hnt (by rw [him]; exact hγ1) (by rw [him]; exact hγ2)
rw [him, sub_self, abs_zero] at hc
have hpos : (0 : ℝ) < 1 / (9 * C0hat (Real.sqrt n + 2)) := by
have h2 := two_le_C0hat (by linarith [Real.sqrt_nonneg (n : ℝ)] :
(1 : ℝ) ≤ Real.sqrt n + 2)
exact one_div_pos.mpr (by linarith)
linarith
· rw [h0] at him
simp at him
linarith
· obtain ⟨m, hm1, hs⟩ := hn2
have him2 : ((-2 : ℂ) * (m : ℂ)).im = 0 := by simp [Complex.mul_im]
rw [hs] at him
rw [him2] at him
linarith
/-- **The rectangle side decomposition** (Zeta23 def, at the variant-B
rectangle coordinates). -/
theorem rectangleIntegral_Jlag_eq (n : ℕ) (T : ℝ) :
RectangleIntegral (Jlag n) (rectZ T) (rectW n T) =
HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt n) (-T) -
HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt n) T +
VIntegral (Jlag n) (2 * Real.sqrt n) (-T) T -
VIntegral (Jlag n) (-5 / 2) (-T) T := by
unfold RectangleIntegral
rw [rectZ_re, rectZ_im, rectW_re, rectW_im]
/-- The norm of a VIntegral is the norm of the plain interval
integral (the I • factor has norm 1). -/
theorem VIntegral_norm {f : ℂ → ℂ} {x y₁ y₂ : ℝ} :
‖VIntegral f x y₁ y₂‖ = ‖∫ t in y₁..y₂, f ((x : ℝ) + (t : ℝ) * Complex.I)‖ := by
unfold VIntegral
rw [norm_smul, Complex.norm_I, one_mul]
/-- Splitting an HIntegral at an interior point (integrability
hypotheses). -/
theorem HIntegral_split {f : ℂ → ℂ} {a b c y : ℝ}
(h1 : IntervalIntegrable (fun σ => f ((σ : ℝ) + (y : ℝ) * Complex.I))
MeasureTheory.volume a b)
(h2 : IntervalIntegrable (fun σ => f ((σ : ℝ) + (y : ℝ) * Complex.I))
MeasureTheory.volume b c) :
HIntegral f a c y = HIntegral f a b y + HIntegral f b c y := by
unfold HIntegral
rw [intervalIntegral.integral_add_adjacent_intervals h1 h2]
/-- **The left-vertical even symmetry** (Jlag is conjugation-symmetric
and the left-vertical point at −t is the conjugate of the one at t). -/
theorem jlag_left_vertical_norm_even (n : ℕ) (t : ℝ) :
‖Jlag n ((-5 / 2 : ℝ) + (-t : ℝ) * Complex.I)‖ =
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ := by
have hconj : ((-5 / 2 : ℝ) : ℂ) + (-t : ℝ) * Complex.I =
(starRingEnd ℂ) (((-5 / 2 : ℝ) : ℂ) + (t : ℝ) * Complex.I) := by
rw [map_add, Complex.conj_ofReal, map_mul, Complex.conj_ofReal, Complex.conj_I]
rw [show ((-t : ℝ) : ℂ) = -((t : ℝ) : ℂ) by push_cast; ring]
ring
rw [hconj, Jlag_conj n (by
intro h
have hre : (((-5 / 2 : ℝ) : ℂ) + (t : ℝ) * Complex.I).re = -5 / 2 := by simp
rw [h] at hre
norm_num at hre), Complex.norm_conj]
/-! ## 2. 6-c-ii: I_III — the left vertical σ = −5/2 -/
/-- Z₂(t) ≥ 0 for t ≥ 1 (0.6·log(t+2) ≥ 0.6 and the loglog term ≥ 0). -/
theorem Z2hat_nonneg {t : ℝ} (ht : 1 ≤ t) : 0 ≤ Z2hat t := by
have ht2 : (0 : ℝ) < t + 2 := by linarith
have hlog1 : (1 : ℝ) ≤ Real.log (t + 2) := by
rw [Real.le_log_iff_exp_le ht2]
have he := Real.exp_one_lt_d9.le
linarith
have hlog2 : (0 : ℝ) ≤ Real.log (Real.log (t + 2)) := Real.log_nonneg hlog1
unfold Z2hat
linarith
/-- **6-c-ii (I_III, the left vertical σ = −5/2)**: the full-side bound.
Kernel ≤ 2 (`kFun_norm_le_two`); for |t| ≥ 10 the 5f tight R-bound capstone
+ the two-unit near count (≤ (2/5)·Z₂(t) since ‖s − ρ‖ ≥ 5/2), for |t| ≤ 10
the perimeter `MZeroProp`; the two tails are equal by the even symmetry. -/
theorem vIntegral_Jlag_left_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)
(hNLZ : NoLowZeros) (hMZ : MZeroProp) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}
(hTn : Real.sqrt n ≤ T) (_hTn1 : T ≤ Real.sqrt n + 1) :
‖VIntegral (Jlag n) (-5 / 2) (-T) T‖ ≤
4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352 := by
classical
-- T ≥ 10 from n ≥ 10⁵
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have h10T : (10 : ℝ) ≤ T := by
have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
linarith
have hT0 : (0 : ℝ) ≤ T := by linarith
have hTT : -T ≤ T := by linarith
-- the path continuity machinery (integrability of the norm integrand)
have hJcont : ∀ t : ℝ, ContinuousAt (Jlag n)
((-5 / 2 : ℝ) + (t : ℝ) * Complex.I) := by
intro t
have hs1 : ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I) ≠ 1 := by
intro h
have hre := congrArg Complex.re h
simp at hre
norm_num at hre
have hA := (kFun_differentiableAt (n := n) hs1).continuousAt
have hB := continuousAt_logDeriv_zeta hs1 (zeta_ne_zero_left_vertical t)
show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _
exact hA.mul hB.neg
have hpath : Continuous fun u : ℝ => ((-5 / 2 : ℝ) + (u : ℝ) * Complex.I) := by
fun_prop
have hcontJ : Continuous fun t : ℝ =>
Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I) := by
rw [continuous_iff_continuousAt]
intro t
have hf : ContinuousAt (fun u : ℝ => ((-5 / 2 : ℝ) + (u : ℝ) * Complex.I)) t :=
hpath.continuousAt
have hcomp : ContinuousAt
(Jlag n ∘ fun u : ℝ => ((-5 / 2 : ℝ) + (u : ℝ) * Complex.I)) t :=
ContinuousAt.comp (g := Jlag n)
(f := fun u : ℝ => ((-5 / 2 : ℝ) + (u : ℝ) * Complex.I)) (x := t)
(hJcont t) hf
exact hcomp
have hcontG : Continuous fun t : ℝ =>
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ :=
continuous_norm.comp hcontJ
have hI : ∀ a b : ℝ, IntervalIntegrable
(fun t : ℝ => ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖)
MeasureTheory.volume a b := fun a b => hcontG.intervalIntegrable a b
-- the cast bridge for the perimeter M₀ (whose point is the ℂ-numeral)
have hcast : ((-5 / 2 : ℂ)) = (((-5 / 2 : ℝ)) : ℂ) := by push_cast; ring
-- the middle piece |t| ≤ 10: the perimeter M₀ bound
have hmid : ∀ t : ℝ, t ∈ Set.Icc (-10 : ℝ) 10 →
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ ≤ 2 * 1.3352 := by
intro t ht
obtain ⟨ht1, ht2⟩ := ht
have habs : |t| ≤ 10 := abs_le.mpr ⟨ht1, ht2⟩
have hMZt : ‖logDeriv riemannZeta ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ ≤
1.3352 := by
have h := hMZ t habs
rwa [hcast] at h
have hre : ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I).re = -5 / 2 := by simp
have hk : ‖kFun n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ ≤ 2 :=
kFun_norm_le_two (by rw [hre]; norm_num)
rw [Jlag_norm_eq]
exact mul_le_mul hk hMZt (norm_nonneg _) (by norm_num)
-- the tails t ∈ [10, T]: the tight R-bound capstone + the near count
have htail : ∀ t : ℝ, t ∈ Set.Icc (10 : ℝ) T →
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ ≤
2 * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) := by
intro t ht
obtain ⟨ht10, htT⟩ := ht
set s := ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I) with hs_def
have hre : s.re = -5 / 2 := by rw [hs_def]; simp
have him : s.im = t := by rw [hs_def]; simp
have hk : ‖kFun n s‖ ≤ 2 := kFun_norm_le_two (by rw [hre]; norm_num)
have hRtight := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := t) (s := s)
hZC hZC2 hNLZ ht10 (le_of_eq hre.symm) (by rw [hre]; norm_num) him
(zeta_ne_zero_left_vertical t)
rw [abs_of_nonneg (by linarith : (0 : ℝ) ≤ t)] at hRtight
have hlogT : Real.log (t + 2) ≤ Real.log (T + 2) :=
Real.log_le_log (by linarith) (by linarith)
-- the near sum ≤ (2/5)·Z₂(t) (‖s − ρ‖ ≥ 5/2 from re s = −5/2)
have hnear : ‖∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)‖ ≤
(2 / 5) * Z2hat t := by
calc ‖∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)‖
≤ ∑ ρ ∈ nearZerosSub t, ‖(zeroMult ρ.1 : ℂ) / (s - ρ.1)‖ :=
norm_sum_le _ _
_ ≤ ∑ ρ ∈ nearZerosSub t, (2 / 5) * (zeroMult ρ.1 : ℝ) := by
apply Finset.sum_le_sum
intro ρ _
have hρre : (0 : ℝ) < ρ.1.re := ρ.2.2.1
have hrere : (s - ρ.1).re = -5 / 2 - ρ.1.re := by
simp [Complex.sub_re, hre]
have hnorm5 : (5 / 2 : ℝ) ≤ ‖s - ρ.1‖ := by
have h1 := abs_re_le_norm (s - ρ.1)
rw [hrere, abs_of_neg (by linarith)] at h1
linarith
have hnormpos : (0 : ℝ) < ‖s - ρ.1‖ := by linarith
have h2 : ‖(zeroMult ρ.1 : ℂ)‖ = (zeroMult ρ.1 : ℝ) := by
rw [show (zeroMult ρ.1 : ℂ) = ((zeroMult ρ.1 : ℝ) : ℂ) by
push_cast; ring, Complex.norm_real]
exact abs_of_nonneg (Nat.cast_nonneg _)
rw [norm_div, h2, div_le_iff₀ hnormpos]
nlinarith [hnorm5, Nat.cast_nonneg (α := ℝ) (zeroMult ρ.1)]
_ = (2 / 5) * ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ) := by
rw [← Finset.mul_sum]
_ ≤ (2 / 5) * Z2hat t :=
mul_le_mul_of_nonneg_left (nearZerosSub_mult_sum_le hZC2 ht10)
(by norm_num)
-- combine: ‖ζ′/ζ‖ ≤ near + tight R
have hlog : ‖logDeriv riemannZeta s‖ ≤
(2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48 := by
have h1 : ‖logDeriv riemannZeta s‖ ≤
‖∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)‖ +
‖logDeriv riemannZeta s -
∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)‖ :=
norm_le_insert' _ _
have hmono := Z2hat_mono (by linarith : (1 : ℝ) ≤ t) htT
have hnn : (0 : ℝ) ≤ Z2hat T := Z2hat_nonneg (by linarith : (1 : ℝ) ≤ T)
linarith [h1, hnear, hRtight, hlogT, hmono, hnn]
rw [Jlag_norm_eq]
exact mul_le_mul hk hlog (norm_nonneg _) (by norm_num)
-- the piecewise integral bounds
have hmidInt : ∫ t in (-10 : ℝ)..(10 : ℝ),
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ ≤
(10 - (-10)) * (2 * 1.3352) := by
have h := intervalIntegral.integral_mono_on (by norm_num : (-10 : ℝ) ≤ 10)
(hI _ _) intervalIntegrable_const (fun t ht => hmid t ht)
rwa [intervalIntegral.integral_const, smul_eq_mul] at h
have htailInt : ∫ t in (10 : ℝ)..T,
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ ≤
(T - 10) * (2 * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48)) := by
have h := intervalIntegral.integral_mono_on h10T (hI _ _)
intervalIntegrable_const (fun t ht => htail t ht)
rwa [intervalIntegral.integral_const, smul_eq_mul] at h
-- the even symmetry: the left piece equals the right tail
have hge : ∀ t : ℝ, ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ =
‖Jlag n ((-5 / 2 : ℝ) + (-t : ℝ) * Complex.I)‖ :=
fun t => (jlag_left_vertical_norm_even n t).symm
have hleft : ∫ t in (-T)..(-10 : ℝ),
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ =
∫ t in (10 : ℝ)..T,
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ := by
calc ∫ t in (-T)..(-10 : ℝ), ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖
= ∫ t in (-T)..(-10 : ℝ),
‖Jlag n ((-5 / 2 : ℝ) + (-t : ℝ) * Complex.I)‖ :=
intervalIntegral.integral_congr (fun t _ => hge t)
_ = ∫ t in -(-10 : ℝ)..-(-T),
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ :=
intervalIntegral.integral_comp_neg
(fun t : ℝ => ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖)
_ = ∫ t in (10 : ℝ)..T,
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ := by
rw [neg_neg, neg_neg]
-- assembly: the three-piece split via the adjacent-intervals lemmas
-- (calc steps are defeq-checked), the even-symmetry identification of
-- the two tails, then the piecewise bounds
have hnn : (0 : ℝ) ≤ Z2hat T := Z2hat_nonneg (by linarith)
have hlognn : (0 : ℝ) ≤ Real.log (T + 2) := Real.log_nonneg (by linarith)
calc ‖VIntegral (Jlag n) (-5 / 2) (-T) T‖
= ‖∫ t in (-T)..T, Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ :=
VIntegral_norm
_ ≤ ∫ t in (-T)..T, ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ :=
intervalIntegral.norm_integral_le_integral_norm hTT
_ = (∫ t in (-T)..(-10 : ℝ), ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖) +
(∫ t in (-10 : ℝ)..T, ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖) :=
(intervalIntegral.integral_add_adjacent_intervals (hI (-T) (-10))
(hI (-10) T)).symm
_ = (∫ t in (-T)..(-10 : ℝ), ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖) +
((∫ t in (-10 : ℝ)..(10 : ℝ),
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖) +
(∫ t in (10 : ℝ)..T,
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖)) := by
congr 1
exact (intervalIntegral.integral_add_adjacent_intervals (hI (-10) 10)
(hI 10 T)).symm
_ = (∫ t in (10 : ℝ)..T, ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖) +
((∫ t in (-10 : ℝ)..(10 : ℝ),
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖) +
(∫ t in (10 : ℝ)..T,
‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖)) := by
rw [hleft]
_ ≤ 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +
40 * 1.3352 := by
linarith [htailInt, hmidInt, hnn, hlognn]
/-! ## 3. 6-c-iii: I_I — the right vertical σ₁ = 2√n (F-E form) -/
/-- **The F-E kernel lemma** (D-074 §9): the uniform-in-t kernel bound at
the right vertical σ = 2√n — ‖kFun n (2√n+it)‖ ≤ e^{√n/2+1/3}+1 for n ≥ 4.
The honest charge: |w/(w−1)| = |1+1/(w−1)| ≤ 1 + 1/‖w−1‖ ≤ 1 + 1/(2√n−1)
(plain triangle + ‖w−1‖ ≥ re(w−1) = 2√n−1 — the worst case is t = 0,
repairing the off-by-one of the t² ≥ n / re ≥ 2√n+1 variants), then
(1+1/(2√n−1))ⁿ ≤ exp(n/(2√n−1)) ≤ exp(√n/2+1/3) ⟺ n ≥ 4. -/
theorem kFun_right_vertical_norm_le_exp_sqrt_add_third {n : ℕ} (hn : 4 ≤ n)
(t : ℝ) :
‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by
have hnR : (4 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have hsq2 : (2 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
have h21 : (0 : ℝ) < 2 * Real.sqrt (n : ℝ) - 1 := by nlinarith [hsq2]
have hsqn : Real.sqrt (n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt (by linarith)
-- w − 1 ≠ 0 and ‖w − 1‖ ≥ 2√n − 1
have hre : ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1).re =
2 * Real.sqrt (n : ℝ) - 1 := by
simp [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.mul_re,
Complex.I_re, Complex.I_im, Complex.one_re]
have hne : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1 ≠ 0 := by
intro h
have h0 : ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1).re = 0 := by
rw [h]; simp
rw [hre] at h0
nlinarith [h21]
have hnorm_w1 : 2 * Real.sqrt (n : ℝ) - 1 ≤
‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ := by
have h1 := abs_re_le_norm ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)
rw [hre, abs_of_nonneg h21.le] at h1
exact h1
-- the base bound ‖1 + 1/(w−1)‖ ≤ 1 + 1/(2√n−1)
have hinv : 1 / ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ ≤
1 / (2 * Real.sqrt (n : ℝ) - 1) :=
one_div_le_one_div_of_le h21 hnorm_w1
have hbase : ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ≤
1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by
calc ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖
≤ ‖(1 : ℂ)‖ + ‖1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ :=
norm_add_le _ _
_ = 1 + 1 / ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ := by
rw [norm_one, norm_div, norm_one]
_ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by linarith [hinv]
have hbasepos : (0 : ℝ) ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by positivity
-- the power + exp chain: (1+1/(2√n−1))ⁿ ≤ exp(n/(2√n−1)) ≤ exp(√n/2+1/3)
have hexp : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1)) ≤
Real.sqrt (n : ℝ) / 2 + 1 / 3 := by
rw [mul_one_div, div_le_iff₀ h21,
show (Real.sqrt (n : ℝ) / 2 + 1 / 3) * (2 * Real.sqrt (n : ℝ) - 1) =
Real.sqrt (n : ℝ) ^ 2 + Real.sqrt (n : ℝ) / 6 - 1 / 3 by ring, hsqn]
linarith [hsq2]
have h1le : 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) ≤
Real.exp (1 / (2 * Real.sqrt (n : ℝ) - 1)) := by
linarith [Real.add_one_le_exp (1 / (2 * Real.sqrt (n : ℝ) - 1))]
have hpow : (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n ≤
Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) := by
calc (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n
≤ (Real.exp (1 / (2 * Real.sqrt (n : ℝ) - 1))) ^ n :=
pow_le_pow_left₀ hbasepos h1le n
_ = Real.exp ((n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1))) :=
(Real.exp_nat_mul _ n).symm
_ ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) := Real.exp_le_exp.mpr hexp
have hpow1 : ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ^ n ≤
(1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n :=
pow_le_pow_left₀ (norm_nonneg _) hbase n
have hwid : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) /
((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) =
1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) := by
field_simp [hne]
ring
unfold kFun
rw [hwid]
calc ‖(1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)) ^ n - 1‖
≤ ‖(1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)) ^ n‖ +
‖(1 : ℂ)‖ := norm_sub_le _ _
_ = ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ^ n + 1 := by
rw [norm_pow, norm_one]
_ ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by
linarith [hpow1.trans hpow]
/-- **6-c-iii (I_I, the right vertical σ₁ = 2√n, F-E form)**: the full-side
bound ‖V‖ ≤ e^{1/3}·IIMaj(n). The F-E kernel (uniform in t) + the DL-6
direct Dirichlet bound ‖ζ′/ζ‖ ≤ 0.57·2^{−(2√n−2)}; the comparison
e^{√n/2+1/3}+1 ≤ e^{1/3}(e^{√n/2}+1) holds since 1 ≤ e^{1/3}. -/
theorem vIntegral_Jlag_right_le_exp_third_IIMaj {n : ℕ} (hn : 100000 ≤ n)
{T : ℝ} (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖ ≤
Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := by
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have hn4 : 4 ≤ n := by omega
have hn5 : 5 ≤ n := by omega
have hsq2 : (2 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
have hT0 : (0 : ℝ) ≤ T := by
have h := Real.sqrt_nonneg (n : ℝ)
linarith
have hTT : -T ≤ T := by linarith
-- zero-freeness + continuity on the right vertical (re = 2√n > 1)
have hzne : ∀ t : ℝ,
riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) ≠ 0 := by
intro t
have hre : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I).re =
2 * Real.sqrt (n : ℝ) := by
simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im]
have h1 : (1 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by nlinarith [hsq2]
exact riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)
have hJcont : ∀ t : ℝ, ContinuousAt (Jlag n)
(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by
intro t
have hs1 : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) ≠ 1 := by
intro h
have hre := congrArg Complex.re h
simp at hre
nlinarith [hsq2]
have hA := (kFun_differentiableAt (n := n) hs1).continuousAt
have hB := continuousAt_logDeriv_zeta hs1 (hzne t)
show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _
exact hA.mul hB.neg
have hpath : Continuous fun u : ℝ =>
(((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I) := by fun_prop
have hcontJ : Continuous fun t : ℝ =>
Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by
rw [continuous_iff_continuousAt]
intro t
have hf : ContinuousAt (fun u : ℝ =>
(((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) t := hpath.continuousAt
have hcomp : ContinuousAt
(Jlag n ∘ fun u : ℝ => (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) t :=
ContinuousAt.comp (g := Jlag n)
(f := fun u : ℝ => (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) (x := t)
(hJcont t) hf
exact hcomp
have hcontG : Continuous fun t : ℝ =>
‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=
continuous_norm.comp hcontJ
have hI2 : IntervalIntegrable
(fun t : ℝ => ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖)
MeasureTheory.volume (-T) T := hcontG.intervalIntegrable _ _
-- the comparison e^{√n/2+1/3}+1 ≤ e^{1/3}(e^{√n/2}+1) (since 1 ≤ e^{1/3})
have hKle : Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 ≤
Real.exp (1 / 3 : ℝ) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) := by
rw [Real.exp_add]
have h1 : (1 : ℝ) ≤ Real.exp (1 / 3 : ℝ) := by
have h := Real.add_one_le_exp (1 / 3 : ℝ)
linarith
have hE := Real.exp_pos (Real.sqrt (n : ℝ) / 2)
nlinarith [h1, hE]
-- the pointwise bound
have hK' : (0 : ℝ) ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by positivity
have hL : (0 : ℝ) ≤ (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by
positivity
have hpt : ∀ t : ℝ, t ∈ Set.Icc (-T) T →
‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
(Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by
intro t _
rw [Jlag_norm_eq]
exact mul_le_mul (kFun_right_vertical_norm_le_exp_sqrt_add_third hn4 t)
(norm_logDeriv_zeta_le_iimZeta hn5) (norm_nonneg _) hK'
have hInt : ∫ t in (-T)..T,
‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
(T - -T) * ((Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by
have h := intervalIntegral.integral_mono_on hTT hI2 intervalIntegrable_const
(fun t ht => hpt t ht)
rwa [intervalIntegral.integral_const, smul_eq_mul] at h
-- the final comparison 2T·K·L ≤ e^{1/3}·IIMaj (T ≤ √n+1, hKle)
have hKL : (0 : ℝ) ≤ (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) :=
mul_nonneg hK' hL
have hnL : (0 : ℝ) ≤ 2 * (Real.sqrt (n : ℝ) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by
have h1 : (0 : ℝ) ≤ Real.sqrt (n : ℝ) + 1 := by positivity
exact mul_nonneg (mul_nonneg (by norm_num) h1) hL
have hfinal : 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) ≤
Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := by
unfold IIMaj
nlinarith [hTn1, hKle, hKL, hnL, Real.exp_pos (1 / 3 : ℝ),
Real.exp_pos (Real.sqrt (n : ℝ) / 2)]
calc ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖
= ‖∫ t in (-T)..T, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=
VIntegral_norm
_ ≤ ∫ t in (-T)..T, ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=
intervalIntegral.norm_integral_le_integral_norm hTT
_ ≤ (T - -T) * ((Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := hInt
_ = 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring
_ ≤ Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := hfinal
/-! ## 4. 6-c-iv: the mid-horizontal segment machine [−5/2, 3] -/
/-- **The arcsinh FTC machine** (6-c-iv core): the direct antiderivative
F(σ) = log((σ−β) + √((σ−β)²+δ²)) of 1/√((σ−β)²+δ²) (Real.arcsinh does
not exist here): g(σ) := (σ−β)+√((σ−β)²+δ²) > 0 (√h > |σ−β|), and
g′ = 1 + (σ−β)/√h = g/√h, so (log g)′ = 1/√h exactly. -/
theorem integral_one_div_sqrt_sq_add_sq (β δ : ℝ) (hδ : 0 < δ) (a b : ℝ) :
∫ σ in a..b, 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) =
Real.log ((b - β) + Real.sqrt ((b - β) ^ 2 + δ ^ 2)) -
Real.log ((a - β) + Real.sqrt ((a - β) ^ 2 + δ ^ 2)) := by
have hh : ∀ σ : ℝ, (0 : ℝ) < (σ - β) ^ 2 + δ ^ 2 := fun σ =>
add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2)
have hgpos : ∀ σ : ℝ, (0 : ℝ) < (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by
intro σ
have h1 : |(σ - β)| < Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by
have h2 : (σ - β) ^ 2 < (σ - β) ^ 2 + δ ^ 2 := by nlinarith [hδ]
have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2
rwa [Real.sqrt_sq_eq_abs] at h3
have h4 : -(σ - β) ≤ |(σ - β)| := neg_le_abs (σ - β)
linarith [h1, h4]
have hderiv : ∀ σ : ℝ, HasDerivAt
(fun σ => Real.log ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)))
(1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by
intro σ
have hhσ := hh σ
have hsqrt0 : Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hhσ)
have hg0 : ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) ≠ 0 := (hgpos σ).ne'
have h1 : HasDerivAt (fun σ => σ - β) 1 σ := (hasDerivAt_id σ).sub_const β
have h2 : HasDerivAt (fun σ => (σ - β) ^ 2 + δ ^ 2) (2 * (σ - β)) σ := by
have h2a := ((hasDerivAt_id σ).sub_const β).pow 2
have h2b := h2a.add_const (δ ^ 2)
simpa using h2b
have h4 : HasDerivAt (fun σ => Real.sqrt ((σ - β) ^ 2 + δ ^ 2))
(2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=
h2.sqrt hhσ.ne'
have h5 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))
(1 + 2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=
h1.add h4
have h6 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))
(((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) /
Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by
convert h5 using 1
field_simp [hsqrt0]
ring
have h7 := h6.log hg0
convert h7 using 1
field_simp [hsqrt0, hg0]
exact intervalIntegral.integral_eq_sub_of_hasDerivAt (fun σ _ => hderiv σ)
(by
apply Continuous.intervalIntegrable
apply Continuous.div continuous_const
· exact Real.continuous_sqrt.comp (by fun_prop :
Continuous fun σ : ℝ => (σ - β) ^ 2 + δ ^ 2)
· intro σ
exact ne_of_gt (Real.sqrt_pos.mpr (hh σ)))
/-- **The right endpoint estimate** F(3) ≤ log(6+δ): √((3−β)²+δ²) ≤
(3−β)+δ for 3−β > 0, so the argument is ≤ 2(3−β)+δ ≤ 6+δ (0 ≤ β). -/
theorem arcsinh_right_endpoint_le {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
(hδ : 0 < δ) :
Real.log ((3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2)) ≤ Real.log (6 + δ) := by
have hx : (0 : ℝ) < 3 - β := by linarith
have hsqrt_le : Real.sqrt ((3 - β) ^ 2 + δ ^ 2) ≤ (3 - β) + δ := by
rw [Real.sqrt_le_iff]
exact ⟨by positivity, by nlinarith [hδ, hx]⟩
have h1 : (0 : ℝ) < (3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2) := by
have h2 := Real.sqrt_nonneg ((3 - β) ^ 2 + δ ^ 2)
nlinarith
have h3 : (3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2) ≤ 6 + δ := by
nlinarith [hsqrt_le, hβ0]
exact Real.log_le_log h1 h3
/-- **The left endpoint estimate** −F(−5/2) ≤ log(7+δ) + 2·log(1/δ):
with u := 5/2+β ∈ (5/2, 7/2), the argument −u+√(u²+δ²) rationalizes to
δ²/(u+√(u²+δ²)) ≥ δ²/(7+δ) > 0, so F(−5/2) ≥ log(δ²/(7+δ)) =
2·log δ − log(7+δ). -/
theorem arcsinh_left_endpoint_le {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
(hδ : 0 < δ) :
-Real.log ((-5 / 2 - β) + Real.sqrt ((-5 / 2 - β) ^ 2 + δ ^ 2)) ≤
Real.log (7 + δ) + 2 * Real.log (1 / δ) := by
have hu : (0 : ℝ) < 5 / 2 + β := by linarith
have hsq : (-5 / 2 - β) ^ 2 = (5 / 2 + β) ^ 2 := by ring
have hneg : (-5 / 2 : ℝ) - β = -(5 / 2 + β) := by ring
rw [hsq, hneg]
set u := 5 / 2 + β with hu_def
have hu2 : u < 7 / 2 := by rw [hu_def]; linarith
have hsqrt_pos : (0 : ℝ) < Real.sqrt (u ^ 2 + δ ^ 2) :=
Real.sqrt_pos.mpr (add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2))
have hg_pos : (0 : ℝ) < -u + Real.sqrt (u ^ 2 + δ ^ 2) := by
have h1 : u < Real.sqrt (u ^ 2 + δ ^ 2) := by
have h2 : u ^ 2 < u ^ 2 + δ ^ 2 := by nlinarith [hδ]
have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2
rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3
linarith
-- the rationalization: −u + √ = δ²/(u + √)
have hrid : -u + Real.sqrt (u ^ 2 + δ ^ 2) =
δ ^ 2 / (u + Real.sqrt (u ^ 2 + δ ^ 2)) := by
rw [eq_div_iff (ne_of_gt (by linarith [hsqrt_pos] :
(0 : ℝ) < u + Real.sqrt (u ^ 2 + δ ^ 2)))]
have hs : (Real.sqrt (u ^ 2 + δ ^ 2)) ^ 2 = u ^ 2 + δ ^ 2 :=
Real.sq_sqrt (by positivity)
nlinarith [hs]
-- the denominator ≤ 7 + δ
have hden : u + Real.sqrt (u ^ 2 + δ ^ 2) ≤ 7 + δ := by
have h1 : Real.sqrt (u ^ 2 + δ ^ 2) ≤ u + δ := by
rw [Real.sqrt_le_iff]
exact ⟨by linarith [hδ, hu.le], by nlinarith [hδ, hu]⟩
nlinarith [h1, hu2]
-- δ²/(7+δ) ≤ δ²/(u+√) = −u+√
have hge : δ ^ 2 / (7 + δ) ≤ -u + Real.sqrt (u ^ 2 + δ ^ 2) := by
rw [hrid]
have h2 : (0 : ℝ) < u + Real.sqrt (u ^ 2 + δ ^ 2) := by linarith [hsqrt_pos]
exact div_le_div_of_nonneg_left (sq_nonneg _) h2 hden
-- log mono + algebra: F(−5/2) ≥ log(δ²/(7+δ)) = 2·log δ − log(7+δ)
have hlog : Real.log (δ ^ 2 / (7 + δ)) ≤ Real.log (-u + Real.sqrt (u ^ 2 + δ ^ 2)) :=
Real.log_le_log (by positivity) hge
have hlogid : Real.log (δ ^ 2 / (7 + δ)) = 2 * Real.log δ - Real.log (7 + δ) := by
rw [Real.log_div (pow_pos hδ 2).ne' (by linarith [hδ] : (7 : ℝ) + δ ≠ 0),
Real.log_pow]
ring
have hlog1 : Real.log (1 / δ) = -Real.log δ := by
rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]
rw [hlogid] at hlog
linarith [hlog, hlog1]
/-- **The per-zero segment integral bound**: ∫_{−5/2}^{3} dσ/√((σ−β)²+δ²)
≤ 2·log(16.5/δ) for 0 < β < 1, 0 < δ ≤ 1 — the two endpoint estimates +
log((6+δ)(7+δ)) ≤ log(16.5²) since (6+δ)(7+δ) ≤ 56 ≤ 272.25. -/
theorem per_zero_integral_le_two_log {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
(hδ : 0 < δ) (hδ1 : δ ≤ 1) :
∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤
2 * Real.log (16.5 / δ) := by
have hftc := integral_one_div_sqrt_sq_add_sq β δ hδ (-5 / 2) 3
have hr := arcsinh_right_endpoint_le hβ0 hβ1 hδ
have hl := arcsinh_left_endpoint_le hβ0 hβ1 hδ
have h1 : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤
Real.log (6 + δ) + Real.log (7 + δ) + 2 * Real.log (1 / δ) := by
rw [hftc]
linarith [hr, hl]
-- the log-mono simplification: log(6+δ) + log(7+δ) ≤ 2·log 16.5
have h2 : Real.log (6 + δ) + Real.log (7 + δ) ≤ 2 * Real.log 16.5 := by
have h3 : Real.log (6 + δ) + Real.log (7 + δ) = Real.log ((6 + δ) * (7 + δ)) :=
(Real.log_mul (by linarith [hδ] : (6 : ℝ) + δ ≠ 0)
(by linarith [hδ] : (7 : ℝ) + δ ≠ 0)).symm
have h4 : Real.log ((6 + δ) * (7 + δ)) ≤ Real.log (16.5 * 16.5) :=
Real.log_le_log (by positivity) (by nlinarith [hδ, hδ1])
have h5 : Real.log (16.5 * 16.5) = 2 * Real.log 16.5 := by
rw [show (16.5 : ℝ) * 16.5 = 16.5 ^ 2 by ring, Real.log_pow]
ring
linarith [h3, h4, h5]
have h6 : 2 * Real.log (16.5 / δ) = 2 * Real.log 16.5 + 2 * Real.log (1 / δ) := by
have h7 : Real.log (1 / δ) = -Real.log δ := by
rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]
rw [Real.log_div (by norm_num) (ne_of_gt hδ), h7]
ring
rw [h6]
linarith [h1, h2]
/-- **6-c-iv (mid-horizontal [−5/2, 3] at height +T)**: the segment bound
‖H‖ ≤ (e⁴+1)·(2·Z₂(T)·log(148.5·Ĉ₀(√n+2)) + 5.5·(10.5·log(T+2)+48)).
Kernel e⁴+1 (the ii′-4 shift lemma at s := w−1); logDeriv split by
norm_le_insert' into the near sum (per-zero arcsinh-FTC machine +
integral_finsetSum + the two-unit count ≤ Z₂(T)) and the tight R-bound
(capstone, constant in σ). -/
theorem hIntegral_Jlag_mid_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)
(hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}
(hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →
ρ.im < Real.sqrt (n : ℝ) + 2 →
1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)
(hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖HIntegral (Jlag n) (-5 / 2) 3 T‖ ≤
(Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by
classical
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have h10T : (10 : ℝ) ≤ T := by
have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
linarith
have hT0 : (0 : ℝ) ≤ T := by linarith
have hn1 : 1 ≤ n := by omega
have hlen : (-5 / 2 : ℝ) ≤ 3 := by norm_num
have hC0 : (0 : ℝ) < C0hat (Real.sqrt (n : ℝ) + 2) := by
have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : ℝ)] :
(1 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)
linarith
have hB0nn : (0 : ℝ) ≤ 2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by
have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : ℝ)] :
(1 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)
have h1 : (1 : ℝ) ≤ 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) := by nlinarith [h2]
have h3 := Real.log_nonneg h1
linarith
-- zero-freeness on the horizontal + the path continuity machines
have hzne : ∀ σ : ℝ, riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 0 :=
fun σ => zeta_ne_zero_horizontal hTwide hn1 hTn hTn1
have hne1 : ∀ σ : ℝ, ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by
intro σ h
have him := congrArg Complex.im h
simp at him
linarith [h10T]
have hpath : Continuous fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I) := by
fun_prop
have hLDc : Continuous fun σ : ℝ =>
logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) := by
rw [continuous_iff_continuousAt]
intro σ
have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=
hpath.continuousAt
exact ContinuousAt.comp (g := logDeriv riemannZeta)
(f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ)
(continuousAt_logDeriv_zeta (hne1 σ) (hzne σ)) hf
have hJcont : ∀ σ : ℝ, ContinuousAt (Jlag n) ((σ : ℝ) + (T : ℝ) * Complex.I) := by
intro σ
have hA := (kFun_differentiableAt (n := n) (hne1 σ)).continuousAt
have hB := continuousAt_logDeriv_zeta (hne1 σ) (hzne σ)
show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _
exact hA.mul hB.neg
have hcontJ : Continuous fun σ : ℝ =>
Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I) := by
rw [continuous_iff_continuousAt]
intro σ
have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=
hpath.continuousAt
exact ContinuousAt.comp (g := Jlag n)
(f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ) (hJcont σ) hf
have hcontG : Continuous fun σ : ℝ =>
‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := continuous_norm.comp hcontJ
have hJintbl : IntervalIntegrable
(fun σ : ℝ => ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖)
MeasureTheory.volume (-5 / 2) 3 := hcontG.intervalIntegrable _ _
have hLDcont : Continuous fun σ : ℝ =>
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=
continuous_norm.comp hLDc
have hLDintbl : IntervalIntegrable
(fun σ : ℝ => ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖)
MeasureTheory.volume (-5 / 2) 3 := hLDcont.intervalIntegrable _ _
have hKLcont : Continuous fun σ : ℝ =>
(Real.exp 4 + 1) * ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=
continuous_const.mul hLDcont
have hKLintbl : IntervalIntegrable
(fun σ : ℝ => (Real.exp 4 + 1) *
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖)
MeasureTheory.volume (-5 / 2) 3 := hKLcont.intervalIntegrable _ _
-- the near-sum denominator never vanishes on the path (else s = ρ is a
-- zero, contra zeta_ne_zero_horizontal)
have hden : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →
∀ σ : ℝ, ((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1 ≠ 0 := by
intro ρ _ σ h0
have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h0
have hz := hzne σ
rw [hs] at hz
exact hz ρ.2.1
have hScont : Continuous fun σ : ℝ =>
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1) := by
have hterm : ∀ ρ ∈ nearZerosSub T, Continuous fun σ : ℝ =>
(zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1) := by
intro ρ hρ
show Continuous ((fun _ : ℝ => (zeroMult ρ.1 : ℂ)) /
(fun σ : ℝ => ((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1))
exact Continuous.div continuous_const (hpath.sub continuous_const) (hden ρ hρ)
exact continuous_finsetSum _ hterm
have hSnorm_cont : Continuous fun σ : ℝ =>
‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=
continuous_norm.comp hScont
have hSnorm_int : IntervalIntegrable
(fun σ : ℝ => ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)
MeasureTheory.volume (-5 / 2) 3 := hSnorm_cont.intervalIntegrable _ _
have hRcont : Continuous fun σ : ℝ =>
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=
continuous_norm.comp (hLDc.sub hScont)
have hRnorm_int : IntervalIntegrable
(fun σ : ℝ => ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)
MeasureTheory.volume (-5 / 2) 3 := hRcont.intervalIntegrable _ _
-- the per-ρ data (δ_ρ := |γ−T| ∈ [c_clear, 1))
have hρdata : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →
(0 : ℝ) < |ρ.1.im - T| ∧ |ρ.1.im - T| < 1 ∧
(1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2))) ≤ |ρ.1.im - T| := by
intro ρ hρ
have hδ1 := mem_nearZerosSub.mp hρ
obtain ⟨hlo, hhi⟩ := abs_lt.mp hδ1
have hγ1 : Real.sqrt (n : ℝ) - 1 < ρ.1.im := by nlinarith [hTn]
have hγ2 : ρ.1.im < Real.sqrt (n : ℝ) + 2 := by nlinarith [hTn1]
have hδge := hTwide ρ.1 ρ.2 hγ1 hγ2
have hδpos : (0 : ℝ) < |ρ.1.im - T| :=
lt_of_lt_of_le (one_div_pos.mpr (by positivity :
(0 : ℝ) < 9 * C0hat (Real.sqrt (n : ℝ) + 2))) hδge
exact ⟨hδpos, hδ1, hδge⟩
-- the kernel bound per σ (the ii′-4 shift lemma at s := w − 1)
have hnT2 : (n : ℝ) ≤ T ^ 2 := by
have h1 : (Real.sqrt (n : ℝ)) ^ 2 ≤ T ^ 2 :=
pow_le_pow_left₀ (Real.sqrt_nonneg _) hTn 2
rwa [Real.sq_sqrt (by positivity : (0 : ℝ) ≤ (n : ℝ))] at h1
have hker : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →
‖kFun n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤ Real.exp 4 + 1 := by
intro σ hσ
obtain ⟨hσ1, hσ2⟩ := hσ
have hre : (((σ : ℝ) + (T : ℝ) * Complex.I) - 1).re = σ - 1 := by simp
have him : (((σ : ℝ) + (T : ℝ) * Complex.I) - 1).im = T := by simp
have h1 := kFun_shift_norm_le_exp_four_add_one (n := n)
(s := (((σ : ℝ) + (T : ℝ) * Complex.I) - 1))
(by rw [hre]; linarith [hσ2]) (by rw [him]; exact hnT2)
rwa [sub_add_cancel] at h1
-- pointwise Jlag ≤ (e⁴+1)·‖logDeriv‖
have hptJ : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →
‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤
(Real.exp 4 + 1) * ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := by
intro σ hσ
rw [Jlag_norm_eq]
exact mul_le_mul (hker σ hσ) le_rfl (norm_nonneg _) (by positivity)
have hJint : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤
(Real.exp 4 + 1) * ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := by
have h := intervalIntegral.integral_mono_on hlen hJintbl hKLintbl
(fun σ hσ => hptJ σ hσ)
rwa [intervalIntegral.integral_const_mul] at h
-- the logDeriv split: ‖logDeriv‖ ≤ ‖Σ‖ + ‖logDeriv − Σ‖
have hsumcont : Continuous fun σ : ℝ =>
‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=
hSnorm_cont.add hRcont
have hsum_intbl : IntervalIntegrable
(fun σ : ℝ => ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)
MeasureTheory.volume (-5 / 2) 3 := hsumcont.intervalIntegrable _ _
have hsplit : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤
(∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) +
(∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) := by
have hpt2 : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤
‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=
fun σ _ => norm_le_insert' _ _
have h := intervalIntegral.integral_mono_on hlen hLDintbl hsum_intbl
(fun σ hσ => hpt2 σ hσ)
rwa [intervalIntegral.integral_add hSnorm_int hRnorm_int] at h
-- the R-part integral (the 5f capstone, constant in σ)
have hR : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤
10.5 * Real.log (T + 2) + 48 := by
intro σ hσ
obtain ⟨hσ1, hσ2⟩ := hσ
have hre : ((σ : ℝ) + (T : ℝ) * Complex.I).re = σ := by simp
have him : ((σ : ℝ) + (T : ℝ) * Complex.I).im = T := by simp
have h := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := T)
(s := ((σ : ℝ) + (T : ℝ) * Complex.I)) hZC hZC2 hNLZ h10T
(by rw [hre]; exact hσ1) (by rw [hre]; exact hσ2) him (hzne σ)
rwa [abs_of_nonneg hT0] at h
have hRint : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) := by
have h := intervalIntegral.integral_mono_on hlen hRnorm_int intervalIntegrable_const
(fun σ hσ => hR σ hσ)
rwa [intervalIntegral.integral_const, smul_eq_mul] at h
-- the near-sum integral: the per-zero arcsinh-FTC machine + the swap
have hnormid : ∀ σ : ℝ, ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ},
‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1‖ =
Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2) := by
intro σ ρ
have h1 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1) =
(σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by
simp [Complex.normSq_apply]
ring
symm
rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _),
← Complex.normSq_eq_norm_sq]
exact h1.symm
have htermcont : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →
Continuous fun σ : ℝ => (zeroMult ρ.1 : ℝ) *
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by
intro ρ hρ
obtain ⟨hδpos, -, -⟩ := hρdata ρ hρ
have hh : ∀ σ : ℝ, (0 : ℝ) < (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by
intro σ
have h3 : ρ.1.im - T ≠ 0 := abs_pos.mp hδpos
have h4 : T - ρ.1.im ≠ 0 := by
intro h5
apply h3
linarith [h5]
exact add_pos_of_nonneg_of_pos (sq_nonneg _) (sq_pos_of_ne_zero h4)
have hsqrtc : Continuous fun σ : ℝ =>
Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2) :=
Real.continuous_sqrt.comp (by fun_prop :
Continuous fun σ : ℝ => (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)
have hsqrt0 : ∀ σ : ℝ,
Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2) ≠ 0 :=
fun σ => ne_of_gt (Real.sqrt_pos.mpr (hh σ))
show Continuous ((fun _ : ℝ => (zeroMult ρ.1 : ℝ)) *
((fun _ : ℝ => (1 : ℝ)) /
(fun σ : ℝ => Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))))
exact Continuous.mul continuous_const
(Continuous.div continuous_const hsqrtc hsqrt0)
-- pointwise: ‖Σ‖ ≤ Σ mult·(1/√)
have hpt : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →
‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by
intro σ _
calc ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖
≤ ∑ ρ ∈ nearZerosSub T, ‖(zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=
norm_sum_le _ _
_ = ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) /
‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1‖ := by
apply Finset.sum_congr rfl
intro ρ _
rw [norm_div]
have h2 : ‖(zeroMult ρ.1 : ℂ)‖ = (zeroMult ρ.1 : ℝ) := by
rw [show (zeroMult ρ.1 : ℂ) = ((zeroMult ρ.1 : ℝ) : ℂ) by
push_cast; ring, Complex.norm_real]
exact abs_of_nonneg (Nat.cast_nonneg _)
rw [h2]
_ = ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by
apply Finset.sum_congr rfl
intro ρ _
rw [hnormid σ ρ, mul_one_div]
-- the swap ∫Σ = Σ∫
have hswap : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
(∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))) =
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by
rw [intervalIntegral.integral_finsetSum
(fun ρ hρ => (htermcont ρ hρ).intervalIntegrable _ _)]
apply Finset.sum_congr rfl
intro ρ _
exact intervalIntegral.integral_const_mul _ _
-- per-ρ: the integral ≤ 2·log(148.5·Ĉ₀(√n+2))
have hper : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →
(∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) ≤
2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by
intro ρ hρ
obtain ⟨hδpos, hδ1, hδge⟩ := hρdata ρ hρ
have hsq : (T - ρ.1.im) ^ 2 = |ρ.1.im - T| ^ 2 := by
rw [sq_abs (ρ.1.im - T)]
ring
have hmain := per_zero_integral_le_two_log ρ.2.2.1 ρ.2.2.2 hδpos hδ1.le
rw [hsq]
have hinv : 1 / |ρ.1.im - T| ≤ 9 * C0hat (Real.sqrt (n : ℝ) + 2) := by
have h := one_div_le_one_div_of_le (one_div_pos.mpr (by positivity :
(0 : ℝ) < 9 * C0hat (Real.sqrt (n : ℝ) + 2))) hδge
rwa [one_div_one_div] at h
have h1 : (16.5 : ℝ) * (1 / |ρ.1.im - T|) ≤
16.5 * (9 * C0hat (Real.sqrt (n : ℝ) + 2)) :=
mul_le_mul_of_nonneg_left hinv (by norm_num)
have h2 : (16.5 : ℝ) / |ρ.1.im - T| ≤ 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) := by
rw [mul_one_div, show (16.5 : ℝ) * (9 * C0hat (Real.sqrt (n : ℝ) + 2)) =
148.5 * C0hat (Real.sqrt (n : ℝ) + 2) by ring] at h1
exact h1
have h3 : Real.log (16.5 / |ρ.1.im - T|) ≤
Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) :=
Real.log_le_log (by positivity) h2
linarith [hmain, h3]
-- the sum bound: Σ mult·∫ ≤ (2·log(148.5·Ĉ₀))·Z₂(T)
have hsum : ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) ≤
(2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T := by
calc ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))
≤ ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) := by
apply Finset.sum_le_sum
intro ρ hρ
exact mul_le_mul_of_nonneg_left (hper ρ hρ) (Nat.cast_nonneg _)
_ = (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) *
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) := by
rw [← Finset.sum_mul, mul_comm]
_ ≤ (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T :=
mul_le_mul_of_nonneg_left (nearZerosSub_mult_sum_le hZC2 h10T) hB0nn
-- the near-sum integral bound
have hRHScont : Continuous fun σ : ℝ =>
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by
exact continuous_finsetSum _ (fun ρ hρ => htermcont ρ hρ)
have hSbound : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤
(2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T := by
have h1 : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤
∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
(∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))) :=
intervalIntegral.integral_mono_on hlen hSnorm_int
(hRHScont.intervalIntegrable _ _) (fun σ hσ => hpt σ hσ)
exact h1.trans (hswap.trans_le hsum)
-- assembly
unfold HIntegral
calc ‖∫ x in (-5 / 2 : ℝ)..(3 : ℝ), Jlag n ((x : ℝ) + (T : ℝ) * Complex.I)‖
≤ ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=
intervalIntegral.norm_integral_le_integral_norm hlen
_ ≤ (Real.exp 4 + 1) * ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := hJint
_ ≤ (Real.exp 4 + 1) *
((∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) +
(∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)) :=
mul_le_mul_of_nonneg_left hsplit (by positivity)
_ ≤ (Real.exp 4 + 1) *
((2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) :=
mul_le_mul_of_nonneg_left (add_le_add hSbound hRint) (by positivity)
_ = (Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by ring
/-- **6-c-iv (the bottom side −T)**: the conj trick (DL-5 pattern). -/
theorem hIntegral_Jlag_mid_neg_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)
(hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}
(hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →
ρ.im < Real.sqrt (n : ℝ) + 2 →
1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)
(hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖HIntegral (Jlag n) (-5 / 2) 3 (-T)‖ ≤
(Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have hT0 : (0 : ℝ) < T := by
have h1 : (0 : ℝ) < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr (by linarith)
linarith
have hconj : HIntegral (Jlag n) (-5 / 2) 3 (-T) =
(starRingEnd ℂ) (HIntegral (Jlag n) (-5 / 2) 3 T) := by
unfold HIntegral
rw [← intervalIntegral.intervalIntegral_conj]
apply intervalIntegral.integral_congr
intro σ hσ
show Jlag n ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =
(starRingEnd ℂ) (Jlag n ((σ : ℝ) + T * Complex.I))
have hid2 : ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =
(starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by simp
rw [hid2]
exact Jlag_conj n (by
intro h
have him : (((σ : ℝ) + T * Complex.I)).im = T := by simp
rw [h] at him
simp at him
linarith [hT0])
rw [hconj, Complex.norm_conj]
exact hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1
/-! ## 5. 6-c-v: the full horizontal assembly (mid + DL-5 tails) -/
/-- **6-c-v (the +T full horizontal side)**: split at 3 — the 6-c-iv mid
bound + the DL-5 dog-leg tail charge. -/
theorem hIntegral_Jlag_full_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)
(hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}
(hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →
ρ.im < Real.sqrt (n : ℝ) + 2 →
1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)
(hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T‖ ≤
(Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ) := by
classical
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have h10T : (10 : ℝ) ≤ T := by
have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
linarith
have hT0 : (0 : ℝ) < T := by linarith
have hn1 : 1 ≤ n := by omega
have hn16 : 16 ≤ n := by omega
have h3le : (3 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by
have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
nlinarith [h1]
-- the mid-path continuity (zero-free via the wide pigeonhole)
have hJcontP : ∀ σ : ℝ, ContinuousAt (Jlag n) ((σ : ℝ) + (T : ℝ) * Complex.I) := by
intro σ
have hs1 : ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by
intro h
have him := congrArg Complex.im h
simp at him
linarith [hT0]
have hA := (kFun_differentiableAt (n := n) hs1).continuousAt
have hB := continuousAt_logDeriv_zeta hs1 (zeta_ne_zero_horizontal hTwide hn1 hTn hTn1)
show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _
exact hA.mul hB.neg
have hpath : Continuous fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I) := by
fun_prop
have hcontJP : Continuous fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I) := by
rw [continuous_iff_continuousAt]
intro σ
have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=
hpath.continuousAt
exact ContinuousAt.comp (g := Jlag n)
(f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ) (hJcontP σ) hf
have hInt1 : IntervalIntegrable (fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I))
MeasureTheory.volume (-5 / 2) 3 := hcontJP.intervalIntegrable _ _
-- the tail-path continuity (zero-free by re ≥ 3 > 1, DL-1)
have hInt2 : IntervalIntegrable (fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I))
MeasureTheory.volume 3 (2 * Real.sqrt (n : ℝ)) := by
apply ContinuousOn.intervalIntegrable
rw [Set.uIcc_of_le h3le]
intro σ hσ
obtain ⟨hσ1, hσ2⟩ := hσ
have hre : ((σ : ℝ) + (T : ℝ) * Complex.I).re = σ := by simp
have him : ((σ : ℝ) + (T : ℝ) * Complex.I).im = T := by simp
have hg : ContinuousWithinAt (Jlag n)
(Set.range fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I))
((σ : ℝ) + (T : ℝ) * Complex.I) :=
(Jlag_differentiableAt_dogleg (s := ((σ : ℝ) + (T : ℝ) * Complex.I))
(by rw [hre]; exact hσ1) (by rw [him]; exact hT0)).continuousAt.continuousWithinAt
have hfp : ContinuousWithinAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I))
(Set.Icc 3 (2 * Real.sqrt (n : ℝ))) σ := hpath.continuousWithinAt
exact ContinuousWithinAt.comp (g := Jlag n)
(f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ) hg hfp
(Set.mapsTo_range _ _)
-- split at 3 and assemble
have hsplit : HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T =
HIntegral (Jlag n) (-5 / 2) 3 T + HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T :=
HIntegral_split hInt1 hInt2
have hmid := hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1
have htail := hIntegral_Jlag_low_le_dogLegUpper hn16 hTn hTn1
have hDLR : DogLegRight (n : ℝ) = ((Real.sqrt (n : ℝ) + 1) / 2) *
(Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) + IIMaj (n : ℝ) / 4 := rfl
rw [hsplit, hDLR]
calc ‖HIntegral (Jlag n) (-5 / 2) 3 T +
HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖
≤ ‖HIntegral (Jlag n) (-5 / 2) 3 T‖ +
‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ := norm_add_le _ _
_ ≤ (Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) +
(((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
IIMaj (n : ℝ) / 4) :=
add_le_add hmid htail
/-- **6-c-v (the −T full horizontal side)**: the conj trick at the full
level (no split needed — intervalIntegral_conj is unconditional). -/
theorem hIntegral_Jlag_full_neg_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)
(hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}
(hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →
ρ.im < Real.sqrt (n : ℝ) + 2 →
1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)
(hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T)‖ ≤
(Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ) := by
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have hT0 : (0 : ℝ) < T := by
have h1 : (0 : ℝ) < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr (by linarith)
linarith
have hconj : HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T) =
(starRingEnd ℂ) (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T) := by
unfold HIntegral
rw [← intervalIntegral.intervalIntegral_conj]
apply intervalIntegral.integral_congr
intro σ hσ
show Jlag n ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =
(starRingEnd ℂ) (Jlag n ((σ : ℝ) + T * Complex.I))
have hid2 : ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =
(starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by simp
rw [hid2]
exact Jlag_conj n (by
intro h
have him : (((σ : ℝ) + T * Complex.I)).im = T := by simp
rw [h] at him
simp at him
linarith [hT0])
rw [hconj, Complex.norm_conj]
exact hIntegral_Jlag_full_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1
/-- **6-c-v (the two horizontal sides)**: the horizontal assembly charge —
2·(mid bound) + 2·DogLegRight. -/
theorem hIntegral_Jlag_full_two_sides (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)
(hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}
(hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →
ρ.im < Real.sqrt (n : ℝ) + 2 →
1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)
(hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T‖ +
‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T)‖ ≤
2 * ((Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) := by
rw [show (2 : ℝ) * ((Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) =
((Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) +
((Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) by ring]
exact add_le_add (hIntegral_Jlag_full_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1)
(hIntegral_Jlag_full_neg_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1)
/-! ## 6. 6-d: the fold — `sfBoundProp : SfBoundProp` -/
/-- Ĉ₀(t) ≤ t for t ≥ 8 (via log x ≤ x/e with 1/e ≤ 0.36789 certified
from e > 2.7182818283, and loglog x ≤ log x − 1). -/
theorem C0hat_le_self {t : ℝ} (ht : 8 ≤ t) : C0hat t ≤ t := by
have ht2 : (0 : ℝ) < t + 2 := by linarith
have ht1 : (1 : ℝ) < t + 2 := by linarith
have hinv : (1 : ℝ) / Real.exp 1 ≤ 0.36789 := by
rw [div_le_iff₀ (Real.exp_pos 1)]
nlinarith [Real.exp_one_gt_d9]
have hL1 : Real.log (t + 2) ≤ (t + 2) / Real.exp 1 := by
have h1 := Real.log_le_sub_one_of_pos (div_pos ht2 (Real.exp_pos 1))
have h2 : Real.log ((t + 2) / Real.exp 1) = Real.log (t + 2) - 1 := by
rw [Real.log_div (ne_of_gt ht2) (Real.exp_pos 1).ne', Real.log_exp]
rw [h2] at h1
linarith [h1]
have hL : Real.log (t + 2) ≤ (t + 2) * 0.36789 := by
have h3 : (t + 2) / Real.exp 1 ≤ (t + 2) * 0.36789 := by
rw [div_eq_mul_one_div]
exact mul_le_mul_of_nonneg_left hinv ht2.le
exact hL1.trans h3
have hLL : Real.log (Real.log (t + 2)) ≤ (t + 2) * 0.36789 := by
have h1 := Real.log_le_sub_one_of_pos (Real.log_pos ht1)
nlinarith [h1, hL]
unfold C0hat
nlinarith [hL, hLL, ht]
/-- **The horizontal pinch** (the E-030 V3 ≤ 0.40 witness made analytic):
the near-sum integral + the R-part ≤ 7·Ĥ(T). Chain (all elementary, no
certified log numerics): Ĉ₀(√n+2) ≤ √n+2 (Ĉ₀(t) ≤ t, t ≥ 318), so
148.5·Ĉ₀(√n+2) ≤ (√n+2)² and its log ≤ 2·log(T+2); Z₂(T) ≤ 2·Ĉ₀(T);
Ĉ₀(T) ≥ 0.433·log(T+2) with 8 ≤ 21·0.433 = 9.093; 5.5 ≤ 7 on the R-part. -/
theorem pinch_horizontal {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}
(hTn : Real.sqrt (n : ℝ) ≤ T) (_hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) ≤ 7 * Hhat T := by
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have hsqrt316 : (316 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
have hT1 : (1 : ℝ) ≤ T := by nlinarith [hsqrt316, hTn]
have hT0 : (0 : ℝ) < T := by nlinarith
-- (a) log(148.5·Ĉ₀(√n+2)) ≤ 2·log(T+2)
have hC0le : C0hat (Real.sqrt (n : ℝ) + 2) ≤ Real.sqrt (n : ℝ) + 2 :=
C0hat_le_self (by nlinarith [hsqrt316])
have h148 : (148.5 : ℝ) ≤ Real.sqrt (n : ℝ) + 2 := by nlinarith [hsqrt316]
have hC0pos : (0 : ℝ) < C0hat (Real.sqrt (n : ℝ) + 2) := by
have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : ℝ)] :
(1 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)
linarith
have hsq1 : 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) ≤ (Real.sqrt (n : ℝ) + 2) ^ 2 := by
have h1 := mul_le_mul hC0le h148 (by norm_num : (0 : ℝ) ≤ (148.5 : ℝ))
(by positivity : (0 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)
nlinarith [h1, hC0pos.le]
have hlogarg : Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤
2 * Real.log (T + 2) := by
have h2 := Real.log_le_log (by positivity) hsq1
have h3 : Real.log ((Real.sqrt (n : ℝ) + 2) ^ 2) = 2 * Real.log (Real.sqrt (n : ℝ) + 2) := by
rw [Real.log_pow]
ring
have h4 : Real.log (Real.sqrt (n : ℝ) + 2) ≤ Real.log (T + 2) :=
Real.log_le_log (by positivity) (by linarith [hTn])
linarith [h2, h3, h4]
-- (b) Z₂(T) ≤ 2·Ĉ₀(T)
have hZ2le : Z2hat T ≤ 2 * C0hat T := by
have hL1 : (1 : ℝ) ≤ Real.log (T + 2) := by
have ht2 : (0 : ℝ) < T + 2 := by linarith
rw [Real.le_log_iff_exp_le ht2]
have he := Real.exp_one_lt_d9.le
linarith
have hLL0 : (0 : ℝ) ≤ Real.log (Real.log (T + 2)) := Real.log_nonneg hL1
unfold Z2hat C0hat
nlinarith [hL1, hLL0]
-- (c) Ĉ₀(T) ≥ 0.433·log(T+2)
have hC0L : 0.433 * Real.log (T + 2) ≤ C0hat T := by
have hL1 : (1 : ℝ) ≤ Real.log (T + 2) := by
have ht2 : (0 : ℝ) < T + 2 := by linarith
rw [Real.le_log_iff_exp_le ht2]
have he := Real.exp_one_lt_d9.le
linarith
have hLL0 : (0 : ℝ) ≤ Real.log (Real.log (T + 2)) := Real.log_nonneg hL1
unfold C0hat
nlinarith [hL1, hLL0]
-- (d) the near part ≤ 21·Ĉ₀(T)²
have hlogT0 : (0 : ℝ) ≤ Real.log (T + 2) := Real.log_nonneg (by linarith)
have hC0T0 : (0 : ℝ) < C0hat T := by
have h2 := two_le_C0hat hT1
linarith
have hnear : 2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤
21 * C0hat T * C0hat T := by
have h1 : 2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤
2 * Z2hat T * (2 * Real.log (T + 2)) := by
have hnn : (0 : ℝ) ≤ 2 * Z2hat T := by
have h := Z2hat_nonneg hT1
positivity
exact mul_le_mul_of_nonneg_left hlogarg hnn
have hZ2L : Z2hat T * Real.log (T + 2) ≤ 2 * C0hat T * Real.log (T + 2) :=
mul_le_mul_of_nonneg_right hZ2le hlogT0
have h8 : 8 * Real.log (T + 2) ≤ 21 * C0hat T := by
have h1 : (8 : ℝ) ≤ 21 * (0.433 : ℝ) := by norm_num
nlinarith [hC0L, h1, hlogT0]
have h3 : (8 * Real.log (T + 2)) * C0hat T ≤ (21 * C0hat T) * C0hat T :=
mul_le_mul h8 le_rfl hC0T0.le (by positivity : (0 : ℝ) ≤ 21 * C0hat T)
nlinarith [h1, hZ2L, h3, hlogT0]
-- (e) the 5.5 ≤ 7 part
have hR0 : (0 : ℝ) ≤ 10.5 * Real.log (T + 2) + 48 := by
have h1 := Real.log_nonneg (by linarith : (1 : ℝ) ≤ T + 2)
nlinarith
have hR : (3 - -5 / 2 : ℝ) * (10.5 * Real.log (T + 2) + 48) ≤
7 * (10.5 * Real.log (T + 2) + 48) := by
have h55 : (3 - -5 / 2 : ℝ) = 5.5 := by norm_num
rw [h55]
nlinarith [hR0]
-- final: 21·Ĉ₀² + 7·R = 7·Ĥ
unfold Hhat
nlinarith [hnear, hR]
/-- **THE FOLD (ii′-6-d)**: `SfBoundProp` from the six declared perimeter
hypotheses — the 6-b sides identity + the bridge (both-signs 4F + triv ≤ 1),
the rectangle side decomposition, the four side bounds of ii′-6-c, the
horizontal pinch, and the F-E absorption e^{1/3} ≤ 1.4 ≤ 2π. -/
theorem sfBoundProp (hRH : RHUpTo (3 * 10 ^ 12)) (hZC : ZeroCountProp)
(hZC2 : ZeroCountProp2) (hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros)
(hMZ : MZeroProp) : SfBoundProp := by
intro n hn hN1
classical
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have hn1 : 1 ≤ n := by omega
have hn16 : 16 ≤ n := by omega
have hsqrt316 : (316 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
have ha : (3 : ℝ) ≤ Real.sqrt (n : ℝ) := by nlinarith [hsqrt316]
obtain ⟨T, hTn, hTn1, hTwide⟩ := exists_zero_avoiding_T_wide hZC ha
have hT1 : (1 : ℝ) ≤ T := by nlinarith [hTn]
have hT2 : (2 : ℝ) ≤ T := by nlinarith
have hT0 : (0 : ℝ) < T := by nlinarith
-- T ≤ 3·10¹² (from n ≤ N₁; the bridge's internal RHUpTo range)
have hTle : T ≤ 3 * 10 ^ 12 := by
have h1 : Real.sqrt (n : ℝ) ≤ 3 * 10 ^ 12 - 1 := by
have h2 := Real.sqrt_le_sqrt hN1
rwa [Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 3 * 10 ^ 12 - 1)] at h2
linarith [hTn1]
-- the sides identity
have hsf := sf_abs_le_rectInt_add_zeroSum hZC hn1 hT1 hTn hTn1 hTwide
-- the bridge (variant with T ≤ 3·10¹² — the internal range actually used)
have hbridge : ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),
(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by
have h2not : (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by
intro h
have hnt := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1
have h21 : (0 : ℝ) < (-2 : ℂ).re := hnt.2.1
norm_num at h21
have hdisj2 : Disjoint (zeroBothWindow_finite T).toFinset {(-2 : ℂ)} := by
rw [Finset.disjoint_left]
intro ρ hρ hρ2
rw [Finset.mem_singleton] at hρ2
exact h2not (hρ2 ▸ hρ)
rw [Finset.sum_union hdisj2, Finset.sum_singleton]
have htriv := trivTerm_norm_le_one n
have hbr := zeroSum_nontriv_norm_le hRH (n := n) (T := T) hTle
have hcount := zeroBothWindow_sum_eq_two_mul hNLZ T
have hZ := hZCG T hT2
calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) +
(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖
≤ ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ +
‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ := norm_add_le _ _
_ ≤ (2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ)) + 1 := by
linarith [hbr, htriv]
_ = 2 * (2 * ∑ ρ ∈ (zeroGlobalWindow_finite T).toFinset, (zeroMult ρ : ℝ)) + 1 := by
rw [hcount]
_ ≤ 4 * FAlt T + 1 := by linarith [hZ]
-- the four side bounds
have hVl := vIntegral_Jlag_left_norm_le hZC hZC2 hNLZ hMZ hn hTn hTn1
have hVr := vIntegral_Jlag_right_le_exp_third_IIMaj hn hTn hTn1
have hH := hIntegral_Jlag_full_two_sides hZC hZC2 hNLZ hn hTwide hTn hTn1
-- ‖RectInt'‖ = (1/2π)·‖RectInt‖
have hnorm : ‖RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)‖ =
(1 / (2 * Real.pi)) * ‖RectangleIntegral (Jlag n) (rectZ T) (rectW n T)‖ := by
unfold RectangleIntegral'
rw [norm_smul]
congr 1
have h1 : ‖(2 : ℂ) * (Real.pi : ℂ) * Complex.I‖ = 2 * Real.pi := by
rw [norm_mul, Complex.norm_I, mul_one, norm_mul]
have h3 : ‖(2 : ℂ)‖ = (2 : ℝ) := by
rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]
exact abs_of_nonneg (by norm_num)
have h4 : ‖(Real.pi : ℂ)‖ = Real.pi := by
rw [Complex.norm_real]
exact abs_of_nonneg Real.pi_nonneg
rw [h3, h4]
rw [norm_div, norm_one, h1]
-- the rectangle norm triangle
have htri : ‖RectangleIntegral (Jlag n) (rectZ T) (rectW n T)‖ ≤
‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T)‖ +
‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T‖ +
‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖ +
‖VIntegral (Jlag n) (-5 / 2) (-T) T‖ := by
rw [rectangleIntegral_Jlag_eq n T]
have h1 := norm_sub_le (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T) -
HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T +
VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T)
(VIntegral (Jlag n) (-5 / 2) (-T) T)
have h2 := norm_add_le (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T) -
HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T)
(VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T)
have h3 := norm_sub_le (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T))
(HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T)
linarith [h1, h2, h3]
-- the horizontal pinch
have hpinch := pinch_horizontal hn hTn hTn1
-- the F-E absorption: e^{1/3} ≤ 1.4 ≤ 2π
have he13 : Real.exp (1 / 3 : ℝ) ≤ 2 * Real.pi := by
have h1 : Real.exp (1 / 3 : ℝ) ≤ 1.4 := by
have h2 : (Real.exp (1 / 3 : ℝ)) ^ 3 ≤ (1.4 : ℝ) ^ 3 := by
have h3 : (Real.exp (1 / 3 : ℝ)) ^ 3 = Real.exp 1 := by
rw [← Real.exp_nat_mul (1 / 3 : ℝ) 3]
congr 1
norm_num
rw [h3]
have h4 : Real.exp 1 ≤ 2.7182818286 := Real.exp_one_lt_d9.le
norm_num1 at ⊢
linarith only [h4]
exact le_of_pow_le_pow_left₀ (by norm_num : (3 : ℕ) ≠ 0) (by norm_num : (0 : ℝ) ≤ 1.4) h2
have h5 : (3 : ℝ) ≤ Real.pi := Real.pi_gt_three.le
nlinarith only [h1, h5]
-- the 1/(2π) comparisons
have h2πpos : (0 : ℝ) < 2 * Real.pi := by positivity
have h2πle : (1 / (2 * Real.pi)) ≤ 1 := by
rw [div_le_iff₀ h2πpos, one_mul]
have h := Real.pi_gt_three.le
linarith
have he13' : Real.exp (1 / 3 : ℝ) / (2 * Real.pi) ≤ 1 := by
rw [div_le_iff₀ h2πpos, one_mul]
exact he13
-- nonneg facts
have hIIMaj0 : (0 : ℝ) ≤ IIMaj (n : ℝ) := by unfold IIMaj; positivity
have hDLR0 : (0 : ℝ) ≤ DogLegRight (n : ℝ) := by unfold DogLegRight IIMaj; positivity
have hC0T0 : (0 : ℝ) < C0hat T := by
have h2 := two_le_C0hat hT1
linarith
have hHhat0 : (0 : ℝ) ≤ Hhat T := by
unfold Hhat
have hL1 : (1 : ℝ) ≤ Real.log (T + 2) := by
have ht2 : (0 : ℝ) < T + 2 := by linarith
rw [Real.le_log_iff_exp_le ht2]
have he := Real.exp_one_lt_d9.le
linarith
nlinarith only [hC0T0.le, hL1]
have hX0 : (0 : ℝ) ≤ 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +
40 * 1.3352 := by
have h1 := Z2hat_nonneg hT1
have h2 := Real.log_nonneg (by linarith : (1 : ℝ) ≤ T + 2)
nlinarith only [hT0.le, h1, h2]
-- the T ≤ √n+1 monotonicity comparisons
have hsqrt0 : (0 : ℝ) ≤ Real.sqrt (n : ℝ) := Real.sqrt_nonneg _
have hlogT1 : (1 : ℝ) ≤ Real.log (T + 2) := by
have ht2 : (0 : ℝ) < T + 2 := by linarith
rw [Real.le_log_iff_exp_le ht2]
have he := Real.exp_one_lt_d9.le
linarith
have hFAlt : FAlt T ≤ FAlt (Real.sqrt (n : ℝ) + 1) := by
unfold FAlt
have hT0' : (0 : ℝ) < T := hT0
have hlog1 : (1 : ℝ) ≤ Real.log T := by
have ht2 : (0 : ℝ) < T := hT0
rw [Real.le_log_iff_exp_le hT0]
have he := Real.exp_one_lt_d9.le
nlinarith only [hTn, hsqrt316, he]
have hA : T * Real.log T ≤ (Real.sqrt (n : ℝ) + 1) * Real.log (Real.sqrt (n : ℝ) + 1) := by
have h1 := Real.log_le_log hT0 (by linarith [hTn1] : T ≤ Real.sqrt (n : ℝ) + 1)
exact mul_le_mul hTn1 h1
(Real.log_nonneg (by linarith [hTn, hsqrt316] : (1 : ℝ) ≤ T)) (by linarith [hsqrt0])
have hB : Real.log T ≤ Real.log (Real.sqrt (n : ℝ) + 1) :=
Real.log_le_log hT0 (by linarith [hTn1])
have hC : Real.log (Real.log T) ≤ Real.log (Real.log (Real.sqrt (n : ℝ) + 1)) := by
apply Real.log_le_log (by linarith [hlog1] : (0 : ℝ) < Real.log T)
have h1 : (1 : ℝ) ≤ Real.log (Real.sqrt (n : ℝ) + 1) := by
have ht2 : (0 : ℝ) < Real.sqrt (n : ℝ) + 1 := by positivity
rw [Real.le_log_iff_exp_le ht2]
have he := Real.exp_one_lt_d9.le
nlinarith only [hsqrt316, he]
have h2 : Real.log T ≤ Real.log (Real.sqrt (n : ℝ) + 1) := hB
exact h2
have hconst : (0 : ℝ) ≤ 1 / (2 * Real.pi) := by positivity
have hA' := mul_le_mul_of_nonneg_left hA hconst
nlinarith only [hA', hB, hC]
have hX : 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) ≤
4 * (Real.sqrt (n : ℝ) + 1) *
((2 / 3) * Z2hat (Real.sqrt (n : ℝ) + 1) + 10.5 * Real.log (Real.sqrt (n : ℝ) + 1 + 2) + 48) := by
have hZ := Z2hat_mono hT1 hTn1
have hlog := Real.log_le_log (by linarith : (0 : ℝ) < T + 2)
(by linarith [hTn1] : T + 2 ≤ Real.sqrt (n : ℝ) + 1 + 2)
have hXle : (2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48 ≤
(2 / 3) * Z2hat (Real.sqrt (n : ℝ) + 1) + 10.5 * Real.log (Real.sqrt (n : ℝ) + 1 + 2) + 48 := by
nlinarith only [hZ, hlog]
have hX0' : (0 : ℝ) ≤ (2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48 := by
have h1 := Z2hat_nonneg hT1
nlinarith only [hlogT1, h1]
have h4 : T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) ≤
(Real.sqrt (n : ℝ) + 1) *
((2 / 3) * Z2hat (Real.sqrt (n : ℝ) + 1) + 10.5 * Real.log (Real.sqrt (n : ℝ) + 1 + 2) + 48) :=
mul_le_mul hTn1 hXle hX0' (by linarith [hsqrt0])
nlinarith only [h4]
have hHhat : Hhat T ≤ Hhat (Real.sqrt (n : ℝ) + 1) := by
unfold Hhat
have hC := C0hat_mono hT1 hTn1
have hC2 : C0hat T ^ 2 ≤ C0hat (Real.sqrt (n : ℝ) + 1) ^ 2 :=
pow_le_pow_left₀ hC0T0.le hC 2
have hlog := Real.log_le_log (by linarith : (0 : ℝ) < T + 2)
(by linarith [hTn1] : T + 2 ≤ Real.sqrt (n : ℝ) + 1 + 2)
nlinarith only [hC2, hlog]
-- the Bn unfold
have hBn : Bn FAlt (n : ℝ) = 4 * FAlt (Real.sqrt (n : ℝ) + 1) +
4 * (Real.sqrt (n : ℝ) + 1) *
((2 / 3) * Z2hat (Real.sqrt (n : ℝ) + 1) + 10.5 * Real.log (Real.sqrt (n : ℝ) + 1 + 2) + 48) +
40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt (n : ℝ) + 1)) +
2 * DogLegRight (n : ℝ) + IIMaj (n : ℝ) + 1 := by
unfold Bn
rfl
rw [hBn]
-- the IIMaj absorption: (1/2π)·e^{1/3}·IIMaj ≤ IIMaj
have hIIMajAbs : (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ)) ≤
IIMaj (n : ℝ) := by
have h1 := mul_le_mul_of_nonneg_right he13' hIIMaj0
calc (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ))
= (Real.exp (1 / 3 : ℝ) / (2 * Real.pi)) * IIMaj (n : ℝ) := by ring
_ ≤ 1 * IIMaj (n : ℝ) := h1
_ = IIMaj (n : ℝ) := by ring
-- the Hhat absorption: (1/2π)·Y ≤ Y for Y ≥ 0
have hHhatAbs : (1 / (2 * Real.pi)) * (2 * (Real.exp 4 + 1) * (7 * Hhat T)) ≤
2 * (Real.exp 4 + 1) * (7 * Hhat T) := by
have hY : (0 : ℝ) ≤ 2 * (Real.exp 4 + 1) * (7 * Hhat T) := by
have h1 : (0 : ℝ) ≤ 7 * Hhat T := by nlinarith only [hHhat0]
positivity
have h1 := mul_le_mul_of_nonneg_right h2πle hY
rwa [one_mul] at h1
have hDLRAbs : (1 / (2 * Real.pi)) * (2 * DogLegRight (n : ℝ)) ≤ 2 * DogLegRight (n : ℝ) := by
have h2DLR0 : (0 : ℝ) ≤ 2 * DogLegRight (n : ℝ) := by positivity
have h1 := mul_le_mul_of_nonneg_right h2πle h2DLR0
rwa [one_mul] at h1
have hXAbs : (1 / (2 * Real.pi)) * (4 * T *
((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352) ≤
4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352 := by
have h1 := mul_le_mul_of_nonneg_right h2πle hX0
rwa [one_mul] at h1
-- the mid-bound pinch absorption: (1/2π)·2(e⁴+1)(NI+5.5R) ≤ (1/2π)·2(e⁴+1)·7·Ĥ
have hPinchAbs : ((1 / (2 * Real.pi)) * (2 * (Real.exp 4 + 1))) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) ≤
((1 / (2 * Real.pi)) * (2 * (Real.exp 4 + 1))) * (7 * Hhat T) :=
mul_le_mul_of_nonneg_left hpinch (by positivity :
(0 : ℝ) ≤ (1 / (2 * Real.pi)) * (2 * (Real.exp 4 + 1)))
-- the giant assembly
have hnormRect : ‖RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)‖ ≤
(1 / (2 * Real.pi)) *
(‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T)‖ +
‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T‖ +
‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖ +
‖VIntegral (Jlag n) (-5 / 2) (-T) T‖) := by
rw [hnorm]
have h1 := mul_le_mul_of_nonneg_left htri (by positivity : (0 : ℝ) ≤ 1 / (2 * Real.pi))
exact h1
-- the per-side (1/2π)-scaled bounds (atom-mults linarith can't do)
have hVr' := mul_le_mul_of_nonneg_left hVr (by positivity : (0 : ℝ) ≤ 1 / (2 * Real.pi))
have hVl' := mul_le_mul_of_nonneg_left hVl (by positivity : (0 : ℝ) ≤ 1 / (2 * Real.pi))
have hH' := mul_le_mul_of_nonneg_left hH (by positivity : (0 : ℝ) ≤ 1 / (2 * Real.pi))
-- |Sf n| ≤ ‖RectInt'‖ + ‖Σ‖, now everything slots in — bisected in two steps
have hstep1 : |Sf n| ≤ (1 / (2 * Real.pi)) *
(2 * ((Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) +
(Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ)) +
(4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352)) +
(4 * FAlt T + 1) := by
linarith only [hsf, hnormRect, hH', hVr', hVl', hbridge]
have hHhat' : (2 * (Real.exp 4 + 1) * 7) * Hhat T ≤
(2 * (Real.exp 4 + 1) * 7) * Hhat (Real.sqrt (n : ℝ) + 1) :=
mul_le_mul_of_nonneg_left hHhat (by positivity : (0 : ℝ) ≤ 2 * (Real.exp 4 + 1) * 7)
have hstep2 : (1 / (2 * Real.pi)) *
(2 * ((Real.exp 4 + 1) *
(2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +
(3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) +
(Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ)) +
(4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352)) +
(4 * FAlt T + 1) ≤
4 * FAlt (Real.sqrt (n : ℝ) + 1) +
4 * (Real.sqrt (n : ℝ) + 1) *
((2 / 3) * Z2hat (Real.sqrt (n : ℝ) + 1) + 10.5 * Real.log (Real.sqrt (n : ℝ) + 1 + 2) + 48) +
40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt (n : ℝ) + 1)) +
2 * DogLegRight (n : ℝ) + IIMaj (n : ℝ) + 1 := by
linarith only [hPinchAbs, hHhatAbs, hDLRAbs, hXAbs, hIIMajAbs, hFAlt, hX, hHhat',
hIIMaj0, hDLR0, hHhat0, hX0]
exact hstep1.trans hstep2
end NguyenRH1
end