← Session 36 — ii′-6-DL dog-leg + side bounds; Paper A review
thinking (29386 chars)
`riemannZeta_ne_zero_of_one_le_re ⦃s : ℂ⦄ (hs : 1 ≤ s.re) : riemannZeta s ≠ 0` — takes only re ✓ (s implicit-instance-ish ⦃s⦄ — strict implicit, determined by hs).
Usage pattern: `riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)` — with s determined by the hs's type ✓.
Now write §3 (6-c-iii) into LiSideBounds.lean. Structure:
```lean
/-! ## 3. 6-c-iii: I_I — the right vertical σ₁ = 2√n (F-E form) -/
/-- **The F-E kernel lemma** (D-074 §9): the uniform-in-t kernel bound at
the right vertical σ = 2√n — ‖kFun n (2√n+it)‖ ≤ e^{√n/2+1/3}+1 for n ≥ 4.
(The honest charge: |w/(w−1)| ≤ 1 + 1/(2√n−1) via the plain triangle
inequality + ‖w−1‖ ≥ re(w−1) = 2√n−1; then (1+1/(2√n−1))ⁿ ≤
exp(n/(2√n−1)) ≤ exp(√n/2+1/3) ⟺ n ≥ 4. Fixes the off-by-one in the
t² ≥ n / re ≥ 2√n+1 variants at t = 0.) -/
theorem kFun_right_vertical_norm_le_exp_sqrt_add_third {n : ℕ} (hn : 4 ≤ n)
(t : ℝ) : ...
```
Wait — (t : ℝ) explicit or implicit? The consumers apply at specific t — explicit fine.
Then the I_I theorem. Let me write the full code.
For the final lemma name: `vIntegral_Jlag_right_le_exp_third_IIMaj`.
Details to nail:
- hn4 : 4 ≤ n := by omega (from hn : 100000 ≤ n) ✓ omega.
- hn5 : 5 ≤ n := by omega.
- The point form everywhere: `(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)` — matching DL-4/DL-6.
Wait — VIntegral_norm gives the integral point as `((x : ℝ) + (t : ℝ) * Complex.I)` where x := 2 * Real.sqrt (n:ℝ) — elaborated `↑(2 * √(↑n)) + ↑t * I` — and DL-6's point: `(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)` — `↑(2*√(↑n)) + ↑t * I` ✓ identical.
Hmm — but there's ONE subtlety: in VIntegral_norm's statement, the point is written `((x : ℝ) + (t : ℝ) * Complex.I)` — since x is ALREADY ℝ, the `(x : ℝ)` is a no-op annotation — elaborated term: `↑x + ↑t * I`? The coercion on x: since f : ℂ → ℂ and + needs ℂ, Lean inserts ↑ on the first argument ✓ `↑x + ↑t * I` ✓. And the t: `(t : ℝ) * Complex.I` — ↑t * I ✓. Same as DL's `↑(2*√n) + ↑t * I` ✓.
But WAIT — in the DL-4 statement the point is `(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)` — hmm, the `t * Complex.I` here — t : ℝ — `↑t * I` ✓ same.
OK. And my §3 statements should use the DL point form `(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)` for consistency with norm_logDeriv_zeta_le_iimZeta and the kernel lemma.
One more check — the kernel lemma's statement point: same DL form. norm_logDeriv_zeta_le_iimZeta's point: same. The VIntegral path: VIntegral (Jlag n) (2 * Real.sqrt (n:ℝ)) (-T) T — x := 2*√(↑n) — after VIntegral_norm: ∫ t in -T..T, Jlag n (↑(2*√(↑n)) + ↑t*I) ✓.
Hmm — will `↑(2*√(↑n))` from VIntegral_norm (with x := 2*√(↑n)) syntactically match the DL point's first term `↑(2*√(↑n))`? VIntegral_norm's x is `2 * Real.sqrt (n:ℝ)` — written identically ✓ same term ✓.
Now — hsq2 : 2 ≤ √(↑n): needed in hzne (1 ≤ 2√n), hne/hsq1 in the kernel lemma, and hexp. Let me structure the kernel lemma with its own hsq2 (from hn : 4 ≤ n).
Kernel lemma:
```lean
theorem kFun_right_vertical_norm_le_exp_sqrt_add_third {n : ℕ} (hn : 4 ≤ n)
(t : ℝ) :
‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by
have hnR : (4 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have hsq : (0 : ℝ) < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr (by linarith)
have hsq2 : (2 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
have h21 : (0 : ℝ) < 2 * Real.sqrt (n : ℝ) - 1 := by nlinarith [hsq2]
have hsqn : Real.sqrt (n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt (by linarith)
-- w − 1 ≠ 0 and ‖w − 1‖ ≥ 2√n − 1
have hre : ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1).re =
2 * Real.sqrt (n : ℝ) - 1 := by
simp [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.mul_re,
Complex.I_re, Complex.I_im, Complex.one_re]
have hne : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1 ≠ 0 := by
intro h
have h0 : ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1).re = 0 := by
rw [h]; simp
rw [hre] at h0
nlinarith [h21]
have hnorm_w1 : 2 * Real.sqrt (n : ℝ) - 1 ≤
‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ := by
have h1 := abs_re_le_norm ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)
rw [hre, abs_of_nonneg h21.le] at h1
exact h1
-- the base bound ‖1 + 1/(w−1)‖ ≤ 1 + 1/(2√n−1)
have hinv : 1 / ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ ≤
1 / (2 * Real.sqrt (n : ℝ) - 1) :=
one_div_le_one_div_of_le h21 hnorm_w1
have hbase : ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ≤
1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by
calc ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖
≤ ‖(1 : ℂ)‖ + ‖1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ :=
norm_add_le _ _
_ = 1 + 1 / ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ := by
rw [norm_one, norm_div, norm_one]
_ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by linarith [hinv]
have hbasepos : (0 : ℝ) ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by positivity
-- the power + exp chain
have hexp : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1)) ≤
Real.sqrt (n : ℝ) / 2 + 1 / 3 := by
rw [mul_one_div, div_le_iff₀ h21]
nlinarith [hsqn, hsq2]
have hpow : (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n ≤
Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) := by
calc (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n
≤ (Real.exp (1 / (2 * Real.sqrt (n : ℝ) - 1))) ^ n :=
pow_le_pow_left₀ hbasepos (Real.add_one_le_exp _) n
_ = Real.exp ((n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1))) :=
(Real.exp_nat_mul _ n).symm
_ ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) := Real.exp_le_exp.mpr hexp
have hpow1 : ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ^ n ≤
(1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n :=
pow_le_pow_left₀ (norm_nonneg _) hbase n
have hwid : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) /
((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) =
1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) := by
field_simp [hne]
ring
unfold kFun
rw [hwid]
calc ‖(1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)) ^ n - 1‖
≤ ‖(1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)) ^ n‖ +
‖(1 : ℂ)‖ := norm_sub_le _ _
_ = ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ^ n + 1 := by
rw [norm_pow, norm_one]
_ ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by
linarith [hpow1.trans hpow]
```
Checks:
- hexp's nlinarith: goal after rw [mul_one_div, div_le_iff₀ h21]: `(n:ℝ) ≤ (√n/2 + 1/3) * (2*√n − 1)`. nlinarith [hsqn, hsq2]: expand RHS: (√n/2)(2√n) − √n/2 + (2/3)√n − 1/3 = √n² − √n/2 + 2√n/3 − 1/3 = n + √n/6 − 1/3. Need n ≤ n + √n/6 − 1/3 ⟺ 1/3 ≤ √n/6 ⟺ 2 ≤ √n ✓ hsq2. nlinarith ring_nf's the product ✓ with √n·√n → (√n)^2 = n via hsqn ✓ closes. Hmm — nlinarith multiplies hypotheses pairwise: does it need a hint product? The goal after ring_nf: n ≤ n + (1/6)√n − 1/3-ish — but the ring_nf of the RHS product requires multiplying out (√n/2+1/3)*(2√n−1) — that's part of GOAL normalization (ring_nf handles products in the goal ✓). The (√n)^2 → n step: hsqn : √n^2 = n as a hint rewrite — nlinarith uses hsqn as an equation hint ✓ standard pattern from DL-4 (line 770: nlinarith [sq_nonneg ..., hnR] with hsqn rw'd first — hmm, DL-4 rw'd hsqn INTO the goal first at line 769/774). For safety, mirror DL-4: rw the goal into explicit form first? DL-4's hkey did `rw [show (2√n−1)^2 + t^2 = 4(√n²) − 4√n + 1 + t² by ring, hsqn]` — they rw [hsqn] after rewriting into √n² form. For my hexp: after div_le_iff₀, goal `n ≤ (√n/2+1/3)*(2√n−1)` — I could `rw [show (√n/2+1/3)*(2√n−1) = √n^2 + √n/6 − 1/3 := by ring]`... wait that identity: (√n/2+1/3)(2√n−1) = √n² − √n/2 + 2√n/3 − 1/3 = √n² + √n(−1/2+2/3) − 1/3 = √n² + √n/6 − 1/3 ✓. `by ring` proves it (ring in √n) ✓. Then rw [hsqn]: √n^2 → n — wait hsqn : √n^2 = n — rw [hsqn] rewrites √n^2 → n ✓ goal: n ≤ n + √n/6 − 1/3 — then linarith [hsq2] ✓ DETERMINISTIC.
Let me use that explicit route:
```lean
have hexp : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1)) ≤
Real.sqrt (n : ℝ) / 2 + 1 / 3 := by
rw [mul_one_div, div_le_iff₀ h21,
show (Real.sqrt (n : ℝ) / 2 + 1 / 3) * (2 * Real.sqrt (n : ℝ) - 1) =
Real.sqrt (n : ℝ) ^ 2 + Real.sqrt (n : ℝ) / 6 - 1 / 3 := by ring, hsqn]
linarith [hsq2]
```
rw chains three rewrites ✓ ends with goal `n ≤ n + √n/6 − 1/3` — linarith [hsq2] ✓ (1/3 ≤ √n/6 ⟺ 2 ≤ √n ✓ linear in √n ✓).
Hmm — the `show ... := by ring` — ring proves `(√n/2 + 1/3)*(2√n − 1) = √n^2 + √n/6 − 1/3` — over ℝ with √n as atom ✓ ring ✓.
Wait — does `rw [mul_one_div]` produce `(n:ℝ)/(2√n−1)`? mul_one_div (a b) : a * (1/b) = a/b ✓. Then div_le_iff₀ h21 : a/b ≤ c ↔ a ≤ c*b — rewrites the iff ✓ goal becomes `(n:ℝ) ≤ (√n/2+1/3)*(2√n−1)` ✓ then the show-rw ✓ then hsqn ✓.
Actually — one concern: `rw [div_le_iff₀ h21]` — div_le_iff₀ : a / b ≤ c ↔ a ≤ c * b ✓ (session-033 banked ✓).
- hpow's calc step 1: pow_le_pow_left₀ hbasepos (Real.add_one_le_exp _) n : (1+1/(2√n−1))^n ≤ (exp(1/(2√n−1)))^n. Real.add_one_le_exp (x) : 1 + x ≤ exp x ✓ with x := 1/(2√n−1) — the `_` unified ✓. pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) (n) : a^n ≤ b^n ✓.
- hpow step 2: (exp(x))^n = exp(n*x) — Real.exp_nat_mul (x) (n : ℕ) : Real.exp (↑n * x) = (Real.exp x)^n — .symm : (exp x)^n = exp(↑n * x) — hmm, but is the cast there? DL-4 line 800-801: `(Real.exp ((n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ))))) := (Real.exp_nat_mul _ n).symm` ✓ same usage ✓.
- hpow step 3: Real.exp_le_exp.mpr hexp : exp(n/(2√n−1)-form) ≤ exp(√n/2+1/3) — the calc line's LHS: Real.exp ((n:ℝ) * (1/(2√n−1))) — hexp : (n:ℝ)*(1/(2√n−1)) ≤ √n/2+1/3 ✓ exp_le_exp.mpr : a ≤ b → exp a ≤ exp b ✓ the a here is (n:ℝ)*(1/(2√n−1)) ✓ matches ✓.
Real.exp_le_exp : Real.exp a ≤ Real.exp b ↔ a ≤ b ✓ standard.
- hpow1: pow_le_pow_left₀ (norm_nonneg _) hbase n : ‖1+1/(w−1)‖^n ≤ (1+1/(2√n−1))^n ✓.
- hwid: field_simp [hne] — goal `w/(w−1) = 1 + 1/(w−1)` — field_simp with hne : w−1 ≠ 0 ✓ then ring ✓. Hmm — DL-4 needed `push_cast; ring` after field_simp — because their hs0/hw1 had cast forms. Mine: w is `↑(2*√(↑n)) + ↑t * I` — field_simp produces something like `↑(2*√↑n) + ↑t*I = (↑(2*√↑n) + ↑t*I − 1) + 1`?? — ring closes over ℂ with cast atoms ✓. If ring fails, add push_cast before ring. Let me preemptively write `field_simp [hne]; ring` and adjust if needed.
Hmm — actually wait: field_simp on `w/(w−1) = 1 + 1/(w−1)`: it might rewrite to `w = (w − 1) + 1` directly? Or `w * (w−1) = (w−1)*w`?? Standard behavior: field_simp [hne] with hne : w−1 ≠ 0 — the goal has denominator (w−1) on both sides — field_simp multiplies both sides by (w−1): `w = (1 + 1/(w−1))*(w−1)` then distributes?? Usually leaves `w = (w - 1) + 1` or similar — ring closes either way ✓.
- unfold kFun: goal `‖(w/(w−1))^n − 1‖ ≤ ...` — rw [hwid] rewrites w/(w−1) → 1+1/(w−1) ✓.
Hmm — `unfold kFun` — does the goal after unfold show `(w/(w-1))^n - 1`? kFun n s := (s/(s-1))^n - 1 ✓ (from kFun_norm_le_two's rfl). unfold kFun at goal ‖kFun n w‖ ≤ e+1 → ‖(w/(w−1))^n − 1‖ ≤ e+1 ✓. rw [hwid] : pattern w/(w−1) ✓.
Wait — will unfold produce the exact `w` form? The statement's kFun n (point) — unfold kFun n (point) → ((point)/(point − 1))^n − 1 ✓ hwid's LHS is exactly (point)/(point−1) ✓.
- The final calc — the `_ = ‖1 + 1/(w−1)‖^n + 1` step: rw [norm_pow, norm_one] : ‖(1+1/(w−1))^n‖ → ‖1+1/(w−1)‖^n ✓ and ‖(1:ℂ)‖ → 1 ✓.
- `linarith [hpow1.trans hpow]` : hpow1.trans hpow : ‖1+1/(w−1)‖^n ≤ exp(√n/2+1/3) ✓ goal: ‖1+1/(w−1)‖^n + 1 ≤ exp(√n/2+1/3)+1 ✓ linarith ✓.
- hnorm_w1's abs_of_nonneg h21.le : |2√n−1| = 2√n−1 ✓ — wait, abs_of_nonneg (h : 0 ≤ a) : |a| = a — h21.le : 0 ≤ 2√n−1 ✓. rw [hre, abs_of_nonneg h21.le] at h1: h1 : |(w−1).re| ≤ ‖w−1‖ — rw [hre] : |2√n−1| ≤ ‖w−1‖ — rw [abs_of_nonneg h21.le] : 2√n−1 ≤ ‖w−1‖ ✓ exact h1 ✓.
Hmm — abs_re_le_norm — in LiTightR used unqualified (line 158: `have h := abs_re_le_norm ((2 + t * Complex.I) - ρ.1)`) ✓ Complex.abs_re_le_norm is opened via `open ... Complex` ✓.
- hbase's calc step 2: `‖(1:ℂ)‖ + ‖1/(w−1)‖ = 1 + 1/‖w−1‖`: rw [norm_one] : ‖(1:ℂ)‖ → 1 ✓; ‖1/(w−1)‖: norm_div → ‖1‖/‖w−1‖ → 1/‖w−1‖: rw [norm_div, norm_one] ✓. Order: rw [norm_one, norm_div, norm_one] — first norm_one rewrites ALL ‖(1:ℂ)‖ occurrences (both the standalone and inside norm_div? — norm_div hasn't fired yet — the term is ‖(1:ℂ)‖ + ‖(1:ℂ)/(w−1)‖ — norm_one fires on both ‖(1:ℂ)‖ atoms: → 1 + (‖(1:ℂ)‖/‖w−1‖)... wait ‖1/(w−1)‖ is ‖HDiv.hDiv (1:ℂ) (w−1)‖ — norm_one's pattern ‖(1:ℂ)‖ — the numerator inside is `(1:ℂ)` but not wrapped in ‖·‖ yet — norm_one only matches the OUTER ‖(1:ℂ)‖ and... hmm: term: `‖(1:ℂ)‖ + ‖(1:ℂ)/(w−1)‖`. norm_one pattern: ‖(1:?_)‖ — matches the first ‖(1:ℂ)‖ ✓ → 1. Does it also match inside the second? The second is ‖(1:ℂ)/(w−1)‖ — the pattern ‖(1:ℂ)‖ doesn't match ‖x/y‖ ✓. So after norm_one: `1 + ‖(1:ℂ)/(w−1)‖`. Then norm_div: ‖a/b‖ → ‖a‖/‖b‖: `1 + ‖(1:ℂ)‖/‖w−1‖`. Then norm_one: `1 + 1/‖w−1‖` ✓. So rw [norm_one, norm_div, norm_one] ✓ as written.
- hbasepos by positivity: 0 ≤ 1 + 1/(2√n−1) — needs 0 ≤ 1/(2√n−1) — positivity with h21 (0 < 2√n−1) in context ✓ (positivity uses local hyps for atoms ✓). Hmm — h21 is in scope ✓.
Now the I_I theorem:
```lean
/-- **6-c-iii (I_I, the right vertical σ₁ = 2√n, F-E form)**: the full-side
bound ‖V‖ ≤ e^{1/3}·IIMaj(n). The F-E kernel (uniform in t) + the DL-6
direct Dirichlet bound; e^{√n/2+1/3}+1 ≤ e^{1/3}(e^{√n/2}+1) since
1 ≤ e^{1/3}. -/
theorem vIntegral_Jlag_right_le_exp_third_IIMaj {n : ℕ} (hn : 100000 ≤ n)
{T : ℝ} (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖ ≤
Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := by
have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
have hn4 : 4 ≤ n := by omega
have hn5 : 5 ≤ n := by omega
have hsq2 : (2 : ℝ) ≤ Real.sqrt (n : ℝ) := by
rw [Real.le_sqrt (by norm_num) (by positivity)]
nlinarith [hnR]
have hT0 : (0 : ℝ) ≤ T := by
have h := Real.sqrt_nonneg (n : ℝ)
linarith
have hTT : -T ≤ T := by linarith
-- zero-freeness + continuity on the right vertical
have hzne : ∀ t : ℝ, riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) ≠ 0 := by
intro t
have hre : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I).re =
2 * Real.sqrt (n : ℝ) := by
simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im]
have h1 : (1 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by nlinarith [hsq2]
exact riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)
have hJcont : ∀ t : ℝ, ContinuousAt (Jlag n)
(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by
intro t
have hs1 : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) ≠ 1 := by
intro h
have hre := congrArg Complex.re h
simp at hre
nlinarith [hsq2]
have hA := (kFun_differentiableAt (n := n) hs1).continuousAt
have hB := continuousAt_logDeriv_zeta hs1 (hzne t)
show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _
exact hA.mul hB.neg
have hpath : Continuous fun u : ℝ =>
(((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I) := by fun_prop
have hcontJ : Continuous fun t : ℝ =>
Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by
rw [continuous_iff_continuousAt]
intro t
have hf : ContinuousAt (fun u : ℝ =>
(((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) t := hpath.continuousAt
have hcomp : ContinuousAt
(Jlag n ∘ fun u : ℝ => (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) t :=
ContinuousAt.comp (g := Jlag n)
(f := fun u : ℝ => (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) (x := t)
(hJcont t) hf
exact hcomp
have hcontG : Continuous fun t : ℝ =>
‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=
continuous_norm.comp hcontJ
have hI2 : IntervalIntegrable
(fun t : ℝ => ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖)
MeasureTheory.volume (-T) T := hcontG.intervalIntegrable _ _
-- the e^{√n/2+1/3}+1 ≤ e^{1/3}(e^{√n/2}+1) comparison
have hKle : Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 ≤
Real.exp (1 / 3 : ℝ) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) := by
rw [Real.exp_add]
have h1 : (1 : ℝ) ≤ Real.exp (1 / 3 : ℝ) := by
have h := Real.add_one_le_exp (1 / 3 : ℝ)
linarith
have hE := Real.exp_pos (Real.sqrt (n : ℝ) / 2)
nlinarith [h1, hE]
-- the pointwise bound
have hK' : (0 : ℝ) ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by positivity
have hL : (0 : ℝ) ≤ (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by
positivity
have hpt : ∀ t : ℝ, t ∈ Set.Icc (-T) T →
‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
(Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by
intro t _
rw [Jlag_norm_eq]
exact mul_le_mul (kFun_right_vertical_norm_le_exp_sqrt_add_third hn4 t)
(norm_logDeriv_zeta_le_iimZeta hn5) (norm_nonneg _) hK'
have hInt : ∫ t in (-T)..T,
‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
(T - -T) * ((Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by
have h := intervalIntegral.integral_mono_on hTT hI2 intervalIntegrable_const
(fun t ht => hpt t ht)
rwa [intervalIntegral.integral_const, smul_eq_mul] at h
-- the final comparison 2T·K·L ≤ e^{1/3}·IIMaj
have hKL : (0 : ℝ) ≤ (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) :=
mul_nonneg hK' hL
have hnL : (0 : ℝ) ≤ 2 * (Real.sqrt (n : ℝ) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by
have h1 : (0 : ℝ) ≤ Real.sqrt (n : ℝ) + 1 := by positivity
exact mul_nonneg (mul_nonneg (by norm_num) h1) hL
have hfinal : 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) ≤
Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := by
unfold IIMaj
nlinarith [hTn1, hKle, hKL, hnL, Real.exp_pos (1 / 3 : ℝ),
Real.exp_pos (Real.sqrt (n : ℝ) / 2)]
calc ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖
= ‖∫ t in (-T)..T, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=
VIntegral_norm
_ ≤ ∫ t in (-T)..T, ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=
intervalIntegral.norm_integral_le_integral_norm hTT
_ ≤ (T - -T) * ((Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := hInt
_ = 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *
((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring
_ ≤ Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := hfinal
```
Concerns:
a) `simp at hre` in hs1 (hJcont): hre : (↑(2√n)+↑t·I).re = (1:ℂ).re — simp → `2*√(↑n) = 1` — nlinarith [hsq2]: 2√n ≥ 4 = 1?? contradiction ✓ (linear: 2·(√n atom) = 1 with √n ≥ 2 ✓ linarith actually — nlinarith fine).
Hmm — will simp fully reduce (↑(2*√(↑n)) + ↑t * I).re? add_re → (↑(2√n)).re + (↑t·I).re; ofReal_re → 2√n; mul_re → t·I.re − (0)·I.im — (↑t).re = t, (↑t).im = 0 — t*0 − 0*1 = 0; RHS (1:ℂ).re → 1. simp set: [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im] ✓ plus Complex.one_re for RHS — add Complex.one_re to the simp set in hs1 (congrArg re of h : point = 1 — RHS is Complex.re 1 — simp needs Complex.one_re ✓). In 6-c-ii's hs1 I used plain `simp at hre` and it worked (gave -5/2 = 1) — simp's default set includes the Complex re/im lemmas ✓ plain simp suffices.
Similarly hzne's hre: `simp [Complex.add_re, ...]` — explicit set — should include nothing extra; plain simp worked in zeta_ne_zero_left_vertical for `.re = -5/2` — for `.re = 2*√n`: plain `by simp`? The DL-4 hre used the explicit set. I'll keep the explicit set (harmless).
b) hT0 : 0 ≤ T — from hTn : √n ≤ T and √n ≥ 0: linarith [Real.sqrt_nonneg (n:ℝ)] — I wrote `have h := Real.sqrt_nonneg (n:ℝ); linarith` ✓.
c) The `(T - -T) * X = 2 * T * X` ring step ✓.
d) hfinal's nlinarith — after unfold IIMaj: goal `2*T*K*L' ≤ e13*(2*(√n+1)*(E+1)*0.57*2^(...))` where K = e^{√n/2+1/3}+1, L' = 0.57*2^(...), E = e^{√n/2}. Note: my L' written as `(0.57:ℝ) * (2:ℝ)^(-(2*√n−2))` and IIMaj's tail: `0.57 * 2 ^ (-(2 * Real.sqrt n - 2))` — SAME ✓ (IIMaj's n here is (n:ℝ) since IIMaj : ℝ → ℝ and I apply at (n:ℝ) — the def's `Real.sqrt n` with n := ↑(n:ℕ) — `Real.sqrt (↑n)` ✓ same as my `Real.sqrt (n:ℝ)` ✓).
Wait — IIMaj (n : ℝ) — applying IIMaj (n:ℝ) where (n:ℝ) = ↑(n:ℕ) — the def unfolds with `Real.sqrt ↑n` ✓ matches my `Real.sqrt (n : ℝ)` — same term ✓.
nlinarith hint analysis (as before): hTn1 : T ≤ √n+1; hKle : K ≤ e13(E+1); hKL : 0 ≤ K*L'; hnL : 0 ≤ 2(√n+1)L'. Goal: 2TKL' ≤ e13·2(√n+1)(E+1)L'. Derivation: 2TKL' ≤ 2(√n+1)KL' [2·(KL'·(√n+1−T))] ≤ 2(√n+1)·e13(E+1)·L' [2(√n+1)L'·(e13(E+1)−K)] = RHS ✓. nlinarith pairwise products: (hTn1, hKL) and (hKle, hnL) ✓ then linear ✓. The ring_nf normalization of monomials T*K*L', K*L'*√n, e13*E*L'*√n... — all distinct monomial atoms ✓ linear after expansion ✓ should close.
Risk: nlinarith's preprocessing might not multiply hKle (a ≤-inequality with the exp sides) by hnL — it does consider pairs of ALL hypotheses including provided ones ✓.
If it fails, fallback: explicit two-step mul_le_mul. I'll write nlinarith first, fallback if error.
e) `Real.add_one_le_exp (1/3 : ℝ) : 1 + 1/3 ≤ exp(1/3)` — linarith → 1 ≤ exp(1/3) ✓.
f) hKle's nlinarith [h1, hE]: goal after rw [Real.exp_add]: `exp(√n/2)*exp(1/3) + 1 ≤ exp(1/3)*(exp(√n/2)+1)`. ring_nf RHS: exp(1/3)*exp(√n/2) + exp(1/3). Goal ⟺ E·e13 + 1 ≤ e13·E + e13 ⟺ 1 ≤ e13 ✓ h1. linarith would do (atoms E·e13 and e13·E normalize to same monomial ✓): actually plain `linarith [h1, hE]` — the products E*e13 vs e13*E — ring_nf in linarith normalizes ✓. nlinarith fine too.
g) `rw [Real.exp_add]` at goal — Real.exp_add (a b) : exp(a+b) = exp a * exp b — the goal's LHS exp(√n/2 + 1/3) ✓ matches.
h) The `show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _` — worked in 6-c-ii ✓.
i) hpt's mul_le_mul: mul_le_mul (hk : ‖kFun‖ ≤ K) (hlog : ‖logDeriv‖ ≤ L') (norm_nonneg _ : 0 ≤ ‖logDeriv‖) (hK' : 0 ≤ K) : ‖kFun‖*‖logDeriv‖ ≤ K*L' ✓ — norm_logDeriv_zeta_le_iimZeta hn5 : ‖logDeriv ζ (point)‖ ≤ 0.57 * 2^(-(2√n−2)) — the point: `(((2 * Real.sqrt (n: ℝ)) : ℝ) + t * Complex.I)` ✓ matches ✓.
Wait — norm_logDeriv_zeta_le_iimZeta's implicit {t : ℝ} — applying `(norm_logDeriv_zeta_le_iimZeta hn5)` leaves t implicit — determined by unification with the goal (the h₂ slot: ‖logDeriv ζ (point-t)‖ ≤ ...) ✓.
j) hI2's `hcontG.intervalIntegrable _ _` : IntervalIntegrable F volume (-T) T ✓.
k) In hInt — intervalIntegrable_const's c := K*L' determined by hpt's bound ✓.
l) `VIntegral_norm` — its point form `((x : ℝ) + (t : ℝ) * Complex.I)` — hmm — actually now I realize a potential MISMATCH: VIntegral_norm's RHS (as written in §1) is `‖∫ t in y₁..y₂, f ((x : ℝ) + (t : ℝ) * Complex.I)‖` — x : ℝ so (x : ℝ) is just x with a coercion to ℂ at the +: `↑x + ↑t * I`. My calc step: `‖∫ t in (-T)..T, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖` — point: `↑(2*√↑n) + ↑t * I` ✓ with x := 2*√(↑n) : ℝ — `↑x = ↑(2*√↑n)` ✓ SAME ✓ — VIntegral_norm applies by rfl-calc ✓ (it worked identically in 6-c-ii).
m) hzne's exact: `riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)` — the hs arg : 1 ≤ (point).re — the by-block: rw [hre] → goal 1 ≤ 2√n — exact h1 ✓. The ⦃s⦄ strict implicit: determined by hs's type — the point is explicit in my by-block's goal ✓ — hmm, strict-implicit: the elaborator needs to determine s from the expected type of hs — which comes from the APPLICATION's expected type: `riemannZeta_ne_zero_of_one_le_re hs : riemannZeta ?s ≠ 0` — my goal (inside hzne after intro t): `riemannZeta (point) ≠ 0` — so ?s := point from the goal ✓ then hs : 1 ≤ (point).re ✓ the by-block elaborates ✓. But I'm using `exact riemannZeta_ne_zero_of_one_le_re (...)` against the goal — the goal fixes ?s ✓.
Hmm — wait, in hzne I wrote `have hre ... ; have h1 ... ; exact riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)`. The `by rw [hre]; exact h1` — the expected type: 1 ≤ (point).re — rw [hre] rewrites (point).re → 2√n: goal 1 ≤ 2√n — exact h1 : 1 ≤ 2√n ✓.
n) fun_prop for hpath: `Continuous fun u : ℝ => (↑(2*√↑n) + u * Complex.I)` — same shape as before ✓ (worked in 6-c-ii).
o) Positivity for hK' : 0 ≤ exp(...) + 1 ✓ (exp_pos). hL : 0 ≤ 0.57 * 2^(-(2√n−2)) — the power: (2:ℝ)^(-(2*√n−2)) — ℝ^ℝ — rpow — positivity proves 0 ≤ via Real.rpow_nonneg? positivity has an extension for rpow ✓. If the `^` is zpow... the exponent -(2√n−2) : ℝ so rpow ✓ positivity handles ✓. (In DL-6's proof, `dirichletC2_nonneg` etc. — and IIMaj-related proofs in LiSkeleton surely did similar positivity ✓.)
p) `Real.exp_pos (1/3 : ℝ)` and `Real.exp_pos (√n/2)` ✓.
q) The final calc's `_ = 2 * T * K * L'` ring step: (T - -T) * (K * L') = 2*T*(K*L')... my stated: `2 * T * (Real.exp ...) * ((0.57) * 2^(...))` — note association: (T - -T)*(K*L') vs 2*T*K*L' — ring normalizes ✓ (K*L' parenthesization differs — ring handles ✓).
r) Naming consistency for Z2hat/IIMaj references — IIMaj is in LiSkeleton ✓ (def, root-imported ✓).
s) One more: `Real.le_sqrt (by norm_num) (by positivity)` — the hyps: (hx : 0 ≤ (2:ℝ)) ✓ norm_num; (hy : 0 ≤ (n:ℝ)) ✓ positivity. Goal 2 ≤ √(↑n) — hmm wait — in hsq2 (I_I theorem) I use the same as the kernel lemma ✓.
t) `nlinarith [hnR]` for (2:ℝ)^2 ≤ ↑n — hnR : 100000 ≤ ↑n ✓ 4 ≤ ↑n ✓.
Now — one thing to double check in the kernel lemma: `Real.le_sqrt` signature: (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ √y ↔ x ^ 2 ≤ y ✓ — rw at goal `2 ≤ √(↑n)` → `(2:ℝ)^2 ≤ ↑n` — nlinarith [hnR] ✓.
Also — in the kernel lemma I don't need hsq (0 < √n) — h21 comes from hsq2 via nlinarith ✓. Drop hsq? Real.sqrt_pos.mpr needs 0 < n... keep minimal: I use hsq2, h21, hsqn, hnR. Drop hsq. Wait — Real.sq_sqrt (by linarith : 0 ≤ (n:ℝ)) : √n^2 = n ✓ needs 0 ≤ ↑n — linarith [hnR] ✓.
u) hwid's field_simp: `field_simp [hne]` — hne : (point) − 1 ≠ 0. Goal: `(point)/((point) − 1) = 1 + 1/((point) − 1)`. field_simp: cross-multiplies — might produce `(point) = ((point) − 1) + 1`?? or `(point) * ((point)−1) = ((point)−1)*(point)`... Either way `ring` closes ✓ (identities in the variable point). DL-4's hwid ended with `push_cast; ring` — theirs had the hw1 rewrite making forms differ. Mine is uniform — try `field_simp [hne]; ring`; if ring fails (e.g., goal has / leftover), adjust.
Actually — safer alternative avoiding field_simp entirely: prove hwid by direct algebra:
```lean
have hwid : w / (w - 1) = 1 + 1 / (w - 1) := by
rw [show w / (w - 1) = (w - 1 + 1) / (w - 1) by ring_nf... ]
```
Meh — field_simp is standard here; DL-4 used it successfully at the same shape (line 807-813 with the same w/(w−1) = 1+1/(w−1) target — they rw [hw1] first because their RHS was in the (w−1)-as-↑(2√n−1) form; mine stays uniform). field_simp [hne] on `w/(w−1) = 1 + 1/(w−1)`: multiplies through by (w−1): `w = (w−1) + 1`?? — hmm, actually field_simp turns `1 + 1/(w−1)` into `((w−1) + 1)/(w−1)` and then cancels denominators: `w = (w−1) + 1` — ring ✓.
v) `Real.exp_nat_mul` — DL-4 line 801: `(Real.exp_nat_mul _ n).symm` : (Real.exp x)^n = Real.exp (↑n * x)?? — the .symm direction: exp_nat_mul (x : ℝ) (n : ℕ) : Real.exp (↑n * x) = (Real.exp x)^n — .symm : (exp x)^n = exp(↑n*x) ✓ — DL-4's calc step `_ = Real.exp ((n:ℝ) * (1/(2√n)))` := (Real.exp_nat_mul _ n).symm ✓ — the `_` for x unified with 1/(2√n) ✓. Mine: same with 1/(2√n−1) ✓.
w) `pow_le_pow_left₀` — signature: (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n ✓ DL-4 used ✓.
x) norm_add_le — `norm_add_le (a b) : ‖a + b‖ ≤ ‖a‖ + ‖b‖` ✓ standard.
y) `abs_of_nonneg h21.le` — h21 : 0 < 2√n−1 — h21.le : 0 ≤ ✓.
z) `one_div_le_one_div_of_le h21 hnorm_w1` : 1/‖w−1‖ ≤ 1/(2√n−1) ✓.
Let me also double-check `Jlag_norm_eq` applicability: Jlag_norm_eq (n) (s) : ‖Jlag n s‖ = ‖kFun n s‖ * ‖logDeriv riemannZeta s‖ ✓ used in hpt via rw [Jlag_norm_eq] — the goal ‖Jlag n (point)‖ ≤ K*L' → ‖kFun n (point)‖*‖logDeriv ζ (point)‖ ≤ K*L' ✓ then mul_le_mul ✓.
Alright — also the file header §3 line: mark DONE after success. And the root-module doc comment — append 6-c-iii to the LiSideBounds bullet at the end.
One more consideration — hexp's show-rw: `(√n/2 + 1/3) * (2√n − 1) = √n^2 + √n/6 − 1/3` — verify by hand: (√n/2)(2√n) = √n². (√n/2)(−1) = −√n/2. (1/3)(2√n) = 2√n/3. (1/3)(−1) = −1/3. Total: √n² + √n(−1/2 + 2/3) − 1/3 = √n² + √n/6 − 1/3 ✓. ring proves ✓.
Then `rw [..., hsqn]` — hsqn : √n^2 = ↑n — rewrites √n^2 → ↑n ✓ goal: ↑n ≤ ↑n + √n/6 − 1/3 — linarith [hsq2] : √n ≥ 2 ⟹ √n/6 ≥ 1/3 ✓ closes ✓.
Wait — CAREFUL: rw [hsqn] rewrites `√n^2` — but the goal ALSO has √n/6 — different pattern (√n not √n^2) ✓ only the square rewrites ✓.
Also — `mul_one_div` : a * (1/b) = a/b ✓ — the goal LHS (n:ℝ) * (1/(2√n−1)) → (n:ℝ)/(2√n−1) ✓ then div_le_iff₀ h21 ✓.
Now write §3. Also update the header comment §3 to DONE after build success, and extend the root-module doc bullet. Let me write the code now.
All templates and signatures confirmed. Writing §3 (6-c-iii) — the F-E kernel lemma + the I_I bound.
tool: Edit
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSideBounds.lean",
"old_string": " _ \u2264 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 := by\n linarith [htailInt, hmidInt, hnn, hlognn]\n\nend NguyenRH1",
"new_string": " _ \u2264 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 := by\n linarith [htailInt, hmidInt, hnn, hlognn]\n\n/-! ## 3. 6-c-iii: I_I \u2014 the right vertical \u03c3\u2081 = 2\u221an (F-E form) -/\n\n/-- **The F-E kernel lemma** (D-074 \u00a79): the uniform-in-t kernel bound at\nthe right vertical \u03c3 = 2\u221an \u2014 \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2+1/3}+1 for n \u2265 4.\nThe honest charge: |w/(w\u22121)| = |1+1/(w\u22121)| \u2264 1 + 1/\u2016w\u22121\u2016 \u2264 1 + 1/(2\u221an\u22121)\n(plain triangle + \u2016w\u22121\u2016 \u2265 re(w\u22121) = 2\u221an\u22121 \u2014 the worst case is t = 0,\nrepairing the off-by-one of the t\u00b2 \u2265 n / re \u2265 2\u221an+1 variants), then\n(1+1/(2\u221an\u22121))\u207f \u2264 exp(n/(2\u221an\u22121)) \u2264 exp(\u221an/2+1/3) \u27fa n \u2265 4. -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_add_third {n : \u2115} (hn : 4 \u2264 n)\n (t : \u211d) :\n \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1 := by\n have hnR : (4 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsq2 : (2 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have h21 : (0 : \u211d) < 2 * Real.sqrt (n : \u211d) - 1 := by nlinarith [hsq2]\n have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n -- w \u2212 1 \u2260 0 and \u2016w \u2212 1\u2016 \u2265 2\u221an \u2212 1\n have hre : ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1).re =\n 2 * Real.sqrt (n : \u211d) - 1 := by\n simp [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.mul_re,\n Complex.I_re, Complex.I_im, Complex.one_re]\n have hne : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1 \u2260 0 := by\n intro h\n have h0 : ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1).re = 0 := by\n rw [h]; simp\n rw [hre] at h0\n nlinarith [h21]\n have hnorm_w1 : 2 * Real.sqrt (n : \u211d) - 1 \u2264\n \u2016(((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1\u2016 := by\n have h1 := abs_re_le_norm ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\n rw [hre, abs_of_nonneg h21.le] at h1\n exact h1\n -- the base bound \u20161 + 1/(w\u22121)\u2016 \u2264 1 + 1/(2\u221an\u22121)\n have hinv : 1 / \u2016(((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1\u2016 \u2264\n 1 / (2 * Real.sqrt (n : \u211d) - 1) :=\n one_div_le_one_div_of_le h21 hnorm_w1\n have hbase : \u20161 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016 \u2264\n 1 + 1 / (2 * Real.sqrt (n : \u211d) - 1) := by\n calc \u20161 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016\n \u2264 \u2016(1 : \u2102)\u2016 + \u20161 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016 :=\n norm_add_le _ _\n _ = 1 + 1 / \u2016(((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1\u2016 := by\n rw [norm_one, norm_div, norm_one]\n _ \u2264 1 + 1 / (2 * Real.sqrt (n : \u211d) - 1) := by linarith [hinv]\n have hbasepos : (0 : \u211d) \u2264 1 + 1 / (2 * Real.sqrt (n : \u211d) - 1) := by positivity\n -- the power + exp chain: (1+1/(2\u221an\u22121))\u207f \u2264 exp(n/(2\u221an\u22121)) \u2264 exp(\u221an/2+1/3)\n have hexp : (n : \u211d) * (1 / (2 * Real.sqrt (n : \u211d) - 1)) \u2264\n Real.sqrt (n : \u211d) / 2 + 1 / 3 := by\n rw [mul_one_div, div_le_iff\u2080 h21,\n show (Real.sqrt (n : \u211d) / 2 + 1 / 3) * (2 * Real.sqrt (n : \u211d) - 1) =\n Real.sqrt (n : \u211d) ^ 2 + Real.sqrt (n : \u211d) / 6 - 1 / 3 := by ring, hsqn]\n linarith [hsq2]\n have hpow : (1 + 1 / (2 * Real.sqrt (n : \u211d) - 1)) ^ n \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) := by\n calc (1 + 1 / (2 * Real.sqrt (n : \u211d) - 1)) ^ n\n \u2264 (Real.exp (1 / (2 * Real.sqrt (n : \u211d) - 1))) ^ n :=\n pow_le_pow_left\u2080 hbasepos (Real.add_one_le_exp _) n\n _ = Real.exp ((n : \u211d) * (1 / (2 * Real.sqrt (n : \u211d) - 1))) :=\n (Real.exp_nat_mul _ n).symm\n _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) := Real.exp_le_exp.mpr hexp\n have hpow1 : \u20161 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016 ^ n \u2264\n (1 + 1 / (2 * Real.sqrt (n : \u211d) - 1)) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) hbase n\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)) : \u211d) + t * Complex.I) - 1) := by\n field_simp [hne]\n ring\n unfold kFun\n rw [hwid]\n calc \u2016(1 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)) ^ n - 1\u2016\n \u2264 \u2016(1 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)) ^ n\u2016 +\n \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n _ = \u20161 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016 ^ n + 1 := by\n rw [norm_pow, norm_one]\n _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1 := by\n linarith [hpow1.trans hpow]\n\n/-- **6-c-iii (I_I, the right vertical \u03c3\u2081 = 2\u221an, F-E form)**: the full-side\nbound \u2016V\u2016 \u2264 e^{1/3}\u00b7IIMaj(n). The F-E kernel (uniform in t) + the DL-6\ndirect Dirichlet bound \u2016\u03b6\u2032/\u03b6\u2016 \u2264 0.57\u00b72^{\u2212(2\u221an\u22122)}; the comparison\ne^{\u221an/2+1/3}+1 \u2264 e^{1/3}(e^{\u221an/2}+1) holds since 1 \u2264 e^{1/3}. -/\ntheorem vIntegral_Jlag_right_le_exp_third_IIMaj {n : \u2115} (hn : 100000 \u2264 n)\n {T : \u211d} (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) (-T) T\u2016 \u2264\n Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := by\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hn4 : 4 \u2264 n := by omega\n have hn5 : 5 \u2264 n := by omega\n have hsq2 : (2 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have hT0 : (0 : \u211d) \u2264 T := by\n have h := Real.sqrt_nonneg (n : \u211d)\n linarith\n have hTT : -T \u2264 T := by linarith\n -- zero-freeness + continuity on the right vertical (re = 2\u221an > 1)\n have hzne : \u2200 t : \u211d,\n riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) \u2260 0 := by\n intro t\n have hre : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I).re =\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 have h1 : (1 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by nlinarith [hsq2]\n exact riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)\n have hJcont : \u2200 t : \u211d, ContinuousAt (Jlag n)\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) := by\n intro t\n have hs1 : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) \u2260 1 := by\n intro h\n have hre := congrArg Complex.re h\n simp at hre\n nlinarith [hsq2]\n have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n have hB := continuousAt_logDeriv_zeta hs1 (hzne t)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hpath : Continuous fun u : \u211d =>\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + u * Complex.I) := by fun_prop\n have hcontJ : Continuous fun t : \u211d =>\n Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro t\n have hf : ContinuousAt (fun u : \u211d =>\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + u * Complex.I)) t := hpath.continuousAt\n have hcomp : ContinuousAt\n (Jlag n \u2218 fun u : \u211d => (((2 * Real.sqrt (n : \u211d)) : \u211d) + u * Complex.I)) t :=\n ContinuousAt.comp (g := Jlag n)\n (f := fun u : \u211d => (((2 * Real.sqrt (n : \u211d)) : \u211d) + u * Complex.I)) (x := t)\n (hJcont t) hf\n exact hcomp\n have hcontG : Continuous fun t : \u211d =>\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 :=\n continuous_norm.comp hcontJ\n have hI2 : IntervalIntegrable\n (fun t : \u211d => \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016)\n MeasureTheory.volume (-T) T := hcontG.intervalIntegrable _ _\n -- the comparison e^{\u221an/2+1/3}+1 \u2264 e^{1/3}(e^{\u221an/2}+1) (since 1 \u2264 e^{1/3})\n have hKle : Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1 \u2264\n Real.exp (1 / 3 : \u211d) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) := by\n rw [Real.exp_add]\n have h1 : (1 : \u211d) \u2264 Real.exp (1 / 3 : \u211d) := by\n have h := Real.add_one_le_exp (1 / 3 : \u211d)\n linarith\n have hE := Real.exp_pos (Real.sqrt (n : \u211d) / 2)\n nlinarith [h1, hE]\n -- the pointwise bound\n have hK' : (0 : \u211d) \u2264 Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1 := by positivity\n have hL : (0 : \u211d) \u2264 (0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n positivity\n have hpt : \u2200 t : \u211d, t \u2208 Set.Icc (-T) T \u2192\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by\n intro t _\n rw [Jlag_norm_eq]\n exact mul_le_mul (kFun_right_vertical_norm_le_exp_sqrt_add_third hn4 t)\n (norm_logDeriv_zeta_le_iimZeta hn5) (norm_nonneg _) hK'\n have hInt : \u222b t in (-T)..T,\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n (T - -T) * ((Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by\n have h := intervalIntegral.integral_mono_on hTT hI2 intervalIntegrable_const\n (fun t ht => hpt t ht)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n -- the final comparison 2T\u00b7K\u00b7L \u2264 e^{1/3}\u00b7IIMaj (T \u2264 \u221an+1, hKle)\n have hKL : (0 : \u211d) \u2264 (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) :=\n mul_nonneg hK' hL\n have hnL : (0 : \u211d) \u2264 2 * (Real.sqrt (n : \u211d) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by\n have h1 : (0 : \u211d) \u2264 Real.sqrt (n : \u211d) + 1 := by positivity\n exact mul_nonneg (mul_nonneg (by norm_num) h1) hL\n have hfinal : 2 * T * (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) \u2264\n Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := by\n unfold IIMaj\n nlinarith [hTn1, hKle, hKL, hnL, Real.exp_pos (1 / 3 : \u211d),\n Real.exp_pos (Real.sqrt (n : \u211d) / 2)]\n calc \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) (-T) T\u2016\n = \u2016\u222b t in (-T)..T, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 :=\n VIntegral_norm\n _ \u2264 \u222b t in (-T)..T, \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 :=\n intervalIntegral.norm_integral_le_integral_norm hTT\n _ \u2264 (T - -T) * ((Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := hInt\n _ = 2 * T * (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by ring\n _ \u2264 Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := hfinal\n\nend NguyenRH1"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`riemannZeta_ne_zero_of_one_le_re ⦃s : ℂ⦄ (hs : 1 ≤ s.re) : riemannZeta s ≠ 0` — takes only re ✓ (s implicit-instance-ish ⦃s⦄ — strict implicit, determined by hs).\n\nUsage pattern: `riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)` — with s determined by the hs's type ✓.\n\nNow write §3 (6-c-iii) into LiSideBounds.lean. Structure:\n\n```lean\n/-! ## 3. 6-c-iii: I_I — the right vertical σ₁ = 2√n (F-E form) -/\n\n/-- **The F-E kernel lemma** (D-074 §9): the uniform-in-t kernel bound at\nthe right vertical σ = 2√n — ‖kFun n (2√n+it)‖ ≤ e^{√n/2+1/3}+1 for n ≥ 4.\n(The honest charge: |w/(w−1)| ≤ 1 + 1/(2√n−1) via the plain triangle\ninequality + ‖w−1‖ ≥ re(w−1) = 2√n−1; then (1+1/(2√n−1))ⁿ ≤\nexp(n/(2√n−1)) ≤ exp(√n/2+1/3) ⟺ n ≥ 4. Fixes the off-by-one in the\nt² ≥ n / re ≥ 2√n+1 variants at t = 0.) -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_add_third {n : ℕ} (hn : 4 ≤ n)\n (t : ℝ) : ...\n```\n\nWait — (t : ℝ) explicit or implicit? The consumers apply at specific t — explicit fine.\n\nThen the I_I theorem. Let me write the full code.\n\nFor the final lemma name: `vIntegral_Jlag_right_le_exp_third_IIMaj`.\n\nDetails to nail:\n- hn4 : 4 ≤ n := by omega (from hn : 100000 ≤ n) ✓ omega.\n- hn5 : 5 ≤ n := by omega.\n- The point form everywhere: `(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)` — matching DL-4/DL-6.\n\nWait — VIntegral_norm gives the integral point as `((x : ℝ) + (t : ℝ) * Complex.I)` where x := 2 * Real.sqrt (n:ℝ) — elaborated `↑(2 * √(↑n)) + ↑t * I` — and DL-6's point: `(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)` — `↑(2*√(↑n)) + ↑t * I` ✓ identical.\n\nHmm — but there's ONE subtlety: in VIntegral_norm's statement, the point is written `((x : ℝ) + (t : ℝ) * Complex.I)` — since x is ALREADY ℝ, the `(x : ℝ)` is a no-op annotation — elaborated term: `↑x + ↑t * I`? The coercion on x: since f : ℂ → ℂ and + needs ℂ, Lean inserts ↑ on the first argument ✓ `↑x + ↑t * I` ✓. And the t: `(t : ℝ) * Complex.I` — ↑t * I ✓. Same as DL's `↑(2*√n) + ↑t * I` ✓.\n\nBut WAIT — in the DL-4 statement the point is `(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)` — hmm, the `t * Complex.I` here — t : ℝ — `↑t * I` ✓ same.\n\nOK. And my §3 statements should use the DL point form `(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)` for consistency with norm_logDeriv_zeta_le_iimZeta and the kernel lemma.\n\nOne more check — the kernel lemma's statement point: same DL form. norm_logDeriv_zeta_le_iimZeta's point: same. The VIntegral path: VIntegral (Jlag n) (2 * Real.sqrt (n:ℝ)) (-T) T — x := 2*√(↑n) — after VIntegral_norm: ∫ t in -T..T, Jlag n (↑(2*√(↑n)) + ↑t*I) ✓.\n\nHmm — will `↑(2*√(↑n))` from VIntegral_norm (with x := 2*√(↑n)) syntactically match the DL point's first term `↑(2*√(↑n))`? VIntegral_norm's x is `2 * Real.sqrt (n:ℝ)` — written identically ✓ same term ✓.\n\nNow — hsq2 : 2 ≤ √(↑n): needed in hzne (1 ≤ 2√n), hne/hsq1 in the kernel lemma, and hexp. Let me structure the kernel lemma with its own hsq2 (from hn : 4 ≤ n).\n\nKernel lemma:\n\n```lean\ntheorem kFun_right_vertical_norm_le_exp_sqrt_add_third {n : ℕ} (hn : 4 ≤ n)\n (t : ℝ) :\n ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by\n have hnR : (4 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hsq : (0 : ℝ) < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr (by linarith)\n have hsq2 : (2 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have h21 : (0 : ℝ) < 2 * Real.sqrt (n : ℝ) - 1 := by nlinarith [hsq2]\n have hsqn : Real.sqrt (n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt (by linarith)\n -- w − 1 ≠ 0 and ‖w − 1‖ ≥ 2√n − 1\n have hre : ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1).re =\n 2 * Real.sqrt (n : ℝ) - 1 := by\n simp [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.mul_re,\n Complex.I_re, Complex.I_im, Complex.one_re]\n have hne : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1 ≠ 0 := by\n intro h\n have h0 : ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1).re = 0 := by\n rw [h]; simp\n rw [hre] at h0\n nlinarith [h21]\n have hnorm_w1 : 2 * Real.sqrt (n : ℝ) - 1 ≤\n ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ := by\n have h1 := abs_re_le_norm ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)\n rw [hre, abs_of_nonneg h21.le] at h1\n exact h1\n -- the base bound ‖1 + 1/(w−1)‖ ≤ 1 + 1/(2√n−1)\n have hinv : 1 / ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ ≤\n 1 / (2 * Real.sqrt (n : ℝ) - 1) :=\n one_div_le_one_div_of_le h21 hnorm_w1\n have hbase : ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ≤\n 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by\n calc ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖\n ≤ ‖(1 : ℂ)‖ + ‖1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ :=\n norm_add_le _ _\n _ = 1 + 1 / ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ := by\n rw [norm_one, norm_div, norm_one]\n _ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by linarith [hinv]\n have hbasepos : (0 : ℝ) ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by positivity\n -- the power + exp chain\n have hexp : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1)) ≤\n Real.sqrt (n : ℝ) / 2 + 1 / 3 := by\n rw [mul_one_div, div_le_iff₀ h21]\n nlinarith [hsqn, hsq2]\n have hpow : (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n ≤\n Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) := by\n calc (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n\n ≤ (Real.exp (1 / (2 * Real.sqrt (n : ℝ) - 1))) ^ n :=\n pow_le_pow_left₀ hbasepos (Real.add_one_le_exp _) n\n _ = Real.exp ((n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1))) :=\n (Real.exp_nat_mul _ n).symm\n _ ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) := Real.exp_le_exp.mpr hexp\n have hpow1 : ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ^ n ≤\n (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n :=\n pow_le_pow_left₀ (norm_nonneg _) hbase n\n have hwid : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) /\n ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) =\n 1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) := by\n field_simp [hne]\n ring\n unfold kFun\n rw [hwid]\n calc ‖(1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)) ^ n - 1‖\n ≤ ‖(1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)) ^ n‖ +\n ‖(1 : ℂ)‖ := norm_sub_le _ _\n _ = ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ^ n + 1 := by\n rw [norm_pow, norm_one]\n _ ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by\n linarith [hpow1.trans hpow]\n```\n\nChecks:\n- hexp's nlinarith: goal after rw [mul_one_div, div_le_iff₀ h21]: `(n:ℝ) ≤ (√n/2 + 1/3) * (2*√n − 1)`. nlinarith [hsqn, hsq2]: expand RHS: (√n/2)(2√n) − √n/2 + (2/3)√n − 1/3 = √n² − √n/2 + 2√n/3 − 1/3 = n + √n/6 − 1/3. Need n ≤ n + √n/6 − 1/3 ⟺ 1/3 ≤ √n/6 ⟺ 2 ≤ √n ✓ hsq2. nlinarith ring_nf's the product ✓ with √n·√n → (√n)^2 = n via hsqn ✓ closes. Hmm — nlinarith multiplies hypotheses pairwise: does it need a hint product? The goal after ring_nf: n ≤ n + (1/6)√n − 1/3-ish — but the ring_nf of the RHS product requires multiplying out (√n/2+1/3)*(2√n−1) — that's part of GOAL normalization (ring_nf handles products in the goal ✓). The (√n)^2 → n step: hsqn : √n^2 = n as a hint rewrite — nlinarith uses hsqn as an equation hint ✓ standard pattern from DL-4 (line 770: nlinarith [sq_nonneg ..., hnR] with hsqn rw'd first — hmm, DL-4 rw'd hsqn INTO the goal first at line 769/774). For safety, mirror DL-4: rw the goal into explicit form first? DL-4's hkey did `rw [show (2√n−1)^2 + t^2 = 4(√n²) − 4√n + 1 + t² by ring, hsqn]` — they rw [hsqn] after rewriting into √n² form. For my hexp: after div_le_iff₀, goal `n ≤ (√n/2+1/3)*(2√n−1)` — I could `rw [show (√n/2+1/3)*(2√n−1) = √n^2 + √n/6 − 1/3 := by ring]`... wait that identity: (√n/2+1/3)(2√n−1) = √n² − √n/2 + 2√n/3 − 1/3 = √n² + √n(−1/2+2/3) − 1/3 = √n² + √n/6 − 1/3 ✓. `by ring` proves it (ring in √n) ✓. Then rw [hsqn]: √n^2 → n — wait hsqn : √n^2 = n — rw [hsqn] rewrites √n^2 → n ✓ goal: n ≤ n + √n/6 − 1/3 — then linarith [hsq2] ✓ DETERMINISTIC. \n\n Let me use that explicit route:\n ```lean\n have hexp : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1)) ≤\n Real.sqrt (n : ℝ) / 2 + 1 / 3 := by\n rw [mul_one_div, div_le_iff₀ h21,\n show (Real.sqrt (n : ℝ) / 2 + 1 / 3) * (2 * Real.sqrt (n : ℝ) - 1) =\n Real.sqrt (n : ℝ) ^ 2 + Real.sqrt (n : ℝ) / 6 - 1 / 3 := by ring, hsqn]\n linarith [hsq2]\n ```\n rw chains three rewrites ✓ ends with goal `n ≤ n + √n/6 − 1/3` — linarith [hsq2] ✓ (1/3 ≤ √n/6 ⟺ 2 ≤ √n ✓ linear in √n ✓).\n\n Hmm — the `show ... := by ring` — ring proves `(√n/2 + 1/3)*(2√n − 1) = √n^2 + √n/6 − 1/3` — over ℝ with √n as atom ✓ ring ✓.\n\n Wait — does `rw [mul_one_div]` produce `(n:ℝ)/(2√n−1)`? mul_one_div (a b) : a * (1/b) = a/b ✓. Then div_le_iff₀ h21 : a/b ≤ c ↔ a ≤ c*b — rewrites the iff ✓ goal becomes `(n:ℝ) ≤ (√n/2+1/3)*(2√n−1)` ✓ then the show-rw ✓ then hsqn ✓.\n\n Actually — one concern: `rw [div_le_iff₀ h21]` — div_le_iff₀ : a / b ≤ c ↔ a ≤ c * b ✓ (session-033 banked ✓).\n\n- hpow's calc step 1: pow_le_pow_left₀ hbasepos (Real.add_one_le_exp _) n : (1+1/(2√n−1))^n ≤ (exp(1/(2√n−1)))^n. Real.add_one_le_exp (x) : 1 + x ≤ exp x ✓ with x := 1/(2√n−1) — the `_` unified ✓. pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) (n) : a^n ≤ b^n ✓.\n\n- hpow step 2: (exp(x))^n = exp(n*x) — Real.exp_nat_mul (x) (n : ℕ) : Real.exp (↑n * x) = (Real.exp x)^n — .symm : (exp x)^n = exp(↑n * x) — hmm, but is the cast there? DL-4 line 800-801: `(Real.exp ((n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ))))) := (Real.exp_nat_mul _ n).symm` ✓ same usage ✓.\n\n- hpow step 3: Real.exp_le_exp.mpr hexp : exp(n/(2√n−1)-form) ≤ exp(√n/2+1/3) — the calc line's LHS: Real.exp ((n:ℝ) * (1/(2√n−1))) — hexp : (n:ℝ)*(1/(2√n−1)) ≤ √n/2+1/3 ✓ exp_le_exp.mpr : a ≤ b → exp a ≤ exp b ✓ the a here is (n:ℝ)*(1/(2√n−1)) ✓ matches ✓.\n\n Real.exp_le_exp : Real.exp a ≤ Real.exp b ↔ a ≤ b ✓ standard.\n\n- hpow1: pow_le_pow_left₀ (norm_nonneg _) hbase n : ‖1+1/(w−1)‖^n ≤ (1+1/(2√n−1))^n ✓.\n\n- hwid: field_simp [hne] — goal `w/(w−1) = 1 + 1/(w−1)` — field_simp with hne : w−1 ≠ 0 ✓ then ring ✓. Hmm — DL-4 needed `push_cast; ring` after field_simp — because their hs0/hw1 had cast forms. Mine: w is `↑(2*√(↑n)) + ↑t * I` — field_simp produces something like `↑(2*√↑n) + ↑t*I = (↑(2*√↑n) + ↑t*I − 1) + 1`?? — ring closes over ℂ with cast atoms ✓. If ring fails, add push_cast before ring. Let me preemptively write `field_simp [hne]; ring` and adjust if needed.\n\n Hmm — actually wait: field_simp on `w/(w−1) = 1 + 1/(w−1)`: it might rewrite to `w = (w − 1) + 1` directly? Or `w * (w−1) = (w−1)*w`?? Standard behavior: field_simp [hne] with hne : w−1 ≠ 0 — the goal has denominator (w−1) on both sides — field_simp multiplies both sides by (w−1): `w = (1 + 1/(w−1))*(w−1)` then distributes?? Usually leaves `w = (w - 1) + 1` or similar — ring closes either way ✓.\n\n- unfold kFun: goal `‖(w/(w−1))^n − 1‖ ≤ ...` — rw [hwid] rewrites w/(w−1) → 1+1/(w−1) ✓.\n\n Hmm — `unfold kFun` — does the goal after unfold show `(w/(w-1))^n - 1`? kFun n s := (s/(s-1))^n - 1 ✓ (from kFun_norm_le_two's rfl). unfold kFun at goal ‖kFun n w‖ ≤ e+1 → ‖(w/(w−1))^n − 1‖ ≤ e+1 ✓. rw [hwid] : pattern w/(w−1) ✓.\n\n Wait — will unfold produce the exact `w` form? The statement's kFun n (point) — unfold kFun n (point) → ((point)/(point − 1))^n − 1 ✓ hwid's LHS is exactly (point)/(point−1) ✓.\n\n- The final calc — the `_ = ‖1 + 1/(w−1)‖^n + 1` step: rw [norm_pow, norm_one] : ‖(1+1/(w−1))^n‖ → ‖1+1/(w−1)‖^n ✓ and ‖(1:ℂ)‖ → 1 ✓.\n\n- `linarith [hpow1.trans hpow]` : hpow1.trans hpow : ‖1+1/(w−1)‖^n ≤ exp(√n/2+1/3) ✓ goal: ‖1+1/(w−1)‖^n + 1 ≤ exp(√n/2+1/3)+1 ✓ linarith ✓.\n\n- hnorm_w1's abs_of_nonneg h21.le : |2√n−1| = 2√n−1 ✓ — wait, abs_of_nonneg (h : 0 ≤ a) : |a| = a — h21.le : 0 ≤ 2√n−1 ✓. rw [hre, abs_of_nonneg h21.le] at h1: h1 : |(w−1).re| ≤ ‖w−1‖ — rw [hre] : |2√n−1| ≤ ‖w−1‖ — rw [abs_of_nonneg h21.le] : 2√n−1 ≤ ‖w−1‖ ✓ exact h1 ✓.\n\n Hmm — abs_re_le_norm — in LiTightR used unqualified (line 158: `have h := abs_re_le_norm ((2 + t * Complex.I) - ρ.1)`) ✓ Complex.abs_re_le_norm is opened via `open ... Complex` ✓.\n\n- hbase's calc step 2: `‖(1:ℂ)‖ + ‖1/(w−1)‖ = 1 + 1/‖w−1‖`: rw [norm_one] : ‖(1:ℂ)‖ → 1 ✓; ‖1/(w−1)‖: norm_div → ‖1‖/‖w−1‖ → 1/‖w−1‖: rw [norm_div, norm_one] ✓. Order: rw [norm_one, norm_div, norm_one] — first norm_one rewrites ALL ‖(1:ℂ)‖ occurrences (both the standalone and inside norm_div? — norm_div hasn't fired yet — the term is ‖(1:ℂ)‖ + ‖(1:ℂ)/(w−1)‖ — norm_one fires on both ‖(1:ℂ)‖ atoms: → 1 + (‖(1:ℂ)‖/‖w−1‖)... wait ‖1/(w−1)‖ is ‖HDiv.hDiv (1:ℂ) (w−1)‖ — norm_one's pattern ‖(1:ℂ)‖ — the numerator inside is `(1:ℂ)` but not wrapped in ‖·‖ yet — norm_one only matches the OUTER ‖(1:ℂ)‖ and... hmm: term: `‖(1:ℂ)‖ + ‖(1:ℂ)/(w−1)‖`. norm_one pattern: ‖(1:?_)‖ — matches the first ‖(1:ℂ)‖ ✓ → 1. Does it also match inside the second? The second is ‖(1:ℂ)/(w−1)‖ — the pattern ‖(1:ℂ)‖ doesn't match ‖x/y‖ ✓. So after norm_one: `1 + ‖(1:ℂ)/(w−1)‖`. Then norm_div: ‖a/b‖ → ‖a‖/‖b‖: `1 + ‖(1:ℂ)‖/‖w−1‖`. Then norm_one: `1 + 1/‖w−1‖` ✓. So rw [norm_one, norm_div, norm_one] ✓ as written.\n\n- hbasepos by positivity: 0 ≤ 1 + 1/(2√n−1) — needs 0 ≤ 1/(2√n−1) — positivity with h21 (0 < 2√n−1) in context ✓ (positivity uses local hyps for atoms ✓). Hmm — h21 is in scope ✓.\n\nNow the I_I theorem:\n\n```lean\n/-- **6-c-iii (I_I, the right vertical σ₁ = 2√n, F-E form)**: the full-side\nbound ‖V‖ ≤ e^{1/3}·IIMaj(n). The F-E kernel (uniform in t) + the DL-6\ndirect Dirichlet bound; e^{√n/2+1/3}+1 ≤ e^{1/3}(e^{√n/2}+1) since\n1 ≤ e^{1/3}. -/\ntheorem vIntegral_Jlag_right_le_exp_third_IIMaj {n : ℕ} (hn : 100000 ≤ n)\n {T : ℝ} (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖ ≤\n Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := by\n have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hn4 : 4 ≤ n := by omega\n have hn5 : 5 ≤ n := by omega\n have hsq2 : (2 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have hT0 : (0 : ℝ) ≤ T := by\n have h := Real.sqrt_nonneg (n : ℝ)\n linarith\n have hTT : -T ≤ T := by linarith\n -- zero-freeness + continuity on the right vertical\n have hzne : ∀ t : ℝ, riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) ≠ 0 := by\n intro t\n have hre : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I).re =\n 2 * Real.sqrt (n : ℝ) := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im]\n have h1 : (1 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by nlinarith [hsq2]\n exact riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)\n have hJcont : ∀ t : ℝ, ContinuousAt (Jlag n)\n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by\n intro t\n have hs1 : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) ≠ 1 := by\n intro h\n have hre := congrArg Complex.re h\n simp at hre\n nlinarith [hsq2]\n have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n have hB := continuousAt_logDeriv_zeta hs1 (hzne t)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hpath : Continuous fun u : ℝ =>\n (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I) := by fun_prop\n have hcontJ : Continuous fun t : ℝ =>\n Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro t\n have hf : ContinuousAt (fun u : ℝ =>\n (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) t := hpath.continuousAt\n have hcomp : ContinuousAt\n (Jlag n ∘ fun u : ℝ => (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) t :=\n ContinuousAt.comp (g := Jlag n)\n (f := fun u : ℝ => (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) (x := t)\n (hJcont t) hf\n exact hcomp\n have hcontG : Continuous fun t : ℝ =>\n ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=\n continuous_norm.comp hcontJ\n have hI2 : IntervalIntegrable\n (fun t : ℝ => ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖)\n MeasureTheory.volume (-T) T := hcontG.intervalIntegrable _ _\n -- the e^{√n/2+1/3}+1 ≤ e^{1/3}(e^{√n/2}+1) comparison\n have hKle : Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 ≤\n Real.exp (1 / 3 : ℝ) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) := by\n rw [Real.exp_add]\n have h1 : (1 : ℝ) ≤ Real.exp (1 / 3 : ℝ) := by\n have h := Real.add_one_le_exp (1 / 3 : ℝ)\n linarith\n have hE := Real.exp_pos (Real.sqrt (n : ℝ) / 2)\n nlinarith [h1, hE]\n -- the pointwise bound\n have hK' : (0 : ℝ) ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by positivity\n have hL : (0 : ℝ) ≤ (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by\n positivity\n have hpt : ∀ t : ℝ, t ∈ Set.Icc (-T) T →\n ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by\n intro t _\n rw [Jlag_norm_eq]\n exact mul_le_mul (kFun_right_vertical_norm_le_exp_sqrt_add_third hn4 t)\n (norm_logDeriv_zeta_le_iimZeta hn5) (norm_nonneg _) hK'\n have hInt : ∫ t in (-T)..T,\n ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n (T - -T) * ((Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by\n have h := intervalIntegral.integral_mono_on hTT hI2 intervalIntegrable_const\n (fun t ht => hpt t ht)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n -- the final comparison 2T·K·L ≤ e^{1/3}·IIMaj\n have hKL : (0 : ℝ) ≤ (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) :=\n mul_nonneg hK' hL\n have hnL : (0 : ℝ) ≤ 2 * (Real.sqrt (n : ℝ) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by\n have h1 : (0 : ℝ) ≤ Real.sqrt (n : ℝ) + 1 := by positivity\n exact mul_nonneg (mul_nonneg (by norm_num) h1) hL\n have hfinal : 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) ≤\n Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := by\n unfold IIMaj\n nlinarith [hTn1, hKle, hKL, hnL, Real.exp_pos (1 / 3 : ℝ),\n Real.exp_pos (Real.sqrt (n : ℝ) / 2)]\n calc ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖\n = ‖∫ t in (-T)..T, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=\n VIntegral_norm\n _ ≤ ∫ t in (-T)..T, ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=\n intervalIntegral.norm_integral_le_integral_norm hTT\n _ ≤ (T - -T) * ((Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := hInt\n _ = 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring\n _ ≤ Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := hfinal\n```\n\nConcerns:\n\na) `simp at hre` in hs1 (hJcont): hre : (↑(2√n)+↑t·I).re = (1:ℂ).re — simp → `2*√(↑n) = 1` — nlinarith [hsq2]: 2√n ≥ 4 = 1?? contradiction ✓ (linear: 2·(√n atom) = 1 with √n ≥ 2 ✓ linarith actually — nlinarith fine).\n\nHmm — will simp fully reduce (↑(2*√(↑n)) + ↑t * I).re? add_re → (↑(2√n)).re + (↑t·I).re; ofReal_re → 2√n; mul_re → t·I.re − (0)·I.im — (↑t).re = t, (↑t).im = 0 — t*0 − 0*1 = 0; RHS (1:ℂ).re → 1. simp set: [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im] ✓ plus Complex.one_re for RHS — add Complex.one_re to the simp set in hs1 (congrArg re of h : point = 1 — RHS is Complex.re 1 — simp needs Complex.one_re ✓). In 6-c-ii's hs1 I used plain `simp at hre` and it worked (gave -5/2 = 1) — simp's default set includes the Complex re/im lemmas ✓ plain simp suffices.\n\nSimilarly hzne's hre: `simp [Complex.add_re, ...]` — explicit set — should include nothing extra; plain simp worked in zeta_ne_zero_left_vertical for `.re = -5/2` — for `.re = 2*√n`: plain `by simp`? The DL-4 hre used the explicit set. I'll keep the explicit set (harmless).\n\nb) hT0 : 0 ≤ T — from hTn : √n ≤ T and √n ≥ 0: linarith [Real.sqrt_nonneg (n:ℝ)] — I wrote `have h := Real.sqrt_nonneg (n:ℝ); linarith` ✓.\n\nc) The `(T - -T) * X = 2 * T * X` ring step ✓.\n\nd) hfinal's nlinarith — after unfold IIMaj: goal `2*T*K*L' ≤ e13*(2*(√n+1)*(E+1)*0.57*2^(...))` where K = e^{√n/2+1/3}+1, L' = 0.57*2^(...), E = e^{√n/2}. Note: my L' written as `(0.57:ℝ) * (2:ℝ)^(-(2*√n−2))` and IIMaj's tail: `0.57 * 2 ^ (-(2 * Real.sqrt n - 2))` — SAME ✓ (IIMaj's n here is (n:ℝ) since IIMaj : ℝ → ℝ and I apply at (n:ℝ) — the def's `Real.sqrt n` with n := ↑(n:ℕ) — `Real.sqrt (↑n)` ✓ same as my `Real.sqrt (n:ℝ)` ✓).\n\nWait — IIMaj (n : ℝ) — applying IIMaj (n:ℝ) where (n:ℝ) = ↑(n:ℕ) — the def unfolds with `Real.sqrt ↑n` ✓ matches my `Real.sqrt (n : ℝ)` — same term ✓.\n\nnlinarith hint analysis (as before): hTn1 : T ≤ √n+1; hKle : K ≤ e13(E+1); hKL : 0 ≤ K*L'; hnL : 0 ≤ 2(√n+1)L'. Goal: 2TKL' ≤ e13·2(√n+1)(E+1)L'. Derivation: 2TKL' ≤ 2(√n+1)KL' [2·(KL'·(√n+1−T))] ≤ 2(√n+1)·e13(E+1)·L' [2(√n+1)L'·(e13(E+1)−K)] = RHS ✓. nlinarith pairwise products: (hTn1, hKL) and (hKle, hnL) ✓ then linear ✓. The ring_nf normalization of monomials T*K*L', K*L'*√n, e13*E*L'*√n... — all distinct monomial atoms ✓ linear after expansion ✓ should close. \n\nRisk: nlinarith's preprocessing might not multiply hKle (a ≤-inequality with the exp sides) by hnL — it does consider pairs of ALL hypotheses including provided ones ✓.\n\nIf it fails, fallback: explicit two-step mul_le_mul. I'll write nlinarith first, fallback if error.\n\ne) `Real.add_one_le_exp (1/3 : ℝ) : 1 + 1/3 ≤ exp(1/3)` — linarith → 1 ≤ exp(1/3) ✓.\n\nf) hKle's nlinarith [h1, hE]: goal after rw [Real.exp_add]: `exp(√n/2)*exp(1/3) + 1 ≤ exp(1/3)*(exp(√n/2)+1)`. ring_nf RHS: exp(1/3)*exp(√n/2) + exp(1/3). Goal ⟺ E·e13 + 1 ≤ e13·E + e13 ⟺ 1 ≤ e13 ✓ h1. linarith would do (atoms E·e13 and e13·E normalize to same monomial ✓): actually plain `linarith [h1, hE]` — the products E*e13 vs e13*E — ring_nf in linarith normalizes ✓. nlinarith fine too.\n\ng) `rw [Real.exp_add]` at goal — Real.exp_add (a b) : exp(a+b) = exp a * exp b — the goal's LHS exp(√n/2 + 1/3) ✓ matches.\n\nh) The `show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _` — worked in 6-c-ii ✓.\n\ni) hpt's mul_le_mul: mul_le_mul (hk : ‖kFun‖ ≤ K) (hlog : ‖logDeriv‖ ≤ L') (norm_nonneg _ : 0 ≤ ‖logDeriv‖) (hK' : 0 ≤ K) : ‖kFun‖*‖logDeriv‖ ≤ K*L' ✓ — norm_logDeriv_zeta_le_iimZeta hn5 : ‖logDeriv ζ (point)‖ ≤ 0.57 * 2^(-(2√n−2)) — the point: `(((2 * Real.sqrt (n: ℝ)) : ℝ) + t * Complex.I)` ✓ matches ✓.\n\nWait — norm_logDeriv_zeta_le_iimZeta's implicit {t : ℝ} — applying `(norm_logDeriv_zeta_le_iimZeta hn5)` leaves t implicit — determined by unification with the goal (the h₂ slot: ‖logDeriv ζ (point-t)‖ ≤ ...) ✓.\n\nj) hI2's `hcontG.intervalIntegrable _ _` : IntervalIntegrable F volume (-T) T ✓.\n\nk) In hInt — intervalIntegrable_const's c := K*L' determined by hpt's bound ✓.\n\nl) `VIntegral_norm` — its point form `((x : ℝ) + (t : ℝ) * Complex.I)` — hmm — actually now I realize a potential MISMATCH: VIntegral_norm's RHS (as written in §1) is `‖∫ t in y₁..y₂, f ((x : ℝ) + (t : ℝ) * Complex.I)‖` — x : ℝ so (x : ℝ) is just x with a coercion to ℂ at the +: `↑x + ↑t * I`. My calc step: `‖∫ t in (-T)..T, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖` — point: `↑(2*√↑n) + ↑t * I` ✓ with x := 2*√(↑n) : ℝ — `↑x = ↑(2*√↑n)` ✓ SAME ✓ — VIntegral_norm applies by rfl-calc ✓ (it worked identically in 6-c-ii).\n\nm) hzne's exact: `riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)` — the hs arg : 1 ≤ (point).re — the by-block: rw [hre] → goal 1 ≤ 2√n — exact h1 ✓. The ⦃s⦄ strict implicit: determined by hs's type — the point is explicit in my by-block's goal ✓ — hmm, strict-implicit: the elaborator needs to determine s from the expected type of hs — which comes from the APPLICATION's expected type: `riemannZeta_ne_zero_of_one_le_re hs : riemannZeta ?s ≠ 0` — my goal (inside hzne after intro t): `riemannZeta (point) ≠ 0` — so ?s := point from the goal ✓ then hs : 1 ≤ (point).re ✓ the by-block elaborates ✓. But I'm using `exact riemannZeta_ne_zero_of_one_le_re (...)` against the goal — the goal fixes ?s ✓.\n\nHmm — wait, in hzne I wrote `have hre ... ; have h1 ... ; exact riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)`. The `by rw [hre]; exact h1` — the expected type: 1 ≤ (point).re — rw [hre] rewrites (point).re → 2√n: goal 1 ≤ 2√n — exact h1 : 1 ≤ 2√n ✓.\n\nn) fun_prop for hpath: `Continuous fun u : ℝ => (↑(2*√↑n) + u * Complex.I)` — same shape as before ✓ (worked in 6-c-ii).\n\no) Positivity for hK' : 0 ≤ exp(...) + 1 ✓ (exp_pos). hL : 0 ≤ 0.57 * 2^(-(2√n−2)) — the power: (2:ℝ)^(-(2*√n−2)) — ℝ^ℝ — rpow — positivity proves 0 ≤ via Real.rpow_nonneg? positivity has an extension for rpow ✓. If the `^` is zpow... the exponent -(2√n−2) : ℝ so rpow ✓ positivity handles ✓. (In DL-6's proof, `dirichletC2_nonneg` etc. — and IIMaj-related proofs in LiSkeleton surely did similar positivity ✓.)\n\np) `Real.exp_pos (1/3 : ℝ)` and `Real.exp_pos (√n/2)` ✓.\n\nq) The final calc's `_ = 2 * T * K * L'` ring step: (T - -T) * (K * L') = 2*T*(K*L')... my stated: `2 * T * (Real.exp ...) * ((0.57) * 2^(...))` — note association: (T - -T)*(K*L') vs 2*T*K*L' — ring normalizes ✓ (K*L' parenthesization differs — ring handles ✓).\n\nr) Naming consistency for Z2hat/IIMaj references — IIMaj is in LiSkeleton ✓ (def, root-imported ✓).\n\ns) One more: `Real.le_sqrt (by norm_num) (by positivity)` — the hyps: (hx : 0 ≤ (2:ℝ)) ✓ norm_num; (hy : 0 ≤ (n:ℝ)) ✓ positivity. Goal 2 ≤ √(↑n) — hmm wait — in hsq2 (I_I theorem) I use the same as the kernel lemma ✓.\n\nt) `nlinarith [hnR]` for (2:ℝ)^2 ≤ ↑n — hnR : 100000 ≤ ↑n ✓ 4 ≤ ↑n ✓.\n\nNow — one thing to double check in the kernel lemma: `Real.le_sqrt` signature: (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ √y ↔ x ^ 2 ≤ y ✓ — rw at goal `2 ≤ √(↑n)` → `(2:ℝ)^2 ≤ ↑n` — nlinarith [hnR] ✓.\n\nAlso — in the kernel lemma I don't need hsq (0 < √n) — h21 comes from hsq2 via nlinarith ✓. Drop hsq? Real.sqrt_pos.mpr needs 0 < n... keep minimal: I use hsq2, h21, hsqn, hnR. Drop hsq. Wait — Real.sq_sqrt (by linarith : 0 ≤ (n:ℝ)) : √n^2 = n ✓ needs 0 ≤ ↑n — linarith [hnR] ✓.\n\nu) hwid's field_simp: `field_simp [hne]` — hne : (point) − 1 ≠ 0. Goal: `(point)/((point) − 1) = 1 + 1/((point) − 1)`. field_simp: cross-multiplies — might produce `(point) = ((point) − 1) + 1`?? or `(point) * ((point)−1) = ((point)−1)*(point)`... Either way `ring` closes ✓ (identities in the variable point). DL-4's hwid ended with `push_cast; ring` — theirs had the hw1 rewrite making forms differ. Mine is uniform — try `field_simp [hne]; ring`; if ring fails (e.g., goal has / leftover), adjust.\n\nActually — safer alternative avoiding field_simp entirely: prove hwid by direct algebra:\n```lean\n have hwid : w / (w - 1) = 1 + 1 / (w - 1) := by\n rw [show w / (w - 1) = (w - 1 + 1) / (w - 1) by ring_nf... ]\n```\nMeh — field_simp is standard here; DL-4 used it successfully at the same shape (line 807-813 with the same w/(w−1) = 1+1/(w−1) target — they rw [hw1] first because their RHS was in the (w−1)-as-↑(2√n−1) form; mine stays uniform). field_simp [hne] on `w/(w−1) = 1 + 1/(w−1)`: multiplies through by (w−1): `w = (w−1) + 1`?? — hmm, actually field_simp turns `1 + 1/(w−1)` into `((w−1) + 1)/(w−1)` and then cancels denominators: `w = (w−1) + 1` — ring ✓.\n\nv) `Real.exp_nat_mul` — DL-4 line 801: `(Real.exp_nat_mul _ n).symm` : (Real.exp x)^n = Real.exp (↑n * x)?? — the .symm direction: exp_nat_mul (x : ℝ) (n : ℕ) : Real.exp (↑n * x) = (Real.exp x)^n — .symm : (exp x)^n = exp(↑n*x) ✓ — DL-4's calc step `_ = Real.exp ((n:ℝ) * (1/(2√n)))` := (Real.exp_nat_mul _ n).symm ✓ — the `_` for x unified with 1/(2√n) ✓. Mine: same with 1/(2√n−1) ✓.\n\nw) `pow_le_pow_left₀` — signature: (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n ✓ DL-4 used ✓.\n\nx) norm_add_le — `norm_add_le (a b) : ‖a + b‖ ≤ ‖a‖ + ‖b‖` ✓ standard.\n\ny) `abs_of_nonneg h21.le` — h21 : 0 < 2√n−1 — h21.le : 0 ≤ ✓.\n\nz) `one_div_le_one_div_of_le h21 hnorm_w1` : 1/‖w−1‖ ≤ 1/(2√n−1) ✓.\n\nLet me also double-check `Jlag_norm_eq` applicability: Jlag_norm_eq (n) (s) : ‖Jlag n s‖ = ‖kFun n s‖ * ‖logDeriv riemannZeta s‖ ✓ used in hpt via rw [Jlag_norm_eq] — the goal ‖Jlag n (point)‖ ≤ K*L' → ‖kFun n (point)‖*‖logDeriv ζ (point)‖ ≤ K*L' ✓ then mul_le_mul ✓.\n\nAlright — also the file header §3 line: mark DONE after success. And the root-module doc comment — append 6-c-iii to the LiSideBounds bullet at the end.\n\nOne more consideration — hexp's show-rw: `(√n/2 + 1/3) * (2√n − 1) = √n^2 + √n/6 − 1/3` — verify by hand: (√n/2)(2√n) = √n². (√n/2)(−1) = −√n/2. (1/3)(2√n) = 2√n/3. (1/3)(−1) = −1/3. Total: √n² + √n(−1/2 + 2/3) − 1/3 = √n² + √n/6 − 1/3 ✓. ring proves ✓.\n\nThen `rw [..., hsqn]` — hsqn : √n^2 = ↑n — rewrites √n^2 → ↑n ✓ goal: ↑n ≤ ↑n + √n/6 − 1/3 — linarith [hsq2] : √n ≥ 2 ⟹ √n/6 ≥ 1/3 ✓ closes ✓.\n\nWait — CAREFUL: rw [hsqn] rewrites `√n^2` — but the goal ALSO has √n/6 — different pattern (√n not √n^2) ✓ only the square rewrites ✓.\n\nAlso — `mul_one_div` : a * (1/b) = a/b ✓ — the goal LHS (n:ℝ) * (1/(2√n−1)) → (n:ℝ)/(2√n−1) ✓ then div_le_iff₀ h21 ✓.\n\nNow write §3. Also update the header comment §3 to DONE after build success, and extend the root-module doc bullet. Let me write the code now.","signature":""},{"type":"text","text":"All templates and signatures confirmed. Writing §3 (6-c-iii) — the F-E kernel lemma + the I_I bound."},{"type":"tool_use","id":"Edit_75","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSideBounds.lean","old_string":" _ ≤ 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 := by\n linarith [htailInt, hmidInt, hnn, hlognn]\n\nend NguyenRH1","new_string":" _ ≤ 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 := by\n linarith [htailInt, hmidInt, hnn, hlognn]\n\n/-! ## 3. 6-c-iii: I_I — the right vertical σ₁ = 2√n (F-E form) -/\n\n/-- **The F-E kernel lemma** (D-074 §9): the uniform-in-t kernel bound at\nthe right vertical σ = 2√n — ‖kFun n (2√n+it)‖ ≤ e^{√n/2+1/3}+1 for n ≥ 4.\nThe honest charge: |w/(w−1)| = |1+1/(w−1)| ≤ 1 + 1/‖w−1‖ ≤ 1 + 1/(2√n−1)\n(plain triangle + ‖w−1‖ ≥ re(w−1) = 2√n−1 — the worst case is t = 0,\nrepairing the off-by-one of the t² ≥ n / re ≥ 2√n+1 variants), then\n(1+1/(2√n−1))ⁿ ≤ exp(n/(2√n−1)) ≤ exp(√n/2+1/3) ⟺ n ≥ 4. -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_add_third {n : ℕ} (hn : 4 ≤ n)\n (t : ℝ) :\n ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by\n have hnR : (4 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hsq2 : (2 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have h21 : (0 : ℝ) < 2 * Real.sqrt (n : ℝ) - 1 := by nlinarith [hsq2]\n have hsqn : Real.sqrt (n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt (by linarith)\n -- w − 1 ≠ 0 and ‖w − 1‖ ≥ 2√n − 1\n have hre : ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1).re =\n 2 * Real.sqrt (n : ℝ) - 1 := by\n simp [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.mul_re,\n Complex.I_re, Complex.I_im, Complex.one_re]\n have hne : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1 ≠ 0 := by\n intro h\n have h0 : ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1).re = 0 := by\n rw [h]; simp\n rw [hre] at h0\n nlinarith [h21]\n have hnorm_w1 : 2 * Real.sqrt (n : ℝ) - 1 ≤\n ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ := by\n have h1 := abs_re_le_norm ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)\n rw [hre, abs_of_nonneg h21.le] at h1\n exact h1\n -- the base bound ‖1 + 1/(w−1)‖ ≤ 1 + 1/(2√n−1)\n have hinv : 1 / ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ ≤\n 1 / (2 * Real.sqrt (n : ℝ) - 1) :=\n one_div_le_one_div_of_le h21 hnorm_w1\n have hbase : ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ≤\n 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by\n calc ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖\n ≤ ‖(1 : ℂ)‖ + ‖1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ :=\n norm_add_le _ _\n _ = 1 + 1 / ‖(((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1‖ := by\n rw [norm_one, norm_div, norm_one]\n _ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by linarith [hinv]\n have hbasepos : (0 : ℝ) ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ) - 1) := by positivity\n -- the power + exp chain: (1+1/(2√n−1))ⁿ ≤ exp(n/(2√n−1)) ≤ exp(√n/2+1/3)\n have hexp : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1)) ≤\n Real.sqrt (n : ℝ) / 2 + 1 / 3 := by\n rw [mul_one_div, div_le_iff₀ h21,\n show (Real.sqrt (n : ℝ) / 2 + 1 / 3) * (2 * Real.sqrt (n : ℝ) - 1) =\n Real.sqrt (n : ℝ) ^ 2 + Real.sqrt (n : ℝ) / 6 - 1 / 3 := by ring, hsqn]\n linarith [hsq2]\n have hpow : (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n ≤\n Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) := by\n calc (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n\n ≤ (Real.exp (1 / (2 * Real.sqrt (n : ℝ) - 1))) ^ n :=\n pow_le_pow_left₀ hbasepos (Real.add_one_le_exp _) n\n _ = Real.exp ((n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ) - 1))) :=\n (Real.exp_nat_mul _ n).symm\n _ ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) := Real.exp_le_exp.mpr hexp\n have hpow1 : ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ^ n ≤\n (1 + 1 / (2 * Real.sqrt (n : ℝ) - 1)) ^ n :=\n pow_le_pow_left₀ (norm_nonneg _) hbase n\n have hwid : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) /\n ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) =\n 1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) := by\n field_simp [hne]\n ring\n unfold kFun\n rw [hwid]\n calc ‖(1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)) ^ n - 1‖\n ≤ ‖(1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)) ^ n‖ +\n ‖(1 : ℂ)‖ := norm_sub_le _ _\n _ = ‖1 + 1 / ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1)‖ ^ n + 1 := by\n rw [norm_pow, norm_one]\n _ ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by\n linarith [hpow1.trans hpow]\n\n/-- **6-c-iii (I_I, the right vertical σ₁ = 2√n, F-E form)**: the full-side\nbound ‖V‖ ≤ e^{1/3}·IIMaj(n). The F-E kernel (uniform in t) + the DL-6\ndirect Dirichlet bound ‖ζ′/ζ‖ ≤ 0.57·2^{−(2√n−2)}; the comparison\ne^{√n/2+1/3}+1 ≤ e^{1/3}(e^{√n/2}+1) holds since 1 ≤ e^{1/3}. -/\ntheorem vIntegral_Jlag_right_le_exp_third_IIMaj {n : ℕ} (hn : 100000 ≤ n)\n {T : ℝ} (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖ ≤\n Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := by\n have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hn4 : 4 ≤ n := by omega\n have hn5 : 5 ≤ n := by omega\n have hsq2 : (2 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have hT0 : (0 : ℝ) ≤ T := by\n have h := Real.sqrt_nonneg (n : ℝ)\n linarith\n have hTT : -T ≤ T := by linarith\n -- zero-freeness + continuity on the right vertical (re = 2√n > 1)\n have hzne : ∀ t : ℝ,\n riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) ≠ 0 := by\n intro t\n have hre : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I).re =\n 2 * Real.sqrt (n : ℝ) := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im]\n have h1 : (1 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by nlinarith [hsq2]\n exact riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)\n have hJcont : ∀ t : ℝ, ContinuousAt (Jlag n)\n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by\n intro t\n have hs1 : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) ≠ 1 := by\n intro h\n have hre := congrArg Complex.re h\n simp at hre\n nlinarith [hsq2]\n have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n have hB := continuousAt_logDeriv_zeta hs1 (hzne t)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hpath : Continuous fun u : ℝ =>\n (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I) := by fun_prop\n have hcontJ : Continuous fun t : ℝ =>\n Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro t\n have hf : ContinuousAt (fun u : ℝ =>\n (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) t := hpath.continuousAt\n have hcomp : ContinuousAt\n (Jlag n ∘ fun u : ℝ => (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) t :=\n ContinuousAt.comp (g := Jlag n)\n (f := fun u : ℝ => (((2 * Real.sqrt (n : ℝ)) : ℝ) + u * Complex.I)) (x := t)\n (hJcont t) hf\n exact hcomp\n have hcontG : Continuous fun t : ℝ =>\n ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=\n continuous_norm.comp hcontJ\n have hI2 : IntervalIntegrable\n (fun t : ℝ => ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖)\n MeasureTheory.volume (-T) T := hcontG.intervalIntegrable _ _\n -- the comparison e^{√n/2+1/3}+1 ≤ e^{1/3}(e^{√n/2}+1) (since 1 ≤ e^{1/3})\n have hKle : Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 ≤\n Real.exp (1 / 3 : ℝ) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) := by\n rw [Real.exp_add]\n have h1 : (1 : ℝ) ≤ Real.exp (1 / 3 : ℝ) := by\n have h := Real.add_one_le_exp (1 / 3 : ℝ)\n linarith\n have hE := Real.exp_pos (Real.sqrt (n : ℝ) / 2)\n nlinarith [h1, hE]\n -- the pointwise bound\n have hK' : (0 : ℝ) ≤ Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1 := by positivity\n have hL : (0 : ℝ) ≤ (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by\n positivity\n have hpt : ∀ t : ℝ, t ∈ Set.Icc (-T) T →\n ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by\n intro t _\n rw [Jlag_norm_eq]\n exact mul_le_mul (kFun_right_vertical_norm_le_exp_sqrt_add_third hn4 t)\n (norm_logDeriv_zeta_le_iimZeta hn5) (norm_nonneg _) hK'\n have hInt : ∫ t in (-T)..T,\n ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n (T - -T) * ((Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := by\n have h := intervalIntegral.integral_mono_on hTT hI2 intervalIntegrable_const\n (fun t ht => hpt t ht)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n -- the final comparison 2T·K·L ≤ e^{1/3}·IIMaj (T ≤ √n+1, hKle)\n have hKL : (0 : ℝ) ≤ (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) :=\n mul_nonneg hK' hL\n have hnL : (0 : ℝ) ≤ 2 * (Real.sqrt (n : ℝ) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by\n have h1 : (0 : ℝ) ≤ Real.sqrt (n : ℝ) + 1 := by positivity\n exact mul_nonneg (mul_nonneg (by norm_num) h1) hL\n have hfinal : 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) ≤\n Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := by\n unfold IIMaj\n nlinarith [hTn1, hKle, hKL, hnL, Real.exp_pos (1 / 3 : ℝ),\n Real.exp_pos (Real.sqrt (n : ℝ) / 2)]\n calc ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) (-T) T‖\n = ‖∫ t in (-T)..T, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=\n VIntegral_norm\n _ ≤ ∫ t in (-T)..T, ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ :=\n intervalIntegral.norm_integral_le_integral_norm hTT\n _ ≤ (T - -T) * ((Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) := hInt\n _ = 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring\n _ ≤ Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := hfinal\n\nend NguyenRH1"},"extra_content":null}]