← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (18267 chars)
`integral_conj {f : X → 𝕜} : ∫ x, conj (f x) ∂μ = conj (∫ x, f x ∂μ)` — exists (Bochner/ContinuousLinearMap.lean:173, RCLike 𝕜). For interval integrals: the interval integral IS a Bochner integral over the interval measure — `∫ x in a..b, f x` unfolds to the measure integral, so `integral_conj` applies (it's about the Bochner integral — the interval notation is defeq). The `conj` here is `starRingEnd 𝕜` presumably (RCLike's conj = starRingEnd 𝕜 for 𝕜 = ℂ ✓).
Now write DL-5. Structure:
```lean
/-! ## 7. The total right-horizontal bound (DL-5, D-074 §3.4) -/
/-- The dog-leg height parameter U = (3/2)·T. -/
theorem hIntegral_Jlag_low_le_dogLegUpper {n : ℕ} {T : ℝ}
(hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ ≤
((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
IIMaj (n : ℝ) / 2 := by
have hT0 : (0 : ℝ) < T := by
have h1 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by
have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have h2 : Real.sqrt 16 ≤ Real.sqrt (n : ℝ) :=
Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : ℝ) ≤ (n : ℝ))
have h3 : Real.sqrt 16 = 4 := by
rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num
rwa [h3] at h2
linarith
have hTn2 : (n : ℝ) ≤ T ^ 2 := by
have h1 := hTn
have h2 : (Real.sqrt (n : ℝ)) ^ 2 ≤ T ^ 2 := by
apply pow_le_pow_left₀ (Real.sqrt_nonneg _) h1
rwa [Real.sq_sqrt (by linarith [Real.sqrt_nonneg (n : ℝ)])] at h2
have hU0 : (0 : ℝ) < (3 / 2) * T := by linarith [hT0]
have hTU : T ≤ (3 / 2) * T := by linarith [hT0]
have hnU : (n : ℝ) ≤ (4 / 9) * ((3 / 2) * T) ^ 2 := by
have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by field_simp; ring
rw [h1]
exact hTn2
have hXR : (3 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by
have h1 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := ... (same sqrt-16 trick)
linarith
have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)
-- the three pieces
have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)
have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)
have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)
-- lengths: U − T = T/2 ≤ (√n+1)/2
have hlen : (3 / 2) * T - T ≤ (Real.sqrt (n : ℝ) + 1) / 2 := by
linarith [hTn1, hTn]
-- assemble
rw [hid]
calc ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T) -
VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T) +
VIntegral (Jlag n) 3 T ((3 / 2) * T)‖
≤ ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T)‖ +
‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ +
‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖ := by
exact norm_sub_le.trans (norm_add_le _ _)
-- hmm: ‖A − B + C‖ ≤ ‖A‖ + ‖B‖ + ‖C‖: norm_sub_le: ‖A−B‖ ≤ ‖A‖+‖B‖; norm_add_le: ‖(A−B)+C‖ ≤ ‖A−B‖+‖C‖ — compose
_ ≤ (8.38 : ℝ) + ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +
IIMaj (n : ℝ) / 2 := by
apply add_le_add (add_le_add hH ?vr ?vl) (le_refl _)
...
```
Hmm — let me structure the assembly more carefully:
‖H_low‖ = ‖H_high − V_right + V_left‖ ≤ ‖H_high‖ + ‖V_right‖ + ‖V_left‖ via:
norm_sub_le : ‖a − b‖ ≤ ‖a‖ + ‖b‖; norm_add_le : ‖a + b‖ ≤ ‖a‖ + ‖b‖.
‖(H − Vr) + Vl‖ ≤ ‖H − Vr‖ + ‖Vl‖ ≤ (‖H‖ + ‖Vr‖) + ‖Vl‖ ✓.
Then:
- ‖H‖ ≤ 8.38 (hH)
- ‖Vr‖ ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 — then ≤ IIMaj/2:
(U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}·1 (hlen, dirichletC2 ≤ 1)
and ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)} ≤ IIMaj/2:
IIMaj/2 = (1/2)·2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} = (√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}.
⟺ ((√n+1)/2)·1 ≤ (√n+1)·0.57 ⟺ 1/2 ≤ 0.57 ✓ trivial.
- ‖Vl‖ ≤ (U−T)·(e^{5/2}+1)/2 ≤ ((√n+1)/2)·(e^{5/2}+1)/2 (hlen) ✓ (that's the VLeftBound form ✓).
The IIMaj/2 proof (Vr ≤ IIMaj/2):
```
have hVr2 : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ ≤ IIMaj (n : ℝ) / 2 := by
refine hVr.trans ?_
-- (U−T)·(e^{√n/2}+1)·(2^{−(2√n−2)}·dirichletC2) ≤ IIMaj/2
have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one
have hC2pos : (0 : ℝ) ≤ dirichletC2 := dirichletC2_nonneg
have hexp_pos : (0 : ℝ) < Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by positivity
have hpow_pos : (0 : ℝ) < (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by positivity
have hlen0 : (0 : ℝ) ≤ (3 / 2) * T - T := by linarith [hT0]
calc ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2)
≤ ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * 1) := by
apply mul_le_mul (mul_le_mul hlen (le_refl _) (add_nonneg (Real.exp_nonneg _) (by norm_num)) hlen0) ?_ (by positivity) (by positivity)
· exact mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _)
_ = IIMaj (n : ℝ) / 2 := by
unfold IIMaj
field_simp
ring
```
Hmm — the IIMaj/2 equality: IIMaj/2 = (1/2)·2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} = (√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} — and my LHS: ((√n+1)/2)(e+1)·2^{−X}·1. Are they EQUAL? LHS = ((√n+1)/2)(e+1)2^{−X}; RHS = (√n+1)(e+1)·0.57·2^{−X} — NOT equal (0.57 ≠ 0.5). So the calc's last step should be ≤ (not =): ((√n+1)/2)(e+1)2^{−X}·1 ≤ (√n+1)(e+1)·0.57·2^{−X} ⟺ 1/2 ≤ 0.57 ⟺ 0.5 ≤ 0.57 ✓ — via mul_le_mul of (1/2 ≤ 0.57) with the common positive factor:
```
_ ≤ IIMaj (n : ℝ) / 2 := by
unfold IIMaj
have h57 : (Real.sqrt (n : ℝ) + 1) / 2 * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * 1) ≤
(Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * 0.57) := by
apply mul_le_mul_of_nonneg_left _ (by positivity)
· apply mul_le_mul_of_nonneg_right _ (by positivity)
norm_num
convert h57 using 1 <;> ring
```
Hmm — the convert: IIMaj/2's unfolded form: 2·(√n+1)·(e+1)·0.57·2^{−X}/2 vs the h57 form (√n+1)·(e+1)·(2^{−X}·0.57) — equal by ring ✓.
This is getting intricate — let me simplify the whole Vr accounting: bound ‖Vr‖ ≤ IIMaj/2 via a direct chain:
```
have hVr2 : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ ≤ IIMaj (n : ℝ) / 2 := by
have h1 := hVr
have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one
-- key numeric: (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·C2 ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}
-- and ((√n+1)/2)·... ≤ IIMaj/2 = (√n+1)·0.57·...·...
have h57 : ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ)) ≤ IIMaj (n : ℝ) / 2 := by
unfold IIMaj
have hpos1 : (0 : ℝ) < (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by positivity
have hpos2 : (0 : ℝ) ≤ Real.sqrt (n : ℝ) + 1 := by linarith [Real.sqrt_nonneg (n : ℝ)]
have hpos3 : (0 : ℝ) ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by positivity
calc ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ))
≤ (Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (0.57 : ℝ)) := by
apply mul_le_mul_of_nonneg_left _ hpos3
· apply mul_le_mul_of_nonneg_right _ hpos1.le
· calc ((Real.sqrt (n : ℝ) + 1) / 2) * (1 : ℝ) ≤ (Real.sqrt (n : ℝ) + 1) * (0.57 : ℝ) := by
apply mul_le_mul_of_nonneg_left _ hpos2
norm_num
_ = ((Real.sqrt (n : ℝ) + 1) / 2) * 1 * 1 ≤ ... -- ugh
```
Getting bogged down in product associativity. SIMPLIFY: prove the key inequality in the cleanest form:
A := ((√n+1)/2)·(e+1)·(2^{−X}·1), B := IIMaj/2. B = (√n+1)·(e+1)·(0.57·2^{−X})... — hmm actually IIMaj = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}: IIMaj/2 = (√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}.
A = ((√n+1)/2)(e+1)·2^{−X}·1 = 0.5·(√n+1)(e+1)·2^{−X}.
B = 0.57·(√n+1)(e+1)·2^{−X}.
A ≤ B ⟺ 0.5 ≤ 0.57 ✓.
Prove via: A = c·K and B = d·K with K = (√n+1)(e+1)·2^{−X} > 0 and c = 0.5 ≤ 0.57 = d:
```
have hK : (0 : ℝ) < (Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by positivity
have eA : ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ)) =
(1 / 2) * ((Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by ring
have eB : IIMaj (n : ℝ) / 2 =
(0.57 : ℝ) * ((Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by
unfold IIMaj
ring
rw [eA, eB]
apply mul_le_mul_of_nonneg_right _ hK.le
norm_num
```
The eB: IIMaj/2 = (1/2)·[2(√n+1)(e+1)·0.57·2^{−X}] = (√n+1)(e+1)·0.57·2^{−X} = 0.57·[(√n+1)(e+1)·2^{−X}] ✓ ring proves it? — unfold IIMaj gives the full form 2·(√n+1)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)} / 2 — ring handles the constants ✓ (the 2·.../2 cancellation — ring over a field handles /2 ✓).
Similarly eA by ring ✓.
Then the full Vr chain:
```
calc ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖
≤ ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := hVr
_ ≤ ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ)) := by
have hlen0 : (0 : ℝ) ≤ (3 / 2) * T - T := by linarith [hT0]
have hpos3 : (0 : ℝ) ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by positivity
have hpos4 : (0 : ℝ) ≤ (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 := by positivity
have h1 : ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) ≤
((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) :=
mul_le_mul hlen (le_refl _) (add_nonneg (Real.exp_nonneg _) (by norm_num)) hlen0
exact mul_le_mul h1 (mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _))
hpos4 (mul_nonneg hpos3 (Real.rpow_nonneg (by norm_num) _))
_ ≤ IIMaj (n : ℝ) / 2 := by
rw [eA, eB]
apply mul_le_mul_of_nonneg_right _ hK.le
norm_num
```
Wait — the second step's mul_le_mul: h1 : (U−T)(e+1) ≤ ((√n+1)/2)(e+1) and hC2-rpow : 2^{−X}·C2 ≤ 2^{−X}·1 — mul_le_mul (h1) (h2) (0 ≤ (2^{−X}·C2)) (0 ≤ ((√n+1)/2)(e+1)) : (U−T)(e+1)·(2^{−X}·C2) ≤ ((√n+1)/2)(e+1)·(2^{−X}·1) ✓ — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b) : a·c ≤ b·d ✓ — with a := (U−T)(e+1), b := ((√n+1)/2)(e+1), c := (2^{−X}·C2), d := (2^{−X}·1): hc : 0 ≤ 2^{−X}·C2 ✓ positivity (C2 ≥ 0 via dirichletC2_nonneg — positivity might not know; provide explicitly); hb : 0 ≤ ((√n+1)/2)(e+1) ✓ positivity.
Then mul_le_mul hlen (le_refl (e+1)) (0 ≤ e+1) (0 ≤ U−T) : (U−T)(e+1) ≤ ((√n+1)/2)(e+1) ✓ — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b) ✓ with a := U−T, b := (√n+1)/2, c := d := e+1: hc : 0 ≤ e+1 ✓ (add_nonneg (exp_nonneg _) 0≤1... — the `add_nonneg (Real.exp_nonneg _) (by norm_num : (0:ℝ) ≤ 1)`); hb : 0 ≤ U−T ✓ hlen0.
The 2^{−X}·C2 ≤ 2^{−X}·1 : mul_le_mul_of_nonneg_left hC2 (0 ≤ 2^{−X}) : C2·2^{−X} ≤ 1·2^{−X} ✓ — but the form is (2^{−X}·C2) ≤ (2^{−X}·1) — mul_le_mul_of_nonneg_left : a ≤ b → 0 ≤ c → c·a ≤ c·b — with c := 2^{−X}, a := C2, b := 1: 2^{−X}·C2 ≤ 2^{−X}·1 ✓ (Real.rpow_nonneg (by norm_num) _ : 0 ≤ 2^{−X} ✓).
OK — and hK/eA/eB as designed. This is doable but long. Let me also double check the Vl assembly:
```
calc ‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖
≤ ((3 / 2) * T - T) * (Real.exp (5 / 2) + 1) / 2 := hVl
_ ≤ ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=
mul_le_mul hlen (le_refl _) (by positivity) hlen0
```
mul_le_mul (hlen : U−T ≤ (√n+1)/2) (le_refl : X ≤ X) (0 ≤ X) (0 ≤ U−T) : (U−T)·X ≤ ((√n+1)/2)·X with X := (e^{5/2}+1)/2 ✓ — wait mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b): a·c ≤ b·d ✓ with a := U−T, b := (√n+1)/2, c = d := (e^{5/2}+1)/2 ✓.
Final assembly:
```
rw [hid]
calc ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T) -
VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T) +
VIntegral (Jlag n) 3 T ((3 / 2) * T)‖
≤ ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T)‖ +
‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ +
‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖ := by
exact (norm_sub_le _ _).trans (norm_add_le _ _) -- hmm
_ ≤ (8.38 : ℝ) + IIMaj (n : ℝ) / 2 + ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by
exact add_le_add (add_le_add hH hVr2) hVl2
_ = ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) + IIMaj (n : ℝ) / 2 := by ring
```
norm composition: ‖(H − Vr) + Vl‖ ≤ ‖H − Vr‖ + ‖Vl‖ (norm_add_le) ≤ ‖H‖ + ‖Vr‖ + ‖Vl‖ (norm_sub_le on the first):
```
have hna : ‖(H − Vr) + Vl‖ ≤ ‖H − Vr‖ + ‖Vl‖ := norm_add_le _ _
have hns : ‖H − Vr‖ ≤ ‖H‖ + ‖Vr‖ := norm_sub_le _ _
linarith [hna, hns]
```
Hmm — norm_add_le : ‖a + b‖ ≤ ‖a‖ + ‖b‖ — for normed groups: `norm_add_le (a b : α) : ‖a + b‖ ≤ ‖a‖ + ‖b‖` ✓; norm_sub_le (a b) : ‖a − b‖ ≤ ‖a‖ + ‖b‖ ✓.
The theorem's statement RHS: ((√n+1)/2)·(e^{5/2}+1)/2 + 8.38 + IIMaj/2 ✓.
Now DL-5b (the lower side):
```lean
/-- The lower right-tail bound by conjugation (D-074 §3.4): for n ≥ 16,
T ∈ [√n, √n+1], ‖HIntegral (Jlag n) 3 (2√n) (−T)‖ ≤ DogLegUpper n
(the conjugate of the upper bound; Jlag_conj + the integral conj
symmetry). -/
theorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : ℕ} {T : ℝ}
(hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T))‖ ≤ ... same RHS := by
have hT0 : (0 : ℝ) < T := ...
have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T) =
(starRingEnd ℂ) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T) := by
unfold HIntegral
rw [← integral_conj]
-- pointwise: conj (Jlag n (σ + T·I)) = Jlag n (σ − T·I) = Jlag n (σ + (−T)·I)
apply intervalIntegral.integral_congr
intro σ hσ
rw [show ((σ : ℝ) + (-T) * Complex.I) = (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) from by
simp [Complex.ext_iff]]
exact (Jlag_conj n (by
have him : 0 < (((σ : ℝ) + T * Complex.I)).im := by simp [hT0]
intro h
rw [h] at him
simp at him)).symm
rw [hconj, ← Complex.norm_eq_abs, ← Complex.norm_eq_abs]
exact hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1
```
Hmm — details:
- `integral_conj : ∫ x, conj (f x) ∂μ = conj (∫ x, f x ∂μ)` — with conj := starRingEnd ℂ ✓. `rw [← integral_conj]` turns the goal's LHS integral `∫ Jlag(σ + (−T)·I)` into... hmm — the goal is `∫ Jlag(σ + (−T)·I) = conj(∫ Jlag(σ+T·I))` — rw [← integral_conj] rewrites conj(∫ f) → ∫ conj(f): the RHS conj(∫ Jlag(σ+T·I)) → ∫ conj(Jlag(σ+T·I)) ✓ then integral_congr with the pointwise identity Jlag(σ+(−T)·I) = conj(Jlag(σ+T·I)) ✓ — from Jlag_conj (n) (hs : (σ+T·I) ≠ 1): Jlag n (conj(σ+T·I)) = conj(Jlag n (σ+T·I)) and conj(σ+T·I) = σ + (−T)·I ✓ — the .symm direction: Jlag(σ+(−T)·I) = conj(Jlag(σ+T·I)) needs: Jlag n (σ+(−T)·I) = Jlag n (conj(σ+T·I)) [by the point identification] = conj(Jlag n (σ+T·I)) [Jlag_conj] ✓ — so the congr's goal: Jlag n (σ + (−T)·I) = conj (Jlag n (σ + T·I)):
```
intro σ hσ
have hid2 : ((σ : ℝ) + (-T) * Complex.I) = (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by
simp [Complex.ext_iff]
rw [hid2, Jlag_conj n (by
intro h
have him : (((σ : ℝ) + T * Complex.I)).im = T := by simp
rw [h] at him
simp at him
linarith [hT0])]
```
Jlag_conj (n) {s} (hs : s ≠ 1) : Jlag n (conj s) = conj (Jlag n s) — with s := σ+T·I: Jlag n (conj(σ+T·I)) = conj(Jlag n (σ+T·I)) ✓ — after rw [hid2] the goal: Jlag n (conj(σ+T·I)) = conj(Jlag n (σ+T·I)) ✓ = Jlag_conj ✓ exactly.
- The intervalIntegral.integral_congr : (∀ x ∈ Ι a b, f x = g x) → ∫ f = ∫ g ✓ (used before — intervalIntegral.integral_congr exists ✓).
- The HIntegral unfold: HIntegral f x₁ x₂ y = ∫ x in x₁..x₂, f (x + y·I) — with f := Jlag n, y := −T: ∫_3^XR Jlag(σ + (−T)·I) ✓.
- The norm step: ‖conj X‖ = ‖X‖: `Complex.norm_conj`?? — or `norm_conj`/`starRingEnd.norm_apply`: (starRingEnd ℂ).norm_apply? — used in LiMoments: "Complex.norm_conj takes starRingEnd DIRECTLY" (session-037 banked) — `Complex.norm_conj (z : ℂ) : ‖(starRingEnd ℂ) z‖ = ‖z‖` ✓ — rw [hconj, Complex.norm_conj] then the RHS's ‖H(T)‖ vs the goal's ‖H(T)‖ — wait the goal after rw [hconj]: ‖conj (H T)‖ ≤ RHS — rw [Complex.norm_conj] : ‖H T‖ ≤ RHS ✓ then exact hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1 ✓.
And the two-side capstone:
```lean
/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for
ii′-6-c): both horizontal right tails, each ≤ DogLegUpper n. -/
theorem dogLegUpper_two_sides {n : ℕ} {T : ℝ}
(hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ +
‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T))‖ ≤
2 * (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
IIMaj (n : ℝ) / 2) := by
rw [show 2 * _ = _ + _ by ring]
exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)
(hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)
```
Hmm — actually for ii′-6-c the two single-side lemmas are the deliverables; the two-side version is a convenience. Include it.
One more consideration — hIntegral_Jlag_low_le_dogLegUpper's norm composition: after rw [hid], the goal is ‖H_high − Vr + Vl‖ ≤ RHS — the norm chain needs care with the associativity of (H − Vr) + Vl vs H − (Vr + ...): hid's RHS is `H(3→XR, U) − V(XR, T→U) + V(3, T→U)` — parsed as `(H − Vr) + Vl` ✓.
Also the norm_add_le/norm_sub_le names: `norm_add_le (a b : α) : ‖a + b‖ ≤ ‖a‖ + ‖b‖` ✓ and `norm_sub_le (a b : α) : ‖a − b‖ ≤ ‖a‖ + ‖b‖` ✓ (used in LiContour ✓).
Let me write DL-5's block now.
`integral_conj` exists. Writing the DL-5 block (upper total + lower by conjugation + two-side capstone).
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"old_string": "end NguyenRH1\n\nend",
"new_string": "/-! ## 7. The total right-horizontal bound (DL-5, D-074 \u00a73.4) -/\n\n/-- **The upper right-tail bound** (D-074 \u00a73.4): for n \u2265 16 and\nT \u2208 [\u221an, \u221an+1] (the T_cut window), U = (3/2)\u00b7T,\n\u2016HIntegral (Jlag n) 3 (2\u221an) T\u2016 \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2 + 8.38 +\nIIMaj(n)/2 \u2014 the exact deformation identity +\nV_left/H_high/V_right piece bounds, all in the zero-free region. -/\ntheorem hIntegral_Jlag_low_le_dogLegUpper {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n have hT0 : (0 : \u211d) < T := by linarith\n have hTn2 : (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 linarith [Real.sqrt_nonneg (n : \u211d)])] at h1\n have hU0 : (0 : \u211d) < (3 / 2) * T := by linarith [hT0]\n have hTU : T \u2264 (3 / 2) * T := by linarith [hT0]\n have hnU : (n : \u211d) \u2264 (4 / 9) * ((3 / 2) * T) ^ 2 := by\n have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by\n field_simp\n ring\n rw [h1]\n exact hTn2\n have hXR : (3 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by linarith\n have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)\n have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)\n have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)\n have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)\n have hlen : (3 / 2) * T - T \u2264 (Real.sqrt (n : \u211d) + 1) / 2 := by linarith [hTn1, hTn]\n have hlen0 : (0 : \u211d) \u2264 (3 / 2) * T - T := by linarith [hT0]\n -- V_left \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2\n have hVl2 : \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by\n refine hVl.trans ?_\n apply mul_le_mul hlen (le_refl _) (by positivity) hlen0\n -- V_right \u2264 IIMaj/2\n have hVr2 : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 \u2264\n IIMaj (n : \u211d) / 2 := by\n have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n have hK : (0 : \u211d) < (Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by\n apply mul_pos (by positivity)\n apply mul_pos (by positivity)\n positivity\n have eA : ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) =\n (1 / 2) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by ring\n have eB : IIMaj (n : \u211d) / 2 =\n (0.57 : \u211d) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by\n unfold IIMaj\n ring\n calc \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016\n \u2264 ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := hVr\n _ \u2264 ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) := by\n have h1 : ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) :=\n mul_le_mul hlen (le_refl _) (by positivity) hlen0\n have h2 : (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 \u2264\n (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d) :=\n mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _)\n exact mul_le_mul h1 h2 (by positivity) (by positivity)\n _ \u2264 IIMaj (n : \u211d) / 2 := by\n rw [eA, eB]\n apply mul_le_mul_of_nonneg_right _ hK.le\n norm_num\n -- assemble via the exact identity\n rw [hid]\n calc \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T) +\n VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016\n \u2264 \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T)\u2016 +\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 +\n \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 := by\n have h1 := norm_add_le\n (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))\n (VIntegral (Jlag n) 3 T ((3 / 2) * T))\n have h2 := norm_sub_le\n (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T))\n (VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))\n linarith [h1, h2]\n _ \u2264 (8.38 : \u211d) + IIMaj (n : \u211d) / 2 +\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=\n add_le_add (add_le_add hH hVr2) hVl2\n _ = ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by ring\n\n/-- **The lower right-tail bound by conjugation** (D-074 \u00a73.4): the\nsame bound holds at im = \u2212T (the integrand is conjugation-symmetric,\nJlag_conj; the interval integral maps conj through). -/\ntheorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by\n have hT0 : (0 : \u211d) < T := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n linarith\n have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T) =\n (starRingEnd \u2102) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T) := by\n unfold HIntegral\n rw [\u2190 integral_conj]\n apply intervalIntegral.integral_congr\n intro \u03c3 h\u03c3\n have hid2 : ((\u03c3 : \u211d) + (-T) * Complex.I) =\n (starRingEnd \u2102) ((\u03c3 : \u211d) + T * Complex.I) := by\n simp [Complex.ext_iff]\n rw [hid2]\n exact Jlag_conj n (by\n intro h\n have him : (((\u03c3 : \u211d) + 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_low_le_dogLegUpper hn hTn hTn1\n\n/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for\nii\u2032-6-c): both horizontal right tails bounded by the dog-leg charge. -/\ntheorem dogLegUpper_two_sides {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 +\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n 2 * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) := by\n rw [show (2 : \u211d) * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +\n (8.38 : \u211d) + IIMaj (n : \u211d) / 2) =\n (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) +\n (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) by ring]\n exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)\n (hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)\n\nend NguyenRH1\n\nend"
}
result 2026-08-26 08:34:29Z → 2026-08-26 08:34:29Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"oldString": "end NguyenRH1\n\nend",
"newString": "/-! ## 7. The total right-horizontal bound (DL-5, D-074 \u00a73.4) -/\n\n/-- **The upper right-tail bound** (D-074 \u00a73.4): for n \u2265 16 and\nT \u2208 [\u221an, \u221an+1] (the T_cut window), U = (3/2)\u00b7T,\n\u2016HIntegral (Jlag n) 3 (2\u221an) T\u2016 \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2 + 8.38 +\nIIMaj(n)/2 \u2014 the exact deformation identity +\nV_left/H_high/V_right piece bounds, all in the zero-free region. -/\ntheorem hIntegral_Jlag_low_le_dogLegUpper {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n have hT0 : (0 : \u211d) < T := by linarith\n have hTn2 : (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 linarith [Real.sqrt_nonneg (n : \u211d)])] at h1\n have hU0 : (0 : \u211d) < (3 / 2) * T := by linarith [hT0]\n have hTU : T \u2264 (3 / 2) * T := by linarith [hT0]\n have hnU : (n : \u211d) \u2264 (4 / 9) * ((3 / 2) * T) ^ 2 := by\n have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by\n field_simp\n ring\n rw [h1]\n exact hTn2\n have hXR : (3 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by linarith\n have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)\n have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)\n have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)\n have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)\n have hlen : (3 / 2) * T - T \u2264 (Real.sqrt (n : \u211d) + 1) / 2 := by linarith [hTn1, hTn]\n have hlen0 : (0 : \u211d) \u2264 (3 / 2) * T - T := by linarith [hT0]\n -- V_left \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2\n have hVl2 : \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by\n refine hVl.trans ?_\n apply mul_le_mul hlen (le_refl _) (by positivity) hlen0\n -- V_right \u2264 IIMaj/2\n have hVr2 : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 \u2264\n IIMaj (n : \u211d) / 2 := by\n have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n have hK : (0 : \u211d) < (Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by\n apply mul_pos (by positivity)\n apply mul_pos (by positivity)\n positivity\n have eA : ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) =\n (1 / 2) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by ring\n have eB : IIMaj (n : \u211d) / 2 =\n (0.57 : \u211d) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by\n unfold IIMaj\n ring\n calc \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016\n \u2264 ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := hVr\n _ \u2264 ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) := by\n have h1 : ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) :=\n mul_le_mul hlen (le_refl _) (by positivity) hlen0\n have h2 : (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 \u2264\n (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d) :=\n mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _)\n exact mul_le_mul h1 h2 (by positivity) (by positivity)\n _ \u2264 IIMaj (n : \u211d) / 2 := by\n rw [eA, eB]\n apply mul_le_mul_of_nonneg_right _ hK.le\n norm_num\n -- assemble via the exact identity\n rw [hid]\n calc \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T) +\n VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016\n \u2264 \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T)\u2016 +\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 +\n \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 := by\n have h1 := norm_add_le\n (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))\n (VIntegral (Jlag n) 3 T ((3 / 2) * T))\n have h2 := norm_sub_le\n (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T))\n (VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))\n linarith [h1, h2]\n _ \u2264 (8.38 : \u211d) + IIMaj (n : \u211d) / 2 +\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=\n add_le_add (add_le_add hH hVr2) hVl2\n _ = ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by ring\n\n/-- **The lower right-tail bound by conjugation** (D-074 \u00a73.4): the\nsame bound holds at im = \u2212T (the integrand is conjugation-symmetric,\nJlag_conj; the interval integral maps conj through). -/\ntheorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by\n have hT0 : (0 : \u211d) < T := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n linarith\n have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T) =\n (starRingEnd \u2102) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T) := by\n unfold HIntegral\n rw [\u2190 integral_conj]\n apply intervalIntegral.integral_congr\n intro \u03c3 h\u03c3\n have hid2 : ((\u03c3 : \u211d) + (-T) * Complex.I) =\n (starRingEnd \u2102) ((\u03c3 : \u211d) + T * Complex.I) := by\n simp [Complex.ext_iff]\n rw [hid2]\n exact Jlag_conj n (by\n intro h\n have him : (((\u03c3 : \u211d) + 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_low_le_dogLegUpper hn hTn hTn1\n\n/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for\nii\u2032-6-c): both horizontal right tails bounded by the dog-leg charge. -/\ntheorem dogLegUpper_two_sides {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 +\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n 2 * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) := by\n rw [show (2 : \u211d) * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +\n (8.38 : \u211d) + IIMaj (n : \u211d) / 2) =\n (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) +\n (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) by ring]\n exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)\n (hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)\n\nend NguyenRH1\n\nend",
"originalFile": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiBasePoints\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n DifferentiableAt \u2102 (Jlag n) s := by\n apply Jlag_differentiableAt\n \u00b7 rintro rfl\n simp at him\n \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n intro s hs\n rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HIntegral (Jlag n) 3 XR T =\n HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n VIntegral (Jlag n) 3 T U := by\n have h0 := rectangleIntegral_Jlag_dogleg_eq_zero (n := n) hT hTU hXR\n unfold RectangleIntegral at h0\n rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n unfold kFun\n simp [map_sub, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n (starRingEnd \u2102) (deriv riemannZeta s) := by\n have h := iteratedDeriv_riemannZeta_conj 1 hs\n rwa [iteratedDeriv_one] at h\n unfold Jlag\n rw [kFun_conj, _root_.riemannZeta_conj, h1]\n simp only [map_mul, map_neg, map_div\u2080]\n\n/-! ## 3. The left-lift bound (DL-2, D-074 \u00a73.3 V_left) -/\n\n/-- **Kernel on the lift**: \u2016kFun n (3+it)\u2016 \u2264 e^{5/2}+1 for n \u2264 t\u00b2\n(D-074 \u00a76: |(3+it)/(2+it)|\u00b2 = (9+t\u00b2)/(4+t\u00b2) = 1 + 5/(4+t\u00b2), whose n-th\npower is \u2264 e^{5n/(2(4+t\u00b2))} \u2264 e^{5/2}). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : \u2115} {t : \u211d}\n (hT : (n : \u211d) \u2264 t ^ 2) :\n \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp (5 / 2) + 1 := by\n rcases Nat.eq_zero_or_pos n with hn | hn\n \u00b7 subst hn\n simp only [kFun, pow_zero, sub_self, norm_zero]\n positivity\n \u00b7 have hnR : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have ht2 : (0 : \u211d) < 4 + t ^ 2 := by positivity\n have hn4t2 : (n : \u211d) \u2264 4 + t ^ 2 := by linarith [hT]\n have hQpos : (0 : \u211d) \u2264 (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n have hQle : (9 + t ^ 2) / (4 + t ^ 2) \u2264 Real.exp (5 / (n : \u211d)) := by\n have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n field_simp [ht2.ne']\n ring\n rw [h1]\n have h2 : 5 / (4 + t ^ 2) \u2264 5 / (n : \u211d) :=\n (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n have h3 := Real.add_one_le_exp (5 / (n : \u211d))\n linarith\n have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 Real.exp 5 := by\n calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 (Real.exp (5 / (n : \u211d))) ^ n :=\n pow_le_pow_left\u2080 hQpos hQle n\n _ = Real.exp 5 := by\n rw [\u2190 Real.exp_nat_mul]\n congr 1\n have hn0 : (n : \u211d) \u2260 0 := by exact_mod_cast hn.ne'\n field_simp [hn0]\n have hns3 : Complex.normSq ((3 : \u211d) + t * Complex.I) = 9 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hns2 : Complex.normSq ((2 : \u211d) + t * Complex.I) = 4 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hnormA : \u2016((3 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (9 + t ^ 2) := by\n have h1 : \u2016((3 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt (Complex.normSq ((3 : \u211d) + t * Complex.I)) := by\n rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n rw [h1, hns3]\n have hnormB : \u2016((2 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (4 + t ^ 2) := by\n have h1 : \u2016((2 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt (Complex.normSq ((2 : \u211d) + t * Complex.I)) := by\n rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n rw [h1, hns2]\n have hnorm : \u2016((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n rw [norm_div, hnormA, hnormB,\n \u2190 Real.sqrt_div (by positivity : (0 : \u211d) \u2264 9 + t ^ 2)]\n have hs1 : ((3 : \u211d) + t * Complex.I) - 1 = (2 : \u211d) + t * Complex.I := by\n push_cast\n ring\n unfold kFun\n rw [hs1]\n calc \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le _ _\n _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n rw [norm_pow, hnorm, norm_one]\n _ \u2264 Real.exp (5 / 2) + 1 := by\n have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n \u2264 Real.exp (5 / 2) := by\n have hx0 : (0 : \u211d) \u2264 Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) :=\n Real.sqrt_nonneg _\n have hx : (0 : \u211d) \u2264 (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n :=\n pow_nonneg hx0 n\n have h5 : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 \u2264 Real.exp 5 := by\n have e : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 =\n ((9 + t ^ 2) / (4 + t ^ 2)) ^ n := by\n rw [\u2190 pow_mul, mul_comm n 2, pow_mul, Real.sq_sqrt hQpos]\n rw [e]\n exact hQn\n have h8 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n =\n Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2) := by\n rw [Real.sqrt_sq hx]\n rw [h8]\n calc Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2)\n \u2264 Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt h5\n _ = Real.exp (5 / 2) := (Real.exp_half 5).symm\n linarith [h4]\n\n/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/\ndef dirichletC3 : \u211d :=\n \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016\n\n/-- Termwise 3-vs-2 comparison for the \u039b L-series: \u039b(n)/n\u00b3 \u2264 (1/2)\u00b7\u039b(n)/n\u00b2. -/\nlemma norm_term_vonMangoldt_three_le_half (n : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 \u2264\n (1 / 2) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 := by\n have h3re : ((3 : \u2102).re) = 3 := rfl\n have h2re : ((2 : \u2102).re) = 2 := rfl\n simp only [LSeries.norm_term_eq, h3re, h2re]\n split\n \u00b7 norm_num\n \u00b7 next hn =>\n rcases eq_or_ne n 1 with rfl | hn1\n \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n \u00b7 have hn2 : 2 \u2264 n := by omega\n have h\u039b : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016 =\n ArithmeticFunction.vonMangoldt n :=\n Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n rw [h\u039b]\n have e : ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d) =\n (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := by\n rw [show (3 : \u211d) = 2 + 1 by norm_num,\n Real.rpow_add (by positivity : (0 : \u211d) < (n : \u211d)), Real.rpow_one]\n field_simp [show (n : \u211d) \u2260 0 by positivity]\n have h12 : (1 : \u211d) / (n : \u211d) \u2264 1 / 2 :=\n one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 2)\n (by exact_mod_cast hn2 : (2 : \u211d) \u2264 (n : \u211d))\n have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d) :=\n div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (n : \u211d)) _)\n calc ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d)\n = (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := e\n _ \u2264 (1 / 2) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) :=\n mul_le_mul_of_nonneg_right h12 hpos\n\n/-- dirichletC3 \u2264 1/2 (the termwise comparison + dirichletC2 \u2264 1) \u2014\nthe certified C_zeta3 = 0.5 of D-074 \u00a74. (A tighter 0.17 build is\npossible via a 6-prime partial sum + antitone-integral tail; the fold\nis indifferent to the constant, so the cheap certified 0.5 is charged.) -/\nlemma dirichletC3_le_half : dirichletC3 \u2264 1 / 2 := by\n have hsum3 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n calc dirichletC3\n = \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 := rfl\n _ \u2264 \u2211' n : \u2115, (1 / 2) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n (hsum2.mul_left (1 / 2))\n _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n _ \u2264 1 / 2 := by linarith [dirichletC2_le_one]\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 dirichletC3 for re s \u2265 3 (the s = 3 clone of the\nDirichlet-series majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : \u2102} (hs : 3 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC3 := by\n have hs1 : (1 : \u211d) < s.re := by linarith\n have h1 : -logDeriv riemannZeta s\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum3 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n \u2264 dirichletC3 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n simp\n exact hs) n) hsumS hsum3\n _ = dirichletC3 := rfl\n calc \u2016logDeriv riemannZeta s\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 dirichletC3 := hle\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 1/2 for re s \u2265 3 (the charged C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : \u2102} (hs : 3 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 1 / 2 :=\n (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half\n\n/-- **The left-lift bound** (D-074 \u00a73.3 V_left): for 0 < T \u2264 U and\nn \u2264 T\u00b2, \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U \u2212 T)\u00b7(e^{5/2}+1)/2. The kernel\n\u2264 e^{5/2}+1 (the 1+5/(4+t\u00b2) computation), the zeta factor \u2264 1/2\n(certified, no perimeter). -/\ntheorem vIntegral_Jlag_three_norm_le {n : \u2115} {T U : \u211d}\n (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n have hnorm : \u2016VIntegral (Jlag n) 3 T U\u2016 =\n \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n rw [hnorm]\n have hbound : \u2200 t \u2208 Set.Ioc T U,\n \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 (Real.exp (5 / 2) + 1) * (1 / 2) := by\n intro t ht\n have htT : T < t := ht.1\n have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n have hre : (3 : \u211d) \u2264 ((3 : \u211d) + t * Complex.I).re := by simp\n have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n have h2 := norm_logDeriv_zeta_le_half (s := (3 : \u211d) + t * Complex.I) hre\n have hnorm3 : \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta ((3 : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n ((3 : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta ((3 : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hnorm3]\n exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n have hint : \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264\n ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n apply intervalIntegral.norm_integral_le_of_norm_le_const\n intro t ht\n rw [Set.uIoc_of_le hTU] at ht\n exact hbound t ht\n have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n rw [habs] at hint\n calc \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016\n \u2264 ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n\n/-! ## 4. The high-horizontal stepping (DL-3, D-074 \u00a77 + D-073 \u00a74) -/\n\n/-- Termwise \u03c3-vs-2 comparison for the \u039b L-series (the (6.10) halving):\n\u039b(m)/m^\u03c3 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7\u039b(m)/m\u00b2 for \u03c3 \u2265 2. -/\nlemma norm_term_vonMangoldt_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) m\u2016 \u2264\n (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n have h\u03c3re : ((\u03c3 : \u211d) + t * Complex.I).re = \u03c3 := by simp\n have h2re : ((2 : \u2102).re) = 2 := rfl\n simp only [LSeries.norm_term_eq, h\u03c3re, h2re]\n split\n \u00b7 norm_num\n \u00b7 next hm =>\n have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n ArithmeticFunction.vonMangoldt m :=\n Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n rw [h\u039b]\n rcases eq_or_ne m 1 with rfl | hm1\n \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n \u00b7 have hm2 : 2 \u2264 m := by omega\n have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ \u03c3 =\n (1 / (m : \u211d) ^ (\u03c3 - 2)) * (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,\n Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]\n field_simp [show (m : \u211d) \u2260 0 by positivity]\n ring_nf\n rw [e]\n have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2), \u2190 one_div]\n apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)\n have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n exact mul_le_mul_of_nonneg_right hle hpos\n\n/-- \u2016\u03b6\u2032/\u03b6(\u03c3+it)\u2016 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2 for \u03c3 \u2265 2 (the (6.10)\nhalving in LSeries form; dirichletC2 \u2264 1 makes the tail free). -/\nlemma norm_logDeriv_zeta_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) :\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n have hs1 : (1 : \u211d) < ((\u03c3 : \u211d) + t * Complex.I).re := by simp; linarith\n have h1 : -logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) ((\u03c3 : \u211d) + t * Complex.I) := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, (2 : \u211d) ^ (-(\u03c3 - 2)) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_le_two_pow h\u03c3 n) hsumS\n (hsum2.mul_left _)\n _ = (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n calc \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := hle\n\n/-- **Kernel envelope** (D-074 \u00a77, the single-exponential form that\nreplaces the unit-step geometric series): \u2016(1+1/((\u03c3\u22121)+iU))\u207f\u2016 \u2264\ne^{(4/9)\u03c3} for \u03c3 \u2265 3 and n \u2264 (4/9)U\u00b2. From the (6.11) core\n\u20161+1/s\u2016 \u2264 1+(re s+1)/normSq s \u2264 1+\u03c3/U\u00b2. -/\ntheorem one_add_div_pow_norm_le_exp_four_ninths {n : \u2115} {\u03c3 U : \u211d}\n (h\u03c3 : 3 \u2264 \u03c3) (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) :\n \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 Real.exp ((4 / 9) * \u03c3) := by\n have hs0 : (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2260 0 := by\n intro h\n have him : (((\u03c3 : \u211d) - 1) + U * Complex.I).im = 0 := by rw [h]; simp\n simp at him\n linarith\n have hle := norm_one_add_one_div_le hs0\n have hre : (((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1 = \u03c3 := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n Complex.sub_re, Complex.one_re]\n have hns : Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) = (\u03c3 - 1) ^ 2 + U ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hstep : ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 \u03c3 / U ^ 2 := by\n rw [hre, hns]\n have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n have h1 : (0 : \u211d) \u2264 (\u03c3 - 1) ^ 2 := sq_nonneg _\n exact (div_le_div_iff_of_pos_left (by linarith : (0 : \u211d) < \u03c3)\n (by positivity) hU2).mpr (by linarith [h1])\n have hstep1 : 1 + ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 1 + \u03c3 / U ^ 2 := by\n linarith [hstep]\n have hpow1 : \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 (1 + \u03c3 / U ^ 2) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep1) n\n have hpow2 : (1 + \u03c3 / U ^ 2) ^ n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n calc (1 + \u03c3 / U ^ 2) ^ n \u2264 (Real.exp (\u03c3 / U ^ 2)) ^ n := by\n have h := Real.add_one_le_exp (\u03c3 / U ^ 2)\n exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n _ = Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := (Real.exp_nat_mul (\u03c3 / U ^ 2) n).symm\n have hexp : (n : \u211d) * (\u03c3 / U ^ 2) \u2264 (4 / 9) * \u03c3 := by\n have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n have h\u03c30 : (0 : \u211d) < \u03c3 := by linarith\n have h1 : (n : \u211d) / U ^ 2 \u2264 4 / 9 := by\n have h2 := div_le_div_of_nonneg_right hnU hU2.le\n rwa [mul_div_cancel_right\u2080 _ hU2.ne'] at h2\n rw [show (n : \u211d) * (\u03c3 / U ^ 2) = ((n : \u211d) / U ^ 2) * \u03c3 by ring]\n exact mul_le_mul_of_nonneg_right h1 h\u03c30.le\n calc \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n\n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := hpow1.trans hpow2\n _ \u2264 Real.exp ((4 / 9) * \u03c3) := Real.exp_le_exp.mpr hexp\n\n/-! ## 5. The product envelope and the integral assembly (DL-3c/d) -/\n\n/-- **The product envelope** (D-074 \u00a77): for \u03c3 \u2265 3, 0 < t, n \u2264 (4/9)t\u00b2,\n\u2016Jlag n (\u03c3+it)\u2016 \u2264 (4\u00b7e^{\u2212c\u03c3} + 4\u00b72^{\u2212\u03c3})\u00b7dirichletC2, c = log 2 \u2212 4/9.\nThe kernel envelope (e^{(4/9)\u03c3}) times the zeta halving (2^{\u2212(\u03c3\u22122)})\ncollapses to the single exponential 4\u00b7e^{\u2212c\u03c3}: no geometric series. -/\ntheorem Jlag_dogleg_norm_le_envelope {n : \u2115} {\u03c3 t : \u211d}\n (h\u03c3 : 3 \u2264 \u03c3) (ht : 0 < t) (hnU : (n : \u211d) \u2264 (4 / 9) * t ^ 2) :\n \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n have hw1 : ((\u03c3 : \u211d) + t * Complex.I) - 1 = ((\u03c3 : \u211d) - 1) + t * Complex.I := by\n ring\n have hs1ne : (((\u03c3 : \u211d) - 1) + t * Complex.I) \u2260 0 := by\n intro h\n have him : (((\u03c3 : \u211d) - 1) + t * Complex.I).im = 0 := by rw [h]; simp\n simp at him\n linarith\n have hwid : ((\u03c3 : \u211d) + t * Complex.I) / (((\u03c3 : \u211d) + t * Complex.I) - 1) =\n 1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I) := by\n rw [hw1]\n field_simp [hs1ne]\n ring\n have hker := one_add_div_pow_norm_le_exp_four_ninths h\u03c3 ht hnU\n have hzeta := norm_logDeriv_zeta_le_two_pow (show (2 : \u211d) \u2264 \u03c3 by linarith) (t := t)\n have hk : \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp ((4 / 9) * \u03c3) + 1 := by\n unfold kFun\n rw [hwid]\n calc \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n _ = \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I))\u2016 ^ n + 1 := by rw [norm_pow, norm_one]\n _ \u2264 Real.exp ((4 / 9) * \u03c3) + 1 := by linarith [hker]\n have hprod : \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2) := by\n have hn3 : \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hn3]\n exact mul_le_mul hk hzeta (norm_nonneg _)\n (add_nonneg (Real.exp_nonneg _) (by norm_num))\n have h2b : (2 : \u211d) ^ (-\u03c3) = Real.exp (-(Real.log 2) * \u03c3) := by\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n have h22 : (2 : \u211d) ^ (2 : \u211d) = 4 := by\n rw [Real.rpow_two]\n norm_num\n have h2a : (2 : \u211d) ^ (-(\u03c3 - 2)) = 4 * (2 : \u211d) ^ (-\u03c3) := by\n rw [show (-(\u03c3 - 2)) = -\u03c3 + 2 by ring, Real.rpow_add (by norm_num : (0 : \u211d) < 2), h2b, h22]\n ring\n have hexp_alg : Real.exp ((4 / 9) * \u03c3) * Real.exp (-(Real.log 2) * \u03c3) =\n Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) := by\n rw [\u2190 Real.exp_add]\n congr 1\n ring\n have halg : (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2))) =\n 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3) := by\n rw [h2a, h2b]\n calc (Real.exp ((4 / 9) * \u03c3) + 1) * (4 * Real.exp (-(Real.log 2) * \u03c3))\n = 4 * (Real.exp ((4 / 9) * \u03c3) * Real.exp (-(Real.log 2) * \u03c3)) +\n 4 * Real.exp (-(Real.log 2) * \u03c3) := by ring\n _ = 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * Real.exp (-(Real.log 2) * \u03c3) := by\n rw [hexp_alg]\n calc \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016\n \u2264 (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2) := hprod\n _ = dirichletC2 * ((Real.exp ((4 / 9) * \u03c3) + 1) * (2 : \u211d) ^ (-(\u03c3 - 2))) := by ring\n _ = dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n rw [halg]\n\n/-- The FTC-bound \u222b\u2083^XR e^{\u2212c\u03c3}d\u03c3 \u2264 e^{\u22123c}/c for c > 0. -/\nlemma integral_exp_neg_le {c XR : \u211d} (hc : 0 < c) (_hXR : 3 \u2264 XR) :\n \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-c * \u03c3) \u2264 Real.exp (-3 * c) / c := by\n have hF : \u2200 x \u2208 Set.uIcc (3 : \u211d) XR,\n HasDerivAt (fun \u03c3 => -Real.exp (-c * \u03c3) / c) (Real.exp (-c * x)) x := by\n intro x hx\n have h2 : HasDerivAt (fun \u03c3 => Real.exp (-c * \u03c3)) (Real.exp (-c * x) * (-c)) x := by\n have h := ((hasDerivAt_id' x).const_mul (-c)).exp\n rwa [mul_one] at h\n have h3 := h2.const_mul (-1 / c)\n rw [show (-1 / c) * (Real.exp (-c * x) * (-c)) = Real.exp (-c * x) by\n field_simp [hc.ne']] at h3\n have h5 : (fun \u03c3 => (-1 / c) * Real.exp (-c * \u03c3)) =\n (fun \u03c3 => -Real.exp (-c * \u03c3) / c) := by\n funext \u03c3\n field_simp [hc.ne']\n rw [h5] at h3\n exact h3\n have hint : IntervalIntegrable (fun \u03c3 => Real.exp (-c * \u03c3)) MeasureTheory.volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn\n have e : Real.exp (-c * 3) = Real.exp (-3 * c) := by\n congr 1\n ring\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint, e]\n have h1 : (0 : \u211d) \u2264 Real.exp (-c * XR) := (Real.exp_pos _).le\n have h2 : (0 : \u211d) < c := hc\n rw [show -Real.exp (-c * XR) / c - -Real.exp (-3 * c) / c =\n (Real.exp (-3 * c) - Real.exp (-c * XR)) / c by\n field_simp [h2.ne']\n ring]\n rw [show Real.exp (-3 * c) / c = (Real.exp (-3 * c) - (0 : \u211d)) / c by ring]\n exact div_le_div_of_nonneg_right (by linarith [h1]) h2.le\n\n/-- The certified exponent-decay constant c = log 2 \u2212 4/9 \u2265 0.2487. -/\nlemma cdog_gt : (0.2487 : \u211d) \u2264 Real.log 2 - 4 / 9 := by\n have h := Real.log_two_gt_d9\n norm_num at h\n linarith\n\n/-- The certified e^{4/3} \u2264 3.8073 (the (1\u2212x/16)\u207b\u00b9\u2076 route + d9 e). -/\nlemma exp_four_thirds_le : Real.exp (4 / 3) \u2264 (3.8073 : \u211d) := by\n have he13 : Real.exp (1 / 3) \u2264 (1.4006 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n rw [show (4 / 3 : \u211d) = 1 + 1 / 3 by norm_num, Real.exp_add]\n calc Real.exp 1 * Real.exp (1 / 3) \u2264 2.7182818286 * 1.4006 :=\n mul_le_mul Real.exp_one_lt_d9.le he13 (Real.exp_pos _).le (by norm_num)\n _ \u2264 3.8073 := by norm_num\n\n/-- **THE HIGH-HORIZONTAL BOUND** (D-074 \u00a77 capstone; D-073 Cor 4.2's\nR(1.5) in single-exponential-envelope form): for 0 < U, n \u2264 (4/9)U\u00b2\n(i.e. U \u2265 (3/2)\u221an) and 3 \u2264 XR, \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 8.38\n(charged; the true value \u2264 1.2 at n = 10\u2075, E-034 V5). Charged with\ndirichletC2 \u2264 1 \u2014 the tight R(1.5) = 5.94 would need a dirichletC2 \u2264\n0.57 build (documented as the tightening path; the fold is\nindifferent: \u0394 \u2248 +2.4 per side). -/\ntheorem hIntegral_Jlag_dogleg_norm_le {n : \u2115} {U XR : \u211d}\n (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) (hXR : 3 \u2264 XR) :\n \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 (8.38 : \u211d) := by\n have hc : (0 : \u211d) < Real.log 2 - 4 / 9 := by\n have h := cdog_gt\n linarith\n have hpt : \u2200 \u03c3 \u2208 Set.Ioc 3 XR,\n \u2016Jlag n ((\u03c3 : \u211d) + U * Complex.I)\u2016 \u2264\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) :=\n fun \u03c3 h\u03c3 => Jlag_dogleg_norm_le_envelope (by linarith [h\u03c3.1]) hU hnU\n have hcontA : Continuous (fun \u03c3 : \u211d => Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) :=\n Real.continuous_exp.comp (continuous_const.mul continuous_id)\n have hcontB : Continuous (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) := by\n have h1 : Continuous (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) :=\n Real.continuous_exp.comp (continuous_const.mul continuous_id)\n have h2 : (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) =\n (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) := by\n funext \u03c3\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n rw [h2]\n exact h1\n have hIntA : IntervalIntegrable (fun \u03c3 : \u211d => 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3))\n MeasureTheory.volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (hcontA.const_mul 4).continuousOn\n have hIntB : IntervalIntegrable (fun \u03c3 : \u211d => 4 * (2 : \u211d) ^ (-\u03c3)) MeasureTheory.volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (hcontB.const_mul 4).continuousOn\n have hIntG : IntervalIntegrable (fun \u03c3 : \u211d =>\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)))\n MeasureTheory.volume 3 XR := by\n have h := (hIntA.add hIntB).const_mul dirichletC2\n convert h using 1\n -- step 1: \u2016H\u2016 \u2264 \u222b envelope\n have h1 : \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264\n \u222b \u03c3 in (3 : \u211d)..XR,\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n unfold HIntegral\n apply intervalIntegral.norm_integral_le_of_norm_le hXR _ hIntG\n exact Filter.Eventually.of_forall (fun \u03c3 h\u03c3 => hpt \u03c3 h\u03c3)\n -- step 2: \u222b envelope = dirichletC2\u00b7(4\u222be^{\u2212c\u03c3} + 4\u222b2^{\u2212\u03c3})\n have h2 : \u222b \u03c3 in (3 : \u211d)..XR,\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3))\n = dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) := by\n rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_add hIntA hIntB]\n -- step 3: the two integral bounds\n have h3a : \u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) \u2264\n Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n rw [intervalIntegral.integral_const_mul]\n have h := integral_exp_neg_le hc hXR\n have he3c : Real.exp (-3 * (Real.log 2 - 4 / 9)) = Real.exp (4 / 3) / 8 := by\n have h3l2 : Real.exp (-(3 * Real.log 2)) = 1 / 8 := by\n have e1 : -(3 * Real.log 2) = Real.log (1 / 8) := by\n rw [show ((1 : \u211d) / 8) = (2 ^ 3 : \u211d)\u207b\u00b9 by norm_num, Real.log_inv, Real.log_pow,\n Nat.cast_ofNat]\n rw [e1, Real.exp_log (by norm_num : (0 : \u211d) < 1 / 8)]\n calc Real.exp (-3 * (Real.log 2 - 4 / 9))\n = Real.exp ((4 / 3) + -(3 * Real.log 2)) := by congr 1; ring\n _ = Real.exp (4 / 3) * Real.exp (-(3 * Real.log 2)) := by rw [Real.exp_add]\n _ = Real.exp (4 / 3) / 8 := by rw [h3l2]; ring\n rw [he3c] at h\n calc 4 * \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)\n \u2264 4 * ((Real.exp (4 / 3) / 8) / (Real.log 2 - 4 / 9)) :=\n mul_le_mul_of_nonneg_left h (by norm_num)\n _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n field_simp [hc.ne']\n ring\n have h3b : \u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3) \u2264 1 / (2 * Real.log 2) := by\n have h2e : (fun \u03c3 : \u211d => 4 * (2 : \u211d) ^ (-\u03c3)) =\n (fun \u03c3 : \u211d => 4 * Real.exp (-(Real.log 2) * \u03c3)) := by\n funext \u03c3\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n rw [h2e, intervalIntegral.integral_const_mul]\n have h := integral_exp_neg_le (Real.log_pos (by norm_num : (1 : \u211d) < 2)) hXR\n have h3l2 : Real.exp (-3 * Real.log 2) = 1 / 8 := by\n have e1 : (-3 * Real.log 2) = Real.log (1 / 8) := by\n rw [show ((1 : \u211d) / 8) = (2 ^ 3 : \u211d)\u207b\u00b9 by norm_num, Real.log_inv, Real.log_pow,\n Nat.cast_ofNat]\n ring\n rw [e1, Real.exp_log (by norm_num : (0 : \u211d) < 1 / 8)]\n rw [h3l2] at h\n calc 4 * \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-(Real.log 2) * \u03c3)\n \u2264 4 * ((1 / 8) / Real.log 2) := by\n apply mul_le_mul_of_nonneg_left h (by norm_num : (0 : \u211d) \u2264 4)\n _ = 1 / (2 * Real.log 2) := by\n field_simp [(Real.log_pos (by norm_num : (1 : \u211d) < 2)).ne']\n norm_num\n -- step 4: the certified assembly\n have hlog2 : (0.6931471803 : \u211d) \u2264 Real.log 2 := Real.log_two_gt_d9.le\n have h48 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) \u2264 (7.6545 : \u211d) := by\n have hcge := cdog_gt\n have h1 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) \u2264 3.8073 / (2 * 0.2487) :=\n div_le_div\u2080 (by norm_num : (0 : \u211d) \u2264 3.8073) exp_four_thirds_le\n (by norm_num : (0 : \u211d) < 2 * 0.2487) (by linarith [hcge])\n calc Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9))\n \u2264 3.8073 / (2 * 0.2487) := h1\n _ \u2264 7.6545 := by norm_num\n have h72 : 1 / (2 * Real.log 2) \u2264 (0.7214 : \u211d) := by\n have h1 : 1 / (2 * Real.log 2) \u2264 1 / (2 * 0.6931471803) :=\n one_div_le_one_div_of_le (by positivity) (by linarith)\n calc 1 / (2 * Real.log 2) \u2264 1 / (2 * 0.6931471803) := h1\n _ \u2264 0.7214 := by norm_num\n have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n have hsum : dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) \u2264 (8.38 : \u211d) := by\n have hA0 : (0 : \u211d) \u2264 Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by positivity\n have hB0 : (0 : \u211d) \u2264 1 / (2 * Real.log 2) := by positivity\n have hIntAB : (0 : \u211d) \u2264 (\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)) := by\n apply add_nonneg\n \u00b7 apply intervalIntegral.integral_nonneg hXR\n intro \u03c3 h\u03c3\n positivity\n \u00b7 apply intervalIntegral.integral_nonneg hXR\n intro \u03c3 h\u03c3\n positivity\n calc dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)))\n \u2264 1 * (Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2)) := by\n apply mul_le_mul hC2 (add_le_add h3a h3b) hIntAB (by norm_num)\n _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2) := by ring\n _ \u2264 7.6545 + 0.7214 := add_le_add h48 h72\n _ \u2264 8.38 := by norm_num\n calc \u2016HIntegral (Jlag n) 3 XR U\u2016\n \u2264 \u222b \u03c3 in (3 : \u211d)..XR,\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := h1\n _ = dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) := h2\n _ \u2264 8.38 := hsum\n\n/-! ## 6. The far-right vertical drop (DL-4, D-074 \u00a78) -/\n\n/-- **Kernel at the far-right vertical** (D-074 \u00a78): for n \u2265 16 and\nt\u00b2 \u2265 n, \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2}+1. (The ii\u2032-4 lemma\n`kFun_shift_norm_le_exp_sqrt_half_add_one` takes re s \u2265 2\u221an, i.e.\nre w \u2265 2\u221an+1 \u2014 this is the w = 2\u221an variant: |1+1/(w\u22121)| \u2264\n1+(2\u221an)/((2\u221an\u22121)\u00b2+t\u00b2) \u2264 1+1/(2\u221an) since 4\u221an\u22121 \u2264 t\u00b2.) -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_half_add_one {n : \u2115} {t : \u211d}\n (hn : 16 \u2264 n) (ht : (n : \u211d) \u2264 t ^ 2) :\n \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsq : (0 : \u211d) < Real.sqrt (n : \u211d) := Real.sqrt_pos.mpr (by linarith)\n have hw1 : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1 =\n ((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I := by\n push_cast\n ring\n have hs0 : ((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I \u2260 0 := by\n intro h\n have him : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).im = 0 := by\n rw [h]; simp\n simp at him\n have ht0 : t = 0 := by\n have h1 : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).im = t := by simp\n linarith\n rw [ht0] at ht\n nlinarith [hnR]\n have hle := norm_one_add_one_div_le hs0\n have hre : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).re + 1 =\n 2 * Real.sqrt (n : \u211d) := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n Complex.sub_re, Complex.one_re]\n have hns : Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) =\n (2 * Real.sqrt (n : \u211d) - 1) ^ 2 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hkey : (2 * Real.sqrt (n : \u211d)) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 / (2 * Real.sqrt (n : \u211d)) := by\n rw [hns]\n have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n have h1 : 4 * Real.sqrt (n : \u211d) - 1 \u2264 t ^ 2 := by\n have h2 : 4 * Real.sqrt (n : \u211d) \u2264 (n : \u211d) + 1 := by\n have h3 : (4 * Real.sqrt (n : \u211d)) ^ 2 \u2264 ((n : \u211d) + 1) ^ 2 := by\n rw [show (4 * Real.sqrt (n : \u211d)) ^ 2 = 16 * (Real.sqrt (n : \u211d) ^ 2) by ring, hsqn]\n nlinarith [sq_nonneg ((n : \u211d) - 1), hnR]\n nlinarith [hsq]\n nlinarith [ht, h2]\n rw [show (2 * Real.sqrt (n : \u211d) - 1) ^ 2 + t ^ 2 =\n 4 * (Real.sqrt (n : \u211d) ^ 2) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2 by ring, hsqn]\n have h4 : (0 : \u211d) < 4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2 := by\n nlinarith [ht, sq_nonneg t, hsq]\n rw [div_le_iff\u2080 h4,\n show (1 / (2 * Real.sqrt (n : \u211d))) * (4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2) =\n (4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2) / (2 * Real.sqrt (n : \u211d)) by\n field_simp [hsq.ne'],\n le_div_iff\u2080 (by linarith [hsq] : (0 : \u211d) < 2 * Real.sqrt (n : \u211d))]\n nlinarith [h1, ht, hsq, hsqn]\n have hstep : 1 + ((((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).re + 1) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 + 1 / (2 * Real.sqrt (n : \u211d)) := by\n rw [hre]\n have h1 : (2 * Real.sqrt (n : \u211d)) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 / (2 * Real.sqrt (n : \u211d)) := hkey\n linarith [h1]\n have hpow1 : \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I))\u2016 ^ n \u2264\n (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep) n\n have hpow2 : (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2) := by\n calc (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n\n \u2264 (Real.exp (1 / (2 * Real.sqrt (n : \u211d)))) ^ n := by\n have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : \u211d)))\n exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n _ = Real.exp ((n : \u211d) * (1 / (2 * Real.sqrt (n : \u211d)))) :=\n (Real.exp_nat_mul _ n).symm\n _ = Real.exp (Real.sqrt (n : \u211d) / 2) := by\n congr 1\n have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n field_simp [hsq.ne']\n nlinarith [hsqn]\n have hwid : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) /\n ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1) =\n 1 + 1 / (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) := by\n rw [hw1]\n field_simp [hs0]\n push_cast\n ring\n unfold kFun\n rw [hwid]\n calc \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le _ _\n _ = \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I))\u2016 ^ n + 1 := by\n rw [norm_pow, norm_one]\n _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by linarith [hpow1.trans hpow2]\n\n/-- **The far-right vertical drop** (D-074 \u00a78 V_right): for n \u2265 16,\n0 < T \u2264 U, T\u00b2 \u2265 n, \u2016VIntegral (Jlag n) (2\u221an) T U\u2016 \u2264\n(U\u2212T)\u00b7(e^{\u221an/2}+1)\u00b72^{\u2212(2\u221an\u22122)}\u00b7dirichletC2 \u2014 exponentially tiny. -/\ntheorem vIntegral_Jlag_right_norm_le {n : \u2115} {T U : \u211d}\n (hn : 16 \u2264 n) (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T U\u2016 \u2264\n (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by\n have hnorm : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T U\u2016 =\n \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n rw [hnorm]\n have hbound : \u2200 t \u2208 Set.Ioc T U,\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by\n intro t ht\n have htT : T < t := ht.1\n have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n have h1 := kFun_right_vertical_norm_le_exp_sqrt_half_add_one hn ht2\n have h2 := norm_logDeriv_zeta_le_two_pow\n (show (2 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsq : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n linarith) (t := t)\n have hnorm3 : \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hnorm3]\n exact mul_le_mul h1 h2 (norm_nonneg _)\n (add_nonneg (Real.exp_nonneg _) (by norm_num))\n have hint : \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n ((Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2)) * |U - T| := by\n apply intervalIntegral.norm_integral_le_of_norm_le_const\n intro t ht\n rw [Set.uIoc_of_le hTU] at ht\n exact hbound t ht\n have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n rw [habs] at hint\n calc \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016\n \u2264 ((Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2)) * (U - T) := hint\n _ = (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by ring\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 875,
"oldLines": 6,
"newStart": 875,
"newLines": 159,
"lines": [
" _ = (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *",
" ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by ring",
" ",
"+/-! ## 7. The total right-horizontal bound (DL-5, D-074 \u00a73.4) -/",
"+",
"+/-- **The upper right-tail bound** (D-074 \u00a73.4): for n \u2265 16 and",
"+T \u2208 [\u221an, \u221an+1] (the T_cut window), U = (3/2)\u00b7T,",
"+\u2016HIntegral (Jlag n) 3 (2\u221an) T\u2016 \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2 + 8.38 +",
"+IIMaj(n)/2 \u2014 the exact deformation identity +",
"+V_left/H_high/V_right piece bounds, all in the zero-free region. -/",
"+theorem hIntegral_Jlag_low_le_dogLegUpper {n : \u2115} {T : \u211d}",
"+ (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :",
"+ \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 \u2264",
"+ ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +",
"+ IIMaj (n : \u211d) / 2 := by",
"+ have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn",
"+ have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by",
"+ have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=",
"+ Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))",
"+ have h2 : Real.sqrt 16 = 4 := by",
"+ rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num",
"+ rwa [h2] at h1",
"+ have hT0 : (0 : \u211d) < T := by linarith",
"+ have hTn2 : (n : \u211d) \u2264 T ^ 2 := by",
"+ have h1 : (Real.sqrt (n : \u211d)) ^ 2 \u2264 T ^ 2 :=",
"+ pow_le_pow_left\u2080 (Real.sqrt_nonneg _) hTn 2",
"+ rwa [Real.sq_sqrt (by linarith [Real.sqrt_nonneg (n : \u211d)])] at h1",
"+ have hU0 : (0 : \u211d) < (3 / 2) * T := by linarith [hT0]",
"+ have hTU : T \u2264 (3 / 2) * T := by linarith [hT0]",
"+ have hnU : (n : \u211d) \u2264 (4 / 9) * ((3 / 2) * T) ^ 2 := by",
"+ have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by",
"+ field_simp",
"+ ring",
"+ rw [h1]",
"+ exact hTn2",
"+ have hXR : (3 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by linarith",
"+ have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)",
"+ have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)",
"+ have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)",
"+ have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)",
"+ have hlen : (3 / 2) * T - T \u2264 (Real.sqrt (n : \u211d) + 1) / 2 := by linarith [hTn1, hTn]",
"+ have hlen0 : (0 : \u211d) \u2264 (3 / 2) * T - T := by linarith [hT0]",
"+ -- V_left \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2",
"+ have hVl2 : \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 \u2264",
"+ ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by",
"+ refine hVl.trans ?_",
"+ apply mul_le_mul hlen (le_refl _) (by positivity) hlen0",
"+ -- V_right \u2264 IIMaj/2",
"+ have hVr2 : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 \u2264",
"+ IIMaj (n : \u211d) / 2 := by",
"+ have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one",
"+ have hK : (0 : \u211d) < (Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *",
"+ ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by",
"+ apply mul_pos (by positivity)",
"+ apply mul_pos (by positivity)",
"+ positivity",
"+ have eA : ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *",
"+ ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) =",
"+ (1 / 2) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *",
"+ ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by ring",
"+ have eB : IIMaj (n : \u211d) / 2 =",
"+ (0.57 : \u211d) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *",
"+ ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by",
"+ unfold IIMaj",
"+ ring",
"+ calc \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016",
"+ \u2264 ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *",
"+ ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := hVr",
"+ _ \u2264 ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *",
"+ ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) := by",
"+ have h1 : ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) \u2264",
"+ ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) :=",
"+ mul_le_mul hlen (le_refl _) (by positivity) hlen0",
"+ have h2 : (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 \u2264",
"+ (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d) :=",
"+ mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _)",
"+ exact mul_le_mul h1 h2 (by positivity) (by positivity)",
"+ _ \u2264 IIMaj (n : \u211d) / 2 := by",
"+ rw [eA, eB]",
"+ apply mul_le_mul_of_nonneg_right _ hK.le",
"+ norm_num",
"+ -- assemble via the exact identity",
"+ rw [hid]",
"+ calc \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -",
"+ VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T) +",
"+ VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016",
"+ \u2264 \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T)\u2016 +",
"+ \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 +",
"+ \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 := by",
"+ have h1 := norm_add_le",
"+ (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -",
"+ VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))",
"+ (VIntegral (Jlag n) 3 T ((3 / 2) * T))",
"+ have h2 := norm_sub_le",
"+ (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T))",
"+ (VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))",
"+ linarith [h1, h2]",
"+ _ \u2264 (8.38 : \u211d) + IIMaj (n : \u211d) / 2 +",
"+ ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=",
"+ add_le_add (add_le_add hH hVr2) hVl2",
"+ _ = ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +",
"+ IIMaj (n : \u211d) / 2 := by ring",
"+",
"+/-- **The lower right-tail bound by conjugation** (D-074 \u00a73.4): the",
"+same bound holds at im = \u2212T (the integrand is conjugation-symmetric,",
"+Jlag_conj; the interval integral maps conj through). -/",
"+theorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : \u2115} {T : \u211d}",
"+ (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :",
"+ \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264",
"+ ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +",
"+ IIMaj (n : \u211d) / 2 := by",
"+ have hT0 : (0 : \u211d) < T := by",
"+ have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn",
"+ have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by",
"+ have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=",
"+ Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))",
"+ have h2 : Real.sqrt 16 = 4 := by",
"+ rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num",
"+ rwa [h2] at h1",
"+ linarith",
"+ have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T) =",
"+ (starRingEnd \u2102) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T) := by",
"+ unfold HIntegral",
"+ rw [\u2190 integral_conj]",
"+ apply intervalIntegral.integral_congr",
"+ intro \u03c3 h\u03c3",
"+ have hid2 : ((\u03c3 : \u211d) + (-T) * Complex.I) =",
"+ (starRingEnd \u2102) ((\u03c3 : \u211d) + T * Complex.I) := by",
"+ simp [Complex.ext_iff]",
"+ rw [hid2]",
"+ exact Jlag_conj n (by",
"+ intro h",
"+ have him : (((\u03c3 : \u211d) + T * Complex.I)).im = T := by simp",
"+ rw [h] at him",
"+ simp at him",
"+ linarith [hT0])",
"+ rw [hconj, Complex.norm_conj]",
"+ exact hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1",
"+",
"+/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for",
"+ii\u2032-6-c): both horizontal right tails bounded by the dog-leg charge. -/",
"+theorem dogLegUpper_two_sides {n : \u2115} {T : \u211d}",
"+ (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :",
"+ \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 +",
"+ \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264",
"+ 2 * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +",
"+ IIMaj (n : \u211d) / 2) := by",
"+ rw [show (2 : \u211d) * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +",
"+ (8.38 : \u211d) + IIMaj (n : \u211d) / 2) =",
"+ (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +",
"+ IIMaj (n : \u211d) / 2) +",
"+ (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +",
"+ IIMaj (n : \u211d) / 2) by ring]",
"+ exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)",
"+ (hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)",
"+",
" end NguyenRH1",
" ",
" end"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"`integral_conj {f : X → 𝕜} : ∫ x, conj (f x) ∂μ = conj (∫ x, f x ∂μ)` — exists (Bochner/ContinuousLinearMap.lean:173, RCLike 𝕜). For interval integrals: the interval integral IS a Bochner integral over the interval measure — `∫ x in a..b, f x` unfolds to the measure integral, so `integral_conj` applies (it's about the Bochner integral — the interval notation is defeq). The `conj` here is `starRingEnd 𝕜` presumably (RCLike's conj = starRingEnd 𝕜 for 𝕜 = ℂ ✓).\n\nNow write DL-5. Structure:\n\n```lean\n/-! ## 7. The total right-horizontal bound (DL-5, D-074 §3.4) -/\n\n/-- The dog-leg height parameter U = (3/2)·T. -/\n\ntheorem hIntegral_Jlag_low_le_dogLegUpper {n : ℕ} {T : ℝ}\n (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ ≤\n ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n IIMaj (n : ℝ) / 2 := by\n have hT0 : (0 : ℝ) < T := by\n have h1 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have h2 : Real.sqrt 16 ≤ Real.sqrt (n : ℝ) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : ℝ) ≤ (n : ℝ))\n have h3 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h3] at h2\n linarith\n have hTn2 : (n : ℝ) ≤ T ^ 2 := by\n have h1 := hTn\n have h2 : (Real.sqrt (n : ℝ)) ^ 2 ≤ T ^ 2 := by\n apply pow_le_pow_left₀ (Real.sqrt_nonneg _) h1\n rwa [Real.sq_sqrt (by linarith [Real.sqrt_nonneg (n : ℝ)])] at h2\n have hU0 : (0 : ℝ) < (3 / 2) * T := by linarith [hT0]\n have hTU : T ≤ (3 / 2) * T := by linarith [hT0]\n have hnU : (n : ℝ) ≤ (4 / 9) * ((3 / 2) * T) ^ 2 := by\n have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by field_simp; ring\n rw [h1]\n exact hTn2\n have hXR : (3 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by\n have h1 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := ... (same sqrt-16 trick)\n linarith\n have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)\n -- the three pieces\n have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)\n have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)\n have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)\n -- lengths: U − T = T/2 ≤ (√n+1)/2\n have hlen : (3 / 2) * T - T ≤ (Real.sqrt (n : ℝ) + 1) / 2 := by\n linarith [hTn1, hTn]\n -- assemble\n rw [hid]\n calc ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T) +\n VIntegral (Jlag n) 3 T ((3 / 2) * T)‖\n ≤ ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T)‖ +\n ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ +\n ‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖ := by\n exact norm_sub_le.trans (norm_add_le _ _)\n -- hmm: ‖A − B + C‖ ≤ ‖A‖ + ‖B‖ + ‖C‖: norm_sub_le: ‖A−B‖ ≤ ‖A‖+‖B‖; norm_add_le: ‖(A−B)+C‖ ≤ ‖A−B‖+‖C‖ — compose\n _ ≤ (8.38 : ℝ) + ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +\n IIMaj (n : ℝ) / 2 := by\n apply add_le_add (add_le_add hH ?vr ?vl) (le_refl _)\n ...\n```\nHmm — let me structure the assembly more carefully:\n\n‖H_low‖ = ‖H_high − V_right + V_left‖ ≤ ‖H_high‖ + ‖V_right‖ + ‖V_left‖ via:\nnorm_sub_le : ‖a − b‖ ≤ ‖a‖ + ‖b‖; norm_add_le : ‖a + b‖ ≤ ‖a‖ + ‖b‖.\n‖(H − Vr) + Vl‖ ≤ ‖H − Vr‖ + ‖Vl‖ ≤ (‖H‖ + ‖Vr‖) + ‖Vl‖ ✓.\n\nThen:\n- ‖H‖ ≤ 8.38 (hH)\n- ‖Vr‖ ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 — then ≤ IIMaj/2: \n (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}·1 (hlen, dirichletC2 ≤ 1)\n and ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)} ≤ IIMaj/2:\n IIMaj/2 = (1/2)·2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} = (√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}.\n ⟺ ((√n+1)/2)·1 ≤ (√n+1)·0.57 ⟺ 1/2 ≤ 0.57 ✓ trivial.\n- ‖Vl‖ ≤ (U−T)·(e^{5/2}+1)/2 ≤ ((√n+1)/2)·(e^{5/2}+1)/2 (hlen) ✓ (that's the VLeftBound form ✓).\n\nThe IIMaj/2 proof (Vr ≤ IIMaj/2): \n```\n have hVr2 : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ ≤ IIMaj (n : ℝ) / 2 := by\n refine hVr.trans ?_\n -- (U−T)·(e^{√n/2}+1)·(2^{−(2√n−2)}·dirichletC2) ≤ IIMaj/2\n have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one\n have hC2pos : (0 : ℝ) ≤ dirichletC2 := dirichletC2_nonneg\n have hexp_pos : (0 : ℝ) < Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by positivity\n have hpow_pos : (0 : ℝ) < (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by positivity\n have hlen0 : (0 : ℝ) ≤ (3 / 2) * T - T := by linarith [hT0]\n calc ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2)\n ≤ ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * 1) := by\n apply mul_le_mul (mul_le_mul hlen (le_refl _) (add_nonneg (Real.exp_nonneg _) (by norm_num)) hlen0) ?_ (by positivity) (by positivity)\n · exact mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _)\n _ = IIMaj (n : ℝ) / 2 := by\n unfold IIMaj\n field_simp\n ring\n```\nHmm — the IIMaj/2 equality: IIMaj/2 = (1/2)·2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} = (√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} — and my LHS: ((√n+1)/2)(e+1)·2^{−X}·1. Are they EQUAL? LHS = ((√n+1)/2)(e+1)2^{−X}; RHS = (√n+1)(e+1)·0.57·2^{−X} — NOT equal (0.57 ≠ 0.5). So the calc's last step should be ≤ (not =): ((√n+1)/2)(e+1)2^{−X}·1 ≤ (√n+1)(e+1)·0.57·2^{−X} ⟺ 1/2 ≤ 0.57 ⟺ 0.5 ≤ 0.57 ✓ — via mul_le_mul of (1/2 ≤ 0.57) with the common positive factor:\n```\n _ ≤ IIMaj (n : ℝ) / 2 := by\n unfold IIMaj\n have h57 : (Real.sqrt (n : ℝ) + 1) / 2 * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * 1) ≤\n (Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * 0.57) := by\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n · apply mul_le_mul_of_nonneg_right _ (by positivity)\n norm_num\n convert h57 using 1 <;> ring\n```\nHmm — the convert: IIMaj/2's unfolded form: 2·(√n+1)·(e+1)·0.57·2^{−X}/2 vs the h57 form (√n+1)·(e+1)·(2^{−X}·0.57) — equal by ring ✓.\n\nThis is getting intricate — let me simplify the whole Vr accounting: bound ‖Vr‖ ≤ IIMaj/2 via a direct chain:\n```\n have hVr2 : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ ≤ IIMaj (n : ℝ) / 2 := by\n have h1 := hVr\n have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one\n -- key numeric: (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·C2 ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}\n -- and ((√n+1)/2)·... ≤ IIMaj/2 = (√n+1)·0.57·...·...\n have h57 : ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ)) ≤ IIMaj (n : ℝ) / 2 := by\n unfold IIMaj\n have hpos1 : (0 : ℝ) < (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by positivity\n have hpos2 : (0 : ℝ) ≤ Real.sqrt (n : ℝ) + 1 := by linarith [Real.sqrt_nonneg (n : ℝ)]\n have hpos3 : (0 : ℝ) ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by positivity\n calc ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ))\n ≤ (Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (0.57 : ℝ)) := by\n apply mul_le_mul_of_nonneg_left _ hpos3\n · apply mul_le_mul_of_nonneg_right _ hpos1.le\n · calc ((Real.sqrt (n : ℝ) + 1) / 2) * (1 : ℝ) ≤ (Real.sqrt (n : ℝ) + 1) * (0.57 : ℝ) := by\n apply mul_le_mul_of_nonneg_left _ hpos2\n norm_num\n _ = ((Real.sqrt (n : ℝ) + 1) / 2) * 1 * 1 ≤ ... -- ugh\n```\nGetting bogged down in product associativity. SIMPLIFY: prove the key inequality in the cleanest form:\nA := ((√n+1)/2)·(e+1)·(2^{−X}·1), B := IIMaj/2. B = (√n+1)·(e+1)·(0.57·2^{−X})... — hmm actually IIMaj = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}: IIMaj/2 = (√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}.\nA = ((√n+1)/2)(e+1)·2^{−X}·1 = 0.5·(√n+1)(e+1)·2^{−X}.\nB = 0.57·(√n+1)(e+1)·2^{−X}.\nA ≤ B ⟺ 0.5 ≤ 0.57 ✓.\n\nProve via: A = c·K and B = d·K with K = (√n+1)(e+1)·2^{−X} > 0 and c = 0.5 ≤ 0.57 = d:\n```\n have hK : (0 : ℝ) < (Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by positivity\n have eA : ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ)) =\n (1 / 2) * ((Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by ring\n have eB : IIMaj (n : ℝ) / 2 =\n (0.57 : ℝ) * ((Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by\n unfold IIMaj\n ring\n rw [eA, eB]\n apply mul_le_mul_of_nonneg_right _ hK.le\n norm_num\n```\nThe eB: IIMaj/2 = (1/2)·[2(√n+1)(e+1)·0.57·2^{−X}] = (√n+1)(e+1)·0.57·2^{−X} = 0.57·[(√n+1)(e+1)·2^{−X}] ✓ ring proves it? — unfold IIMaj gives the full form 2·(√n+1)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)} / 2 — ring handles the constants ✓ (the 2·.../2 cancellation — ring over a field handles /2 ✓).\n\nSimilarly eA by ring ✓.\n\nThen the full Vr chain:\n```\n calc ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖\n ≤ ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := hVr\n _ ≤ ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ)) := by\n have hlen0 : (0 : ℝ) ≤ (3 / 2) * T - T := by linarith [hT0]\n have hpos3 : (0 : ℝ) ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by positivity\n have hpos4 : (0 : ℝ) ≤ (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 := by positivity\n have h1 : ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) ≤\n ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) :=\n mul_le_mul hlen (le_refl _) (add_nonneg (Real.exp_nonneg _) (by norm_num)) hlen0\n exact mul_le_mul h1 (mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _))\n hpos4 (mul_nonneg hpos3 (Real.rpow_nonneg (by norm_num) _))\n _ ≤ IIMaj (n : ℝ) / 2 := by\n rw [eA, eB]\n apply mul_le_mul_of_nonneg_right _ hK.le\n norm_num\n```\nWait — the second step's mul_le_mul: h1 : (U−T)(e+1) ≤ ((√n+1)/2)(e+1) and hC2-rpow : 2^{−X}·C2 ≤ 2^{−X}·1 — mul_le_mul (h1) (h2) (0 ≤ (2^{−X}·C2)) (0 ≤ ((√n+1)/2)(e+1)) : (U−T)(e+1)·(2^{−X}·C2) ≤ ((√n+1)/2)(e+1)·(2^{−X}·1) ✓ — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b) : a·c ≤ b·d ✓ — with a := (U−T)(e+1), b := ((√n+1)/2)(e+1), c := (2^{−X}·C2), d := (2^{−X}·1): hc : 0 ≤ 2^{−X}·C2 ✓ positivity (C2 ≥ 0 via dirichletC2_nonneg — positivity might not know; provide explicitly); hb : 0 ≤ ((√n+1)/2)(e+1) ✓ positivity.\n\nThen mul_le_mul hlen (le_refl (e+1)) (0 ≤ e+1) (0 ≤ U−T) : (U−T)(e+1) ≤ ((√n+1)/2)(e+1) ✓ — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b) ✓ with a := U−T, b := (√n+1)/2, c := d := e+1: hc : 0 ≤ e+1 ✓ (add_nonneg (exp_nonneg _) 0≤1... — the `add_nonneg (Real.exp_nonneg _) (by norm_num : (0:ℝ) ≤ 1)`); hb : 0 ≤ U−T ✓ hlen0.\n\nThe 2^{−X}·C2 ≤ 2^{−X}·1 : mul_le_mul_of_nonneg_left hC2 (0 ≤ 2^{−X}) : C2·2^{−X} ≤ 1·2^{−X} ✓ — but the form is (2^{−X}·C2) ≤ (2^{−X}·1) — mul_le_mul_of_nonneg_left : a ≤ b → 0 ≤ c → c·a ≤ c·b — with c := 2^{−X}, a := C2, b := 1: 2^{−X}·C2 ≤ 2^{−X}·1 ✓ (Real.rpow_nonneg (by norm_num) _ : 0 ≤ 2^{−X} ✓).\n\nOK — and hK/eA/eB as designed. This is doable but long. Let me also double check the Vl assembly:\n```\n calc ‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖\n ≤ ((3 / 2) * T - T) * (Real.exp (5 / 2) + 1) / 2 := hVl\n _ ≤ ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=\n mul_le_mul hlen (le_refl _) (by positivity) hlen0\n```\nmul_le_mul (hlen : U−T ≤ (√n+1)/2) (le_refl : X ≤ X) (0 ≤ X) (0 ≤ U−T) : (U−T)·X ≤ ((√n+1)/2)·X with X := (e^{5/2}+1)/2 ✓ — wait mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b): a·c ≤ b·d ✓ with a := U−T, b := (√n+1)/2, c = d := (e^{5/2}+1)/2 ✓.\n\nFinal assembly:\n```\n rw [hid]\n calc ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T) +\n VIntegral (Jlag n) 3 T ((3 / 2) * T)‖\n ≤ ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T)‖ +\n ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ +\n ‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖ := by\n exact (norm_sub_le _ _).trans (norm_add_le _ _) -- hmm\n _ ≤ (8.38 : ℝ) + IIMaj (n : ℝ) / 2 + ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by\n exact add_le_add (add_le_add hH hVr2) hVl2\n _ = ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) + IIMaj (n : ℝ) / 2 := by ring\n```\nnorm composition: ‖(H − Vr) + Vl‖ ≤ ‖H − Vr‖ + ‖Vl‖ (norm_add_le) ≤ ‖H‖ + ‖Vr‖ + ‖Vl‖ (norm_sub_le on the first): \n```\n have hna : ‖(H − Vr) + Vl‖ ≤ ‖H − Vr‖ + ‖Vl‖ := norm_add_le _ _\n have hns : ‖H − Vr‖ ≤ ‖H‖ + ‖Vr‖ := norm_sub_le _ _\n linarith [hna, hns]\n```\nHmm — norm_add_le : ‖a + b‖ ≤ ‖a‖ + ‖b‖ — for normed groups: `norm_add_le (a b : α) : ‖a + b‖ ≤ ‖a‖ + ‖b‖` ✓; norm_sub_le (a b) : ‖a − b‖ ≤ ‖a‖ + ‖b‖ ✓.\n\nThe theorem's statement RHS: ((√n+1)/2)·(e^{5/2}+1)/2 + 8.38 + IIMaj/2 ✓.\n\nNow DL-5b (the lower side):\n```lean\n/-- The lower right-tail bound by conjugation (D-074 §3.4): for n ≥ 16,\nT ∈ [√n, √n+1], ‖HIntegral (Jlag n) 3 (2√n) (−T)‖ ≤ DogLegUpper n\n(the conjugate of the upper bound; Jlag_conj + the integral conj\nsymmetry). -/\ntheorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : ℕ} {T : ℝ}\n (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T))‖ ≤ ... same RHS := by\n have hT0 : (0 : ℝ) < T := ...\n have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T) =\n (starRingEnd ℂ) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T) := by\n unfold HIntegral\n rw [← integral_conj]\n -- pointwise: conj (Jlag n (σ + T·I)) = Jlag n (σ − T·I) = Jlag n (σ + (−T)·I)\n apply intervalIntegral.integral_congr\n intro σ hσ\n rw [show ((σ : ℝ) + (-T) * Complex.I) = (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) from by\n simp [Complex.ext_iff]]\n exact (Jlag_conj n (by\n have him : 0 < (((σ : ℝ) + T * Complex.I)).im := by simp [hT0]\n intro h\n rw [h] at him\n simp at him)).symm\n rw [hconj, ← Complex.norm_eq_abs, ← Complex.norm_eq_abs]\n exact hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1\n```\nHmm — details: \n- `integral_conj : ∫ x, conj (f x) ∂μ = conj (∫ x, f x ∂μ)` — with conj := starRingEnd ℂ ✓. `rw [← integral_conj]` turns the goal's LHS integral `∫ Jlag(σ + (−T)·I)` into... hmm — the goal is `∫ Jlag(σ + (−T)·I) = conj(∫ Jlag(σ+T·I))` — rw [← integral_conj] rewrites conj(∫ f) → ∫ conj(f): the RHS conj(∫ Jlag(σ+T·I)) → ∫ conj(Jlag(σ+T·I)) ✓ then integral_congr with the pointwise identity Jlag(σ+(−T)·I) = conj(Jlag(σ+T·I)) ✓ — from Jlag_conj (n) (hs : (σ+T·I) ≠ 1): Jlag n (conj(σ+T·I)) = conj(Jlag n (σ+T·I)) and conj(σ+T·I) = σ + (−T)·I ✓ — the .symm direction: Jlag(σ+(−T)·I) = conj(Jlag(σ+T·I)) needs: Jlag n (σ+(−T)·I) = Jlag n (conj(σ+T·I)) [by the point identification] = conj(Jlag n (σ+T·I)) [Jlag_conj] ✓ — so the congr's goal: Jlag n (σ + (−T)·I) = conj (Jlag n (σ + T·I)): \n ```\n intro σ hσ\n have hid2 : ((σ : ℝ) + (-T) * Complex.I) = (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by\n simp [Complex.ext_iff]\n rw [hid2, 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 ```\n Jlag_conj (n) {s} (hs : s ≠ 1) : Jlag n (conj s) = conj (Jlag n s) — with s := σ+T·I: Jlag n (conj(σ+T·I)) = conj(Jlag n (σ+T·I)) ✓ — after rw [hid2] the goal: Jlag n (conj(σ+T·I)) = conj(Jlag n (σ+T·I)) ✓ = Jlag_conj ✓ exactly.\n- The intervalIntegral.integral_congr : (∀ x ∈ Ι a b, f x = g x) → ∫ f = ∫ g ✓ (used before — intervalIntegral.integral_congr exists ✓).\n- The HIntegral unfold: HIntegral f x₁ x₂ y = ∫ x in x₁..x₂, f (x + y·I) — with f := Jlag n, y := −T: ∫_3^XR Jlag(σ + (−T)·I) ✓.\n- The norm step: ‖conj X‖ = ‖X‖: `Complex.norm_conj`?? — or `norm_conj`/`starRingEnd.norm_apply`: (starRingEnd ℂ).norm_apply? — used in LiMoments: \"Complex.norm_conj takes starRingEnd DIRECTLY\" (session-037 banked) — `Complex.norm_conj (z : ℂ) : ‖(starRingEnd ℂ) z‖ = ‖z‖` ✓ — rw [hconj, Complex.norm_conj] then the RHS's ‖H(T)‖ vs the goal's ‖H(T)‖ — wait the goal after rw [hconj]: ‖conj (H T)‖ ≤ RHS — rw [Complex.norm_conj] : ‖H T‖ ≤ RHS ✓ then exact hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1 ✓.\n\nAnd the two-side capstone:\n```lean\n/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for\nii′-6-c): both horizontal right tails, each ≤ DogLegUpper n. -/\ntheorem dogLegUpper_two_sides {n : ℕ} {T : ℝ}\n (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ +\n ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T))‖ ≤\n 2 * (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n IIMaj (n : ℝ) / 2) := by\n rw [show 2 * _ = _ + _ by ring]\n exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)\n (hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)\n```\nHmm — actually for ii′-6-c the two single-side lemmas are the deliverables; the two-side version is a convenience. Include it.\n\nOne more consideration — hIntegral_Jlag_low_le_dogLegUpper's norm composition: after rw [hid], the goal is ‖H_high − Vr + Vl‖ ≤ RHS — the norm chain needs care with the associativity of (H − Vr) + Vl vs H − (Vr + ...): hid's RHS is `H(3→XR, U) − V(XR, T→U) + V(3, T→U)` — parsed as `(H − Vr) + Vl` ✓.\n\nAlso the norm_add_le/norm_sub_le names: `norm_add_le (a b : α) : ‖a + b‖ ≤ ‖a‖ + ‖b‖` ✓ and `norm_sub_le (a b : α) : ‖a − b‖ ≤ ‖a‖ + ‖b‖` ✓ (used in LiContour ✓).\n\nLet me write DL-5's block now.","signature":""},{"type":"text","text":"`integral_conj` exists. Writing the DL-5 block (upper total + lower by conjugation + two-side capstone)."},{"type":"tool_use","id":"Edit_377","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 7. The total right-horizontal bound (DL-5, D-074 §3.4) -/\n\n/-- **The upper right-tail bound** (D-074 §3.4): for n ≥ 16 and\nT ∈ [√n, √n+1] (the T_cut window), U = (3/2)·T,\n‖HIntegral (Jlag n) 3 (2√n) T‖ ≤ ((√n+1)/2)·(e^{5/2}+1)/2 + 8.38 +\nIIMaj(n)/2 — the exact deformation identity +\nV_left/H_high/V_right piece bounds, all in the zero-free region. -/\ntheorem hIntegral_Jlag_low_le_dogLegUpper {n : ℕ} {T : ℝ}\n (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ ≤\n ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n IIMaj (n : ℝ) / 2 := by\n have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hsqrt4 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n have h1 : Real.sqrt 16 ≤ Real.sqrt (n : ℝ) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : ℝ) ≤ (n : ℝ))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n have hT0 : (0 : ℝ) < T := by linarith\n have hTn2 : (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 linarith [Real.sqrt_nonneg (n : ℝ)])] at h1\n have hU0 : (0 : ℝ) < (3 / 2) * T := by linarith [hT0]\n have hTU : T ≤ (3 / 2) * T := by linarith [hT0]\n have hnU : (n : ℝ) ≤ (4 / 9) * ((3 / 2) * T) ^ 2 := by\n have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by\n field_simp\n ring\n rw [h1]\n exact hTn2\n have hXR : (3 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by linarith\n have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)\n have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)\n have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)\n have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)\n have hlen : (3 / 2) * T - T ≤ (Real.sqrt (n : ℝ) + 1) / 2 := by linarith [hTn1, hTn]\n have hlen0 : (0 : ℝ) ≤ (3 / 2) * T - T := by linarith [hT0]\n -- V_left ≤ ((√n+1)/2)·(e^{5/2}+1)/2\n have hVl2 : ‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖ ≤\n ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by\n refine hVl.trans ?_\n apply mul_le_mul hlen (le_refl _) (by positivity) hlen0\n -- V_right ≤ IIMaj/2\n have hVr2 : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ ≤\n IIMaj (n : ℝ) / 2 := by\n have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one\n have hK : (0 : ℝ) < (Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by\n apply mul_pos (by positivity)\n apply mul_pos (by positivity)\n positivity\n have eA : ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ)) =\n (1 / 2) * ((Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by ring\n have eB : IIMaj (n : ℝ) / 2 =\n (0.57 : ℝ) * ((Real.sqrt (n : ℝ) + 1) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by\n unfold IIMaj\n ring\n calc ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖\n ≤ ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := hVr\n _ ≤ ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ)) := by\n have h1 : ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) ≤\n ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) :=\n mul_le_mul hlen (le_refl _) (by positivity) hlen0\n have h2 : (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 ≤\n (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * (1 : ℝ) :=\n mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _)\n exact mul_le_mul h1 h2 (by positivity) (by positivity)\n _ ≤ IIMaj (n : ℝ) / 2 := by\n rw [eA, eB]\n apply mul_le_mul_of_nonneg_right _ hK.le\n norm_num\n -- assemble via the exact identity\n rw [hid]\n calc ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T) +\n VIntegral (Jlag n) 3 T ((3 / 2) * T)‖\n ≤ ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T)‖ +\n ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ +\n ‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖ := by\n have h1 := norm_add_le\n (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T))\n (VIntegral (Jlag n) 3 T ((3 / 2) * T))\n have h2 := norm_sub_le\n (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T))\n (VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T))\n linarith [h1, h2]\n _ ≤ (8.38 : ℝ) + IIMaj (n : ℝ) / 2 +\n ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=\n add_le_add (add_le_add hH hVr2) hVl2\n _ = ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n IIMaj (n : ℝ) / 2 := by ring\n\n/-- **The lower right-tail bound by conjugation** (D-074 §3.4): the\nsame bound holds at im = −T (the integrand is conjugation-symmetric,\nJlag_conj; the interval integral maps conj through). -/\ntheorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : ℕ} {T : ℝ}\n (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T)‖ ≤\n ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n IIMaj (n : ℝ) / 2 := by\n have hT0 : (0 : ℝ) < T := by\n have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hsqrt4 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n have h1 : Real.sqrt 16 ≤ Real.sqrt (n : ℝ) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : ℝ) ≤ (n : ℝ))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n linarith\n have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T) =\n (starRingEnd ℂ) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T) := by\n unfold HIntegral\n rw [← integral_conj]\n apply intervalIntegral.integral_congr\n intro σ hσ\n have hid2 : ((σ : ℝ) + (-T) * Complex.I) =\n (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by\n simp [Complex.ext_iff]\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_low_le_dogLegUpper hn hTn hTn1\n\n/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for\nii′-6-c): both horizontal right tails bounded by the dog-leg charge. -/\ntheorem dogLegUpper_two_sides {n : ℕ} {T : ℝ}\n (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ +\n ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T)‖ ≤\n 2 * (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n IIMaj (n : ℝ) / 2) := by\n rw [show (2 : ℝ) * (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +\n (8.38 : ℝ) + IIMaj (n : ℝ) / 2) =\n (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n IIMaj (n : ℝ) / 2) +\n (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n IIMaj (n : ℝ) / 2) by ring]\n exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)\n (hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)\n\nend NguyenRH1\n\nend"},"extra_content":null}]