← Session 36 — ii′-6-DL dog-leg + side bounds; Paper A review
thinking (59441 chars)
- `Real.continuous_sqrt : Continuous (√· : ℝ → ℝ)` ✓ (Analysis/Real/Sqrt.lean:126 — and line 95 shows `sqrt.continuous` in the NNReal? — the ℝ one at 126 ✓). The first at :95 is `Real.sqrt.continuous`? Anyway — `Real.continuous_sqrt` exists ✓.
- `neg_sq (a) : (-a)^2 = a^2` ✓ (Algebra/Ring/Commute — root namespace).
- `sq_abs (a) : |a|^2 = a^2` ✓ @[simp] (root).
- `Continuous.div (hf) (hg) (h₀ : ∀ x, g x ≠ 0)` ✓.
All confirmed. Now write §4. Given the size, I'll write it in two chunks: first the arcsinh-FTC machine (lemmas 1–4), build-check that alone, then the mid-horizontal bound (5–6). Actually — write the whole §4 and iterate; the error loop is ~25 s per elaboration which is fine.
Let me draft the full §4 now. Points of care:
- All `∫ σ in a..b, ... + ...` get parens.
- The per-σ HasDerivAt chain with convert + field_simp.
- uIcc membership for integral_eq_sub_of_hasDerivAt — hderiv : ∀ x ∈ uIcc a b — I prove ∀ σ (global), then `fun σ _ => hF σ`.
Let me also double-check `hasDerivAt_id` — signature: `theorem hasDerivAt_id (x : 𝕜) : HasDerivAt id 1 x` ✓ standard.
`HasDerivAt.sub_const (hf : HasDerivAt f f' x) (c : 𝕜) : HasDerivAt (fun x => f x - c) f' x` ✓ standard.
For the per-ρ norm identity: ‖(↑σ + ↑T·I) − ρ‖ = √((σ−ρ.re)² + (T−ρ.im)²):
```lean
have hnormid : ∀ σ : ℝ, ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ‖ =
Real.sqrt ((σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2) := by
intro σ
have h1 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ) =
(σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2 := by
simp [Complex.normSq_apply]
ring
rw [← h1]
-- ‖z‖ = √(normSq z)
exact (Complex.norm_def _).symm??
```
Hmm — what IS the norm-def lemma? `Complex.norm_def : ‖z‖ = Real.sqrt (normSq z)`? or `Complex.norm_eq_sqrt_normSq`? Let me check: In Mathlib, `Complex.norm` is defined as `Real.sqrt (normSq z)` via `Complex.norm (z : ℂ) : ℝ := Real.sqrt (normSq z)`? Actually the Norm instance: `instNorm : Norm ℂ := ⟨fun z => Real.sqrt (normSq z)⟩`. So `‖z‖ = Real.sqrt (normSq z)` is rfl! There's `Complex.norm_def : ‖z‖ = Real.sqrt (normSq z)`? — I recall `Complex.norm_def (z : ℂ) : ‖z‖ = Real.sqrt (normSq z) := rfl`. If it's rfl, then `rw [← h1]` turns goal `‖z‖ = √((σ−β)²+(T−γ)²)` into `‖z‖ = √(normSq z)` — then `rfl`?? — is `‖z‖` DEFEQ `√(normSq z)`? Yes via instNorm. So `exact rfl`?? Hmm — rfl might work if the Norm instance unfolds reducibly. There's `Complex.norm_def` — let me grep. Actually — safer: `Complex.normSq_eq_norm_sq : normSq z = ‖z‖ ^ 2` — gives ‖z‖² = normSq z, then ‖z‖ = √(normSq z) via (Real.sqrt_sq (norm_nonneg)).symm-ish:
```lean
have h2 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ) =
‖(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ)‖ ^ 2 := Complex.normSq_eq_norm_sq _
-- want ‖z‖ = √(X) where normSq z = X
rw [← h1] at h2 -- h2 : X = ‖z‖^2 where X := (σ−β)²+(T−γ)²
-- ‖z‖ = √X: both nonneg, squares equal
have h3 : (0:ℝ) ≤ ‖(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ)‖ := norm_nonneg _
have h4 : ‖(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ)‖ = Real.sqrt ((σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2) := by
rw [← h2] -- goal: ‖z‖ = √(‖z‖^2)?? no...
```
Hmm — cleaner: `Real.sqrt_eq_iff_eq_sq (hx : 0 ≤ x) (hy : 0 ≤ y) : √x = y ↔ x = y^2`? — DL-5 used `Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)` ✓ EXISTS. So:
```lean
have hnormid : ‖z‖ = Real.sqrt X := by
rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _)] -- hmm direction: √X = ‖z‖
-- goal: √X = ‖z‖ ↔ X = ‖z‖^2
sorry
```
Real.sqrt_eq_iff_eq_sq (hx : 0 ≤ x) (hy : 0 ≤ y) : Real.sqrt x = y ↔ x = y ^ 2. So:
```lean
symm
rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _)]
-- goal: X = ‖z‖^2
rw [← Complex.normSq_eq_norm_sq]
exact h1
```
Hmm — goal ‖z‖ = √X; symm → √X = ‖z‖; rw [Real.sqrt_eq_iff_eq_sq hX hnorm] → goal X = ‖z‖^2; rw [← Complex.normSq_eq_norm_sq] → normSq z = ‖z‖^2?? — wait — `Complex.normSq_eq_norm_sq (z) : normSq z = ‖z‖^2` — rw [← that] at goal X = ‖z‖^2 — the ← direction: pattern ‖z‖^2 → normSq z: goal becomes X = normSq z — exact h1 (h1 : normSq z = X — hmm — need X = normSq z — h1.symm ✓). So exact h1.symm. Let me restructure:
```lean
have hnormid : ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ‖ =
Real.sqrt ((σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2) := by
have h1 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ) =
(σ - ρ.re) ^ 2 + (T - ρ.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
```
Hmm — h1's simp [Complex.normSq_apply]: normSq z = z.re*z.re + z.im*z.im (normSq_apply : normSq z = z.re * z.re + z.im * z.im? — from LiContour's hD_rel line 474: `D = s.re * s.re + s.im * s.im := by rw [hD_def, Complex.normSq_apply s]` ✓). So simp [Complex.normSq_apply] turns goal into re/im form, then simp computes re/im of ((↑σ+↑T·I)−ρ): sub_re: σ − ρ.re... wait: (↑σ+↑T·I−ρ).re = (↑σ+↑T·I).re − ρ.re = σ − ρ.re ✓; im: T − ρ.im ✓. Then goal: (σ−ρ.re)*(σ−ρ.re) + (T−ρ.im)*(T−ρ.im) = (σ−ρ.re)^2 + (T−ρ.im)^2 — ring ✓ (sq vs *2 form — ring handles).
The simp call: `simp [Complex.normSq_apply]` — will simp also compute the re/im? Complex.sub_re etc. are simp lemmas ✓ default simp set includes them ✓ probably reduces fully to the ring-closable form. If not, add the explicit list. Then `ring`.
Now — the FULL §4 draft. Let me write it. I'll be careful about:
(a) parens around all integral summands.
(b) the positivity side conditions.
For (5) hIntegral_Jlag_mid_norm_le — the full proof:
```lean
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
-- the C₀ positivity facts
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
-- zero-freeness on the horizontal (for continuity)
have hzne : ∀ σ : ℝ, riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 0 :=
fun σ => zeta_ne_zero_horizontal hTwide hn1 hTn hTn1
-- continuity of the path integrands
...
```
Wait — zeta_ne_zero_horizontal's hn is (1 ≤ n) ✓ and σ — its statement: riemannZeta ((σ:ℝ) + (T:ℝ)*I) ≠ 0 ✓.
Continuity of ‖logDeriv‖, ‖R‖, ‖Σ‖, ‖Jlag‖ on the path — same machine as 6-c-ii but with zeta_ne_zero_horizontal:
```lean
have hJcont : ∀ σ : ℝ, 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 -- T = 0
linarith [hT0] -- T ≥ 316 ≠ 0... wait him : T = 0? (1:ℂ).im = 0 — him : (point).im = Complex.im 1 → T = 0 — linarith with h10T ✓
have hA := (kFun_differentiableAt (n := n) hs1).continuousAt
have hB := continuousAt_logDeriv_zeta hs1 (hzne σ)
show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _
exact hA.mul hB.neg
```
Hmm — him : (↑σ + ↑T·I).im = (1:ℂ).im — simp → T = 0 ✓ then linarith [h10T] ✓.
For ‖R‖ continuity: R = logDeriv ζ − Σ:
```lean
have hRcont : Continuous fun σ : ℝ =>
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ := by
apply continuous_norm.comp
apply Continuous.sub
· -- logDeriv continuous
rw [continuous_iff_continuousAt]
intro σ
have hs1 : ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := ...
have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ := hpath.continuousAt
exact ContinuousAt.comp (g := logDeriv riemannZeta) (f := ...) (x := σ)
(continuousAt_logDeriv_zeta hs1 (hzne σ)) hf
· -- the near sum continuous
apply continuous_finset_sum
intro ρ hρ
apply Continuous.div continuous_const
· -- the denominator continuous
exact hpath.sub continuous_const
· intro σ
-- denominator ≠ 0: else s = ρ, ζ s = ζ ρ = 0 vs hzne
have hne : ((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1 ≠ 0 := by
intro h
have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h
have h1 := hzne σ
rw [hs] at h1
exact h1 ρ.2.1
exact hne σ -- hmm, the h₀ for Continuous.div is ∀ x, g x ≠ 0
```
Wait — Continuous.div (hf) (hg) (h₀ : ∀ x, g x ≠ 0) — so I need ∀ σ, (↑σ+↑T·I) − ρ.1 ≠ 0 ✓ from the hzne argument ✓.
`continuous_finset_sum : (∀ i ∈ s, Continuous (f i)) → Continuous fun x => ∑ i ∈ s, f i x` ✓ exists (continuous_finset_sum s h).
`hpath : Continuous fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I) := by fun_prop` ✓.
For the logDeriv branch — the ContinuousAt.comp pinned pattern ✓. Actually — I realize I can factor a small helper for the composition since it repeats: skip, inline is fine.
For ‖Σ‖ continuity: same denominator machine + norm.
For ‖Jlag‖: hJcont machine + norm (as 6-c-ii).
The kernel bound hker (as drafted above).
The R-bound pointwise:
```lean
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
```
Hmm — the capstone's bound: 10.5·log(|T|+2)+48 — rw [abs_of_nonneg hT0] at h : |T| → T ✓.
The near-sum pointwise split and per-term norm — the s in the capstone's sum is (↑σ + ↑T·I): terms (zeroMult ρ.1 : ℂ)/((↑σ+↑T·I) − ρ.1) ✓ — my ‖Σ‖ integrand matches ✓.
The integral estimates:
```lean
-- ∫ ‖R‖ ≤ (3−(−5/2))·K_R
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 hRintbl intervalIntegrable_const
(fun σ hσ => hR σ hσ)
rwa [intervalIntegral.integral_const, smul_eq_mul] at h
```
The near-sum integral — the heart:
```lean
-- per-ρ data: δ_ρ := |ρ.1.im − T|
-- per-σ pointwise: ‖Σ‖ ≤ Σ m·(1/√((σ−β)²+δ²))
have hΣbound : ∫ σ in (-5/2 : ℝ)..3,
‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤
2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by
-- step 1: pointwise norm_sum_le + per-term norms
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 : ℂ) / (...)‖
≤ ∑ ρ ∈ 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 σ ρ] -- ‖s−ρ‖ = √((σ−β)²+(T−γ)²)
rw [mul_one_div] -- m * (1/√) = m/√
...
```
Hmm wait — hnormid needs ρ : ℂ — with ρ : {ρ : ℂ // IsNontrivialZero ρ} I apply to ρ.1 ✓.
- The integral of the RHS:
```lean
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 ρ _ => hterm_int ρ)]
apply Finset.sum_congr rfl
intro ρ _
exact intervalIntegral.integral_const_mul _ _
```
where hterm_int ρ : IntervalIntegrable (fun σ => (zeroMult ρ.1 : ℝ) * (1/√((σ−ρ.1.re)²+(T−ρ.1.im)²))) volume (−5/2) 3 — continuity: const · (1/√h) — 1/√h continuous since h > 0 — h = (σ−β)²+(T−γ)² > 0 needs (T−γ)² > 0 OR (σ−β)² > 0 — T−γ ≠ 0: since δ_ρ = |γ−T| ≥ c_clear > 0 ⟹ γ ≠ T ⟹ (T−γ)² > 0 ✓. So h ≥ (T−γ)² > 0 ✓ per ρ (needs mem_nearZerosSub for the clearance!). So hterm_int ρ needs ρ ∈ nearZerosSub T — in integral_finsetSum the hypothesis is ∀ i ∈ s, Integrable — so hterm_int takes the membership ✓.
Hmm wait — for the per-ρ facts (δ bounds), I need them per ρ ∈ nearZerosSub T — collect as a have:
```lean
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ρ
have hγ1 : Real.sqrt (n : ℝ) - 1 < ρ.1.im := by
have := abs_lt.mp hδ1
nlinarith [Real.sqrt_nonneg (n : ℝ), hTn, hTn1]
have hγ2 : ρ.1.im < Real.sqrt (n : ℝ) + 2 := by
have := abs_lt.mp hδ1
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 (√n+2))) hδge
exact ⟨hδpos, hδ1, hδge⟩
```
abs_lt.mp : |a| < b ↔ −b < a ∧ a < b ✓.
hγ1: from |γ−T| < 1: −1 < γ−T ∧ γ−T < 1: γ > T−1 ≥ √n−1 ✓ (T ≥ √n ⟹ T−1 ≥ √n−1) — nlinarith [hTn]. hγ2: γ < T+1 ≤ √n+2 ✓ nlinarith [hTn1].
Then per-ρ per-σ integrand bound via the per-zero machine:
```lean
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ρ
-- rewrite (T − γ)² = δ²
have hsq : ∀ σ : ℝ, (T - ρ.1.im) ^ 2 = |ρ.1.im - T| ^ 2 := by
intro σ
rw [← sq_abs (ρ.1.im - T)] -- hmm: |γ−T|² = (γ−T)² = (T−γ)²
ring
-- hmm — direction: want the integrand's (T−γ)² replaced by δ² with δ := |γ−T|
```
Hmm — (T−γ)² = (γ−T)² = |γ−T|²: `neg_sq (T - γ) : (-(T−γ))² = (T−γ)²` — and −(T−γ) = γ−T by ring. And sq_abs : |γ−T|² = (γ−T)². So (T−γ)² = (γ−T)² = |γ−T|² — i.e. (T−γ)² = |γ−T|²:
```lean
have hsq : (T - ρ.1.im) ^ 2 = |ρ.1.im - T| ^ 2 := by
rw [← sq_abs (ρ.1.im - T)]
ring_nf
```
(T−γ)² = |γ−T|²: rw [← sq_abs (ρ.1.im − T)]: RHS |γ−T|² → (γ−T)²: goal (T−γ)² = (γ−T)² — ring_nf closes? (T−γ)² = (γ−T)² — ring proves ✓ `by ring`. So:
```lean
rw [← sq_abs (ρ.1.im - T)]
ring -- hmm this is the tactic for the remaining goal
```
Wait the structure:
```lean
have hsq : (T - ρ.1.im) ^ 2 = |ρ.1.im - T| ^ 2 := by
rw [← sq_abs (ρ.1.im - T)]
ring
```
rw [← sq_abs] : pattern |?a|^2 → ?a^2 — the goal's RHS |γ−T|^2 → (γ−T)²: goal (T−γ)² = (γ−T)² — `ring` closes ✓.
Then the per-zero machine with δ := |γ−T|: per_zero_integral_le_two_log {β := ρ.1.re} {δ := |ρ.1.im − T|} (hβ0 : 0 < ρ.1.re := ρ.2.2.1) (hβ1 : ρ.1.re < 1 := ρ.2.2.2) (hδ := hδpos) (hδ1 : |γ−T| ≤ 1 := hδ1.le):
But — the per-zero lemma's integral is over (σ−β)² + δ² — the near-sum's integrand has (σ−ρ.1.re)² + (T−ρ.1.im)² — rewrite via hsq: ∫ 1/√((σ−β)²+(T−γ)²) = ∫ 1/√((σ−β)²+δ²) — pointwise congr (integral_congr) or just state the per-zero lemma with (T−γ)² directly and apply sq_abs INSIDE. Cleaner: state the per-zero lemma about (σ−β)² + δ² and convert the integral by integral_congr with the per-σ identity (T−γ)² = δ².
Ugh — integral_congr needs EqOn on uIcc — fine: fun σ _ => congrArg (fun X => 1/√((σ−β)²+X)) (hsq σ)... — simpler: rw [hsq] everywhere before integrating? The integrand is fun σ => 1/√((σ−β)²+(T−γ)²) — rw [hsq] at the INTEGRAL: hsq : (T−γ)² = δ² — the integral's integrand contains (T−γ)² — rw [hsq] rewrites it ✓ (it's a closed subterm, σ-free ✓). So in hper:
```lean
rw [show ∀ σ : ℝ, (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) =
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + |ρ.1.im - T| ^ 2)) from fun σ => by rw [hsq]]
```
Hmm — the integrand rewrite inside ∫ — can't rw under a binder directly... Actually you CAN: rw [hsq] rewrites the closed term (T−γ)² wherever it appears including under binders ✓ — hsq's LHS (T − ρ.1.im)^2 is σ-free ✓ so `rw [hsq]` at the goal (the integral inequality) works ✓.
So:
```lean
have hmain := per_zero_integral_le_two_log ρ.2.2.1 ρ.2.2.2 hδpos hδ1.le
-- hmain : ∫ σ in -5/2..3, 1/√((σ−β)²+δ²) ≤ 2·log(16.5/δ)
rw [hsq] at hmain ⊢??
```
Hmm — per_zero's integral has δ² from the start. The GOAL (hper's) has (T−γ)². rw [hsq] at the goal: (T−γ)² → δ² ✓ then the goal matches hmain's LHS ✓ then `exact hmain.trans (the clearance comparison)`.
The clearance comparison: 2·log(16.5/δ) ≤ 2·log(148.5·C0hat(√n+2)):
```lean
have hcmp : 2 * Real.log (16.5 / |ρ.1.im - T|) ≤
2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by
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 [h3]
exact hmain.trans hcmp
```
positivity for 0 < 16.5/δ: δ > 0 ✓ (hδpos in context — positivity uses it? 16.5/|γ−T| — |γ−T| > 0 from hδpos ✓ positivity should find it; fallback: div_pos (by norm_num) hδpos).
Then the sum assembly:
```lean
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 : ℝ) * (∫ ...)
≤ ∑ ρ ∈ 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.mul_sum]
apply Finset.sum_congr rfl
intro ρ _
ring
_ ≤ (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
```
hB0nn : 0 ≤ 2·log(148.5·C0hat(√n+2)) : log ≥ 0 ⟸ 148.5·C0hat ≥ 1 ⟸ C0hat ≥ 2... wait — C0hat(√n+2) ≥ 2 (two_le_C0hat) ⟹ 148.5·C0hat ≥ 297 ≥ 1 ✓ Real.log_nonneg ✓ by positivity? — 2·log(...) — positivity can't do log ≥ 0 without 1 ≤ argument — provide:
```lean
have hB0nn : (0 : ℝ) ≤ 2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by
have h1 : (1 : ℝ) ≤ 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) := by
have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : ℝ)] :
(1 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)
nlinarith
have h3 := Real.log_nonneg h1
linarith
```
Then the hΣbound conclusion: ∫‖Σ‖ ≤ ∫(RHS-sum) [integral_mono_on with hpt] = Σ m·∫ [hswap] ≤ B0·Z2hat [hsum] = 2·Z2hat·log — wait the final form: 2 * Z2hat T * Real.log (148.5·C0hat) vs hsum's (2·log)·Z2hat — ring-equivalent — linarith or a final calc rearrangement. I'll state hΣbound with the (2·log)·Z2hat form... no — the FINAL theorem's NI is 2 * Z2hat T * Real.log (...). Let me keep hΣbound as ≤ (2·log)·Z2hat and rearrange in the final linarith (atoms: Z2hat T, log — the products (2·log)·Z2hat vs 2·Z2hat·log — ring_nf normalizes ✓ linarith handles ✓).
The integral_mono_on for hΣbound's first step:
```lean
have h1 : ∫ σ in (-5/2 : ℝ)..3,
‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (...)‖ ≤
∫ σ in (-5/2 : ℝ)..3,
(∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))) :=
intervalIntegral.integral_mono_on hlen hΣnorm_int hRHS_int (fun σ hσ => hpt σ hσ)
-- then hswap, hsum
calc ... ≤ (2 * Real.log ...) * Z2hat T := h1.trans (hswap ▸ hsum)
```
hswap ▸ hsum: hswap : ∫ RHS-sum = Σ m·∫ — rw [hswap] at... — h1.trans: ∫‖Σ‖ ≤ ∫RHS-sum; ∫RHS-sum = Σ (hswap); Σ ≤ B0·Z2hat (hsum) — so `h1.trans (hswap.trans_le hsum)`?? — hswap : A = B — hswap.trans_le : A ≤ C ⟸ B ≤ C — `Eq.trans_le : a = b → b ≤ c → a ≤ c` ✓ hswap.trans_le hsum : ∫RHS-sum ≤ B0·Z2hat ✓ then h1.trans that ✓.
Integrability: hΣnorm_int (the complex-sum norm — continuous via the denominator machine) and hRHS_int (Finset.sum of per-term — per-term hterm_int ✓ then `Continuous.intervalIntegrable` of the sum — `continuous_finset_sum` hmm — for IntervalIntegrable of the SUM: intervalIntegral.integral_finsetSum needs per-term IntervalIntegrable for the equality hswap ✓; and for integral_mono_on's hg (RHS integrability): the sum's IntervalIntegrable — from per-term: `IntervalIntegrable.sum`? — there's `IntervalIntegrable_finset_sum`? — or prove Continuous (the sum) via continuous_finset_sum ✓ then Continuous.intervalIntegrable ✓. I'll do the Continuous route for hg:
```lean
have hRHScont : Continuous fun σ : ℝ =>
∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *
(1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by
apply continuous_finset_sum
intro ρ hρ
apply Continuous.mul continuous_const
apply Continuous.div continuous_const
· exact hsqrtCont ρ hρ -- Continuous fun σ => √((σ−β)²+(T−γ)²)
· intro σ
exact hsqrt_ne ρ hρ σ -- √(...) ≠ 0
```
where hsqrtCont: (Real.continuous_sqrt).comp (by fun_prop : Continuous fun σ => (σ−ρ.1.re)² + (T−ρ.1.im)²) and hsqrt_ne: √h ≠ 0 ⟸ h > 0 ⟸ (T−γ)² > 0 ⟸ γ ≠ T ⟸ δ > 0 (hρdata).
Hmm — fun_prop for `Continuous fun σ : ℝ => (σ - ρ.1.re)^2 + (T - ρ.1.im)^2` — polynomial ✓ fun_prop handles ✓.
continuous_finset_sum signature: `theorem continuous_finset_sum (s : Finset ι) (hf : ∀ i ∈ s, Continuous (f i)) : Continuous fun x => ∑ i ∈ s, f i x` ✓ exists (Topology/Algebra/InfiniteSum? — it's `continuous_finset_sum` in Mathlib.Topology.Algebra.BigOperators? — exists for sure; the name might be `continuous_finset_sum` ✓).
For integral_finsetSum's per-term integrability (hswap): per-term (fun σ => m * (1/√h)) — Continuous (same machine) ⟹ Continuous.intervalIntegrable ✓.
And hΣnorm_int — the norm of the complex sum:
```lean
have hΣnorm_int : IntervalIntegrable (fun σ : ℝ =>
‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /
(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) MeasureTheory.volume (-5/2) 3 := by
apply Continuous.intervalIntegrable
apply continuous_norm.comp
apply continuous_finset_sum
intro ρ hρ
apply Continuous.div continuous_const
· exact hpath.sub continuous_const
· intro σ
-- (↑σ+↑T·I) − ρ.1 ≠ 0
have hne : ((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1 ≠ 0 := by
intro h
have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h
have h1 := hzne σ
rw [hs] at h1
exact h1 ρ.2.1
exact hne σ
```
Hmm — Continuous.div's h₀ : ∀ x, g x ≠ 0 — with g := fun σ => (↑σ+↑T·I) − ρ.1 — so `intro σ` then the per-σ hne — restructure:
```lean
· intro σ h0
have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h0
exact (hzne σ) (hs ▸ ρ.2.1)
```
Cleaner: h0 : (↑σ+↑T·I) − ρ.1 = 0 — wait Continuous.div's h₀ : ∀ x, g x ≠ 0 — so intro σ; show (↑σ+↑T·I)−ρ.1 ≠ 0: intro h0; hs := sub_eq_zero.mp h0 : ↑σ+↑T·I = ρ.1; (hzne σ) : ζ(↑σ+↑T·I) ≠ 0; rw [hs] at hzne: ζ(ρ.1) ≠ 0 — exact (hzne ρ.2.1)... ρ.2.1 : riemannZeta ρ.1 = 0 ✓ contradiction ✓.
```lean
· intro σ
intro h0
have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h0
have hz := hzne σ
rw [hs] at hz
exact hz ρ.2.1
```
Hmm — `intro σ; intro h0` → `intro σ h0` ✓.
Same denominator-ne-zero for the hRcont's sum part ✓ (share a have hden : ∀ ρ ∈ nearZerosSub T, ∀ σ, (↑σ+↑T·I) − ρ.1 ≠ 0).
Wait — actually for the R-integrand continuity, the sum needs the same h₀ per term ✓ share.
Also hRintbl : IntervalIntegrable of the R-norm integrand ✓ via hRcont.intervalIntegrable.
Now the top-level assembly of hIntegral_Jlag_mid_norm_le:
```lean
-- kernel bound per σ
have hker : ∀ σ : ℝ, σ ∈ Set.Icc (-5/2 : ℝ) 3 →
‖kFun n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤ Real.exp 4 + 1 := ... (as drafted)
-- 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)
-- ∫‖Jlag‖ ≤ (e⁴+1)·∫‖logDeriv‖
have hJint : ∫ σ in (-5/2 : ℝ)..3, ‖Jlag n _‖ ≤
(Real.exp 4 + 1) * ∫ σ in (-5/2 : ℝ)..3, ‖logDeriv riemannZeta _‖ := by
have h := intervalIntegral.integral_mono_on hlen hJintbl hKLintbl (fun σ hσ => hptJ σ hσ)
rw [intervalIntegral.integral_const_mul] at h
exact h
```
Hmm — mul_le_mul (h₁ : ‖kFun‖ ≤ e⁴+1) (h₂ : ‖logDeriv‖ ≤ ‖logDeriv‖) (c0 : 0 ≤ ‖logDeriv‖) (b0 : 0 ≤ e⁴+1) : ‖kFun‖·‖logDeriv‖ ≤ (e⁴+1)·‖logDeriv‖ ✓ — h₂ := le_rfl ✓.
```lean
-- ∫‖logDeriv‖ ≤ ∫‖R‖ + ∫‖Σ‖
have hsplit : ∫ σ in (-5/2 : ℝ)..3, ‖logDeriv riemannZeta _‖ ≤
(∫ σ in (-5/2 : ℝ)..3, ‖∑ ...‖) +
(∫ σ in (-5/2 : ℝ)..3, ‖logDeriv − ∑...‖) := by
have hpt2 : ∀ σ : ℝ, σ ∈ Set.Icc (-5/2 : ℝ) 3 →
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤
‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (...)‖ +
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) - ∑ ...‖ :=
fun σ _ => norm_le_insert' _ _
have h := intervalIntegral.integral_mono_on hlen hLDintbl hsumIntbl (fun σ hσ => hpt2 σ hσ)
rw [intervalIntegral.integral_add hΣnorm_int hRnorm_int] at h
exact h
```
where hsumIntbl : IntervalIntegrable (fun σ => ‖Σ‖ + ‖R‖) := hΣnorm_int.add hRnorm_int — `IntervalIntegrable.add` ✓. And intervalIntegral.integral_add (hf : IntervalIntegrable) (hg) : ∫(f+g) = ∫f + ∫g ✓ — the pointwise sum integrand (fun σ => ‖Σ‖ + ‖R‖) ✓.
Wait — integral_add signature: `intervalIntegral.integral_add (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) : ∫ x in a..b, f x + g x ∂μ = (∫ x in a..b, f x ∂μ) + ∫ x in a..b, g x ∂μ` ✓ exists. rw [integral_add hΣnorm_int hRnorm_int] at h — h's RHS is ∫(fun σ => ‖Σ‖ + ‖R‖) — the lemma's LHS pattern ∫ x, f x + g x — matches with f := fun σ => ‖Σ‖, g := fun σ => ‖R‖ ✓ rewrites to (∫‖Σ‖) + (∫‖R‖) ✓.
Final:
```lean
calc ‖HIntegral (Jlag n) (-5/2) 3 T‖
= ‖∫ σ in (-5/2)..3, Jlag n ((σ:ℝ) + (T:ℝ)*Complex.I)‖ := rfl (HIntegral def)
_ ≤ ∫ σ in (-5/2)..3, ‖Jlag n _‖ := intervalIntegral.norm_integral_le_integral_norm hlen
_ ≤ (Real.exp 4 + 1) * ∫ σ in .., ‖logDeriv _‖ := hJint
_ ≤ (Real.exp 4 + 1) * ((∫‖Σ‖) + (∫‖R‖)) := by rw [hsplit]??
```
Hmm — HIntegral's def: HIntegral f x₁ x₂ y = ∫ x in x₁..x₂, f (x + y*I) — the point form: `(↑x + ↑y*I)` — my points: `((σ : ℝ) + (T : ℝ) * Complex.I)` ✓ — so HIntegral (Jlag n) (-5/2) 3 T = ∫ σ in -5/2..3, Jlag n (↑σ + ↑T*I) — DEFEQ (unfold HIntegral) ✓ — the calc's first step `= ... := rfl`? — unfold needed: `by unfold HIntegral` — or just write the calc starting from the norm-integral directly with a leading `by unfold HIntegral; exact ...`? Cleaner:
```lean
unfold HIntegral
calc ‖∫ σ in (-5/2 : ℝ)..(3 : ℝ), Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖
≤ ∫ σ in (-5/2 : ℝ)..(3 : ℝ), ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=
intervalIntegral.norm_integral_le_integral_norm hlen
...
```
Wait — HIntegral's point: `f (x + y * I)` with x y : ℝ — `↑x + ↑y * I` ✓ same as mine ✓.
Hmm — does `unfold HIntegral` work at the goal ‖HIntegral (Jlag n) (-5/2) 3 T‖ ≤ ...? — unfolds to ‖∫ x in -5/2..3, Jlag n (↑x + ↑T*I)‖ ≤ ... ✓.
Then:
```lean
_ ≤ (Real.exp 4 + 1) * ∫ σ in (-5/2 : ℝ)..(3 : ℝ),
‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := hJint
_ ≤ (Real.exp 4 + 1) * ((∫ σ in .., ‖Σ‖) + (∫ σ in .., ‖R‖)) := by
nlinarith? -- mul_le_mul_of_nonneg_left hsplit (e⁴+1 ≥ 0)
exact mul_le_mul_of_nonneg_left hsplit (by positivity)
_ ≤ (Real.exp 4 + 1) * ((2 * Real.log (148.5 * C0hat (√n+2))) * Z2hat T +
(3 - -5/2) * (10.5 * Real.log (T + 2) + 48)) :=
mul_le_mul_of_nonneg_left (add_le_add hΣbound hRint) (by positivity)
_ = (Real.exp 4 + 1) * (2 * Z2hat T * Real.log (148.5 * C0hat (√n+2)) +
(3 - -5/2) * (10.5 * Real.log (T + 2) + 48)) := by ring_nf
```
The last: (2·log)·Z2hat vs 2·Z2hat·log — ring/ring_nf ✓ — hmm — goal: (e⁴+1)*((2*log)*Z2hat + X) = (e⁴+1)*(2*Z2hat*log + X) — `by ring` ✓ (atoms: log, Z2hat T, X-components — ring treats log(148.5·C0hat...) as atom ✓ ring handles the commuted products ✓).
positivity for 0 ≤ e⁴+1: exp_pos ✓ positivity ✓.
For hsplit's mul: mul_le_mul_of_nonneg_left hsplit (0 ≤ e⁴+1) : (e⁴+1)·(∫‖logDeriv‖) ≤ (e⁴+1)·((∫‖Σ‖)+(∫‖R‖)) ✓ — matches the calc's `_ ≤ (e⁴+1)*((∫‖Σ‖)+(∫‖R‖))` ✓.
Now — the missing continuity/integrability pieces list for the top theorem:
- hpath ✓ (fun_prop)
- hJcont → hcontJ → hcontG → hJintbl (IntervalIntegrable ‖Jlag‖)
- hLDintbl : IntervalIntegrable ‖logDeriv‖ — from continuousAt_logDeriv_zeta machine
- hΣnorm_int : IntervalIntegrable ‖Σ‖ (the complex-sum norm — denominator machine)
- hRnorm_int : IntervalIntegrable ‖R‖ = ‖logDeriv − Σ‖ — continuous: sub of (logDeriv-cont, sum-cont) + norm
- hKLintbl : IntervalIntegrable (fun σ => (e⁴+1)·‖logDeriv‖) := hLDintbl.const_mul? — `IntervalIntegrable.const_mul`? or via Continuous: continuous_const.mul hLDcont ✓ then intervalIntegrable. Use the Continuous route: hKLcont := continuous_const.mul hLDcont; hKLintbl := hKLcont.intervalIntegrable _ _.
So I need CONTINUOUS versions: hLDcont : Continuous fun σ => ‖logDeriv ζ (↑σ+↑T·I)‖ := continuous_norm.comp (logDeriv-path-continuity). The logDeriv path continuity:
```lean
have hLDc : Continuous fun σ : ℝ => logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) := by
rw [continuous_iff_continuousAt]
intro σ
have hs1 : ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := hne1-shared
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 (hs1 σ) (hzne σ)) hf
```
hne1-shared : ∀ σ, (↑σ+↑T·I) ≠ 1 := fun σ => ... (the im argument).
The Jlag path continuity hJcont (as before, using kFun_differentiableAt + logDeriv) → hcontJ via the comp pattern → hcontG.
And the sum continuity hΣcont : Continuous fun σ => Σ_ρ (zeroMult ρ.1:ℶ)/((↑σ+↑T·I)−ρ.1) — the continuous_finset_sum + Continuous.div + hden.
And hRcont := continuous_norm.comp (hLDc'.sub hΣcont) where hLDc' : Continuous fun σ => logDeriv ζ (↑σ+↑T·I) — WITHOUT norm (the sub needs the un-normed): hRcont : Continuous fun σ => ‖logDeriv _ − Σ‖ = continuous_norm.comp (hLDc.sub hΣcont) ✓.
And hΣnorm_cont : Continuous fun σ => ‖Σ‖ := continuous_norm.comp hΣcont ✓.
OK. This is a hefty but mechanical file section. Also the per-ρ integrand continuity htermcont:
```lean
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ρ
apply Continuous.mul continuous_const
apply Continuous.div continuous_const
· exact Real.continuous_sqrt.comp (by fun_prop :
Continuous fun σ : ℝ => (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)
· intro σ
have h1 : (0 : ℝ) < (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by
have h2 : (0 : ℝ) < (T - ρ.1.im) ^ 2 := by
apply sq_pos_of_ne_zero
intro h3
rw [show (T - ρ.1.im) = 0 → T = ρ.1.im from sub_eq_zero.mp, ...]
positivity
exact ne_of_gt (Real.sqrt_pos.mpr h1)
```
Hmm — sq_pos_of_ne_zero (h : a ≠ 0) : 0 < a^2 ✓ exists. T − γ ≠ 0: from δ := |γ−T| > 0: |γ−T| > 0 ⟹ γ−T ≠ 0 (abs_pos) ⟹ T−γ ≠ 0 ✓:
```lean
have h2 : (0 : ℝ) < (T - ρ.1.im) ^ 2 := by
have h3 : ρ.1.im - T ≠ 0 := abs_pos.mp hδpos
have h4 : T - ρ.1.im ≠ 0 := by
intro h5
apply h3
linarith [h5] -- γ − T = −(T−γ) = 0
exact sq_pos_of_ne_zero h4
nlinarith? -- (σ−β)² ≥ 0 + (T−γ)² > 0 ⟹ sum > 0
exact add_pos_of_nonneg_of_pos (sq_nonneg _) h2
```
h3 : γ − T ≠ 0 := abs_pos.mp hδpos ✓ (abs_pos : 0 < |a| ↔ a ≠ 0). h4 : T−γ ≠ 0: intro h5: T−γ = 0; then γ−T = 0 by linarith ✓ (or sub_eq_zero.mp h5 : T = γ → γ − T = 0 by linarith/rw).
Then 1/√h ≠ 0: √h > 0 ⟹ √h ≠ 0 (ne_of_gt) ⟹ 1/√h... — Continuous.div's h₀ is about the DENOMINATOR √h ≠ 0 ✓ ne_of_gt (Real.sqrt_pos.mpr h1) ✓.
And hterm_int for integral_finsetSum := (htermcont ρ hρ).intervalIntegrable _ _.
And hRHScont (the sum): continuous_finset_sum with per-term htermcont ✓ — wait — the sum's per-term functions must match: `fun σ => (zeroMult ρ.1 : ℝ) * (1/√((σ−ρ.1.re)²+(T−ρ.1.im)²))` ✓ same as htermcont ✓.
NOW — one more piece: the hswap step uses integral_finsetSum which needs per-term IntervalIntegrable of the EXACT summand functions `fun σ => (zeroMult ρ.1:ℝ) * (1/Real.sqrt ((σ−ρ.1.re)^2+(T−ρ.1.im)^2))` ✓ htermcont.intervalIntegrable.
And the hswap sum-congr: ∫ (fun σ => m*(1/√h)) σ... integral_const_mul (r : 𝕜) (f : ℝ → 𝕜) : ∫ x in a..b, r * f x = r * ∫ x in a..b, f x ✓ per-ρ: (zeroMult ρ.1 : ℝ) * ∫ 1/√h ✓ — so after integral_finsetSum, the RHS is Σ_ρ ∫σ m·(1/√h) dσ = Σ_ρ m·∫σ 1/√h dσ via sum_congr with integral_const_mul ✓.
Phew. Also — the `classical` tactic at the start (for nearZerosSub decidability) ✓ (used in 6-c-ii ✓).
Let me now also define the arcsinh machine carefully (lemma 1). Full statement:
```lean
/-- **The arcsinh FTC machine** (6-c-iv core): the per-zero horizontal
segment integral — the direct antiderivative
F(σ) = log((σ−β) + √((σ−β)²+δ²)) has F′ = 1/√(·) exactly (Real.arcsinh
does not exist here). -/
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_abs_le (σ - β)
have h5 : (0 : ℝ) < Real.sqrt ((σ - β) ^ 2 + δ ^ 2) + (σ - β) := by linarith [h1, h4]
linarith [h5]
```
Hmm — h5 : 0 < √h + (σ−β) — then goal 0 < (σ−β) + √h — linarith [h5] (commuted sum — linarith handles add_comm? — the atoms are √h and (σ−β) — goal (σ−β)+√h > 0 from √h+(σ−β) > 0 — linarith normalizes ✓).
Wait h4 : -(σ−β) ≤ |σ−β| and h1 : |σ−β| < √h: −(σ−β) < √h ⟹ 0 < √h + (σ−β) ✓ linarith.
```lean
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)
convert h2b using 1
ring
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]
ring
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 σ)))
```
Hmm — concerns:
(a) `(hasDerivAt_id.sub_const β)` — hasDerivAt_id : HasDerivAt id 1 ?x — the x implicit? `theorem hasDerivAt_id (x : 𝕜) : HasDerivAt id 1 x` — x explicit. `(hasDerivAt_id σ).sub_const β : HasDerivAt (fun x => x − β) 1 σ` ✓ — the function `fun x => x − β` vs my `fun σ => σ − β` ✓ alpha-same.
(b) h2a's derivative: HasDerivAt.pow gives `↑2 * (σ−β)^(2−1) * 1` — h2b's convert: goal `HasDerivAt (fun σ => (σ−β)^2+δ^2) (2*(σ−β)) σ` — convert h2b using 1: function parts defeq (h2b's function: fun x => (x−β)^2 + δ^2 ✓), derivative: `↑2 * (σ−β)^1 * 1 = 2*(σ−β)` — `ring` ✓. But — will `convert h2b using 1` produce the derivative equation in a ring-provable form? It should produce `2 * (σ−β) = ↑2 * (σ−β)^1 * 1` or the reverse — ring either way ✓.
Hmm — HasDerivAt.pow's exact statement: `theorem HasDerivAt.pow (hf : HasDerivAt f f' x) (n : ℕ) : HasDerivAt (fun y => f y ^ n) ((n : 𝕜) * f x ^ (n - 1) * f') x`? — I think it's `(n : 𝕜) * (f x)^(n−1) * f'` — hmm — or is it `n * f x ^ (n - 1) * f'` with n as ℕ cast ✓ whatever — ring handles numeral-cast forms? — `↑2 * (σ−β)^1 * 1` — ring normalizes casts of numerals ✓.
(c) h6's convert + field_simp + ring: goal after convert: `(g σ)/√h = 1 + 2(σ−β)/(2√h)` (or reversed) — field_simp [hsqrt0]: clears √h denominators: LHS·... — expect to leave a polynomial identity in (σ−β), √h — but there's √h²?? — field_simp might produce `((σ−β)+√h)*2 = 2√h + 2(σ−β)`?? — hmm: (g/√h) = 1 + 2(σ−β)/(2√h): RHS = (2√h + 2(σ−β))/(2√h): so g/√h = (2√h+2(σ−β))/(2√h) ⟺ g·2√h = (2√h+2(σ−β))·√h ⟺ 2·g = 2√h + 2(σ−β) (after dividing by √h — field_simp keeps the relation g·2√h = (2√h + 2(σ−β))√h — then ring can't simplify √h·√h... — field_simp is supposed to clear ALL denominators: multiply both sides by 2√h: g·2√h... wait — LHS g/√h · 2√h = 2g; RHS [1 + 2(σ−β)/(2√h)]·2√h = 2√h + 2(σ−β). So field_simp leaves `2·g = 2√h + 2(σ−β)` ⟺ g = √h + (σ−β) where g := (σ−β)+√h — ring closes ✓ (no √h² appears ✓). If field_simp instead produces the un-cleared form, ring still closes ✓.
(d) h7's convert + field_simp + ring: goal `1/√h = (g/√h)/g` (or reversed): field_simp [hsqrt0, hg0]: multiply by √h·g: g·g?? — (g/√h)/g · (√h·g) = g; LHS (1/√h)·(√h·g) = g. So leaves `g = g` — closed by field_simp itself?? — or `ring`. If field_simp fully closes, the trailing `ring` errors. Hmm. To be safe against both outcomes: use `field_simp [hsqrt0, hg0]` ALONE first; if "no goals" — hmm no: `convert h7 using 1; field_simp [hsqrt0, hg0]; ring` — if field_simp closes, ring fails with "no goals". The error message will tell me and I drop the ring. Alternatively use `try ring`: `field_simp [hsqrt0, hg0]; try ring`?? — `try` swallows the no-goals... actually `ring` with no goals — the tactic FAILS ("no goals to be solved") — wrapping in `try` makes it succeed-vacuously?? — no — `try tac` runs tac and ignores FAILURE — if there are no goals, the enclosing block is already done — `try ring` is harmless?? — hmm, actually when there are no goals, ANY tactic including try errors?? No — `try ring` with no goals: try catches the failure ✓ fine. But cleaner to avoid: after convert, the goal is an equation — field_simp USUALLY leaves a ring-goal per the banked gotcha ("field_simp often closes goals (trailing ring errors — banked 4×)" — meaning field_simp closed them and ring errored!). The banked pattern suggests field_simp; ring is RISKY either way. Banked alternative (session-038): "div_add_div + div_eq_div_iff + ring as the always-works fraction pattern".
Deterministic alternative for h7's derivative equation: `1/√h = (g/√h)/g`:
```lean
rw [div_div, div_eq_mul_inv, mul_inv_cancel₀ hsqrt0] -- hmm
```
Let me think: (g/√h)/g = g/(√h·g) [div_div] = (g/g)·(1/√h)?? — (g/√h)/g = g·(1/√h)/g = (1/√h)·(g/g) = (1/√h)·1 = 1/√h ✓. So:
```lean
have : (((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) /
Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) / ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) =
1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by
field_simp [hsqrt0, hg0]
rw [this] at h7??
```
Hmm — h7 : HasDerivAt (log∘g) ((g/√h)/g) σ — the convert approach: `convert h7 using 1` leaves `1/√h = (g/√h)/g` (goal direction: target-deriv = produced-deriv? convert's remaining goal: (target) = (source)?? — `convert h7 using 1` where target is my hderiv's statement (1/√h) and source h7 ((g/√h)/g): the new goal: `1 / √h = (g σ / √h) / g σ`. Then `field_simp [hsqrt0, hg0]` normalizes: it might close or leave `g·√h = √h·g` (ring/rfl). Add `ring` and adjust based on error. I'll go with field_simp; ring and adjust.
(e) integral_eq_sub_of_hasDerivAt's hderiv : ∀ x ∈ uIcc a b — I pass `fun σ _ => hderiv σ` ✓.
(f) The final FTC result: ∫ = F b − F a with F := fun σ => log(g σ) ✓ matches the statement ✓ (the lemma's f' := fun σ => 1/√h σ ✓).
Now lemma 2 (right endpoint):
```lean
theorem arcsinh_right_endpoint_le {β δ : ℝ} (hβ : β < 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, hx]
exact Real.log_le_log h1 h3
```
Real.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y^2 — the membership: (3−β)²+δ² ≤ ((3−β)+δ)² = (3−β)²+2(3−β)δ+δ² ⟺ 0 ≤ 2(3−β)δ ✓ nlinarith [hδ, hx] — needs the product (3−β)·δ ≥ 0 — nlinarith pairwise ✓ (hx, hδ).
h3: (3−β) + √ ≤ (3−β) + ((3−β)+δ) = 2(3−β)+δ ≤ 6+δ ⟺ 2(3−β) ≤ 6 ⟺ β ≥ 0?? — WAIT: 2(3−β) ≤ 6 ⟺ 3−β ≤ 3 ⟺ β ≥ 0 — but hβ : β < 1 gives β < 1, NOT 0 ≤ β! For the RIGHT endpoint I need... 3−β ≤ 3 ⟺ β ≥ 0. Hmm — the recipe says "num ≤ 2(3−β)+δ ≤ 6+δ" — this needs β ≥ 0 ✓ (zeros have re > 0). So the right endpoint lemma ALSO needs 0 < β (or β ≥ 0). Let me add (hβ0 : 0 < β) to the right endpoint lemma. nlinarith [hsqrt_le, hβ0] : (3−β)+√ ≤ 2(3−β)+δ: from hsqrt_le; then 2(3−β)+δ ≤ 6+δ: 2(3−β) ≤ 6 ⟺ β ≥ 0 ✓ hβ0. ✓
Lemma 3 (left endpoint):
```lean
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
-- rewrite (−5/2−β)² = (5/2+β)² and group −5/2−β = −(5/2+β)
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
-- u ∈ (5/2, 7/2)
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 [div_eq_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]
-- 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
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 (by positivity : (δ:ℝ)^2 ≠ 0) (by positivity : (7:ℝ)+δ ≠ 0),
Real.log_pow]
ring
-- log(1/δ) = −log δ
have hlog1 : Real.log (1 / δ) = -Real.log δ := by
rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]
-- assemble: −log g ≤ −(2 log δ − log(7+δ)) = log(7+δ) + 2·log(1/δ)
linarith [hlog, hlogid ▸ ..., hlog1]
```
Hmm — the final assemble: goal −log(g) ≤ log(7+δ) + 2·log(1/δ). Have: hlog : 2logδ − log(7+δ) ≤ log g (via hlogid ▸ hlog); hlog1 : log(1/δ) = −logδ. linarith [hlog, hlog1] with hlogid used to rewrite hlog's LHS: I'll rewrite hlog by hlogid first:
```lean
rw [hlogid] at hlog
linarith [hlog, hlog1]
```
hlog : 2·log δ − log(7+δ) ≤ log(g); goal: −log(g) ≤ log(7+δ) + 2·log(1/δ); with hlog1 : log(1/δ) = −log δ: RHS = log(7+δ) − 2·logδ; goal ⟺ −log g ≤ log(7+δ) − 2 log δ ⟺ 2 log δ − log(7+δ) ≤ log g ✓ hlog ✓ linarith.
positivity side-conditions: (δ:ℝ)^2 ≠ 0 := pow_ne_zero 2 (ne_of_gt hδ) — positivity proves 0 < δ^2 → ne' hmm — `by positivity : (0:ℝ) < δ^2` then .ne'. Let me write: `(pow_pos hδ 2).ne'`. And (7+δ ≠ 0) := (by linarith [hδ] : (0:ℝ) < 7+δ).ne'. And the hlog's positivity arg: 0 < δ²/(7+δ) := by positivity — needs 0 < δ² (pow_pos hδ 2 in context? — positivity can prove 0 < δ^2 from hδ? — positivity extensions for ^: strict needs base > 0 — from hδ in context ✓ probably; fallback div_pos (pow_pos hδ 2) (by linarith [hδ])).
Also `div_le_div_of_nonneg_left (sq_nonneg _) h2 hden : δ²/(7+δ) ≤ δ²/(u+√)` — signature: (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c) : a/c ≤ a/b — a := δ², b := u+√, c := 7+δ ✓ δ²/(7+δ) ≤ δ²/(u+√) ✓ — matches the goal after rw [hrid] ✓.
Wait — Real.sqrt_sq_eq_abs in hg_pos: √(u²) = |u| ✓ then abs_of_pos hu : |u| = u ✓ rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3 — h3 : |u| < √(u²+δ²) → after abs_of_pos: u < √ ✓.
Hmm — Real.sqrt_lt_sqrt (sq_nonneg _) h2 : √(u²) < √(u²+δ²) — the first arg: 0 ≤ u² ✓ sq_nonneg ✓.
Lemma 4 (combine + log-mono):
```lean
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
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]
```
Concerns:
- arcsinh_right_endpoint_le hβ0 hβ1 hδ — I said the right endpoint needs BOTH hβ0 (for the ≤6+δ) — signature (hβ : β < 1) earlier — NOW needs (hβ0 : 0 < β) too? — the right endpoint: (3−β) ≤ 3 ⟺ β ≥ 0 ✓ hβ0; and 3−β > 0 for the sqrt_le's positivity? — sqrt_le_iff needs 0 ≤ (3−β)+δ ✓ positivity [hδ]; and the product (3−β)·δ ≥ 0 needs 3−β ≥ 0 ⟸ β ≤ 3 ✓ from β < 1. And g3 > 0 needs 3−β > 0 ✓ β < 1. So right endpoint needs BOTH (hβ0 : 0 < β) (hβ1 : β < 1) — wait: for the nlinarith [hδ, hx] in sqrt_le: 2(3−β)δ ≥ 0: needs 3−β ≥ 0 ✓ hβ1 (β < 1 ⟹ 3−β > 2 > 0) ✓. And h3's 2(3−β) ≤ 6: β ≥ 0 ✓ hβ0. So signature (hβ0 : 0 < β) (hβ1 : β < 1) — update: hx : 0 < 3−β from hβ1; the 2(3−β) ≤ 6 from hβ0 ✓.
- h2's linarith [h3 ▸ h4, h5]: h3 : log(6+δ)+log(7+δ) = log((6+δ)(7+δ)) — h3 ▸ h4 — `▸` at term level: rewrites h4 by h3 — direction: h3 : A = B — h3 ▸ h4 rewrites occurrences of A in h4's type by B — h4 : log((6+δ)(7+δ)) ≤ log(16.5·16.5) — no A in h4 — WRONG direction: I need log(6+δ)+log(7+δ) ≤ ... — use: linarith [h3, h4, h5] — all as atom equations/inequalities ✓ linarith combines ✓ (no ▸ needed):
goal: log(6+δ) + log(7+δ) ≤ 2·log 16.5; h3 : LHS = log(prod); h4 : log(prod) ≤ log(16.5·16.5); h5 : log(16.5·16.5) = 2·log 16.5 ✓ linarith closes ✓.
- h4's positivity: 0 < (6+δ)(7+δ) — by positivity with hδ in context ✓ (6+δ > 0 from hδ... positivity needs to derive 0 < 6+δ — hδ : 0 < δ in context ✓ positivity ✓).
- h4's nlinarith [hδ, hδ1] : (6+δ)(7+δ) ≤ 16.5·16.5: expand: 42 + 13δ + δ² ≤ 272.25: needs δ² ≤ δ·δ ≤ 1·1 = 1... nlinarith pairwise: (hδ1 : δ ≤ 1)² gives δ² ≤ 1 ✓; then 42 + 13·1 + 1 = 56 ≤ 272.25 ✓ nlinarith finds ✓.
- (Real.log_mul ...).symm for h3 — the ne conditions: 6+δ ≠ 0 and 7+δ ≠ 0 — `by linarith [hδ] : (6:ℝ) + δ ≠ 0` — hmm — the goal (6:ℝ)+δ ≠ 0 — from hδ : 0 < δ: 6+δ > 0 ⟹ ≠ 0 — linarith proves ≠? — banked: "linarith proves ≠ directly" ✓ (LiAssembly banked gotcha ✓).
- h6: Real.log_div (by norm_num : (16.5:ℝ) ≠ 0) (ne_of_gt hδ) : log(16.5/δ) = log 16.5 − log δ; rw [h7] : −log δ → log(1/δ)... wait h7 : log(1/δ) = −log δ — rw [h7] rewrites log(1/δ) → −log δ — but I want the OTHER direction (−log δ → log(1/δ)) — rw [← h7] ✓. Let me redo: goal: 2·log(16.5/δ) = 2·log 16.5 + 2·log(1/δ). rw [Real.log_div ...] : LHS's log(16.5/δ) → log 16.5 − log δ: goal 2·(log16.5 − logδ) = 2·log16.5 + 2·log(1/δ). rw [← h7] : pattern −log δ → log(1/δ)?? — ← h7 rewrites occurrences of RHS of h7 (−log δ) with LHS (log(1/δ)) ✓: goal 2·(log16.5 + log(1/δ)) = 2·log16.5 + 2·log(1/δ) — hmm — wait: 2·(log16.5 − logδ) — the term −log δ is `Neg.neg (log δ)`? or `log16.5 − logδ` is HSub — ← h7's pattern `-(log δ)`: HSub.hSub (log16.5) (logδ) — is that Neg.neg? NO — a − b is Sub, not Neg. rw [← h7] would rewrite `-Real.log δ` as a NEGATION — inside `log16.5 − logδ` there's no standalone `−logδ` negation term (it's a sub). So rw [← h7] fails to find the pattern!! Fix: rw [h7] the OTHER way — transform the goal's RHS instead: the goal after log_div-rw: `2*(log16.5 − logδ) = 2*log16.5 + 2*log(1/δ)` — rw [h7] rewrites `log(1/δ)` → `−logδ` ✓ (h7's LHS log(1/δ) appears in the goal's RHS ✓): goal `2*(log16.5 − logδ) = 2*log16.5 + 2*(−logδ)` — `ring` ✓. So:
```lean
rw [Real.log_div (by norm_num) (ne_of_gt hδ), h7]
ring
```
h7 rewrites log(1/δ) → −log δ ✓ then ring: 2(log16.5 − logδ) = 2log16.5 − 2logδ ✓ closes ✓ — h7 must be proved BEFORE this rw (it's the have above ✓).
Wait — in my draft h6 the h7-rw is inside: `rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]` for h7's proof: h7 : log(1/δ) = −log δ: rw [Real.log_div ...] at goal: log(1/δ) = −log δ — log(1/δ) → log 1 − log δ: goal log 1 − log δ = −log δ — rw [Real.log_one] : 0 − log δ = −log δ — rw [zero_sub] : −log δ = −log δ rfl ✓ — rw closes ✓.
- The per_zero lemma's final form `2 * Real.log (16.5 / δ)` ✓.
Also — for hper's use, I need per_zero at δ := |γ−T|: hδ : 0 < |γ−T| (hδpos), hδ1 : |γ−T| ≤ 1 (hδ1.le) ✓.
Now — hβ0/hβ1 for ρ.1: ρ.2.2.1 : 0 < ρ.1.re ✓ ρ.2.2.2 : ρ.1.re < 1 ✓.
One more piece of §4 — lemma 5/6's `unfold HIntegral` start and the final calc. And lemma 6 (neg) cloning DL-5's conj:
```lean
theorem hIntegral_Jlag_mid_neg_norm_le (hZC ...) (same hyps) :
‖HIntegral (Jlag n) (-5/2) 3 (-T)‖ ≤ (same RHS) := by
have hT0 : (0:ℝ) < T := by ... (√n ≥ 316)
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
```
— clone DL-5 verbatim modulo coordinates ✓. Note: DL-5's `((σ : ℝ) + T * Complex.I)` — T : ℝ coerced ✓ same form ✓.
`intervalIntegral.intervalIntegral_conj` — signature: `∫ x in a..b, (starRingEnd ℂ) (f x) = (starRingEnd ℂ) (∫ x in a..b, f x)`? — DL-5 used `rw [← intervalIntegral.intervalIntegral_conj]` — ✓ same usage.
hT0 : 0 < T — from √n ≥ √100000: hsqrt316 : 316 ≤ √n? — simpler: 0 < √n (Real.sqrt_pos.mpr (by linarith [hnR])) and √n ≤ T ⟹ 0 < T ✓ linarith.
OK — NOW let me also think about whether hIntegral_Jlag_mid_norm_le's Jlag-integral equality (unfold HIntegral) works: HIntegral f x₁ x₂ y := ∫ x in x₁..x₂, f (x + y*I) — the points: `(↑x + ↑y*I)` with x y : ℝ — my written integrand `Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)` — same elaboration `↑σ + ↑T * I`?? — HIntegral's body: `f (x + y * I)` — x : ℝ, y * I — the + : needs ℂ: `↑x + ↑y * I`?? — how was it elaborated in DL-5/rectangleIntegral_Jlag_eq? — in rectangleIntegral_Jlag_eq the HIntegral form matched the RectangleIntegral def ✓ and DL-5's conj proof used `((σ : ℝ) + T * Complex.I)` ✓ so the elaborated form is `↑σ + ↑T * I`?? — hmm — in DL-5's hid2: `((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I)` — with explicit ((−T : ℝ) : ℂ)?? — they wrote `(((−T : ℝ)) : ℂ)` — hmm no: `(((−T : ℝ)) : ℂ)` vs `(↑(−T) : ℂ)`... — whatever — my forms will match DL-5's ✓ (clone exactly).
Wait — one subtlety: in HIntegral's def `f (x + y * I)` — is the elaborated point `↑x + ↑y * Complex.I` or `↑x + ↑(y) * Complex.I`? — same thing ✓.
But — when I `unfold HIntegral` at the goal ‖HIntegral (Jlag n) (-5/2) 3 T‖ ≤ ..., the integrand becomes `fun x => Jlag n (↑x + ↑T * I)` — and my subsequent haves are stated with `((σ : ℝ) + (T : ℝ) * Complex.I)` — matching ✓ (norm_integral_le_integral_norm's application will unify the integrand ✓ defeq ✓).
Hmm — actually — rectangleIntegral_Jlag_eq used `HIntegral (Jlag n) (-5/2) (2*√n) (-T)` etc. and VIntegral_norm handled the V side; the H-side norm: is there an HIntegral_norm analog? HIntegral f a b y = ∫ σ in a..b, f (↑σ+↑y·I) — no I-factor — so ‖HIntegral‖ = ‖∫‖ directly ✓ no VIntegral_norm needed ✓.
Now — writing the whole §4. It's long; let me be methodical. I'll write it in one Edit, then iterate on errors.
One more check — `intervalIntegral.integral_mono_on hlen hJintbl hKLintbl (fun σ hσ => hptJ σ hσ)` — hKLintbl : IntervalIntegrable (fun σ => (e⁴+1) * ‖logDeriv _‖) — from hLDcont: hKLcont := continuous_const.mul (continuous_norm.comp hLDc)... — hmm wait — hptJ's RHS is (e⁴+1)·‖logDeriv‖ — the hg in integral_mono_on must be the interval-integrability of THAT lambda ✓.
And hsplit's hsumIntbl : IntervalIntegrable (fun σ => ‖Σ‖ + ‖R‖) — hmm — integral_mono_on's hg — the RHS integrand (fun σ => ‖Σ σ‖ + ‖R σ‖) — from hΣnorm_cont.add hRcont ✓ .intervalIntegrable.
Naming (all inside the theorem as have's): hpath, hne1, hJcont, hcontJ, hcontG, hJintbl, hLDc, hLDcont, hLDintbl, hKLcont, hKLintbl, hΣcont, hΣnorm_cont, hΣnorm_int, hRcont, hRnorm_int, hsumcont, hsum_intbl, hker, hptJ, hJint, hpt2, hsplit, hRint, hpt, hρdata, htermcont, hRHScont, hswap, hper, hsum, hΣbound, hB0nn.
OK — write it. For hne1 (the ∀ σ, point ≠ 1):
```lean
have hne1 : ∀ σ : ℝ, ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by
intro σ h
have him := congrArg Complex.im h
simp at him
nlinarith [h10T]
```
him : T = 0 (simp computes im) — h10T : 10 ≤ T ⟹ T ≥ 10 ≠ 0 ✓ nlinarith? — him : T = 0 and 10 ≤ T — linarith ✓ (linear) — use linarith [h10T].
For hs1 inside hJcont (6-c-ii had it as re-argument — here the point's re varies with σ — the im argument works for ALL σ: point = 1 ⟹ im = T = 0 ≠ ✓).
Let me now write §4 in full.
All signatures verified. Writing §4 (6-c-iv) — the arcsinh-FTC machine, endpoint estimates, per-zero bound, and the two mid-horizontal theorems.
tool: Edit
input
{
"_raw": "{\"replace_all\":false,\"file_path\":\"D:\\\\Python\\\\Quantum\\\\research\\\\lean\\\\NguyenRH1\\\\NguyenRH1\\\\LiSideBounds.lean\",\"old_string\":\" _ = 2 * T * (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by ring\\n _ \u2264 Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := hfinal\\n\\nend NguyenRH1\",\"new_string\":\" _ = 2 * T * (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by ring\\n _ \u2264 Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := hfinal\\n\\n/-! ## 4. 6-c-iv: the mid-horizontal segment machine [\u22125/2, 3] -/\\n\\n/-- **The arcsinh FTC machine** (6-c-iv core): the direct antiderivative\\nF(\u03c3) = log((\u03c3\u2212\u03b2) + \u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2)) of 1/\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2) (Real.arcsinh does\\nnot exist here): g(\u03c3) := (\u03c3\u2212\u03b2)+\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2) > 0 (\u221ah > |\u03c3\u2212\u03b2|), and\\ng\u2032 = 1 + (\u03c3\u2212\u03b2)/\u221ah = g/\u221ah, so (log g)\u2032 = 1/\u221ah exactly. -/\\ntheorem integral_one_div_sqrt_sq_add_sq (\u03b2 \u03b4 : \u211d) (h\u03b4 : 0 < \u03b4) (a b : \u211d) :\\n \u222b \u03c3 in a..b, 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) =\\n Real.log ((b - \u03b2) + Real.sqrt ((b - \u03b2) ^ 2 + \u03b4 ^ 2)) -\\n Real.log ((a - \u03b2) + Real.sqrt ((a - \u03b2) ^ 2 + \u03b4 ^ 2)) := by\\n have hh : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2 := fun \u03c3 =>\\n add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos h\u03b4 2)\\n have hgpos : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\\n intro \u03c3\\n have h1 : |(\u03c3 - \u03b2)| < Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\\n have h2 : (\u03c3 - \u03b2) ^ 2 < (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2 := by nlinarith [h\u03b4]\\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\\n rwa [Real.sqrt_sq_eq_abs] at h3\\n have h4 : -(\u03c3 - \u03b2) \u2264 |(\u03c3 - \u03b2)| := neg_abs_le (\u03c3 - \u03b2)\\n linarith [h1, h4]\\n have hderiv : \u2200 \u03c3 : \u211d, HasDerivAt\\n (fun \u03c3 => Real.log ((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)))\\n (1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u03c3 := by\\n intro \u03c3\\n have hh\u03c3 := hh \u03c3\\n have hsqrt0 : Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2260 0 := ne_of_gt (Real.sqrt_pos.mpr hh\u03c3)\\n have hg0 : ((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2260 0 := (hgpos \u03c3).ne'\\n have h1 : HasDerivAt (fun \u03c3 => \u03c3 - \u03b2) 1 \u03c3 := hasDerivAt_id.sub_const \u03b2\\n have h2 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) (2 * (\u03c3 - \u03b2)) \u03c3 := by\\n have h2a := (hasDerivAt_id.sub_const \u03b2).pow 2\\n have h2b := h2a.add_const (\u03b4 ^ 2)\\n convert h2b using 1\\n ring\\n have h4 : HasDerivAt (fun \u03c3 => Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\\n (2 * (\u03c3 - \u03b2) / (2 * Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))) \u03c3 :=\\n h2.sqrt hh\u03c3.ne'\\n have h5 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\\n (1 + 2 * (\u03c3 - \u03b2) / (2 * Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))) \u03c3 :=\\n h1.add h4\\n have h6 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\\n (((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) /\\n Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u03c3 := by\\n convert h5 using 1\\n field_simp [hsqrt0]\\n ring\\n have h7 := h6.log hg0\\n convert h7 using 1\\n field_simp [hsqrt0, hg0]\\n ring\\n exact intervalIntegral.integral_eq_sub_of_hasDerivAt (fun \u03c3 _ => hderiv \u03c3)\\n (by\\n apply Continuous.intervalIntegrable\\n apply Continuous.div continuous_const\\n \u00b7 exact Real.continuous_sqrt.comp (by fun_prop :\\n Continuous fun \u03c3 : \u211d => (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)\\n \u00b7 intro \u03c3\\n exact ne_of_gt (Real.sqrt_pos.mpr (hh \u03c3)))\\n\\n/-- **The right endpoint estimate** F(3) \u2264 log(6+\u03b4): \u221a((3\u2212\u03b2)\u00b2+\u03b4\u00b2) \u2264\\n(3\u2212\u03b2)+\u03b4 for 3\u2212\u03b2 > 0, so the argument is \u2264 2(3\u2212\u03b2)+\u03b4 \u2264 6+\u03b4 (0 \u2264 \u03b2). -/\\ntheorem arcsinh_right_endpoint_le {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\\n (h\u03b4 : 0 < \u03b4) :\\n Real.log ((3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2264 Real.log (6 + \u03b4) := by\\n have hx : (0 : \u211d) < 3 - \u03b2 := by linarith\\n have hsqrt_le : Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264 (3 - \u03b2) + \u03b4 := by\\n rw [Real.sqrt_le_iff]\\n exact \u27e8by positivity, by nlinarith [h\u03b4, hx]\u27e9\\n have h1 : (0 : \u211d) < (3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\\n have h2 := Real.sqrt_nonneg ((3 - \u03b2) ^ 2 + \u03b4 ^ 2)\\n nlinarith\\n have h3 : (3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264 6 + \u03b4 := by\\n nlinarith [hsqrt_le, h\u03b20]\\n exact Real.log_le_log h1 h3\\n\\n/-- **The left endpoint estimate** \u2212F(\u22125/2) \u2264 log(7+\u03b4) + 2\u00b7log(1/\u03b4):\\nwith u := 5/2+\u03b2 \u2208 (5/2, 7/2), the argument \u2212u+\u221a(u\u00b2+\u03b4\u00b2) rationalizes to\\n\u03b4\u00b2/(u+\u221a(u\u00b2+\u03b4\u00b2)) \u2265 \u03b4\u00b2/(7+\u03b4) > 0, so F(\u22125/2) \u2265 log(\u03b4\u00b2/(7+\u03b4)) =\\n2\u00b7log \u03b4 \u2212 log(7+\u03b4). -/\\ntheorem arcsinh_left_endpoint_le {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\\n (h\u03b4 : 0 < \u03b4) :\\n -Real.log ((-5 / 2 - \u03b2) + Real.sqrt ((-5 / 2 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2264\\n Real.log (7 + \u03b4) + 2 * Real.log (1 / \u03b4) := by\\n have hu : (0 : \u211d) < 5 / 2 + \u03b2 := by linarith\\n have hsq : (-5 / 2 - \u03b2) ^ 2 = (5 / 2 + \u03b2) ^ 2 := by ring\\n have hneg : (-5 / 2 : \u211d) - \u03b2 = -(5 / 2 + \u03b2) := by ring\\n rw [hsq, hneg]\\n set u := 5 / 2 + \u03b2 with hu_def\\n have hu2 : u < 7 / 2 := by rw [hu_def]; linarith\\n have hsqrt_pos : (0 : \u211d) < Real.sqrt (u ^ 2 + \u03b4 ^ 2) :=\\n Real.sqrt_pos.mpr (add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos h\u03b4 2))\\n have hg_pos : (0 : \u211d) < -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\\n have h1 : u < Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\\n have h2 : u ^ 2 < u ^ 2 + \u03b4 ^ 2 := by nlinarith [h\u03b4]\\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\\n rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3\\n linarith\\n -- the rationalization: \u2212u + \u221a = \u03b4\u00b2/(u + \u221a)\\n have hrid : -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) =\\n \u03b4 ^ 2 / (u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)) := by\\n rw [div_eq_iff (ne_of_gt (by linarith [hsqrt_pos] :\\n (0 : \u211d) < u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)))]\\n have hs : (Real.sqrt (u ^ 2 + \u03b4 ^ 2)) ^ 2 = u ^ 2 + \u03b4 ^ 2 :=\\n Real.sq_sqrt (by positivity)\\n nlinarith [hs]\\n -- the denominator \u2264 7 + \u03b4\\n have hden : u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) \u2264 7 + \u03b4 := by\\n have h1 : Real.sqrt (u ^ 2 + \u03b4 ^ 2) \u2264 u + \u03b4 := by\\n rw [Real.sqrt_le_iff]\\n exact \u27e8by linarith [h\u03b4, hu.le], by nlinarith [h\u03b4, hu]\u27e9\\n nlinarith [h1, hu2]\\n -- \u03b4\u00b2/(7+\u03b4) \u2264 \u03b4\u00b2/(u+\u221a) = \u2212u+\u221a\\n have hge : \u03b4 ^ 2 / (7 + \u03b4) \u2264 -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\\n rw [hrid]\\n have h2 : (0 : \u211d) < u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by linarith [hsqrt_pos]\\n exact div_le_div_of_nonneg_left (sq_nonneg _) h2 hden\\n -- log mono + algebra: F(\u22125/2) \u2265 log(\u03b4\u00b2/(7+\u03b4)) = 2\u00b7log \u03b4 \u2212 log(7+\u03b4)\\n have hlog : Real.log (\u03b4 ^ 2 / (7 + \u03b4)) \u2264 Real.log (-u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)) :=\\n Real.log_le_log (by positivity) hge\\n have hlogid : Real.log (\u03b4 ^ 2 / (7 + \u03b4)) = 2 * Real.log \u03b4 - Real.log (7 + \u03b4) := by\\n rw [Real.log_div (pow_pos h\u03b4 2).ne' (by linarith [h\u03b4] : (7 : \u211d) + \u03b4 \u2260 0),\\n Real.log_pow]\\n ring\\n have hlog1 : Real.log (1 / \u03b4) = -Real.log \u03b4 := by\\n rw [Real.log_div one_ne_zero (ne_of_gt h\u03b4), Real.log_one, zero_sub]\\n rw [hlogid] at hlog\\n linarith [hlog, hlog1]\\n\\n/-- **The per-zero segment integral bound**: \u222b_{\u22125/2}^{3} d\u03c3/\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2)\\n\u2264 2\u00b7log(16.5/\u03b4) for 0 < \u03b2 < 1, 0 < \u03b4 \u2264 1 \u2014 the two endpoint estimates +\\nlog((6+\u03b4)(7+\u03b4)) \u2264 log(16.5\u00b2) since (6+\u03b4)(7+\u03b4) \u2264 56 \u2264 272.25. -/\\ntheorem per_zero_integral_le_two_log {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\\n (h\u03b4 : 0 < \u03b4) (h\u03b41 : \u03b4 \u2264 1) :\\n \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264\\n 2 * Real.log (16.5 / \u03b4) := by\\n have hftc := integral_one_div_sqrt_sq_add_sq \u03b2 \u03b4 h\u03b4 (-5 / 2) 3\\n have hr := arcsinh_right_endpoint_le h\u03b20 h\u03b21 h\u03b4\\n have hl := arcsinh_left_endpoint_le h\u03b20 h\u03b21 h\u03b4\\n have h1 : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264\\n Real.log (6 + \u03b4) + Real.log (7 + \u03b4) + 2 * Real.log (1 / \u03b4) := by\\n rw [hftc]\\n linarith [hr, hl]\\n -- the log-mono simplification: log(6+\u03b4) + log(7+\u03b4) \u2264 2\u00b7log 16.5\\n have h2 : Real.log (6 + \u03b4) + Real.log (7 + \u03b4) \u2264 2 * Real.log 16.5 := by\\n have h3 : Real.log (6 + \u03b4) + Real.log (7 + \u03b4) = Real.log ((6 + \u03b4) * (7 + \u03b4)) :=\\n (Real.log_mul (by linarith [h\u03b4] : (6 : \u211d) + \u03b4 \u2260 0)\\n (by linarith [h\u03b4] : (7 : \u211d) + \u03b4 \u2260 0)).symm\\n have h4 : Real.log ((6 + \u03b4) * (7 + \u03b4)) \u2264 Real.log (16.5 * 16.5) :=\\n Real.log_le_log (by positivity) (by nlinarith [h\u03b4, h\u03b41])\\n have h5 : Real.log (16.5 * 16.5) = 2 * Real.log 16.5 := by\\n rw [show (16.5 : \u211d) * 16.5 = 16.5 ^ 2 by ring, Real.log_pow]\\n ring\\n linarith [h3, h4, h5]\\n have h6 : 2 * Real.log (16.5 / \u03b4) = 2 * Real.log 16.5 + 2 * Real.log (1 / \u03b4) := by\\n have h7 : Real.log (1 / \u03b4) = -Real.log \u03b4 := by\\n rw [Real.log_div one_ne_zero (ne_of_gt h\u03b4), Real.log_one, zero_sub]\\n rw [Real.log_div (by norm_num) (ne_of_gt h\u03b4), h7]\\n ring\\n rw [h6]\\n linarith [h1, h2]\\n\\n/-- **6-c-iv (mid-horizontal [\u22125/2, 3] at height +T)**: the segment bound\\n\u2016H\u2016 \u2264 (e\u2074+1)\u00b7(2\u00b7Z\u2082(T)\u00b7log(148.5\u00b7\u0108\u2080(\u221an+2)) + 5.5\u00b7(10.5\u00b7log(T+2)+48)).\\nKernel e\u2074+1 (the ii\u2032-4 shift lemma at s := w\u22121); logDeriv split by\\nnorm_le_insert' into the near sum (per-zero arcsinh-FTC machine +\\nintegral_finsetSum + the two-unit count \u2264 Z\u2082(T)) and the tight R-bound\\n(capstone, constant in \u03c3). -/\\ntheorem hIntegral_Jlag_mid_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\\n (hNLZ : NoLowZeros) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt (n : \u211d) - 1 < \u03c1.im \u2192\\n \u03c1.im < Real.sqrt (n : \u211d) + 2 \u2192\\n 1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264 |\u03c1.im - T|)\\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\\n \u2016HIntegral (Jlag n) (-5 / 2) 3 T\u2016 \u2264\\n (Real.exp 4 + 1) *\\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\\n classical\\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\\n have h10T : (10 : \u211d) \u2264 T := by\\n have h1 : (10 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\\n rw [Real.le_sqrt (by norm_num) (by positivity)]\\n nlinarith [hnR]\\n linarith\\n have hT0 : (0 : \u211d) \u2264 T := by linarith\\n have hn1 : 1 \u2264 n := by omega\\n have hlen : (-5 / 2 : \u211d) \u2264 3 := by norm_num\\n have hC0 : (0 : \u211d) < C0hat (Real.sqrt (n : \u211d) + 2) := by\\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : \u211d)] :\\n (1 : \u211d) \u2264 Real.sqrt (n : \u211d) + 2)\\n linarith\\n have hB0nn : (0 : \u211d) \u2264 2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) := by\\n have h1 : (1 : \u211d) \u2264 148.5 * C0hat (Real.sqrt (n : \u211d) + 2) := by nlinarith [hC0]\\n have h3 := Real.log_nonneg h1\\n linarith\\n -- zero-freeness on the horizontal + the path continuity machines\\n have hzne : \u2200 \u03c3 : \u211d, riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) \u2260 0 :=\\n fun \u03c3 => zeta_ne_zero_horizontal hTwide hn1 hTn hTn1\\n have hne1 : \u2200 \u03c3 : \u211d, ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) \u2260 1 := by\\n intro \u03c3 h\\n have him := congrArg Complex.im h\\n simp at him\\n linarith [h10T]\\n have hpath : Continuous fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I) := by\\n fun_prop\\n have hLDc : Continuous fun \u03c3 : \u211d =>\\n logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\\n rw [continuous_iff_continuousAt]\\n intro \u03c3\\n have hf : ContinuousAt (fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) \u03c3 :=\\n hpath.continuousAt\\n exact ContinuousAt.comp (g := logDeriv riemannZeta)\\n (f := fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) (x := \u03c3)\\n (continuousAt_logDeriv_zeta (hne1 \u03c3) (hzne \u03c3)) hf\\n have hJcont : \u2200 \u03c3 : \u211d, ContinuousAt (Jlag n) ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\\n intro \u03c3\\n have hA := (kFun_differentiableAt (n := n) (hne1 \u03c3)).continuousAt\\n have hB := continuousAt_logDeriv_zeta (hne1 \u03c3) (hzne \u03c3)\\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\\n exact hA.mul hB.neg\\n have hcontJ : Continuous fun \u03c3 : \u211d =>\\n Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\\n rw [continuous_iff_continuousAt]\\n intro \u03c3\\n have hf : ContinuousAt (fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) \u03c3 :=\\n hpath.continuousAt\\n exact ContinuousAt.comp (g := Jlag n)\\n (f := fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) (x := \u03c3) (hJcont \u03c3) hf\\n have hcontG : Continuous fun \u03c3 : \u211d =>\\n \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := continuous_norm.comp hcontJ\\n have hJintbl : IntervalIntegrable\\n (fun \u03c3 : \u211d => \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\\n MeasureTheory.volume (-5 / 2) 3 := hcontG.intervalIntegrable _ _\\n have hLDcont : Continuous fun \u03c3 : \u211d =>\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 :=\\n continuous_norm.comp hLDc\\n have hLDintbl : IntervalIntegrable\\n (fun \u03c3 : \u211d => \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\\n MeasureTheory.volume (-5 / 2) 3 := hLDcont.intervalIntegrable _ _\\n have hKLcont : Continuous fun \u03c3 : \u211d =>\\n (Real.exp 4 + 1) * \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 :=\\n continuous_const.mul hLDcont\\n have hKLintbl : IntervalIntegrable\\n (fun \u03c3 : \u211d => (Real.exp 4 + 1) *\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\\n MeasureTheory.volume (-5 / 2) 3 := hKLcont.intervalIntegrable _ _\\n -- the near-sum denominator never vanishes on the path (else s = \u03c1 is a\\n -- zero, contra zeta_ne_zero_horizontal)\\n have hden : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\\n \u2200 \u03c3 : \u211d, ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1 \u2260 0 := by\\n intro \u03c1 _ \u03c3 h0\\n have hs : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) = \u03c1.1 := sub_eq_zero.mp h0\\n have hz := hzne \u03c3\\n rw [hs] at hz\\n exact hz \u03c1.2.1\\n have h\u03a3cont : Continuous fun \u03c3 : \u211d =>\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1) := by\\n apply continuous_finset_sum\\n intro \u03c1 h\u03c1\\n exact Continuous.div continuous_const (hpath.sub continuous_const) (hden \u03c1 h\u03c1)\\n have h\u03a3norm_cont : Continuous fun \u03c3 : \u211d =>\\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\\n continuous_norm.comp h\u03a3cont\\n have h\u03a3norm_int : IntervalIntegrable\\n (fun \u03c3 : \u211d => \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\\n MeasureTheory.volume (-5 / 2) 3 := h\u03a3norm_cont.intervalIntegrable _ _\\n have hRcont : Continuous fun \u03c3 : \u211d =>\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\\n continuous_norm.comp (hLDc.sub h\u03a3cont)\\n have hRnorm_int : IntervalIntegrable\\n (fun \u03c3 : \u211d => \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\\n MeasureTheory.volume (-5 / 2) 3 := hRcont.intervalIntegrable _ _\\n -- the per-\u03c1 data (\u03b4_\u03c1 := |\u03b3\u2212T| \u2208 [c_clear, 1))\\n have h\u03c1data : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\\n (0 : \u211d) < |\u03c1.1.im - T| \u2227 |\u03c1.1.im - T| < 1 \u2227\\n (1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2))) \u2264 |\u03c1.1.im - T| := by\\n intro \u03c1 h\u03c1\\n have h\u03b41 := mem_nearZerosSub.mp h\u03c1\\n obtain \u27e8hlo, hhi\u27e9 := abs_lt.mp h\u03b41\\n have h\u03b31 : Real.sqrt (n : \u211d) - 1 < \u03c1.1.im := by nlinarith [hTn]\\n have h\u03b32 : \u03c1.1.im < Real.sqrt (n : \u211d) + 2 := by nlinarith [hTn1]\\n have h\u03b4ge := hTwide \u03c1.1 \u03c1.2 h\u03b31 h\u03b32\\n have h\u03b4pos : (0 : \u211d) < |\u03c1.1.im - T| :=\\n lt_of_lt_of_le (one_div_pos.mpr (by positivity :\\n (0 : \u211d) < 9 * C0hat (Real.sqrt (n : \u211d) + 2))) h\u03b4ge\\n exact \u27e8h\u03b4pos, h\u03b41, h\u03b4ge\u27e9\\n -- the kernel bound per \u03c3 (the ii\u2032-4 shift lemma at s := w \u2212 1)\\n have hnT2 : (n : \u211d) \u2264 T ^ 2 := by\\n have h1 : (Real.sqrt (n : \u211d)) ^ 2 \u2264 T ^ 2 :=\\n pow_le_pow_left\u2080 (Real.sqrt_nonneg _) hTn 2\\n rwa [Real.sq_sqrt (by positivity : (0 : \u211d) \u2264 (n : \u211d))] at h1\\n have hker : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\\n \u2016kFun n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264 Real.exp 4 + 1 := by\\n intro \u03c3 h\u03c3\\n obtain \u27e8h\u03c31, h\u03c32\u27e9 := h\u03c3\\n have hre : (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1).re = \u03c3 - 1 := by simp\\n have him : (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1).im = T := by simp\\n have h1 := kFun_shift_norm_le_exp_four_add_one (n := n)\\n (s := (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1))\\n (by rw [hre]; linarith [h\u03c32]) (by rw [him]; exact hnT2)\\n rwa [sub_add_cancel] at h1\\n -- pointwise Jlag \u2264 (e\u2074+1)\u00b7\u2016logDeriv\u2016\\n have hptJ : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\\n \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\\n (Real.exp 4 + 1) * \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := by\\n intro \u03c3 h\u03c3\\n rw [Jlag_norm_eq]\\n exact mul_le_mul (hker \u03c3 h\u03c3) le_rfl (norm_nonneg _) (by positivity)\\n have hJint : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\\n (Real.exp 4 + 1) * \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := by\\n have h := intervalIntegral.integral_mono_on hlen hJintbl hKLintbl\\n (fun \u03c3 h\u03c3 => hptJ \u03c3 h\u03c3)\\n rwa [intervalIntegral.integral_const_mul] at h\\n -- the logDeriv split: \u2016logDeriv\u2016 \u2264 \u2016\u03a3\u2016 + \u2016logDeriv \u2212 \u03a3\u2016\\n have hsumcont : Continuous fun \u03c3 : \u211d =>\\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\\n h\u03a3norm_cont.add hRcont\\n have hsum_intbl : IntervalIntegrable\\n (fun \u03c3 : \u211d => \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\\n MeasureTheory.volume (-5 / 2) 3 := hsumcont.intervalIntegrable _ _\\n have hsplit : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016) +\\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016) := by\\n have hpt2 : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\\n fun \u03c3 _ => norm_le_insert' _ _\\n have h := intervalIntegral.integral_mono_on hlen hLDintbl hsum_intbl\\n (fun \u03c3 h\u03c3 => hpt2 \u03c3 h\u03c3)\\n rwa [intervalIntegral.integral_add h\u03a3norm_int hRnorm_int] at h\\n -- the R-part integral (the 5f capstone, constant in \u03c3)\\n have hR : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\\n 10.5 * Real.log (T + 2) + 48 := by\\n intro \u03c3 h\u03c3\\n obtain \u27e8h\u03c31, h\u03c32\u27e9 := h\u03c3\\n have hre : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I).re = \u03c3 := by simp\\n have him : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I).im = T := by simp\\n have h := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := T)\\n (s := ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)) hZC hZC2 hNLZ h10T\\n (by rw [hre]; exact h\u03c31) (by rw [hre]; exact h\u03c32) him (hzne \u03c3)\\n rwa [abs_of_nonneg hT0] at h\\n have hRint : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) := by\\n have h := intervalIntegral.integral_mono_on hlen hRnorm_int intervalIntegrable_const\\n (fun \u03c3 h\u03c3 => hR \u03c3 h\u03c3)\\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\\n -- the near-sum integral: the per-zero arcsinh-FTC machine + the swap\\n have hnormid : \u2200 \u03c3 : \u211d, \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\\n \u2016((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1\u2016 =\\n Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2) := by\\n intro \u03c3 \u03c1\\n have h1 : Complex.normSq (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1) =\\n (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2 := by\\n simp [Complex.normSq_apply]\\n ring\\n symm\\n rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _),\\n \u2190 Complex.normSq_eq_norm_sq]\\n exact h1.symm\\n have htermcont : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\\n Continuous fun \u03c3 : \u211d => (zeroMult \u03c1.1 : \u211d) *\\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\\n intro \u03c1 h\u03c1\\n obtain \u27e8h\u03b4pos, -, -\u27e9 := h\u03c1data \u03c1 h\u03c1\\n have hh : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2 := by\\n intro \u03c3\\n have h3 : \u03c1.1.im - T \u2260 0 := abs_pos.mp h\u03b4pos\\n have h4 : T - \u03c1.1.im \u2260 0 := by\\n intro h5\\n apply h3\\n linarith [h5]\\n exact add_pos_of_nonneg_of_pos (sq_nonneg _) (sq_pos_of_ne_zero h4)\\n apply Continuous.mul continuous_const\\n apply Continuous.div continuous_const\\n \u00b7 exact Real.continuous_sqrt.comp (by fun_prop :\\n Continuous fun \u03c3 : \u211d => (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)\\n \u00b7 intro \u03c3\\n exact ne_of_gt (Real.sqrt_pos.mpr (hh \u03c3))\\n have hpt : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2"
}
raw content_json (database row)
[{"type":"thinking","thinking":"- `Real.continuous_sqrt : Continuous (√· : ℝ → ℝ)` ✓ (Analysis/Real/Sqrt.lean:126 — and line 95 shows `sqrt.continuous` in the NNReal? — the ℝ one at 126 ✓). The first at :95 is `Real.sqrt.continuous`? Anyway — `Real.continuous_sqrt` exists ✓.\n- `neg_sq (a) : (-a)^2 = a^2` ✓ (Algebra/Ring/Commute — root namespace).\n- `sq_abs (a) : |a|^2 = a^2` ✓ @[simp] (root).\n- `Continuous.div (hf) (hg) (h₀ : ∀ x, g x ≠ 0)` ✓.\n\nAll confirmed. Now write §4. Given the size, I'll write it in two chunks: first the arcsinh-FTC machine (lemmas 1–4), build-check that alone, then the mid-horizontal bound (5–6). Actually — write the whole §4 and iterate; the error loop is ~25 s per elaboration which is fine.\n\nLet me draft the full §4 now. Points of care:\n- All `∫ σ in a..b, ... + ...` get parens.\n- The per-σ HasDerivAt chain with convert + field_simp.\n- uIcc membership for integral_eq_sub_of_hasDerivAt — hderiv : ∀ x ∈ uIcc a b — I prove ∀ σ (global), then `fun σ _ => hF σ`.\n\nLet me also double-check `hasDerivAt_id` — signature: `theorem hasDerivAt_id (x : 𝕜) : HasDerivAt id 1 x` ✓ standard.\n\n`HasDerivAt.sub_const (hf : HasDerivAt f f' x) (c : 𝕜) : HasDerivAt (fun x => f x - c) f' x` ✓ standard.\n\nFor the per-ρ norm identity: ‖(↑σ + ↑T·I) − ρ‖ = √((σ−ρ.re)² + (T−ρ.im)²):\n```lean\nhave hnormid : ∀ σ : ℝ, ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ‖ =\n Real.sqrt ((σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2) := by\n intro σ\n have h1 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ) =\n (σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n rw [← h1]\n -- ‖z‖ = √(normSq z)\n exact (Complex.norm_def _).symm?? \n```\nHmm — what IS the norm-def lemma? `Complex.norm_def : ‖z‖ = Real.sqrt (normSq z)`? or `Complex.norm_eq_sqrt_normSq`? Let me check: In Mathlib, `Complex.norm` is defined as `Real.sqrt (normSq z)` via `Complex.norm (z : ℂ) : ℝ := Real.sqrt (normSq z)`? Actually the Norm instance: `instNorm : Norm ℂ := ⟨fun z => Real.sqrt (normSq z)⟩`. So `‖z‖ = Real.sqrt (normSq z)` is rfl! There's `Complex.norm_def : ‖z‖ = Real.sqrt (normSq z)`? — I recall `Complex.norm_def (z : ℂ) : ‖z‖ = Real.sqrt (normSq z) := rfl`. If it's rfl, then `rw [← h1]` turns goal `‖z‖ = √((σ−β)²+(T−γ)²)` into `‖z‖ = √(normSq z)` — then `rfl`?? — is `‖z‖` DEFEQ `√(normSq z)`? Yes via instNorm. So `exact rfl`?? Hmm — rfl might work if the Norm instance unfolds reducibly. There's `Complex.norm_def` — let me grep. Actually — safer: `Complex.normSq_eq_norm_sq : normSq z = ‖z‖ ^ 2` — gives ‖z‖² = normSq z, then ‖z‖ = √(normSq z) via (Real.sqrt_sq (norm_nonneg)).symm-ish:\n```lean\n have h2 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ) =\n ‖(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ)‖ ^ 2 := Complex.normSq_eq_norm_sq _\n -- want ‖z‖ = √(X) where normSq z = X\n rw [← h1] at h2 -- h2 : X = ‖z‖^2 where X := (σ−β)²+(T−γ)²\n -- ‖z‖ = √X: both nonneg, squares equal\n have h3 : (0:ℝ) ≤ ‖(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ)‖ := norm_nonneg _\n have h4 : ‖(((σ : ℝ) + (T : ℝ) * Complex.I) - ρ)‖ = Real.sqrt ((σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2) := by\n rw [← h2] -- goal: ‖z‖ = √(‖z‖^2)?? no...\n```\nHmm — cleaner: `Real.sqrt_eq_iff_eq_sq (hx : 0 ≤ x) (hy : 0 ≤ y) : √x = y ↔ x = y^2`? — DL-5 used `Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)` ✓ EXISTS. So:\n```lean\n have hnormid : ‖z‖ = Real.sqrt X := by\n rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _)] -- hmm direction: √X = ‖z‖\n -- goal: √X = ‖z‖ ↔ X = ‖z‖^2\n sorry\n```\nReal.sqrt_eq_iff_eq_sq (hx : 0 ≤ x) (hy : 0 ≤ y) : Real.sqrt x = y ↔ x = y ^ 2. So:\n```lean\n symm\n rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _)]\n -- goal: X = ‖z‖^2\n rw [← Complex.normSq_eq_norm_sq]\n exact h1\n```\nHmm — goal ‖z‖ = √X; symm → √X = ‖z‖; rw [Real.sqrt_eq_iff_eq_sq hX hnorm] → goal X = ‖z‖^2; rw [← Complex.normSq_eq_norm_sq] → normSq z = ‖z‖^2?? — wait — `Complex.normSq_eq_norm_sq (z) : normSq z = ‖z‖^2` — rw [← that] at goal X = ‖z‖^2 — the ← direction: pattern ‖z‖^2 → normSq z: goal becomes X = normSq z — exact h1 (h1 : normSq z = X — hmm — need X = normSq z — h1.symm ✓). So exact h1.symm. Let me restructure:\n\n```lean\nhave hnormid : ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ‖ =\n Real.sqrt ((σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2) := by\n have h1 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ) =\n (σ - ρ.re) ^ 2 + (T - ρ.im) ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n symm\n rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _), ← Complex.normSq_eq_norm_sq]\n exact h1.symm\n```\n\nHmm — h1's simp [Complex.normSq_apply]: normSq z = z.re*z.re + z.im*z.im (normSq_apply : normSq z = z.re * z.re + z.im * z.im? — from LiContour's hD_rel line 474: `D = s.re * s.re + s.im * s.im := by rw [hD_def, Complex.normSq_apply s]` ✓). So simp [Complex.normSq_apply] turns goal into re/im form, then simp computes re/im of ((↑σ+↑T·I)−ρ): sub_re: σ − ρ.re... wait: (↑σ+↑T·I−ρ).re = (↑σ+↑T·I).re − ρ.re = σ − ρ.re ✓; im: T − ρ.im ✓. Then goal: (σ−ρ.re)*(σ−ρ.re) + (T−ρ.im)*(T−ρ.im) = (σ−ρ.re)^2 + (T−ρ.im)^2 — ring ✓ (sq vs *2 form — ring handles).\n\nThe simp call: `simp [Complex.normSq_apply]` — will simp also compute the re/im? Complex.sub_re etc. are simp lemmas ✓ default simp set includes them ✓ probably reduces fully to the ring-closable form. If not, add the explicit list. Then `ring`.\n\nNow — the FULL §4 draft. Let me write it. I'll be careful about:\n(a) parens around all integral summands.\n(b) the positivity side conditions.\n\nFor (5) hIntegral_Jlag_mid_norm_le — the full proof:\n\n```lean\ntheorem hIntegral_Jlag_mid_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\n (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →\n ρ.im < Real.sqrt (n : ℝ) + 2 → 1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)\n (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) (-5 / 2) 3 T‖ ≤\n (Real.exp 4 + 1) * (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\n classical\n have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have h10T : (10 : ℝ) ≤ T := by\n have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n linarith\n have hT0 : (0 : ℝ) ≤ T := by linarith\n have hn1 : 1 ≤ n := by omega\n have hlen : (-5 / 2 : ℝ) ≤ 3 := by norm_num\n -- the C₀ positivity facts\n have hC0 : (0 : ℝ) < C0hat (Real.sqrt (n : ℝ) + 2) := by\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : ℝ)] : (1 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)\n linarith\n -- zero-freeness on the horizontal (for continuity)\n have hzne : ∀ σ : ℝ, riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 0 :=\n fun σ => zeta_ne_zero_horizontal hTwide hn1 hTn hTn1\n -- continuity of the path integrands\n ...\n```\n\nWait — zeta_ne_zero_horizontal's hn is (1 ≤ n) ✓ and σ — its statement: riemannZeta ((σ:ℝ) + (T:ℝ)*I) ≠ 0 ✓.\n\nContinuity of ‖logDeriv‖, ‖R‖, ‖Σ‖, ‖Jlag‖ on the path — same machine as 6-c-ii but with zeta_ne_zero_horizontal:\n\n```lean\n have hJcont : ∀ σ : ℝ, ContinuousAt (Jlag n) ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n intro σ\n have hs1 : ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by\n intro h\n have him := congrArg Complex.im h\n simp at him -- T = 0\n linarith [hT0] -- T ≥ 316 ≠ 0... wait him : T = 0? (1:ℂ).im = 0 — him : (point).im = Complex.im 1 → T = 0 — linarith with h10T ✓\n have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n have hB := continuousAt_logDeriv_zeta hs1 (hzne σ)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n```\n\nHmm — him : (↑σ + ↑T·I).im = (1:ℂ).im — simp → T = 0 ✓ then linarith [h10T] ✓.\n\nFor ‖R‖ continuity: R = logDeriv ζ − Σ: \n```lean\n have hRcont : Continuous fun σ : ℝ =>\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ := by\n apply continuous_norm.comp\n apply Continuous.sub\n · -- logDeriv continuous\n rw [continuous_iff_continuousAt]\n intro σ\n have hs1 : ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := ...\n have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ := hpath.continuousAt\n exact ContinuousAt.comp (g := logDeriv riemannZeta) (f := ...) (x := σ)\n (continuousAt_logDeriv_zeta hs1 (hzne σ)) hf\n · -- the near sum continuous\n apply continuous_finset_sum\n intro ρ hρ\n apply Continuous.div continuous_const\n · -- the denominator continuous\n exact hpath.sub continuous_const\n · intro σ\n -- denominator ≠ 0: else s = ρ, ζ s = ζ ρ = 0 vs hzne\n have hne : ((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1 ≠ 0 := by\n intro h\n have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h\n have h1 := hzne σ\n rw [hs] at h1\n exact h1 ρ.2.1\n exact hne σ -- hmm, the h₀ for Continuous.div is ∀ x, g x ≠ 0\n```\n\nWait — Continuous.div (hf) (hg) (h₀ : ∀ x, g x ≠ 0) — so I need ∀ σ, (↑σ+↑T·I) − ρ.1 ≠ 0 ✓ from the hzne argument ✓.\n\n`continuous_finset_sum : (∀ i ∈ s, Continuous (f i)) → Continuous fun x => ∑ i ∈ s, f i x` ✓ exists (continuous_finset_sum s h).\n\n`hpath : Continuous fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I) := by fun_prop` ✓.\n\nFor the logDeriv branch — the ContinuousAt.comp pinned pattern ✓. Actually — I realize I can factor a small helper for the composition since it repeats: skip, inline is fine.\n\nFor ‖Σ‖ continuity: same denominator machine + norm.\n\nFor ‖Jlag‖: hJcont machine + norm (as 6-c-ii).\n\nThe kernel bound hker (as drafted above).\n\nThe R-bound pointwise:\n```lean\n have hR : ∀ σ : ℝ, σ ∈ Set.Icc (-5/2 : ℝ) 3 →\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n 10.5 * Real.log (T + 2) + 48 := by\n intro σ hσ\n obtain ⟨hσ1, hσ2⟩ := hσ\n have hre : ((σ : ℝ) + (T : ℝ) * Complex.I).re = σ := by simp [...]\n have him : ((σ : ℝ) + (T : ℝ) * Complex.I).im = T := by simp [...]\n have h := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := T)\n (s := ((σ : ℝ) + (T : ℝ) * Complex.I)) hZC hZC2 hNLZ h10T\n (by rw [hre]; exact hσ1) (by rw [hre]; exact hσ2) him (hzne σ)\n rwa [abs_of_nonneg hT0] at h\n```\n\nHmm — the capstone's bound: 10.5·log(|T|+2)+48 — rw [abs_of_nonneg hT0] at h : |T| → T ✓.\n\nThe near-sum pointwise split and per-term norm — the s in the capstone's sum is (↑σ + ↑T·I): terms (zeroMult ρ.1 : ℂ)/((↑σ+↑T·I) − ρ.1) ✓ — my ‖Σ‖ integrand matches ✓.\n\nThe integral estimates:\n```lean\n -- ∫ ‖R‖ ≤ (3−(−5/2))·K_R\n have hRint : ∫ σ in (-5/2 : ℝ)..3,\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n (3 - -5/2) * (10.5 * Real.log (T + 2) + 48) := by\n have h := intervalIntegral.integral_mono_on hlen hRintbl intervalIntegrable_const\n (fun σ hσ => hR σ hσ)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n```\n\nThe near-sum integral — the heart:\n\n```lean\n -- per-ρ data: δ_ρ := |ρ.1.im − T|\n -- per-σ pointwise: ‖Σ‖ ≤ Σ m·(1/√((σ−β)²+δ²))\n have hΣbound : ∫ σ in (-5/2 : ℝ)..3,\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n 2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by\n -- step 1: pointwise norm_sum_le + per-term norms\n have hpt : ∀ σ : ℝ, σ ∈ Set.Icc (-5/2 : ℝ) 3 →\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n intro σ _\n calc ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (...)‖\n ≤ ∑ ρ ∈ nearZerosSub T, ‖(zeroMult ρ.1 : ℂ) / (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\n norm_sum_le _ _\n _ = ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) / ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1‖ := by\n apply Finset.sum_congr rfl\n intro ρ _\n rw [norm_div]\n have h2 : ‖(zeroMult ρ.1 : ℂ)‖ = (zeroMult ρ.1 : ℝ) := by\n rw [show (zeroMult ρ.1 : ℂ) = ((zeroMult ρ.1 : ℝ) : ℂ) by push_cast; ring,\n Complex.norm_real]\n exact abs_of_nonneg (Nat.cast_nonneg _)\n rw [h2]\n _ = ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n apply Finset.sum_congr rfl\n intro ρ _\n rw [hnormid σ ρ] -- ‖s−ρ‖ = √((σ−β)²+(T−γ)²)\n rw [mul_one_div] -- m * (1/√) = m/√\n ...\n```\n\nHmm wait — hnormid needs ρ : ℂ — with ρ : {ρ : ℂ // IsNontrivialZero ρ} I apply to ρ.1 ✓.\n\n- The integral of the RHS:\n```lean\n have hswap : ∫ σ in (-5/2 : ℝ)..3,\n (∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))) =\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (∫ σ in (-5/2 : ℝ)..3, 1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n rw [intervalIntegral.integral_finsetSum (fun ρ _ => hterm_int ρ)]\n apply Finset.sum_congr rfl\n intro ρ _\n exact intervalIntegral.integral_const_mul _ _\n```\nwhere hterm_int ρ : IntervalIntegrable (fun σ => (zeroMult ρ.1 : ℝ) * (1/√((σ−ρ.1.re)²+(T−ρ.1.im)²))) volume (−5/2) 3 — continuity: const · (1/√h) — 1/√h continuous since h > 0 — h = (σ−β)²+(T−γ)² > 0 needs (T−γ)² > 0 OR (σ−β)² > 0 — T−γ ≠ 0: since δ_ρ = |γ−T| ≥ c_clear > 0 ⟹ γ ≠ T ⟹ (T−γ)² > 0 ✓. So h ≥ (T−γ)² > 0 ✓ per ρ (needs mem_nearZerosSub for the clearance!). So hterm_int ρ needs ρ ∈ nearZerosSub T — in integral_finsetSum the hypothesis is ∀ i ∈ s, Integrable — so hterm_int takes the membership ✓.\n\nHmm wait — for the per-ρ facts (δ bounds), I need them per ρ ∈ nearZerosSub T — collect as a have:\n```lean\n have hρdata : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\n (0 : ℝ) < |ρ.1.im - T| ∧ |ρ.1.im - T| < 1 ∧\n (1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2))) ≤ |ρ.1.im - T| := by\n intro ρ hρ\n have hδ1 := mem_nearZerosSub.mp hρ\n have hγ1 : Real.sqrt (n : ℝ) - 1 < ρ.1.im := by\n have := abs_lt.mp hδ1\n nlinarith [Real.sqrt_nonneg (n : ℝ), hTn, hTn1]\n have hγ2 : ρ.1.im < Real.sqrt (n : ℝ) + 2 := by\n have := abs_lt.mp hδ1\n nlinarith [hTn1]\n have hδge := hTwide ρ.1 ρ.2 hγ1 hγ2\n have hδpos : (0 : ℝ) < |ρ.1.im - T| :=\n lt_of_lt_of_le (one_div_pos.mpr (by positivity : (0:ℝ) < 9 * C0hat (√n+2))) hδge\n exact ⟨hδpos, hδ1, hδge⟩\n```\n\nabs_lt.mp : |a| < b ↔ −b < a ∧ a < b ✓.\n\nhγ1: from |γ−T| < 1: −1 < γ−T ∧ γ−T < 1: γ > T−1 ≥ √n−1 ✓ (T ≥ √n ⟹ T−1 ≥ √n−1) — nlinarith [hTn]. hγ2: γ < T+1 ≤ √n+2 ✓ nlinarith [hTn1].\n\nThen per-ρ per-σ integrand bound via the per-zero machine:\n```lean\n have hper : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\n (∫ σ in (-5/2 : ℝ)..3, 1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) ≤\n 2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by\n intro ρ hρ\n obtain ⟨hδpos, hδ1, hδge⟩ := hρdata ρ hρ\n -- rewrite (T − γ)² = δ²\n have hsq : ∀ σ : ℝ, (T - ρ.1.im) ^ 2 = |ρ.1.im - T| ^ 2 := by\n intro σ\n rw [← sq_abs (ρ.1.im - T)] -- hmm: |γ−T|² = (γ−T)² = (T−γ)²\n ring\n -- hmm — direction: want the integrand's (T−γ)² replaced by δ² with δ := |γ−T|\n```\nHmm — (T−γ)² = (γ−T)² = |γ−T|²: `neg_sq (T - γ) : (-(T−γ))² = (T−γ)²` — and −(T−γ) = γ−T by ring. And sq_abs : |γ−T|² = (γ−T)². So (T−γ)² = (γ−T)² = |γ−T|² — i.e. (T−γ)² = |γ−T|²:\n```lean\n have hsq : (T - ρ.1.im) ^ 2 = |ρ.1.im - T| ^ 2 := by\n rw [← sq_abs (ρ.1.im - T)]\n ring_nf\n```\n(T−γ)² = |γ−T|²: rw [← sq_abs (ρ.1.im − T)]: RHS |γ−T|² → (γ−T)²: goal (T−γ)² = (γ−T)² — ring_nf closes? (T−γ)² = (γ−T)² — ring proves ✓ `by ring`. So:\n```lean\n rw [← sq_abs (ρ.1.im - T)]\n ring -- hmm this is the tactic for the remaining goal\n```\nWait the structure: \n```lean\n have hsq : (T - ρ.1.im) ^ 2 = |ρ.1.im - T| ^ 2 := by\n rw [← sq_abs (ρ.1.im - T)]\n ring\n```\nrw [← sq_abs] : pattern |?a|^2 → ?a^2 — the goal's RHS |γ−T|^2 → (γ−T)²: goal (T−γ)² = (γ−T)² — `ring` closes ✓.\n\nThen the per-zero machine with δ := |γ−T|: per_zero_integral_le_two_log {β := ρ.1.re} {δ := |ρ.1.im − T|} (hβ0 : 0 < ρ.1.re := ρ.2.2.1) (hβ1 : ρ.1.re < 1 := ρ.2.2.2) (hδ := hδpos) (hδ1 : |γ−T| ≤ 1 := hδ1.le):\n\nBut — the per-zero lemma's integral is over (σ−β)² + δ² — the near-sum's integrand has (σ−ρ.1.re)² + (T−ρ.1.im)² — rewrite via hsq: ∫ 1/√((σ−β)²+(T−γ)²) = ∫ 1/√((σ−β)²+δ²) — pointwise congr (integral_congr) or just state the per-zero lemma with (T−γ)² directly and apply sq_abs INSIDE. Cleaner: state the per-zero lemma about (σ−β)² + δ² and convert the integral by integral_congr with the per-σ identity (T−γ)² = δ².\n\nUgh — integral_congr needs EqOn on uIcc — fine: fun σ _ => congrArg (fun X => 1/√((σ−β)²+X)) (hsq σ)... — simpler: rw [hsq] everywhere before integrating? The integrand is fun σ => 1/√((σ−β)²+(T−γ)²) — rw [hsq] at the INTEGRAL: hsq : (T−γ)² = δ² — the integral's integrand contains (T−γ)² — rw [hsq] rewrites it ✓ (it's a closed subterm, σ-free ✓). So in hper: \n```lean\n rw [show ∀ σ : ℝ, (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) =\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + |ρ.1.im - T| ^ 2)) from fun σ => by rw [hsq]]\n```\nHmm — the integrand rewrite inside ∫ — can't rw under a binder directly... Actually you CAN: rw [hsq] rewrites the closed term (T−γ)² wherever it appears including under binders ✓ — hsq's LHS (T − ρ.1.im)^2 is σ-free ✓ so `rw [hsq]` at the goal (the integral inequality) works ✓.\n\nSo:\n```lean\n have hmain := per_zero_integral_le_two_log ρ.2.2.1 ρ.2.2.2 hδpos hδ1.le\n -- hmain : ∫ σ in -5/2..3, 1/√((σ−β)²+δ²) ≤ 2·log(16.5/δ)\n rw [hsq] at hmain ⊢?? \n```\nHmm — per_zero's integral has δ² from the start. The GOAL (hper's) has (T−γ)². rw [hsq] at the goal: (T−γ)² → δ² ✓ then the goal matches hmain's LHS ✓ then `exact hmain.trans (the clearance comparison)`.\n\nThe clearance comparison: 2·log(16.5/δ) ≤ 2·log(148.5·C0hat(√n+2)):\n```lean\n have hcmp : 2 * Real.log (16.5 / |ρ.1.im - T|) ≤\n 2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by\n have hinv : 1 / |ρ.1.im - T| ≤ 9 * C0hat (Real.sqrt (n : ℝ) + 2) := by\n have h := one_div_le_one_div_of_le (one_div_pos.mpr (by positivity :\n (0:ℝ) < 9 * C0hat (Real.sqrt (n : ℝ) + 2))) hδge\n rwa [one_div_one_div] at h\n have h1 : 16.5 * (1 / |ρ.1.im - T|) ≤ 16.5 * (9 * C0hat (Real.sqrt (n : ℝ) + 2)) :=\n mul_le_mul_of_nonneg_left hinv (by norm_num)\n have h2 : 16.5 / |ρ.1.im - T| ≤ 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) := by\n rw [mul_one_div, show (16.5 : ℝ) * (9 * C0hat (Real.sqrt (n : ℝ) + 2)) =\n 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) by ring] at h1\n exact h1\n have h3 : Real.log (16.5 / |ρ.1.im - T|) ≤\n Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) :=\n Real.log_le_log (by positivity) h2\n linarith [h3]\n exact hmain.trans hcmp\n```\n\npositivity for 0 < 16.5/δ: δ > 0 ✓ (hδpos in context — positivity uses it? 16.5/|γ−T| — |γ−T| > 0 from hδpos ✓ positivity should find it; fallback: div_pos (by norm_num) hδpos).\n\nThen the sum assembly:\n```lean\n have hsum : ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (∫ σ in (-5/2 : ℝ)..3, 1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) ≤\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T := by\n calc ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) * (∫ ...) \n ≤ ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) := by\n apply Finset.sum_le_sum\n intro ρ hρ\n exact mul_le_mul_of_nonneg_left (hper ρ hρ) (Nat.cast_nonneg _)\n _ = (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) *\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) := by\n rw [← Finset.mul_sum]\n apply Finset.sum_congr rfl\n intro ρ _\n ring\n _ ≤ (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T :=\n mul_le_mul_of_nonneg_left (nearZerosSub_mult_sum_le hZC2 h10T) hB0nn\n```\nhB0nn : 0 ≤ 2·log(148.5·C0hat(√n+2)) : log ≥ 0 ⟸ 148.5·C0hat ≥ 1 ⟸ C0hat ≥ 2... wait — C0hat(√n+2) ≥ 2 (two_le_C0hat) ⟹ 148.5·C0hat ≥ 297 ≥ 1 ✓ Real.log_nonneg ✓ by positivity? — 2·log(...) — positivity can't do log ≥ 0 without 1 ≤ argument — provide: \n```lean\n have hB0nn : (0 : ℝ) ≤ 2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by\n have h1 : (1 : ℝ) ≤ 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) := by\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : ℝ)] :\n (1 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)\n nlinarith\n have h3 := Real.log_nonneg h1\n linarith\n```\n\nThen the hΣbound conclusion: ∫‖Σ‖ ≤ ∫(RHS-sum) [integral_mono_on with hpt] = Σ m·∫ [hswap] ≤ B0·Z2hat [hsum] = 2·Z2hat·log — wait the final form: 2 * Z2hat T * Real.log (148.5·C0hat) vs hsum's (2·log)·Z2hat — ring-equivalent — linarith or a final calc rearrangement. I'll state hΣbound with the (2·log)·Z2hat form... no — the FINAL theorem's NI is 2 * Z2hat T * Real.log (...). Let me keep hΣbound as ≤ (2·log)·Z2hat and rearrange in the final linarith (atoms: Z2hat T, log — the products (2·log)·Z2hat vs 2·Z2hat·log — ring_nf normalizes ✓ linarith handles ✓).\n\nThe integral_mono_on for hΣbound's first step:\n```lean\n have h1 : ∫ σ in (-5/2 : ℝ)..3,\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (...)‖ ≤\n ∫ σ in (-5/2 : ℝ)..3,\n (∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))) :=\n intervalIntegral.integral_mono_on hlen hΣnorm_int hRHS_int (fun σ hσ => hpt σ hσ)\n -- then hswap, hsum\n calc ... ≤ (2 * Real.log ...) * Z2hat T := h1.trans (hswap ▸ hsum)\n```\nhswap ▸ hsum: hswap : ∫ RHS-sum = Σ m·∫ — rw [hswap] at... — h1.trans: ∫‖Σ‖ ≤ ∫RHS-sum; ∫RHS-sum = Σ (hswap); Σ ≤ B0·Z2hat (hsum) — so `h1.trans (hswap.trans_le hsum)`?? — hswap : A = B — hswap.trans_le : A ≤ C ⟸ B ≤ C — `Eq.trans_le : a = b → b ≤ c → a ≤ c` ✓ hswap.trans_le hsum : ∫RHS-sum ≤ B0·Z2hat ✓ then h1.trans that ✓.\n\nIntegrability: hΣnorm_int (the complex-sum norm — continuous via the denominator machine) and hRHS_int (Finset.sum of per-term — per-term hterm_int ✓ then `Continuous.intervalIntegrable` of the sum — `continuous_finset_sum` hmm — for IntervalIntegrable of the SUM: intervalIntegral.integral_finsetSum needs per-term IntervalIntegrable for the equality hswap ✓; and for integral_mono_on's hg (RHS integrability): the sum's IntervalIntegrable — from per-term: `IntervalIntegrable.sum`? — there's `IntervalIntegrable_finset_sum`? — or prove Continuous (the sum) via continuous_finset_sum ✓ then Continuous.intervalIntegrable ✓. I'll do the Continuous route for hg:\n```lean\n have hRHScont : Continuous fun σ : ℝ =>\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n apply continuous_finset_sum\n intro ρ hρ\n apply Continuous.mul continuous_const\n apply Continuous.div continuous_const\n · exact hsqrtCont ρ hρ -- Continuous fun σ => √((σ−β)²+(T−γ)²)\n · intro σ\n exact hsqrt_ne ρ hρ σ -- √(...) ≠ 0\n```\nwhere hsqrtCont: (Real.continuous_sqrt).comp (by fun_prop : Continuous fun σ => (σ−ρ.1.re)² + (T−ρ.1.im)²) and hsqrt_ne: √h ≠ 0 ⟸ h > 0 ⟸ (T−γ)² > 0 ⟸ γ ≠ T ⟸ δ > 0 (hρdata).\n\nHmm — fun_prop for `Continuous fun σ : ℝ => (σ - ρ.1.re)^2 + (T - ρ.1.im)^2` — polynomial ✓ fun_prop handles ✓.\n\ncontinuous_finset_sum signature: `theorem continuous_finset_sum (s : Finset ι) (hf : ∀ i ∈ s, Continuous (f i)) : Continuous fun x => ∑ i ∈ s, f i x` ✓ exists (Topology/Algebra/InfiniteSum? — it's `continuous_finset_sum` in Mathlib.Topology.Algebra.BigOperators? — exists for sure; the name might be `continuous_finset_sum` ✓).\n\nFor integral_finsetSum's per-term integrability (hswap): per-term (fun σ => m * (1/√h)) — Continuous (same machine) ⟹ Continuous.intervalIntegrable ✓.\n\nAnd hΣnorm_int — the norm of the complex sum:\n```lean\n have hΣnorm_int : IntervalIntegrable (fun σ : ℝ =>\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) MeasureTheory.volume (-5/2) 3 := by\n apply Continuous.intervalIntegrable\n apply continuous_norm.comp\n apply continuous_finset_sum\n intro ρ hρ\n apply Continuous.div continuous_const\n · exact hpath.sub continuous_const\n · intro σ\n -- (↑σ+↑T·I) − ρ.1 ≠ 0\n have hne : ((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1 ≠ 0 := by\n intro h\n have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h\n have h1 := hzne σ\n rw [hs] at h1\n exact h1 ρ.2.1\n exact hne σ\n```\n\nHmm — Continuous.div's h₀ : ∀ x, g x ≠ 0 — with g := fun σ => (↑σ+↑T·I) − ρ.1 — so `intro σ` then the per-σ hne — restructure:\n```lean\n · intro σ h0\n have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h0\n exact (hzne σ) (hs ▸ ρ.2.1)\n```\nCleaner: h0 : (↑σ+↑T·I) − ρ.1 = 0 — wait Continuous.div's h₀ : ∀ x, g x ≠ 0 — so intro σ; show (↑σ+↑T·I)−ρ.1 ≠ 0: intro h0; hs := sub_eq_zero.mp h0 : ↑σ+↑T·I = ρ.1; (hzne σ) : ζ(↑σ+↑T·I) ≠ 0; rw [hs] at hzne: ζ(ρ.1) ≠ 0 — exact (hzne ρ.2.1)... ρ.2.1 : riemannZeta ρ.1 = 0 ✓ contradiction ✓.\n\n```lean\n · intro σ\n intro h0\n have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h0\n have hz := hzne σ\n rw [hs] at hz\n exact hz ρ.2.1\n```\n\nHmm — `intro σ; intro h0` → `intro σ h0` ✓.\n\nSame denominator-ne-zero for the hRcont's sum part ✓ (share a have hden : ∀ ρ ∈ nearZerosSub T, ∀ σ, (↑σ+↑T·I) − ρ.1 ≠ 0).\n\nWait — actually for the R-integrand continuity, the sum needs the same h₀ per term ✓ share.\n\nAlso hRintbl : IntervalIntegrable of the R-norm integrand ✓ via hRcont.intervalIntegrable.\n\nNow the top-level assembly of hIntegral_Jlag_mid_norm_le:\n\n```lean\n -- kernel bound per σ\n have hker : ∀ σ : ℝ, σ ∈ Set.Icc (-5/2 : ℝ) 3 →\n ‖kFun n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤ Real.exp 4 + 1 := ... (as drafted)\n -- pointwise Jlag ≤ (e⁴+1)·‖logDeriv‖\n have hptJ : ∀ σ : ℝ, σ ∈ Set.Icc (-5/2 : ℝ) 3 →\n ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\n (Real.exp 4 + 1) * ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := by\n intro σ hσ\n rw [Jlag_norm_eq]\n exact mul_le_mul (hker σ hσ) le_rfl (norm_nonneg _) (by positivity)\n -- ∫‖Jlag‖ ≤ (e⁴+1)·∫‖logDeriv‖\n have hJint : ∫ σ in (-5/2 : ℝ)..3, ‖Jlag n _‖ ≤\n (Real.exp 4 + 1) * ∫ σ in (-5/2 : ℝ)..3, ‖logDeriv riemannZeta _‖ := by\n have h := intervalIntegral.integral_mono_on hlen hJintbl hKLintbl (fun σ hσ => hptJ σ hσ)\n rw [intervalIntegral.integral_const_mul] at h\n exact h\n```\n\nHmm — mul_le_mul (h₁ : ‖kFun‖ ≤ e⁴+1) (h₂ : ‖logDeriv‖ ≤ ‖logDeriv‖) (c0 : 0 ≤ ‖logDeriv‖) (b0 : 0 ≤ e⁴+1) : ‖kFun‖·‖logDeriv‖ ≤ (e⁴+1)·‖logDeriv‖ ✓ — h₂ := le_rfl ✓.\n\n```lean\n -- ∫‖logDeriv‖ ≤ ∫‖R‖ + ∫‖Σ‖\n have hsplit : ∫ σ in (-5/2 : ℝ)..3, ‖logDeriv riemannZeta _‖ ≤\n (∫ σ in (-5/2 : ℝ)..3, ‖∑ ...‖) +\n (∫ σ in (-5/2 : ℝ)..3, ‖logDeriv − ∑...‖) := by\n have hpt2 : ∀ σ : ℝ, σ ∈ Set.Icc (-5/2 : ℝ) 3 →\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) / (...)‖ +\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) - ∑ ...‖ :=\n fun σ _ => norm_le_insert' _ _\n have h := intervalIntegral.integral_mono_on hlen hLDintbl hsumIntbl (fun σ hσ => hpt2 σ hσ)\n rw [intervalIntegral.integral_add hΣnorm_int hRnorm_int] at h\n exact h\n```\nwhere hsumIntbl : IntervalIntegrable (fun σ => ‖Σ‖ + ‖R‖) := hΣnorm_int.add hRnorm_int — `IntervalIntegrable.add` ✓. And intervalIntegral.integral_add (hf : IntervalIntegrable) (hg) : ∫(f+g) = ∫f + ∫g ✓ — the pointwise sum integrand (fun σ => ‖Σ‖ + ‖R‖) ✓.\n\nWait — integral_add signature: `intervalIntegral.integral_add (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) : ∫ x in a..b, f x + g x ∂μ = (∫ x in a..b, f x ∂μ) + ∫ x in a..b, g x ∂μ` ✓ exists. rw [integral_add hΣnorm_int hRnorm_int] at h — h's RHS is ∫(fun σ => ‖Σ‖ + ‖R‖) — the lemma's LHS pattern ∫ x, f x + g x — matches with f := fun σ => ‖Σ‖, g := fun σ => ‖R‖ ✓ rewrites to (∫‖Σ‖) + (∫‖R‖) ✓.\n\nFinal:\n```lean\n calc ‖HIntegral (Jlag n) (-5/2) 3 T‖\n = ‖∫ σ in (-5/2)..3, Jlag n ((σ:ℝ) + (T:ℝ)*Complex.I)‖ := rfl (HIntegral def)\n _ ≤ ∫ σ in (-5/2)..3, ‖Jlag n _‖ := intervalIntegral.norm_integral_le_integral_norm hlen\n _ ≤ (Real.exp 4 + 1) * ∫ σ in .., ‖logDeriv _‖ := hJint\n _ ≤ (Real.exp 4 + 1) * ((∫‖Σ‖) + (∫‖R‖)) := by rw [hsplit]?? \n```\n\nHmm — HIntegral's def: HIntegral f x₁ x₂ y = ∫ x in x₁..x₂, f (x + y*I) — the point form: `(↑x + ↑y*I)` — my points: `((σ : ℝ) + (T : ℝ) * Complex.I)` ✓ — so HIntegral (Jlag n) (-5/2) 3 T = ∫ σ in -5/2..3, Jlag n (↑σ + ↑T*I) — DEFEQ (unfold HIntegral) ✓ — the calc's first step `= ... := rfl`? — unfold needed: `by unfold HIntegral` — or just write the calc starting from the norm-integral directly with a leading `by unfold HIntegral; exact ...`? Cleaner:\n```lean\n unfold HIntegral\n calc ‖∫ σ in (-5/2 : ℝ)..(3 : ℝ), Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖\n ≤ ∫ σ in (-5/2 : ℝ)..(3 : ℝ), ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=\n intervalIntegral.norm_integral_le_integral_norm hlen\n ...\n```\n\nWait — HIntegral's point: `f (x + y * I)` with x y : ℝ — `↑x + ↑y * I` ✓ same as mine ✓.\n\nHmm — does `unfold HIntegral` work at the goal ‖HIntegral (Jlag n) (-5/2) 3 T‖ ≤ ...? — unfolds to ‖∫ x in -5/2..3, Jlag n (↑x + ↑T*I)‖ ≤ ... ✓.\n\nThen:\n```lean\n _ ≤ (Real.exp 4 + 1) * ∫ σ in (-5/2 : ℝ)..(3 : ℝ),\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := hJint\n _ ≤ (Real.exp 4 + 1) * ((∫ σ in .., ‖Σ‖) + (∫ σ in .., ‖R‖)) := by\n nlinarith? -- mul_le_mul_of_nonneg_left hsplit (e⁴+1 ≥ 0)\n exact mul_le_mul_of_nonneg_left hsplit (by positivity)\n _ ≤ (Real.exp 4 + 1) * ((2 * Real.log (148.5 * C0hat (√n+2))) * Z2hat T +\n (3 - -5/2) * (10.5 * Real.log (T + 2) + 48)) :=\n mul_le_mul_of_nonneg_left (add_le_add hΣbound hRint) (by positivity)\n _ = (Real.exp 4 + 1) * (2 * Z2hat T * Real.log (148.5 * C0hat (√n+2)) +\n (3 - -5/2) * (10.5 * Real.log (T + 2) + 48)) := by ring_nf\n```\n\nThe last: (2·log)·Z2hat vs 2·Z2hat·log — ring/ring_nf ✓ — hmm — goal: (e⁴+1)*((2*log)*Z2hat + X) = (e⁴+1)*(2*Z2hat*log + X) — `by ring` ✓ (atoms: log, Z2hat T, X-components — ring treats log(148.5·C0hat...) as atom ✓ ring handles the commuted products ✓).\n\npositivity for 0 ≤ e⁴+1: exp_pos ✓ positivity ✓.\n\nFor hsplit's mul: mul_le_mul_of_nonneg_left hsplit (0 ≤ e⁴+1) : (e⁴+1)·(∫‖logDeriv‖) ≤ (e⁴+1)·((∫‖Σ‖)+(∫‖R‖)) ✓ — matches the calc's `_ ≤ (e⁴+1)*((∫‖Σ‖)+(∫‖R‖))` ✓.\n\nNow — the missing continuity/integrability pieces list for the top theorem:\n- hpath ✓ (fun_prop)\n- hJcont → hcontJ → hcontG → hJintbl (IntervalIntegrable ‖Jlag‖)\n- hLDintbl : IntervalIntegrable ‖logDeriv‖ — from continuousAt_logDeriv_zeta machine\n- hΣnorm_int : IntervalIntegrable ‖Σ‖ (the complex-sum norm — denominator machine)\n- hRnorm_int : IntervalIntegrable ‖R‖ = ‖logDeriv − Σ‖ — continuous: sub of (logDeriv-cont, sum-cont) + norm\n- hKLintbl : IntervalIntegrable (fun σ => (e⁴+1)·‖logDeriv‖) := hLDintbl.const_mul? — `IntervalIntegrable.const_mul`? or via Continuous: continuous_const.mul hLDcont ✓ then intervalIntegrable. Use the Continuous route: hKLcont := continuous_const.mul hLDcont; hKLintbl := hKLcont.intervalIntegrable _ _.\n\nSo I need CONTINUOUS versions: hLDcont : Continuous fun σ => ‖logDeriv ζ (↑σ+↑T·I)‖ := continuous_norm.comp (logDeriv-path-continuity). The logDeriv path continuity:\n```lean\n have hLDc : Continuous fun σ : ℝ => logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro σ\n have hs1 : ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := hne1-shared\n have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ := hpath.continuousAt\n exact ContinuousAt.comp (g := logDeriv riemannZeta)\n (f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ)\n (continuousAt_logDeriv_zeta (hs1 σ) (hzne σ)) hf\n```\n\nhne1-shared : ∀ σ, (↑σ+↑T·I) ≠ 1 := fun σ => ... (the im argument).\n\nThe Jlag path continuity hJcont (as before, using kFun_differentiableAt + logDeriv) → hcontJ via the comp pattern → hcontG.\n\nAnd the sum continuity hΣcont : Continuous fun σ => Σ_ρ (zeroMult ρ.1:ℶ)/((↑σ+↑T·I)−ρ.1) — the continuous_finset_sum + Continuous.div + hden.\n\nAnd hRcont := continuous_norm.comp (hLDc'.sub hΣcont) where hLDc' : Continuous fun σ => logDeriv ζ (↑σ+↑T·I) — WITHOUT norm (the sub needs the un-normed): hRcont : Continuous fun σ => ‖logDeriv _ − Σ‖ = continuous_norm.comp (hLDc.sub hΣcont) ✓.\n\nAnd hΣnorm_cont : Continuous fun σ => ‖Σ‖ := continuous_norm.comp hΣcont ✓.\n\nOK. This is a hefty but mechanical file section. Also the per-ρ integrand continuity htermcont:\n```lean\n have htermcont : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\n Continuous fun σ : ℝ => (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n intro ρ hρ\n obtain ⟨hδpos, -, -⟩ := hρdata ρ hρ\n apply Continuous.mul continuous_const\n apply Continuous.div continuous_const\n · exact Real.continuous_sqrt.comp (by fun_prop :\n Continuous fun σ : ℝ => (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)\n · intro σ\n have h1 : (0 : ℝ) < (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by\n have h2 : (0 : ℝ) < (T - ρ.1.im) ^ 2 := by\n apply sq_pos_of_ne_zero\n intro h3\n rw [show (T - ρ.1.im) = 0 → T = ρ.1.im from sub_eq_zero.mp, ...]\n positivity\n exact ne_of_gt (Real.sqrt_pos.mpr h1)\n```\n\nHmm — sq_pos_of_ne_zero (h : a ≠ 0) : 0 < a^2 ✓ exists. T − γ ≠ 0: from δ := |γ−T| > 0: |γ−T| > 0 ⟹ γ−T ≠ 0 (abs_pos) ⟹ T−γ ≠ 0 ✓:\n```lean\n have h2 : (0 : ℝ) < (T - ρ.1.im) ^ 2 := by\n have h3 : ρ.1.im - T ≠ 0 := abs_pos.mp hδpos\n have h4 : T - ρ.1.im ≠ 0 := by\n intro h5\n apply h3\n linarith [h5] -- γ − T = −(T−γ) = 0\n exact sq_pos_of_ne_zero h4\n nlinarith? -- (σ−β)² ≥ 0 + (T−γ)² > 0 ⟹ sum > 0\n exact add_pos_of_nonneg_of_pos (sq_nonneg _) h2\n```\n\nh3 : γ − T ≠ 0 := abs_pos.mp hδpos ✓ (abs_pos : 0 < |a| ↔ a ≠ 0). h4 : T−γ ≠ 0: intro h5: T−γ = 0; then γ−T = 0 by linarith ✓ (or sub_eq_zero.mp h5 : T = γ → γ − T = 0 by linarith/rw).\n\nThen 1/√h ≠ 0: √h > 0 ⟹ √h ≠ 0 (ne_of_gt) ⟹ 1/√h... — Continuous.div's h₀ is about the DENOMINATOR √h ≠ 0 ✓ ne_of_gt (Real.sqrt_pos.mpr h1) ✓.\n\nAnd hterm_int for integral_finsetSum := (htermcont ρ hρ).intervalIntegrable _ _.\n\nAnd hRHScont (the sum): continuous_finset_sum with per-term htermcont ✓ — wait — the sum's per-term functions must match: `fun σ => (zeroMult ρ.1 : ℝ) * (1/√((σ−ρ.1.re)²+(T−ρ.1.im)²))` ✓ same as htermcont ✓.\n\nNOW — one more piece: the hswap step uses integral_finsetSum which needs per-term IntervalIntegrable of the EXACT summand functions `fun σ => (zeroMult ρ.1:ℝ) * (1/Real.sqrt ((σ−ρ.1.re)^2+(T−ρ.1.im)^2))` ✓ htermcont.intervalIntegrable.\n\nAnd the hswap sum-congr: ∫ (fun σ => m*(1/√h)) σ... integral_const_mul (r : 𝕜) (f : ℝ → 𝕜) : ∫ x in a..b, r * f x = r * ∫ x in a..b, f x ✓ per-ρ: (zeroMult ρ.1 : ℝ) * ∫ 1/√h ✓ — so after integral_finsetSum, the RHS is Σ_ρ ∫σ m·(1/√h) dσ = Σ_ρ m·∫σ 1/√h dσ via sum_congr with integral_const_mul ✓.\n\nPhew. Also — the `classical` tactic at the start (for nearZerosSub decidability) ✓ (used in 6-c-ii ✓).\n\nLet me now also define the arcsinh machine carefully (lemma 1). Full statement:\n\n```lean\n/-- **The arcsinh FTC machine** (6-c-iv core): the per-zero horizontal\nsegment integral — the direct antiderivative\nF(σ) = log((σ−β) + √((σ−β)²+δ²)) has F′ = 1/√(·) exactly (Real.arcsinh\ndoes not exist here). -/\ntheorem integral_one_div_sqrt_sq_add_sq (β δ : ℝ) (hδ : 0 < δ) (a b : ℝ) :\n ∫ σ in a..b, 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) =\n Real.log ((b - β) + Real.sqrt ((b - β) ^ 2 + δ ^ 2)) -\n Real.log ((a - β) + Real.sqrt ((a - β) ^ 2 + δ ^ 2)) := by\n have hh : ∀ σ : ℝ, (0 : ℝ) < (σ - β) ^ 2 + δ ^ 2 := fun σ =>\n add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2)\n have hgpos : ∀ σ : ℝ, (0 : ℝ) < (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n intro σ\n have h1 : |(σ - β)| < Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n have h2 : (σ - β) ^ 2 < (σ - β) ^ 2 + δ ^ 2 := by nlinarith [hδ]\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n rwa [Real.sqrt_sq_eq_abs] at h3\n have h4 : -(σ - β) ≤ |(σ - β)| := neg_abs_le (σ - β)\n have h5 : (0 : ℝ) < Real.sqrt ((σ - β) ^ 2 + δ ^ 2) + (σ - β) := by linarith [h1, h4]\n linarith [h5]\n```\n\nHmm — h5 : 0 < √h + (σ−β) — then goal 0 < (σ−β) + √h — linarith [h5] (commuted sum — linarith handles add_comm? — the atoms are √h and (σ−β) — goal (σ−β)+√h > 0 from √h+(σ−β) > 0 — linarith normalizes ✓).\n\nWait h4 : -(σ−β) ≤ |σ−β| and h1 : |σ−β| < √h: −(σ−β) < √h ⟹ 0 < √h + (σ−β) ✓ linarith.\n\n```lean\n have hderiv : ∀ σ : ℝ, HasDerivAt\n (fun σ => Real.log ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)))\n (1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by\n intro σ\n have hhσ := hh σ\n have hsqrt0 : Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hhσ)\n have hg0 : ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) ≠ 0 := (hgpos σ).ne'\n have h1 : HasDerivAt (fun σ => σ - β) 1 σ := hasDerivAt_id.sub_const β\n have h2 : HasDerivAt (fun σ => (σ - β) ^ 2 + δ ^ 2) (2 * (σ - β)) σ := by\n have h2a := (hasDerivAt_id.sub_const β).pow 2\n have h2b := h2a.add_const (δ ^ 2)\n convert h2b using 1\n ring\n have h4 : HasDerivAt (fun σ => Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n (2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=\n h2.sqrt hhσ.ne'\n have h5 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n (1 + 2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=\n h1.add h4\n have h6 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n (((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) /\n Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by\n convert h5 using 1\n field_simp [hsqrt0]\n ring\n have h7 := h6.log hg0\n convert h7 using 1\n field_simp [hsqrt0, hg0]\n ring\n exact intervalIntegral.integral_eq_sub_of_hasDerivAt (fun σ _ => hderiv σ)\n (by\n apply Continuous.intervalIntegrable\n apply Continuous.div continuous_const\n · exact Real.continuous_sqrt.comp (by fun_prop :\n Continuous fun σ : ℝ => (σ - β) ^ 2 + δ ^ 2)\n · intro σ\n exact ne_of_gt (Real.sqrt_pos.mpr (hh σ)))\n```\n\nHmm — concerns:\n(a) `(hasDerivAt_id.sub_const β)` — hasDerivAt_id : HasDerivAt id 1 ?x — the x implicit? `theorem hasDerivAt_id (x : 𝕜) : HasDerivAt id 1 x` — x explicit. `(hasDerivAt_id σ).sub_const β : HasDerivAt (fun x => x − β) 1 σ` ✓ — the function `fun x => x − β` vs my `fun σ => σ − β` ✓ alpha-same.\n\n(b) h2a's derivative: HasDerivAt.pow gives `↑2 * (σ−β)^(2−1) * 1` — h2b's convert: goal `HasDerivAt (fun σ => (σ−β)^2+δ^2) (2*(σ−β)) σ` — convert h2b using 1: function parts defeq (h2b's function: fun x => (x−β)^2 + δ^2 ✓), derivative: `↑2 * (σ−β)^1 * 1 = 2*(σ−β)` — `ring` ✓. But — will `convert h2b using 1` produce the derivative equation in a ring-provable form? It should produce `2 * (σ−β) = ↑2 * (σ−β)^1 * 1` or the reverse — ring either way ✓.\n\nHmm — HasDerivAt.pow's exact statement: `theorem HasDerivAt.pow (hf : HasDerivAt f f' x) (n : ℕ) : HasDerivAt (fun y => f y ^ n) ((n : 𝕜) * f x ^ (n - 1) * f') x`? — I think it's `(n : 𝕜) * (f x)^(n−1) * f'` — hmm — or is it `n * f x ^ (n - 1) * f'` with n as ℕ cast ✓ whatever — ring handles numeral-cast forms? — `↑2 * (σ−β)^1 * 1` — ring normalizes casts of numerals ✓.\n\n(c) h6's convert + field_simp + ring: goal after convert: `(g σ)/√h = 1 + 2(σ−β)/(2√h)` (or reversed) — field_simp [hsqrt0]: clears √h denominators: LHS·... — expect to leave a polynomial identity in (σ−β), √h — but there's √h²?? — field_simp might produce `((σ−β)+√h)*2 = 2√h + 2(σ−β)`?? — hmm: (g/√h) = 1 + 2(σ−β)/(2√h): RHS = (2√h + 2(σ−β))/(2√h): so g/√h = (2√h+2(σ−β))/(2√h) ⟺ g·2√h = (2√h+2(σ−β))·√h ⟺ 2·g = 2√h + 2(σ−β) (after dividing by √h — field_simp keeps the relation g·2√h = (2√h + 2(σ−β))√h — then ring can't simplify √h·√h... — field_simp is supposed to clear ALL denominators: multiply both sides by 2√h: g·2√h... wait — LHS g/√h · 2√h = 2g; RHS [1 + 2(σ−β)/(2√h)]·2√h = 2√h + 2(σ−β). So field_simp leaves `2·g = 2√h + 2(σ−β)` ⟺ g = √h + (σ−β) where g := (σ−β)+√h — ring closes ✓ (no √h² appears ✓). If field_simp instead produces the un-cleared form, ring still closes ✓.\n\n(d) h7's convert + field_simp + ring: goal `1/√h = (g/√h)/g` (or reversed): field_simp [hsqrt0, hg0]: multiply by √h·g: g·g?? — (g/√h)/g · (√h·g) = g; LHS (1/√h)·(√h·g) = g. So leaves `g = g` — closed by field_simp itself?? — or `ring`. If field_simp fully closes, the trailing `ring` errors. Hmm. To be safe against both outcomes: use `field_simp [hsqrt0, hg0]` ALONE first; if \"no goals\" — hmm no: `convert h7 using 1; field_simp [hsqrt0, hg0]; ring` — if field_simp closes, ring fails with \"no goals\". The error message will tell me and I drop the ring. Alternatively use `try ring`: `field_simp [hsqrt0, hg0]; try ring`?? — `try` swallows the no-goals... actually `ring` with no goals — the tactic FAILS (\"no goals to be solved\") — wrapping in `try` makes it succeed-vacuously?? — no — `try tac` runs tac and ignores FAILURE — if there are no goals, the enclosing block is already done — `try ring` is harmless?? — hmm, actually when there are no goals, ANY tactic including try errors?? No — `try ring` with no goals: try catches the failure ✓ fine. But cleaner to avoid: after convert, the goal is an equation — field_simp USUALLY leaves a ring-goal per the banked gotcha (\"field_simp often closes goals (trailing ring errors — banked 4×)\" — meaning field_simp closed them and ring errored!). The banked pattern suggests field_simp; ring is RISKY either way. Banked alternative (session-038): \"div_add_div + div_eq_div_iff + ring as the always-works fraction pattern\". \n\nDeterministic alternative for h7's derivative equation: `1/√h = (g/√h)/g`:\n```lean\n rw [div_div, div_eq_mul_inv, mul_inv_cancel₀ hsqrt0] -- hmm\n```\nLet me think: (g/√h)/g = g/(√h·g) [div_div] = (g/g)·(1/√h)?? — (g/√h)/g = g·(1/√h)/g = (1/√h)·(g/g) = (1/√h)·1 = 1/√h ✓. So:\n```lean\n have : (((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) /\n Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) / ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) =\n 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n field_simp [hsqrt0, hg0]\n rw [this] at h7?? \n```\nHmm — h7 : HasDerivAt (log∘g) ((g/√h)/g) σ — the convert approach: `convert h7 using 1` leaves `1/√h = (g/√h)/g` (goal direction: target-deriv = produced-deriv? convert's remaining goal: (target) = (source)?? — `convert h7 using 1` where target is my hderiv's statement (1/√h) and source h7 ((g/√h)/g): the new goal: `1 / √h = (g σ / √h) / g σ`. Then `field_simp [hsqrt0, hg0]` normalizes: it might close or leave `g·√h = √h·g` (ring/rfl). Add `ring` and adjust based on error. I'll go with field_simp; ring and adjust.\n\n(e) integral_eq_sub_of_hasDerivAt's hderiv : ∀ x ∈ uIcc a b — I pass `fun σ _ => hderiv σ` ✓.\n\n(f) The final FTC result: ∫ = F b − F a with F := fun σ => log(g σ) ✓ matches the statement ✓ (the lemma's f' := fun σ => 1/√h σ ✓).\n\nNow lemma 2 (right endpoint):\n```lean\ntheorem arcsinh_right_endpoint_le {β δ : ℝ} (hβ : β < 1) (hδ : 0 < δ) :\n Real.log ((3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2)) ≤ Real.log (6 + δ) := by\n have hx : (0 : ℝ) < 3 - β := by linarith\n have hsqrt_le : Real.sqrt ((3 - β) ^ 2 + δ ^ 2) ≤ (3 - β) + δ := by\n rw [Real.sqrt_le_iff]\n exact ⟨by positivity, by nlinarith [hδ, hx]⟩\n have h1 : (0 : ℝ) < (3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2) := by\n have h2 := Real.sqrt_nonneg ((3 - β) ^ 2 + δ ^ 2)\n nlinarith\n have h3 : (3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2) ≤ 6 + δ := by nlinarith [hsqrt_le, hx]\n exact Real.log_le_log h1 h3\n```\n\nReal.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y^2 — the membership: (3−β)²+δ² ≤ ((3−β)+δ)² = (3−β)²+2(3−β)δ+δ² ⟺ 0 ≤ 2(3−β)δ ✓ nlinarith [hδ, hx] — needs the product (3−β)·δ ≥ 0 — nlinarith pairwise ✓ (hx, hδ).\n\nh3: (3−β) + √ ≤ (3−β) + ((3−β)+δ) = 2(3−β)+δ ≤ 6+δ ⟺ 2(3−β) ≤ 6 ⟺ β ≥ 0?? — WAIT: 2(3−β) ≤ 6 ⟺ 3−β ≤ 3 ⟺ β ≥ 0 — but hβ : β < 1 gives β < 1, NOT 0 ≤ β! For the RIGHT endpoint I need... 3−β ≤ 3 ⟺ β ≥ 0. Hmm — the recipe says \"num ≤ 2(3−β)+δ ≤ 6+δ\" — this needs β ≥ 0 ✓ (zeros have re > 0). So the right endpoint lemma ALSO needs 0 < β (or β ≥ 0). Let me add (hβ0 : 0 < β) to the right endpoint lemma. nlinarith [hsqrt_le, hβ0] : (3−β)+√ ≤ 2(3−β)+δ: from hsqrt_le; then 2(3−β)+δ ≤ 6+δ: 2(3−β) ≤ 6 ⟺ β ≥ 0 ✓ hβ0. ✓\n\nLemma 3 (left endpoint):\n```lean\ntheorem arcsinh_left_endpoint_le {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) (hδ : 0 < δ) :\n -Real.log ((-5 / 2 - β) + Real.sqrt ((-5 / 2 - β) ^ 2 + δ ^ 2)) ≤\n Real.log (7 + δ) + 2 * Real.log (1 / δ) := by\n have hu : (0 : ℝ) < 5 / 2 + β := by linarith\n -- rewrite (−5/2−β)² = (5/2+β)² and group −5/2−β = −(5/2+β)\n have hsq : (-5 / 2 - β) ^ 2 = (5 / 2 + β) ^ 2 := by ring\n have hneg : (-5 / 2 : ℝ) - β = -(5 / 2 + β) := by ring\n rw [hsq, hneg]\n set u := 5 / 2 + β with hu_def\n -- u ∈ (5/2, 7/2)\n have hu2 : u < 7 / 2 := by rw [hu_def]; linarith\n have hsqrt_pos : (0 : ℝ) < Real.sqrt (u ^ 2 + δ ^ 2) :=\n Real.sqrt_pos.mpr (add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2))\n have hg_pos : (0 : ℝ) < -u + Real.sqrt (u ^ 2 + δ ^ 2) := by\n have h1 : u < Real.sqrt (u ^ 2 + δ ^ 2) := by\n have h2 : u ^ 2 < u ^ 2 + δ ^ 2 := by nlinarith [hδ]\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3\n linarith\n -- the rationalization: −u + √ = δ²/(u + √)\n have hrid : -u + Real.sqrt (u ^ 2 + δ ^ 2) = δ ^ 2 / (u + Real.sqrt (u ^ 2 + δ ^ 2)) := by\n rw [div_eq_iff (ne_of_gt (by linarith [hsqrt_pos] : (0:ℝ) < u + Real.sqrt (u^2+δ^2)))]\n have hs : (Real.sqrt (u ^ 2 + δ ^ 2)) ^ 2 = u ^ 2 + δ ^ 2 :=\n Real.sq_sqrt (by positivity)\n nlinarith [hs]\n -- denominator ≤ 7 + δ\n have hden : u + Real.sqrt (u ^ 2 + δ ^ 2) ≤ 7 + δ := by\n have h1 : Real.sqrt (u ^ 2 + δ ^ 2) ≤ u + δ := by\n rw [Real.sqrt_le_iff]\n exact ⟨by linarith [hδ, hu.le], by nlinarith [hδ, hu]⟩\n nlinarith [h1, hu2]\n -- δ²/(7+δ) ≤ δ²/(u+√) = −u+√\n have hge : δ ^ 2 / (7 + δ) ≤ -u + Real.sqrt (u ^ 2 + δ ^ 2) := by\n rw [hrid]\n have h2 : (0 : ℝ) < u + Real.sqrt (u ^ 2 + δ ^ 2) := by linarith [hsqrt_pos]\n exact div_le_div_of_nonneg_left (sq_nonneg _) h2 hden\n -- log mono + algebra\n have hlog : Real.log (δ ^ 2 / (7 + δ)) ≤ Real.log (-u + Real.sqrt (u ^ 2 + δ ^ 2)) :=\n Real.log_le_log (by positivity) hge\n have hlogid : Real.log (δ ^ 2 / (7 + δ)) = 2 * Real.log δ - Real.log (7 + δ) := by\n rw [Real.log_div (by positivity : (δ:ℝ)^2 ≠ 0) (by positivity : (7:ℝ)+δ ≠ 0),\n Real.log_pow]\n ring\n -- log(1/δ) = −log δ\n have hlog1 : Real.log (1 / δ) = -Real.log δ := by\n rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]\n -- assemble: −log g ≤ −(2 log δ − log(7+δ)) = log(7+δ) + 2·log(1/δ)\n linarith [hlog, hlogid ▸ ..., hlog1]\n```\n\nHmm — the final assemble: goal −log(g) ≤ log(7+δ) + 2·log(1/δ). Have: hlog : 2logδ − log(7+δ) ≤ log g (via hlogid ▸ hlog); hlog1 : log(1/δ) = −logδ. linarith [hlog, hlog1] with hlogid used to rewrite hlog's LHS: I'll rewrite hlog by hlogid first:\n```lean\n rw [hlogid] at hlog\n linarith [hlog, hlog1]\n```\nhlog : 2·log δ − log(7+δ) ≤ log(g); goal: −log(g) ≤ log(7+δ) + 2·log(1/δ); with hlog1 : log(1/δ) = −log δ: RHS = log(7+δ) − 2·logδ; goal ⟺ −log g ≤ log(7+δ) − 2 log δ ⟺ 2 log δ − log(7+δ) ≤ log g ✓ hlog ✓ linarith.\n\npositivity side-conditions: (δ:ℝ)^2 ≠ 0 := pow_ne_zero 2 (ne_of_gt hδ) — positivity proves 0 < δ^2 → ne' hmm — `by positivity : (0:ℝ) < δ^2` then .ne'. Let me write: `(pow_pos hδ 2).ne'`. And (7+δ ≠ 0) := (by linarith [hδ] : (0:ℝ) < 7+δ).ne'. And the hlog's positivity arg: 0 < δ²/(7+δ) := by positivity — needs 0 < δ² (pow_pos hδ 2 in context? — positivity can prove 0 < δ^2 from hδ? — positivity extensions for ^: strict needs base > 0 — from hδ in context ✓ probably; fallback div_pos (pow_pos hδ 2) (by linarith [hδ])).\n\nAlso `div_le_div_of_nonneg_left (sq_nonneg _) h2 hden : δ²/(7+δ) ≤ δ²/(u+√)` — signature: (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c) : a/c ≤ a/b — a := δ², b := u+√, c := 7+δ ✓ δ²/(7+δ) ≤ δ²/(u+√) ✓ — matches the goal after rw [hrid] ✓.\n\nWait — Real.sqrt_sq_eq_abs in hg_pos: √(u²) = |u| ✓ then abs_of_pos hu : |u| = u ✓ rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3 — h3 : |u| < √(u²+δ²) → after abs_of_pos: u < √ ✓.\n\nHmm — Real.sqrt_lt_sqrt (sq_nonneg _) h2 : √(u²) < √(u²+δ²) — the first arg: 0 ≤ u² ✓ sq_nonneg ✓.\n\nLemma 4 (combine + log-mono):\n```lean\ntheorem per_zero_integral_le_two_log {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)\n (hδ : 0 < δ) (hδ1 : δ ≤ 1) :\n ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤\n 2 * Real.log (16.5 / δ) := by\n have hftc := integral_one_div_sqrt_sq_add_sq β δ hδ (-5/2) 3\n have hr := arcsinh_right_endpoint_le hβ0 hβ1 hδ\n have hl := arcsinh_left_endpoint_le hβ0 hβ1 hδ\n have h1 : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤\n Real.log (6 + δ) + Real.log (7 + δ) + 2 * Real.log (1 / δ) := by\n rw [hftc]\n linarith [hr, hl]\n -- the log-mono simplification\n have h2 : Real.log (6 + δ) + Real.log (7 + δ) ≤ 2 * Real.log 16.5 := by\n have h3 : Real.log (6 + δ) + Real.log (7 + δ) = Real.log ((6 + δ) * (7 + δ)) :=\n (Real.log_mul (by linarith [hδ] : (6:ℝ)+δ ≠ 0) (by linarith [hδ] : (7:ℝ)+δ ≠ 0)).symm\n have h4 : Real.log ((6 + δ) * (7 + δ)) ≤ Real.log (16.5 * 16.5) :=\n Real.log_le_log (by positivity) (by nlinarith [hδ, hδ1])\n have h5 : Real.log (16.5 * 16.5) = 2 * Real.log 16.5 := by\n rw [show (16.5 : ℝ) * 16.5 = 16.5 ^ 2 by ring, Real.log_pow]\n ring\n linarith [h3 ▸ h4, h5]\n have h6 : 2 * Real.log (16.5 / δ) = 2 * Real.log 16.5 + 2 * Real.log (1 / δ) := by\n have h7 : Real.log (1 / δ) = -Real.log δ := by\n rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]\n rw [Real.log_div (by norm_num) (ne_of_gt hδ), h7]\n ring\n rw [h6]\n linarith [h1, h2]\n```\n\nConcerns:\n- arcsinh_right_endpoint_le hβ0 hβ1 hδ — I said the right endpoint needs BOTH hβ0 (for the ≤6+δ) — signature (hβ : β < 1) earlier — NOW needs (hβ0 : 0 < β) too? — the right endpoint: (3−β) ≤ 3 ⟺ β ≥ 0 ✓ hβ0; and 3−β > 0 for the sqrt_le's positivity? — sqrt_le_iff needs 0 ≤ (3−β)+δ ✓ positivity [hδ]; and the product (3−β)·δ ≥ 0 needs 3−β ≥ 0 ⟸ β ≤ 3 ✓ from β < 1. And g3 > 0 needs 3−β > 0 ✓ β < 1. So right endpoint needs BOTH (hβ0 : 0 < β) (hβ1 : β < 1) — wait: for the nlinarith [hδ, hx] in sqrt_le: 2(3−β)δ ≥ 0: needs 3−β ≥ 0 ✓ hβ1 (β < 1 ⟹ 3−β > 2 > 0) ✓. And h3's 2(3−β) ≤ 6: β ≥ 0 ✓ hβ0. So signature (hβ0 : 0 < β) (hβ1 : β < 1) — update: hx : 0 < 3−β from hβ1; the 2(3−β) ≤ 6 from hβ0 ✓.\n- h2's linarith [h3 ▸ h4, h5]: h3 : log(6+δ)+log(7+δ) = log((6+δ)(7+δ)) — h3 ▸ h4 — `▸` at term level: rewrites h4 by h3 — direction: h3 : A = B — h3 ▸ h4 rewrites occurrences of A in h4's type by B — h4 : log((6+δ)(7+δ)) ≤ log(16.5·16.5) — no A in h4 — WRONG direction: I need log(6+δ)+log(7+δ) ≤ ... — use: linarith [h3, h4, h5] — all as atom equations/inequalities ✓ linarith combines ✓ (no ▸ needed):\n goal: log(6+δ) + log(7+δ) ≤ 2·log 16.5; h3 : LHS = log(prod); h4 : log(prod) ≤ log(16.5·16.5); h5 : log(16.5·16.5) = 2·log 16.5 ✓ linarith closes ✓.\n- h4's positivity: 0 < (6+δ)(7+δ) — by positivity with hδ in context ✓ (6+δ > 0 from hδ... positivity needs to derive 0 < 6+δ — hδ : 0 < δ in context ✓ positivity ✓).\n- h4's nlinarith [hδ, hδ1] : (6+δ)(7+δ) ≤ 16.5·16.5: expand: 42 + 13δ + δ² ≤ 272.25: needs δ² ≤ δ·δ ≤ 1·1 = 1... nlinarith pairwise: (hδ1 : δ ≤ 1)² gives δ² ≤ 1 ✓; then 42 + 13·1 + 1 = 56 ≤ 272.25 ✓ nlinarith finds ✓.\n- (Real.log_mul ...).symm for h3 — the ne conditions: 6+δ ≠ 0 and 7+δ ≠ 0 — `by linarith [hδ] : (6:ℝ) + δ ≠ 0` — hmm — the goal (6:ℝ)+δ ≠ 0 — from hδ : 0 < δ: 6+δ > 0 ⟹ ≠ 0 — linarith proves ≠? — banked: \"linarith proves ≠ directly\" ✓ (LiAssembly banked gotcha ✓).\n- h6: Real.log_div (by norm_num : (16.5:ℝ) ≠ 0) (ne_of_gt hδ) : log(16.5/δ) = log 16.5 − log δ; rw [h7] : −log δ → log(1/δ)... wait h7 : log(1/δ) = −log δ — rw [h7] rewrites log(1/δ) → −log δ — but I want the OTHER direction (−log δ → log(1/δ)) — rw [← h7] ✓. Let me redo: goal: 2·log(16.5/δ) = 2·log 16.5 + 2·log(1/δ). rw [Real.log_div ...] : LHS's log(16.5/δ) → log 16.5 − log δ: goal 2·(log16.5 − logδ) = 2·log16.5 + 2·log(1/δ). rw [← h7] : pattern −log δ → log(1/δ)?? — ← h7 rewrites occurrences of RHS of h7 (−log δ) with LHS (log(1/δ)) ✓: goal 2·(log16.5 + log(1/δ)) = 2·log16.5 + 2·log(1/δ) — hmm — wait: 2·(log16.5 − logδ) — the term −log δ is `Neg.neg (log δ)`? or `log16.5 − logδ` is HSub — ← h7's pattern `-(log δ)`: HSub.hSub (log16.5) (logδ) — is that Neg.neg? NO — a − b is Sub, not Neg. rw [← h7] would rewrite `-Real.log δ` as a NEGATION — inside `log16.5 − logδ` there's no standalone `−logδ` negation term (it's a sub). So rw [← h7] fails to find the pattern!! Fix: rw [h7] the OTHER way — transform the goal's RHS instead: the goal after log_div-rw: `2*(log16.5 − logδ) = 2*log16.5 + 2*log(1/δ)` — rw [h7] rewrites `log(1/δ)` → `−logδ` ✓ (h7's LHS log(1/δ) appears in the goal's RHS ✓): goal `2*(log16.5 − logδ) = 2*log16.5 + 2*(−logδ)` — `ring` ✓. So:\n```lean\n rw [Real.log_div (by norm_num) (ne_of_gt hδ), h7]\n ring\n```\nh7 rewrites log(1/δ) → −log δ ✓ then ring: 2(log16.5 − logδ) = 2log16.5 − 2logδ ✓ closes ✓ — h7 must be proved BEFORE this rw (it's the have above ✓).\n\nWait — in my draft h6 the h7-rw is inside: `rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]` for h7's proof: h7 : log(1/δ) = −log δ: rw [Real.log_div ...] at goal: log(1/δ) = −log δ — log(1/δ) → log 1 − log δ: goal log 1 − log δ = −log δ — rw [Real.log_one] : 0 − log δ = −log δ — rw [zero_sub] : −log δ = −log δ rfl ✓ — rw closes ✓.\n\n- The per_zero lemma's final form `2 * Real.log (16.5 / δ)` ✓.\n\nAlso — for hper's use, I need per_zero at δ := |γ−T|: hδ : 0 < |γ−T| (hδpos), hδ1 : |γ−T| ≤ 1 (hδ1.le) ✓.\n\nNow — hβ0/hβ1 for ρ.1: ρ.2.2.1 : 0 < ρ.1.re ✓ ρ.2.2.2 : ρ.1.re < 1 ✓.\n\nOne more piece of §4 — lemma 5/6's `unfold HIntegral` start and the final calc. And lemma 6 (neg) cloning DL-5's conj:\n```lean\ntheorem hIntegral_Jlag_mid_neg_norm_le (hZC ...) (same hyps) :\n ‖HIntegral (Jlag n) (-5/2) 3 (-T)‖ ≤ (same RHS) := by\n have hT0 : (0:ℝ) < T := by ... (√n ≥ 316)\n have hconj : HIntegral (Jlag n) (-5/2) 3 (-T) =\n (starRingEnd ℂ) (HIntegral (Jlag n) (-5/2) 3 T) := by\n unfold HIntegral\n rw [← intervalIntegral.intervalIntegral_conj]\n apply intervalIntegral.integral_congr\n intro σ hσ\n show Jlag n ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =\n (starRingEnd ℂ) (Jlag n ((σ : ℝ) + T * Complex.I))\n have hid2 : ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =\n (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by simp\n rw [hid2]\n exact Jlag_conj n (by\n intro h\n have him : (((σ : ℝ) + T * Complex.I)).im = T := by simp\n rw [h] at him\n simp at him\n linarith [hT0])\n rw [hconj, Complex.norm_conj]\n exact hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n```\n— clone DL-5 verbatim modulo coordinates ✓. Note: DL-5's `((σ : ℝ) + T * Complex.I)` — T : ℝ coerced ✓ same form ✓.\n\n`intervalIntegral.intervalIntegral_conj` — signature: `∫ x in a..b, (starRingEnd ℂ) (f x) = (starRingEnd ℂ) (∫ x in a..b, f x)`? — DL-5 used `rw [← intervalIntegral.intervalIntegral_conj]` — ✓ same usage.\n\nhT0 : 0 < T — from √n ≥ √100000: hsqrt316 : 316 ≤ √n? — simpler: 0 < √n (Real.sqrt_pos.mpr (by linarith [hnR])) and √n ≤ T ⟹ 0 < T ✓ linarith.\n\nOK — NOW let me also think about whether hIntegral_Jlag_mid_norm_le's Jlag-integral equality (unfold HIntegral) works: HIntegral f x₁ x₂ y := ∫ x in x₁..x₂, f (x + y*I) — the points: `(↑x + ↑y*I)` with x y : ℝ — my written integrand `Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)` — same elaboration `↑σ + ↑T * I`?? — HIntegral's body: `f (x + y * I)` — x : ℝ, y * I — the + : needs ℂ: `↑x + ↑y * I`?? — how was it elaborated in DL-5/rectangleIntegral_Jlag_eq? — in rectangleIntegral_Jlag_eq the HIntegral form matched the RectangleIntegral def ✓ and DL-5's conj proof used `((σ : ℝ) + T * Complex.I)` ✓ so the elaborated form is `↑σ + ↑T * I`?? — hmm — in DL-5's hid2: `((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I)` — with explicit ((−T : ℝ) : ℂ)?? — they wrote `(((−T : ℝ)) : ℂ)` — hmm no: `(((−T : ℝ)) : ℂ)` vs `(↑(−T) : ℂ)`... — whatever — my forms will match DL-5's ✓ (clone exactly).\n\nWait — one subtlety: in HIntegral's def `f (x + y * I)` — is the elaborated point `↑x + ↑y * Complex.I` or `↑x + ↑(y) * Complex.I`? — same thing ✓.\n\nBut — when I `unfold HIntegral` at the goal ‖HIntegral (Jlag n) (-5/2) 3 T‖ ≤ ..., the integrand becomes `fun x => Jlag n (↑x + ↑T * I)` — and my subsequent haves are stated with `((σ : ℝ) + (T : ℝ) * Complex.I)` — matching ✓ (norm_integral_le_integral_norm's application will unify the integrand ✓ defeq ✓).\n\nHmm — actually — rectangleIntegral_Jlag_eq used `HIntegral (Jlag n) (-5/2) (2*√n) (-T)` etc. and VIntegral_norm handled the V side; the H-side norm: is there an HIntegral_norm analog? HIntegral f a b y = ∫ σ in a..b, f (↑σ+↑y·I) — no I-factor — so ‖HIntegral‖ = ‖∫‖ directly ✓ no VIntegral_norm needed ✓.\n\nNow — writing the whole §4. It's long; let me be methodical. I'll write it in one Edit, then iterate on errors.\n\nOne more check — `intervalIntegral.integral_mono_on hlen hJintbl hKLintbl (fun σ hσ => hptJ σ hσ)` — hKLintbl : IntervalIntegrable (fun σ => (e⁴+1) * ‖logDeriv _‖) — from hLDcont: hKLcont := continuous_const.mul (continuous_norm.comp hLDc)... — hmm wait — hptJ's RHS is (e⁴+1)·‖logDeriv‖ — the hg in integral_mono_on must be the interval-integrability of THAT lambda ✓.\n\nAnd hsplit's hsumIntbl : IntervalIntegrable (fun σ => ‖Σ‖ + ‖R‖) — hmm — integral_mono_on's hg — the RHS integrand (fun σ => ‖Σ σ‖ + ‖R σ‖) — from hΣnorm_cont.add hRcont ✓ .intervalIntegrable.\n\nNaming (all inside the theorem as have's): hpath, hne1, hJcont, hcontJ, hcontG, hJintbl, hLDc, hLDcont, hLDintbl, hKLcont, hKLintbl, hΣcont, hΣnorm_cont, hΣnorm_int, hRcont, hRnorm_int, hsumcont, hsum_intbl, hker, hptJ, hJint, hpt2, hsplit, hRint, hpt, hρdata, htermcont, hRHScont, hswap, hper, hsum, hΣbound, hB0nn.\n\nOK — write it. For hne1 (the ∀ σ, point ≠ 1): \n```lean\n have hne1 : ∀ σ : ℝ, ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by\n intro σ h\n have him := congrArg Complex.im h\n simp at him\n nlinarith [h10T]\n```\nhim : T = 0 (simp computes im) — h10T : 10 ≤ T ⟹ T ≥ 10 ≠ 0 ✓ nlinarith? — him : T = 0 and 10 ≤ T — linarith ✓ (linear) — use linarith [h10T].\n\nFor hs1 inside hJcont (6-c-ii had it as re-argument — here the point's re varies with σ — the im argument works for ALL σ: point = 1 ⟹ im = T = 0 ≠ ✓).\n\nLet me now write §4 in full.","signature":""},{"type":"text","text":"All signatures verified. Writing §4 (6-c-iv) — the arcsinh-FTC machine, endpoint estimates, per-zero bound, and the two mid-horizontal theorems."},{"type":"tool_use","id":"Edit_95","name":"Edit","input":{"_raw":"{\"replace_all\":false,\"file_path\":\"D:\\\\Python\\\\Quantum\\\\research\\\\lean\\\\NguyenRH1\\\\NguyenRH1\\\\LiSideBounds.lean\",\"old_string\":\" _ = 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring\\n _ ≤ Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := hfinal\\n\\nend NguyenRH1\",\"new_string\":\" _ = 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring\\n _ ≤ Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := hfinal\\n\\n/-! ## 4. 6-c-iv: the mid-horizontal segment machine [−5/2, 3] -/\\n\\n/-- **The arcsinh FTC machine** (6-c-iv core): the direct antiderivative\\nF(σ) = log((σ−β) + √((σ−β)²+δ²)) of 1/√((σ−β)²+δ²) (Real.arcsinh does\\nnot exist here): g(σ) := (σ−β)+√((σ−β)²+δ²) > 0 (√h > |σ−β|), and\\ng′ = 1 + (σ−β)/√h = g/√h, so (log g)′ = 1/√h exactly. -/\\ntheorem integral_one_div_sqrt_sq_add_sq (β δ : ℝ) (hδ : 0 < δ) (a b : ℝ) :\\n ∫ σ in a..b, 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) =\\n Real.log ((b - β) + Real.sqrt ((b - β) ^ 2 + δ ^ 2)) -\\n Real.log ((a - β) + Real.sqrt ((a - β) ^ 2 + δ ^ 2)) := by\\n have hh : ∀ σ : ℝ, (0 : ℝ) < (σ - β) ^ 2 + δ ^ 2 := fun σ =>\\n add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2)\\n have hgpos : ∀ σ : ℝ, (0 : ℝ) < (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\\n intro σ\\n have h1 : |(σ - β)| < Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\\n have h2 : (σ - β) ^ 2 < (σ - β) ^ 2 + δ ^ 2 := by nlinarith [hδ]\\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\\n rwa [Real.sqrt_sq_eq_abs] at h3\\n have h4 : -(σ - β) ≤ |(σ - β)| := neg_abs_le (σ - β)\\n linarith [h1, h4]\\n have hderiv : ∀ σ : ℝ, HasDerivAt\\n (fun σ => Real.log ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)))\\n (1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by\\n intro σ\\n have hhσ := hh σ\\n have hsqrt0 : Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hhσ)\\n have hg0 : ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) ≠ 0 := (hgpos σ).ne'\\n have h1 : HasDerivAt (fun σ => σ - β) 1 σ := hasDerivAt_id.sub_const β\\n have h2 : HasDerivAt (fun σ => (σ - β) ^ 2 + δ ^ 2) (2 * (σ - β)) σ := by\\n have h2a := (hasDerivAt_id.sub_const β).pow 2\\n have h2b := h2a.add_const (δ ^ 2)\\n convert h2b using 1\\n ring\\n have h4 : HasDerivAt (fun σ => Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\\n (2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=\\n h2.sqrt hhσ.ne'\\n have h5 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\\n (1 + 2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=\\n h1.add h4\\n have h6 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\\n (((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) /\\n Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by\\n convert h5 using 1\\n field_simp [hsqrt0]\\n ring\\n have h7 := h6.log hg0\\n convert h7 using 1\\n field_simp [hsqrt0, hg0]\\n ring\\n exact intervalIntegral.integral_eq_sub_of_hasDerivAt (fun σ _ => hderiv σ)\\n (by\\n apply Continuous.intervalIntegrable\\n apply Continuous.div continuous_const\\n · exact Real.continuous_sqrt.comp (by fun_prop :\\n Continuous fun σ : ℝ => (σ - β) ^ 2 + δ ^ 2)\\n · intro σ\\n exact ne_of_gt (Real.sqrt_pos.mpr (hh σ)))\\n\\n/-- **The right endpoint estimate** F(3) ≤ log(6+δ): √((3−β)²+δ²) ≤\\n(3−β)+δ for 3−β > 0, so the argument is ≤ 2(3−β)+δ ≤ 6+δ (0 ≤ β). -/\\ntheorem arcsinh_right_endpoint_le {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)\\n (hδ : 0 < δ) :\\n Real.log ((3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2)) ≤ Real.log (6 + δ) := by\\n have hx : (0 : ℝ) < 3 - β := by linarith\\n have hsqrt_le : Real.sqrt ((3 - β) ^ 2 + δ ^ 2) ≤ (3 - β) + δ := by\\n rw [Real.sqrt_le_iff]\\n exact ⟨by positivity, by nlinarith [hδ, hx]⟩\\n have h1 : (0 : ℝ) < (3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2) := by\\n have h2 := Real.sqrt_nonneg ((3 - β) ^ 2 + δ ^ 2)\\n nlinarith\\n have h3 : (3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2) ≤ 6 + δ := by\\n nlinarith [hsqrt_le, hβ0]\\n exact Real.log_le_log h1 h3\\n\\n/-- **The left endpoint estimate** −F(−5/2) ≤ log(7+δ) + 2·log(1/δ):\\nwith u := 5/2+β ∈ (5/2, 7/2), the argument −u+√(u²+δ²) rationalizes to\\nδ²/(u+√(u²+δ²)) ≥ δ²/(7+δ) > 0, so F(−5/2) ≥ log(δ²/(7+δ)) =\\n2·log δ − log(7+δ). -/\\ntheorem arcsinh_left_endpoint_le {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)\\n (hδ : 0 < δ) :\\n -Real.log ((-5 / 2 - β) + Real.sqrt ((-5 / 2 - β) ^ 2 + δ ^ 2)) ≤\\n Real.log (7 + δ) + 2 * Real.log (1 / δ) := by\\n have hu : (0 : ℝ) < 5 / 2 + β := by linarith\\n have hsq : (-5 / 2 - β) ^ 2 = (5 / 2 + β) ^ 2 := by ring\\n have hneg : (-5 / 2 : ℝ) - β = -(5 / 2 + β) := by ring\\n rw [hsq, hneg]\\n set u := 5 / 2 + β with hu_def\\n have hu2 : u < 7 / 2 := by rw [hu_def]; linarith\\n have hsqrt_pos : (0 : ℝ) < Real.sqrt (u ^ 2 + δ ^ 2) :=\\n Real.sqrt_pos.mpr (add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2))\\n have hg_pos : (0 : ℝ) < -u + Real.sqrt (u ^ 2 + δ ^ 2) := by\\n have h1 : u < Real.sqrt (u ^ 2 + δ ^ 2) := by\\n have h2 : u ^ 2 < u ^ 2 + δ ^ 2 := by nlinarith [hδ]\\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\\n rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3\\n linarith\\n -- the rationalization: −u + √ = δ²/(u + √)\\n have hrid : -u + Real.sqrt (u ^ 2 + δ ^ 2) =\\n δ ^ 2 / (u + Real.sqrt (u ^ 2 + δ ^ 2)) := by\\n rw [div_eq_iff (ne_of_gt (by linarith [hsqrt_pos] :\\n (0 : ℝ) < u + Real.sqrt (u ^ 2 + δ ^ 2)))]\\n have hs : (Real.sqrt (u ^ 2 + δ ^ 2)) ^ 2 = u ^ 2 + δ ^ 2 :=\\n Real.sq_sqrt (by positivity)\\n nlinarith [hs]\\n -- the denominator ≤ 7 + δ\\n have hden : u + Real.sqrt (u ^ 2 + δ ^ 2) ≤ 7 + δ := by\\n have h1 : Real.sqrt (u ^ 2 + δ ^ 2) ≤ u + δ := by\\n rw [Real.sqrt_le_iff]\\n exact ⟨by linarith [hδ, hu.le], by nlinarith [hδ, hu]⟩\\n nlinarith [h1, hu2]\\n -- δ²/(7+δ) ≤ δ²/(u+√) = −u+√\\n have hge : δ ^ 2 / (7 + δ) ≤ -u + Real.sqrt (u ^ 2 + δ ^ 2) := by\\n rw [hrid]\\n have h2 : (0 : ℝ) < u + Real.sqrt (u ^ 2 + δ ^ 2) := by linarith [hsqrt_pos]\\n exact div_le_div_of_nonneg_left (sq_nonneg _) h2 hden\\n -- log mono + algebra: F(−5/2) ≥ log(δ²/(7+δ)) = 2·log δ − log(7+δ)\\n have hlog : Real.log (δ ^ 2 / (7 + δ)) ≤ Real.log (-u + Real.sqrt (u ^ 2 + δ ^ 2)) :=\\n Real.log_le_log (by positivity) hge\\n have hlogid : Real.log (δ ^ 2 / (7 + δ)) = 2 * Real.log δ - Real.log (7 + δ) := by\\n rw [Real.log_div (pow_pos hδ 2).ne' (by linarith [hδ] : (7 : ℝ) + δ ≠ 0),\\n Real.log_pow]\\n ring\\n have hlog1 : Real.log (1 / δ) = -Real.log δ := by\\n rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]\\n rw [hlogid] at hlog\\n linarith [hlog, hlog1]\\n\\n/-- **The per-zero segment integral bound**: ∫_{−5/2}^{3} dσ/√((σ−β)²+δ²)\\n≤ 2·log(16.5/δ) for 0 < β < 1, 0 < δ ≤ 1 — the two endpoint estimates +\\nlog((6+δ)(7+δ)) ≤ log(16.5²) since (6+δ)(7+δ) ≤ 56 ≤ 272.25. -/\\ntheorem per_zero_integral_le_two_log {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)\\n (hδ : 0 < δ) (hδ1 : δ ≤ 1) :\\n ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤\\n 2 * Real.log (16.5 / δ) := by\\n have hftc := integral_one_div_sqrt_sq_add_sq β δ hδ (-5 / 2) 3\\n have hr := arcsinh_right_endpoint_le hβ0 hβ1 hδ\\n have hl := arcsinh_left_endpoint_le hβ0 hβ1 hδ\\n have h1 : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤\\n Real.log (6 + δ) + Real.log (7 + δ) + 2 * Real.log (1 / δ) := by\\n rw [hftc]\\n linarith [hr, hl]\\n -- the log-mono simplification: log(6+δ) + log(7+δ) ≤ 2·log 16.5\\n have h2 : Real.log (6 + δ) + Real.log (7 + δ) ≤ 2 * Real.log 16.5 := by\\n have h3 : Real.log (6 + δ) + Real.log (7 + δ) = Real.log ((6 + δ) * (7 + δ)) :=\\n (Real.log_mul (by linarith [hδ] : (6 : ℝ) + δ ≠ 0)\\n (by linarith [hδ] : (7 : ℝ) + δ ≠ 0)).symm\\n have h4 : Real.log ((6 + δ) * (7 + δ)) ≤ Real.log (16.5 * 16.5) :=\\n Real.log_le_log (by positivity) (by nlinarith [hδ, hδ1])\\n have h5 : Real.log (16.5 * 16.5) = 2 * Real.log 16.5 := by\\n rw [show (16.5 : ℝ) * 16.5 = 16.5 ^ 2 by ring, Real.log_pow]\\n ring\\n linarith [h3, h4, h5]\\n have h6 : 2 * Real.log (16.5 / δ) = 2 * Real.log 16.5 + 2 * Real.log (1 / δ) := by\\n have h7 : Real.log (1 / δ) = -Real.log δ := by\\n rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]\\n rw [Real.log_div (by norm_num) (ne_of_gt hδ), h7]\\n ring\\n rw [h6]\\n linarith [h1, h2]\\n\\n/-- **6-c-iv (mid-horizontal [−5/2, 3] at height +T)**: the segment bound\\n‖H‖ ≤ (e⁴+1)·(2·Z₂(T)·log(148.5·Ĉ₀(√n+2)) + 5.5·(10.5·log(T+2)+48)).\\nKernel e⁴+1 (the ii′-4 shift lemma at s := w−1); logDeriv split by\\nnorm_le_insert' into the near sum (per-zero arcsinh-FTC machine +\\nintegral_finsetSum + the two-unit count ≤ Z₂(T)) and the tight R-bound\\n(capstone, constant in σ). -/\\ntheorem hIntegral_Jlag_mid_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\\n (hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\\n (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →\\n ρ.im < Real.sqrt (n : ℝ) + 2 →\\n 1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)\\n (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\\n ‖HIntegral (Jlag n) (-5 / 2) 3 T‖ ≤\\n (Real.exp 4 + 1) *\\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\\n classical\\n have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\\n have h10T : (10 : ℝ) ≤ T := by\\n have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by\\n rw [Real.le_sqrt (by norm_num) (by positivity)]\\n nlinarith [hnR]\\n linarith\\n have hT0 : (0 : ℝ) ≤ T := by linarith\\n have hn1 : 1 ≤ n := by omega\\n have hlen : (-5 / 2 : ℝ) ≤ 3 := by norm_num\\n have hC0 : (0 : ℝ) < C0hat (Real.sqrt (n : ℝ) + 2) := by\\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : ℝ)] :\\n (1 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)\\n linarith\\n have hB0nn : (0 : ℝ) ≤ 2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by\\n have h1 : (1 : ℝ) ≤ 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) := by nlinarith [hC0]\\n have h3 := Real.log_nonneg h1\\n linarith\\n -- zero-freeness on the horizontal + the path continuity machines\\n have hzne : ∀ σ : ℝ, riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 0 :=\\n fun σ => zeta_ne_zero_horizontal hTwide hn1 hTn hTn1\\n have hne1 : ∀ σ : ℝ, ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by\\n intro σ h\\n have him := congrArg Complex.im h\\n simp at him\\n linarith [h10T]\\n have hpath : Continuous fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I) := by\\n fun_prop\\n have hLDc : Continuous fun σ : ℝ =>\\n logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) := by\\n rw [continuous_iff_continuousAt]\\n intro σ\\n have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=\\n hpath.continuousAt\\n exact ContinuousAt.comp (g := logDeriv riemannZeta)\\n (f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ)\\n (continuousAt_logDeriv_zeta (hne1 σ) (hzne σ)) hf\\n have hJcont : ∀ σ : ℝ, ContinuousAt (Jlag n) ((σ : ℝ) + (T : ℝ) * Complex.I) := by\\n intro σ\\n have hA := (kFun_differentiableAt (n := n) (hne1 σ)).continuousAt\\n have hB := continuousAt_logDeriv_zeta (hne1 σ) (hzne σ)\\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\\n exact hA.mul hB.neg\\n have hcontJ : Continuous fun σ : ℝ =>\\n Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I) := by\\n rw [continuous_iff_continuousAt]\\n intro σ\\n have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=\\n hpath.continuousAt\\n exact ContinuousAt.comp (g := Jlag n)\\n (f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ) (hJcont σ) hf\\n have hcontG : Continuous fun σ : ℝ =>\\n ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := continuous_norm.comp hcontJ\\n have hJintbl : IntervalIntegrable\\n (fun σ : ℝ => ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖)\\n MeasureTheory.volume (-5 / 2) 3 := hcontG.intervalIntegrable _ _\\n have hLDcont : Continuous fun σ : ℝ =>\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=\\n continuous_norm.comp hLDc\\n have hLDintbl : IntervalIntegrable\\n (fun σ : ℝ => ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖)\\n MeasureTheory.volume (-5 / 2) 3 := hLDcont.intervalIntegrable _ _\\n have hKLcont : Continuous fun σ : ℝ =>\\n (Real.exp 4 + 1) * ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=\\n continuous_const.mul hLDcont\\n have hKLintbl : IntervalIntegrable\\n (fun σ : ℝ => (Real.exp 4 + 1) *\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖)\\n MeasureTheory.volume (-5 / 2) 3 := hKLcont.intervalIntegrable _ _\\n -- the near-sum denominator never vanishes on the path (else s = ρ is a\\n -- zero, contra zeta_ne_zero_horizontal)\\n have hden : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\\n ∀ σ : ℝ, ((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1 ≠ 0 := by\\n intro ρ _ σ h0\\n have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h0\\n have hz := hzne σ\\n rw [hs] at hz\\n exact hz ρ.2.1\\n have hΣcont : Continuous fun σ : ℝ =>\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1) := by\\n apply continuous_finset_sum\\n intro ρ hρ\\n exact Continuous.div continuous_const (hpath.sub continuous_const) (hden ρ hρ)\\n have hΣnorm_cont : Continuous fun σ : ℝ =>\\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\\n continuous_norm.comp hΣcont\\n have hΣnorm_int : IntervalIntegrable\\n (fun σ : ℝ => ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)\\n MeasureTheory.volume (-5 / 2) 3 := hΣnorm_cont.intervalIntegrable _ _\\n have hRcont : Continuous fun σ : ℝ =>\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\\n continuous_norm.comp (hLDc.sub hΣcont)\\n have hRnorm_int : IntervalIntegrable\\n (fun σ : ℝ => ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)\\n MeasureTheory.volume (-5 / 2) 3 := hRcont.intervalIntegrable _ _\\n -- the per-ρ data (δ_ρ := |γ−T| ∈ [c_clear, 1))\\n have hρdata : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\\n (0 : ℝ) < |ρ.1.im - T| ∧ |ρ.1.im - T| < 1 ∧\\n (1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2))) ≤ |ρ.1.im - T| := by\\n intro ρ hρ\\n have hδ1 := mem_nearZerosSub.mp hρ\\n obtain ⟨hlo, hhi⟩ := abs_lt.mp hδ1\\n have hγ1 : Real.sqrt (n : ℝ) - 1 < ρ.1.im := by nlinarith [hTn]\\n have hγ2 : ρ.1.im < Real.sqrt (n : ℝ) + 2 := by nlinarith [hTn1]\\n have hδge := hTwide ρ.1 ρ.2 hγ1 hγ2\\n have hδpos : (0 : ℝ) < |ρ.1.im - T| :=\\n lt_of_lt_of_le (one_div_pos.mpr (by positivity :\\n (0 : ℝ) < 9 * C0hat (Real.sqrt (n : ℝ) + 2))) hδge\\n exact ⟨hδpos, hδ1, hδge⟩\\n -- the kernel bound per σ (the ii′-4 shift lemma at s := w − 1)\\n have hnT2 : (n : ℝ) ≤ T ^ 2 := by\\n have h1 : (Real.sqrt (n : ℝ)) ^ 2 ≤ T ^ 2 :=\\n pow_le_pow_left₀ (Real.sqrt_nonneg _) hTn 2\\n rwa [Real.sq_sqrt (by positivity : (0 : ℝ) ≤ (n : ℝ))] at h1\\n have hker : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\\n ‖kFun n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤ Real.exp 4 + 1 := by\\n intro σ hσ\\n obtain ⟨hσ1, hσ2⟩ := hσ\\n have hre : (((σ : ℝ) + (T : ℝ) * Complex.I) - 1).re = σ - 1 := by simp\\n have him : (((σ : ℝ) + (T : ℝ) * Complex.I) - 1).im = T := by simp\\n have h1 := kFun_shift_norm_le_exp_four_add_one (n := n)\\n (s := (((σ : ℝ) + (T : ℝ) * Complex.I) - 1))\\n (by rw [hre]; linarith [hσ2]) (by rw [him]; exact hnT2)\\n rwa [sub_add_cancel] at h1\\n -- pointwise Jlag ≤ (e⁴+1)·‖logDeriv‖\\n have hptJ : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\\n ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\\n (Real.exp 4 + 1) * ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := by\\n intro σ hσ\\n rw [Jlag_norm_eq]\\n exact mul_le_mul (hker σ hσ) le_rfl (norm_nonneg _) (by positivity)\\n have hJint : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\\n (Real.exp 4 + 1) * ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := by\\n have h := intervalIntegral.integral_mono_on hlen hJintbl hKLintbl\\n (fun σ hσ => hptJ σ hσ)\\n rwa [intervalIntegral.integral_const_mul] at h\\n -- the logDeriv split: ‖logDeriv‖ ≤ ‖Σ‖ + ‖logDeriv − Σ‖\\n have hsumcont : Continuous fun σ : ℝ =>\\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\\n hΣnorm_cont.add hRcont\\n have hsum_intbl : IntervalIntegrable\\n (fun σ : ℝ => ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)\\n MeasureTheory.volume (-5 / 2) 3 := hsumcont.intervalIntegrable _ _\\n have hsplit : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) +\\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) := by\\n have hpt2 : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\\n fun σ _ => norm_le_insert' _ _\\n have h := intervalIntegral.integral_mono_on hlen hLDintbl hsum_intbl\\n (fun σ hσ => hpt2 σ hσ)\\n rwa [intervalIntegral.integral_add hΣnorm_int hRnorm_int] at h\\n -- the R-part integral (the 5f capstone, constant in σ)\\n have hR : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\\n 10.5 * Real.log (T + 2) + 48 := by\\n intro σ hσ\\n obtain ⟨hσ1, hσ2⟩ := hσ\\n have hre : ((σ : ℝ) + (T : ℝ) * Complex.I).re = σ := by simp\\n have him : ((σ : ℝ) + (T : ℝ) * Complex.I).im = T := by simp\\n have h := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := T)\\n (s := ((σ : ℝ) + (T : ℝ) * Complex.I)) hZC hZC2 hNLZ h10T\\n (by rw [hre]; exact hσ1) (by rw [hre]; exact hσ2) him (hzne σ)\\n rwa [abs_of_nonneg hT0] at h\\n have hRint : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) := by\\n have h := intervalIntegral.integral_mono_on hlen hRnorm_int intervalIntegrable_const\\n (fun σ hσ => hR σ hσ)\\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\\n -- the near-sum integral: the per-zero arcsinh-FTC machine + the swap\\n have hnormid : ∀ σ : ℝ, ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ},\\n ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1‖ =\\n Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2) := by\\n intro σ ρ\\n have h1 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1) =\\n (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by\\n simp [Complex.normSq_apply]\\n ring\\n symm\\n rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _),\\n ← Complex.normSq_eq_norm_sq]\\n exact h1.symm\\n have htermcont : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\\n Continuous fun σ : ℝ => (zeroMult ρ.1 : ℝ) *\\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\\n intro ρ hρ\\n obtain ⟨hδpos, -, -⟩ := hρdata ρ hρ\\n have hh : ∀ σ : ℝ, (0 : ℝ) < (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by\\n intro σ\\n have h3 : ρ.1.im - T ≠ 0 := abs_pos.mp hδpos\\n have h4 : T - ρ.1.im ≠ 0 := by\\n intro h5\\n apply h3\\n linarith [h5]\\n exact add_pos_of_nonneg_of_pos (sq_nonneg _) (sq_pos_of_ne_zero h4)\\n apply Continuous.mul continuous_const\\n apply Continuous.div continuous_const\\n · exact Real.continuous_sqrt.comp (by fun_prop :\\n Continuous fun σ : ℝ => (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)\\n · intro σ\\n exact ne_of_gt (Real.sqrt_pos.mpr (hh σ))\\n have hpt : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2"},"extra_content":null}]