← Session 29 — ii′-5e-v: circle bound (far-tail + series bounds)
thinking (11149 chars)
Now c-iii: `logDeriv_circle_le` + `Fexpr_circle_le`.
**logDeriv_circle_le** design:
```
theorem logDeriv_circle_le {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}
(hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R)
(hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →
1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)
(hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|)
{s : ℂ} (hs : ‖s‖ = R) (hsz : ¬ IsNontrivialZero s) :
‖logDeriv riemannZeta s‖ ≤ dirichletC2 +
200000 * (Real.log R) ^ 2 + 192 * C0hat (4 * (k : ℝ) + 9 / 2) * A0count * (Real.log R) ^ 2 +
100 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2
```
Hmm — let me simplify the RHS form: dirichletC2 + 200000·L² + 300·Ĉ₀·A₀·L² (folding 192+100 → 300). Regions:
(i) 2 ≤ re s: Dirichlet: ‖logDeriv ζ‖ ≤ dirichletC2 ≤ RHS ✓ (rest nonneg).
(ii) −5/2 ≤ re s ∧ re s ≤ 2: |t| ≥ 10 (auto): capstones + near:
‖logDeriv ζ s‖ ≤ ‖logDeriv ζ s − near‖ + ‖near‖ ≤ 200000·(log|t|)² + ‖near‖.
near: ‖Σ_{ρ ∈ nearZeros t} m/(s−ρ)‖ ≤ Σ ‖m/(s−ρ)‖ = Σ m/‖s−ρ‖ ≤ 32Ĉ₀·(Σ m) ≤ 32Ĉ₀·3A₀·log(3·max|t−1||t+1|+5) ≤ 96·Ĉ₀·A₀·2L = 192·Ĉ₀·A₀·L ≤ 192·Ĉ₀·A₀·L².
log|t| ≤ log R (|t| ≤ R).
Sub-split re ≥ 1/2 (5c: 100000) vs re < 1/2 (5d-left: 200000) — uniform 200000.
Note: the capstones need t = s.im (hsim : s.im = t ✓ rfl with t := s.im) and ζ s ≠ 0 (hsz via... ζ s ≠ 0 ⟸ hsz + re ≥ 1? NO — the capstone takes (hs0 : riemannZeta s ≠ 0): ζ s ≠ 0 from hsz (s not a nontrivial zero) + re s ≥ −5/2: if ζ s = 0: zeta_zero_classification: nontrivial (hsz ✗), 0 (‖s‖ = R > 0 ✗), −2n (re s ≥ −5/2 > −4: −2n with n ≥ 1: −2n ≤ −2: possible for re s ∈ [−5/2, −2]: −2n = −2: s = −2: re = −2 ∈ [−5/2, 2] ✓ POSSIBLE — need to exclude s = −2: ‖s‖ = R ≥ 16002 ≠ 2 ✓ trivially! ‖(−2:ℂ)‖ = 2 ≠ R ✓.) So ζ s ≠ 0 ✓.
(iii) re s < −5/2: the FE route:
logDeriv ζ s = −logDeriv ζ(1−s) − (logDeriv ΓR s + logDeriv ΓR(1−s)) via logDeriv_zeta_fe — the 10 hypotheses:
- hs0' : s ≠ 0 (‖s‖ = R > 0: s = 0 ⟹ ‖s‖ = 0 ✗).
- hs1' : s ≠ 1 (re < −5/2 < 1: s = 1 ⟹ re = 1 ✗).
- hG : Gammaℝ s ≠ 0: rw [ne_eq, Complex.Gammaℝ_eq_zero_iff]; rintro ⟨m, hm⟩: s = −2m: s/2 = −m: contradiction with the pole-avoidance hpoles (below).
- hζ : ζ s ≠ 0: zeta_zero_classification: nontrivial ✗ (hsz); 0 ✗; −2n: s = −2n: s/2 = −n: hpoles ✗.
- hd : DifferentiableAt Gammaℝ s := differentiableAt_Gammaℝ_of_not_neg_nat hpoles.
- hpoles : ∀ m : ℕ, s / 2 ≠ -(m : ℂ): split im s = 0 vs ≠ 0:
- im s ≠ 0: (s/2).im ≠ 0 ⟹ s/2 ≠ −(m:ℂ) (real) ✓.
- im s = 0: s = re s = −R?? wait — im s = 0 and ‖s‖ = R and re s < −5/2: s = −R (s real, |s| = R, re < 0): (s/2) = −R/2: −R/2 = −m ⟺ R/2 = m: |R/2 − m| = 0 < 1/4 contradicts hgapInt (m : ℤ) ✓.
- at 1−s: 1−s ≠ 0 (s ≠ 1 ✓); 1−s ≠ 1 (s ≠ 0 ✓); Gammaℝ(1−s) ≠ 0: (1−s)/2 ∉ −ℕ: re((1−s)/2) = (1−re s)/2 > (1+5/2)/2 = 1.75 > 0 ⟹ ≠ −m ✓ (re(−m) = −m ≤ 0 ✗); ζ(1−s) ≠ 0: re(1−s) = 1−re s > 1+5/2 > 1: riemannZeta_ne_zero_of_one_le_re (1 ≤ re(1−s)) (1−s ≠ 1) ✓; DifferentiableAt Gammaℝ(1−s): differentiableAt_Gammaℝ_of_not_neg_nat ((1−s)/2 ∉ −ℕ ✓).
Then:
‖logDeriv ζ s‖ = ‖−logDeriv ζ(1−s) − (bracket)‖ ≤ ‖logDeriv ζ(1−s)‖ + ‖bracket‖ ≤ dirichletC2 + ‖bracket‖ (re(1−s) ≥ 7/2 ≥ 2: Dirichlet ✓).
bracket := logDeriv ΓR s + logDeriv ΓR(1−s) = −(logπ)/2 + ½ψ(s/2) + (−(logπ)/2 + ½ψ((1−s)/2)) via logDeriv_Gammaℝ_eq_of_not_neg_nat (s/2 ∉ −ℕ ✓ hpoles; (1−s)/2 ∉ −ℕ ✓).
‖bracket‖ ≤ log π + ½(‖ψ(s/2)‖ + ‖ψ((1−s)/2)‖):
- ‖ψ(s/2)‖: two sub-cases: |im(s/2)| ≥ 5: sub-log: 3 + log‖s/2‖ + π ≤ 3 + log(R/2) + 3.15 ≤ 7 + log(R/2) ≤ 62+23·log(2+R/2)·... hmm just bound ≤ 62 + 23·log(2+R/2) uniformly via digamma_circle_le! I have digamma_circle_le (hgapInt) already — use it directly for ALL s ✓: ‖ψ(s/2)‖ ≤ 62 + 23·log(2+R/2) ✓.
- ‖ψ((1−s)/2)‖: re((1−s)/2) = (1−re s)/2 > 1.75: digamma_right_le: ≤ 48 + 23·log(2+‖(1−s)/2‖): ‖(1−s)/2‖ = ‖1−s‖/2 ≤ (1+R)/2: log(2+‖(1−s)/2‖) ≤ log(2+(1+R)/2) ≤ log(2+R) hmm: 2+(1+R)/2 = (5+R)/2 ≤ R ⟺ 5 ≤ R ✓: ≤ log R = L... or just ≤ log(2+R) ≤ log(2R) = log2+L ≤ 1+L. Let me use log(2+(1+R)/2) ≤ L: 2+(1+R)/2 ≤ R ⟺ 5 ≤ R ✓ so log ≤ L ✓. So ‖ψ((1−s)/2)‖ ≤ 48 + 23·L.
bracket ≤ 2 + ½(62+23·log(2+R/2)) + ½(48+23·L) ≤ 2 + 31+11.5·L + 24+11.5·L = 57+23L (log(2+R/2) ≤ L ✓ (2+R/2 ≤ R ⟺ 4 ≤ R)).
So case (iii): ‖logDeriv ζ‖ ≤ dirichletC2 + 57 + 23·L.
Absorb 57+23L ≤ 100·A₀·Ĉ₀·L² ✓ (A₀ ≥ 1, Ĉ₀ ≥ 2, L ≥ 9: 57 ≤ 57·... 100·A₀Ĉ₀L² ≥ 100·2·81 = 16200 ≥ 57+23L ⟸ 23L ≤ 23·A₀Ĉ₀L² ✓ 57 ≤ 57·A₀Ĉ₀L²/(162)·... 57 ≤ 57/162·A₀Ĉ₀L² ≤ A₀Ĉ₀L²: total ≤ (57/162 + 23)·A₀Ĉ₀L² ≤ 24·A₀Ĉ₀L² ≤ 100·A₀Ĉ₀L² ✓).
So uniform: ‖logDeriv ζ s‖ ≤ dirichletC2 + max(0, 200000L² + 192Ĉ₀A₀L², 100A₀Ĉ₀L²) — final RHS: dirichletC2 + 200000·L² + 300·A₀·Ĉ₀·L² ✓ (192 ≤ 300, 100 ≤ 300, and region (i) needs just dirichletC2 ≤ RHS ✓ with the others nonneg).
**Fexpr_circle_le**:
```
theorem Fexpr_circle_le {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}
(hRlo : 4*(k:ℝ)+5/2 ≤ R) (hRhi : R ≤ 4*(k:ℝ)+3)
(hgap : ...) (hgapInt : ∀ m : ℤ, 1/4 ≤ |R/2 − (m:ℝ)|)
{s : ℂ} (hs : ‖s‖ = R) :
‖Fexpr s‖ ≤ 2 * lowZeroConst + dirichletC2 +
400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2
```
Assembly: unfold Fexpr: Fexpr s = logDeriv ζ s − seriesFun s + 1/s + 1/(s−1) − (logπ:ℂ)/2 + digamma (s/2)/2.
norm chain:
‖Fexpr s‖ ≤ ‖logDeriv ζ s‖ + ‖seriesFun s‖ + ‖1/s‖ + ‖1/(s−1)‖ + ‖(logπ)/2‖ + ‖digamma (s/2)/2‖.
Via successive: ‖a − b + c + d − e + f‖ ≤ ...:
‖X − seriesFun + Y‖ ≤ ‖X − seriesFun‖ + ‖Y‖ (norm_add_le) hmm — the expression structure: ((((logDeriv − seriesFun) + 1/s) + 1/(s−1)) − c) + ψ: norm ≤ ‖(((logDeriv − seriesFun) + 1/s) + 1/(s−1)) − c‖ + ‖ψ‖ ≤ ‖((logDeriv − seriesFun) + 1/s) + 1/(s−1)‖ + ‖c‖ + ‖ψ‖ ≤ ... chain of norm_add_le/norm_sub_le. ~6 lines.
Pieces:
- hsz := not_isNontrivialZero_on_gapCircle hk hRlo hgap hs.
- ‖seriesFun s‖ ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(4k+9/2)·L² ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(R+2)·L² (C0hat_mono: 4k+9/2 ≤ R+2 ⟺ 4k+5/2 ≤ R ✓ hRlo; mono needs 1 ≤ 4k+9/2 ✓).
- ‖logDeriv ζ s‖ ≤ dirichletC2 + 200000·L² + 300·A₀·Ĉ₀(4k+9/2)·L² ≤ dirichletC2 + 200000·L² + 300·A₀·Ĉ₀(R+2)·L².
- ψ-elem: ‖digamma (s/2)/2‖ = ‖digamma (s/2)‖/2 ≤ (62+23·log(2+R/2))/2 ≤ 31+12·L ≤ 13·A₀Ĉ₀(R+2)L² (absorbed as computed).
- 1/s + 1/(s−1) ≤ 2 ≤ (2/162)·A₀Ĉ₀L² ≤ A₀Ĉ₀L².
- ‖(logπ)/2‖ ≤ 1 ≤ A₀Ĉ₀L².
- 200000·L² ≤ 100000·A₀Ĉ₀L² (A₀Ĉ₀ ≥ 2).
Total: 2·lowZeroConst + dirichletC2 + [2900 + 300 + 13 + 1 + 1 + 100000]·A₀Ĉ₀(R+2)L² = 2·lowZeroConst + dirichletC2 + 103215·A₀Ĉ₀(R+2)L² ≤ 400000·... ✓.
Let me now write c-iii. First logDeriv_circle_le with the three regions. The region (ii) |t| ≥ 10: re s ∈ [−5/2, 2] ⟹ re² ≤ 25/4: im² = R²−re² ≥ R²−25/4: |im| ≥ 10: from R−|im| = re²/(R+|im|) ≤ (25/4)/R: |im| ≥ R−25/(4R) ≥ 10 ⟺ 25/(4R) ≤ R−10 ⟸ R ≥ 16002: linarith: 25/(4R) ≤ 1 ≤ R−10·... 25/(4R) = 6.25/R ≤ 6.25/16002 < 1 ≤ R−10·... R−10 ≥ 15992 ≥ 1 > 25/(4R)·... need |im| ≥ R − 25/(4R) ≥ 10: R − 25/(4R) ≥ 10 ⟺ R − 10 ≥ 25/(4R) ⟸ 25/(4R) ≤ 25/(4·16002) = 0.0004 ≤ 15992 ≤ R−10 ✓.
The norm_circle_sub_abs_im_le gives R−|im| ≤ B/R with B := 25/4 (re² ≤ 25/4 ✓): R−|im| ≤ (25/4)/R: |im| ≥ R−(25/4)/R ≥ 10 ✓ linarith.
For region (ii)'s near-sum:
```
have hnear : ‖∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖
≤ 32 * C0hat (4*(k:ℝ)+9/2) * (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) := by
calc ‖∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖
≤ ∑ ρ ∈ nearZeros s.im, ‖(zeroMult ρ : ℂ) / (s - ρ)‖ := norm_sum_le _ _
_ = ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) / ‖s - ρ‖ := by
apply Finset.sum_congr rfl
intro ρ hρ
rw [norm_div, RCLike.norm_natCast]
_ ≤ ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) * (32 * C0hat (4*(k:ℝ)+9/2)) := by
apply Finset.sum_le_sum
intro ρ hρ
have hsep := gapCircle_sep_of_mem_nearZeros hk hRlo hgap hs hρ
-- m/‖s−ρ‖ ≤ m·(32Ĉ₀) ⟸ 1/‖s−ρ‖ ≤ 32Ĉ₀ ⟸ 1/(32Ĉ₀) ≤ ‖s−ρ‖
rw [show (zeroMult ρ : ℝ) / ‖s - ρ‖ = (zeroMult ρ : ℝ) * (1 / ‖s - ρ‖) from by ring]
rw [show (zeroMult ρ : ℝ) * (32 * C0hat (4*(k:ℝ)+9/2)) = (zeroMult ρ : ℝ) * (32 * C0hat (4*(k:ℝ)+9/2)) from rfl]
apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
-- 1/‖s−ρ‖ ≤ 32Ĉ₀ ⟺ 1/(32Ĉ₀) ≤ ‖s−ρ‖ (via one_div_le_one_div_of_le with positive)
have h1 : (0 : ℝ) < 1 / (32 * C0hat (4*(k:ℝ)+9/2)) := by positivity
have h2 : (0 : ℝ) < ‖s - ρ‖ := by linarith [hsep, h1]
rw [one_div_le_one_div_of_le h2 hsep] -- hmm: one_div_le_one_div_of_le (ha : 0 < a) (hb : a ≤ b) : 1/b ≤ 1/a
-- goal after: 1/‖s−ρ‖ ≤ 32·Ĉ₀ = 1/(1/(32Ĉ₀)): one_div_le_one_div_of_le h2 hsep : 1/‖s−ρ‖ ≤ 1/(1/(32Ĉ₀)): then 1/(1/(32Ĉ₀)) = 32Ĉ₀ (one_div_one_div)
have h3 : 1 / (1 / (32 * C0hat (4*(k:ℝ)+9/2))) = 32 * C0hat (4*(k:ℝ)+9/2) := one_div_one_div _
rw [h3] at * — hmm careful; do:
exact (one_div_le_one_div_of_le h2 hsep).trans_eq (one_div_one_div _)
_ = (32 * C0hat (4*(k:ℝ)+9/2)) * ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) := by
rw [Finset.mul_sum] -- hmm: Σ m·(32Ĉ₀) = (32Ĉ₀)·Σm: mul_comm forms: m·c = c·m: sum_congr (mul_comm) then mul_sum
_ ≤ (32 * C0hat (4*(k:ℝ)+9/2)) * (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) :=
mul_le_mul_of_nonneg_left nearZeros_count_le (by positivity)
_ = 32 * C0hat (4*(k:ℝ)+9/2) * (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) := rfl
```
The sum_congr for m·c = c·m: `Finset.sum_congr rfl (fun ρ hρ => mul_comm _ _)`.
Hmm — norm_sum_le : ‖∑ x ∈ s, f x‖ ≤ ∑ x ∈ s, ‖f x‖ — `norm_sum_le (s : Finset ι) (f : ι → α) : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖` ✓.
The capstone application:
```
have hcap : ‖logDeriv riemannZeta s - ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖
≤ 200000 * (Real.log |s.im|) ^ 2 := by
by_cases hhalf : (1 : ℝ) / 2 ≤ s.re
· have h := logDeriv_riemannZeta_sub_nearZeros_le (t := s.im) ht10 rfl hhalf (by linarith [hσ2] : s.re ≤ 7/2) hζs
exact h.trans (by ...)
· push Not at hhalf
have h := logDeriv_riemannZeta_sub_nearZeros_le_left (t := s.im) ht10 rfl (by linarith [hσ25]) (by linarith [hhalf] : s.re ≤ 1/2) hζs
exact h
```
with ht10 : 10 ≤ |s.im|, hζs : riemannZeta s ≠ 0, hσ25 : −5/2 ≤ s.re, hσ2 : s.re ≤ 2.
Then region (ii) final:
```
calc ‖logDeriv riemannZeta s‖
≤ ‖logDeriv riemannZeta s - ∑ ...‖ + ‖∑ ...‖ := by
have h1 : logDeriv riemannZeta s = (logDeriv riemannZeta s - ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)) + ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ) := by rw [sub_add_cancel]
rw [h1]
exact norm_add_le _ _
_ ≤ 200000 * (Real.log |s.im|) ^ 2 + (32·Ĉ₀·3A₀·log(...)) := add_le_add hcap hnear
_ ≤ 200000 * (Real.log R) ^ 2 + 192·Ĉ₀·A₀·L² := ...
```
log|s.im| ≤ log R (|s.im| ≤ R ✓ abs_im_le_norm+hs; log mono, |s.im| ≥ 10 > 0): (Real.log |s.im|)^2 ≤ (Real.log R)^2: both ≥ 0: pow_le_pow_left₀ (Real.log_nonneg (|s.im| ≥ 10 ≥ 1)) (log|s.im| ≤ log R) 2 ✓.
And 32Ĉ₀·3A₀·log(3·max|t−1||t+1|+5) ≤ 192·Ĉ₀·A₀·L: max|t−1||t+1| = |t|+1 ≤ R+1: log(3(R+1)+5) = log(3R+8) ≤ log(4R) ≤ 2L ⟸ 8 ≤ R and log 4 ≤ L ✓. 32·3 = 96: 96Ĉ₀A₀·2L = 192Ĉ₀A₀L ≤ 192Ĉ₀A₀L² (L ≥ 1).
Region (i) is trivial (Dirichlet + nonneg RHS parts).
Region (iii): the FE identity + bracket bound — biggest single block (~150 lines).
Then Fexpr_circle_le (~80 lines).
Let me write logDeriv_circle_le first.
Committed. Now c-iii: `logDeriv_circle_le` (three regions) — writing the region structure.
tool: Edit
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
"old_string": "end NguyenRH1\n\nend",
"new_string": "/-! ## 12. The logDeriv circle bound and the Fexpr assembly (5e-v-c-iii)\n\n`logDeriv_circle_le`: three regions \u2014 (i) re s \u2265 2: the Dirichlet\nbound; (ii) re s \u2208 [\u22125/2, 2] (automatically |im s| \u2265 10): the 5c/5d\ncapstones + the near sum \u2264 32\u00b7\u0108\u2080\u00b7(near count); (iii) re s < \u22125/2: the\nFE identity `logDeriv_zeta_fe` + Dirichlet at 1\u2212s + the \u0393R bracket\nvia `logDeriv_Gamma\u211d_eq_of_not_neg_nat` (which also discharges the\nreal point s = \u2212R). Uniform:\n\u2016logDeriv \u03b6 s\u2016 \u2264 dirichletC2 + 200000\u00b7(log R)\u00b2 + 300\u00b7A\u2080\u00b7\u0108\u2080\u00b7(log R)\u00b2.\n\n`Fexpr_circle_le`: \u2016Fexpr s\u2016 \u2264 2\u00b7lowZeroConst + dirichletC2 +\n400000\u00b7A\u2080\u00b7\u0108\u2080(R+2)\u00b7(log R)\u00b2. -/\n\n/-- **The logDeriv bound on the gap circle.** -/\ntheorem logDeriv_circle_le {k : \u2115} (hk : 4000 \u2264 k) {R : \u211d}\n (hRlo : 4 * (k : \u211d) + 5 / 2 \u2264 R)\n (hgap : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192\n 1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2)) \u2264 |\u03c1.im - R| \u2228 1 \u2264 |\u03c1.im - R|)\n (hgapInt : \u2200 m : \u2124, 1 / 4 \u2264 |R / 2 - (m : \u211d)|)\n {s : \u2102} (hs : \u2016s\u2016 = R) (hsz : \u00ac IsNontrivialZero s) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC2 +\n 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n classical\n have h\u01082 : (2 : \u211d) \u2264 C0hat (4 * (k : \u211d) + 9 / 2) := two_le_C0hat (by\n have hkR : (1 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast (by omega : 1 \u2264 k)\n linarith)\n have hR : (16002 : \u211d) \u2264 R := by\n have hkR : (16000 : \u211d) \u2264 4 * (k : \u211d) := by\n have h1 : (4000 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk\n linarith\n linarith [hRlo]\n have hRpos : (0 : \u211d) < R := by linarith [hR]\n have hlogR : (9 : \u211d) \u2264 Real.log R := nine_le_log_of_16002_le hR\n have hlogRnn : (0 : \u211d) \u2264 Real.log R := by linarith [hlogR]\n have hA0 := A0count_pos.le\n have h\u0108pos : (0 : \u211d) < C0hat (4 * (k : \u211d) + 9 / 2) := by linarith [h\u01082]\n have hnnR : (0 : \u211d) \u2264 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n apply add_nonneg (mul_nonneg (by norm_num) (pow_two_nonneg _))\n exact mul_nonneg (mul_nonneg (by norm_num) hA0)\n (mul_nonneg h\u0108pos.le (pow_two_nonneg _))\n -- \u03b6 s \u2260 0 on the whole circle\n have h\u03b6s : riemannZeta s \u2260 0 := by\n intro h\n rcases zeta_zero_classification h with hn | h0 | \u27e8n, hn, h2n\u27e9\n \u00b7 exact hsz hn\n \u00b7 rw [h0, norm_zero] at hs\n linarith [hs, hR]\n \u00b7 have hnorm2 : \u2016(-2 : \u2102) * (n : \u2102)\u2016 \u2264 2 * (n : \u211d) := by\n rw [\u2190 h2n]\n have h1 : \u2016(-2 : \u2102)\u2016 = 2 := by\n rw [show (-2 : \u2102) = ((-2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [norm_mul, h1, Complex.norm_natCast]\n rw [\u2190 h2n] at hnorm2\n have hR2 : R \u2264 2 * (n : \u211d) := by rw [\u2190 hs]; exact hnorm2\n have hre : (-2 : \u211d) < -5 / 2 \u2192 False := by norm_num\n by_cases hcase : 2 \u2264 s.re\n \u00b7 exact absurd h rfl hsz\n \u00b7 push Not at hcase\n by_cases hcase2 : -5 / 2 \u2264 s.re\n \u00b7 -- s = \u22122n with re \u2208 [\u22125/2, 2]: n = 1, s = \u22122: \u2016s\u2016 = 2 < R\n have hn1 : n = 1 := by\n have hre2 : s.re = -2 * (n : \u211d) := by\n rw [h2n]\n simp [Complex.mul_re, Complex.natCast_re, Complex.ofReal_re]\n have hnn : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hbound : -5 / 2 \u2264 -2 * (n : \u211d) \u2227 -2 * (n : \u211d) \u2264 2 := by\n rw [\u2190 hre2]\n exact \u27e8hcase2, hcase\u27e9\n have h1 : (n : \u211d) < 2 := by linarith [hbound]\n have h2 : (n : \u211d) \u2264 1 := by linarith [h1]\n have h3 : n \u2264 1 := by exact_mod_cast h2\n omega\n rw [hn1] at h2n\n have h4 : \u2016s\u2016 = 2 := by\n rw [h2n]\n rw [show (-2 : \u2102) * ((1 : \u2115) : \u2102) = ((-2 : \u211d) : \u2102) by push_cast; ring,\n Complex.norm_real]\n norm_num\n rw [hs] at h4\n linarith [h4, hR]\n \u00b7 push Not at hcase2\n exact absurd h rfl hsz\n -- the three regions\n by_cases hreg1 : 2 \u2264 s.re\n \u00b7 -- (i) the Dirichlet bound\n have h1 := norm_logDeriv_zeta_le_dirichlet hreg1\n linarith [h1, hnnR, dirichletC2_nonneg]\n \u00b7 push Not at hreg1\n by_cases hreg2 : -5 / 2 \u2264 s.re\n \u00b7 -- (ii) the capstones + the near sum\n have ht10 : (10 : \u211d) \u2264 |s.im| := by\n have hre25 : s.re ^ 2 \u2264 25 / 4 := by\n have h1 : -5 / 2 \u2264 s.re \u2227 s.re \u2264 2 := \u27e8hreg2, hreg1.le\u27e9\n nlinarith [sq_nonneg s.re]\n have hRt : R - |s.im| \u2264 (25 / 4) / R :=\n norm_circle_sub_abs_im_le hs hRpos hre25\n have h1 : (25 / 4 : \u211d) / R \u2264 1 := by\n rw [div_le_one hRpos]\n linarith [hR]\n have ht_le : |s.im| \u2264 R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n linarith [hRt, h1, ht_le, hR]\n -- the near sum\n have hnear : \u2016\u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u2102) / (s - \u03c1)\u2016\n \u2264 32 * C0hat (4 * (k : \u211d) + 9 / 2) *\n (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) := by\n calc \u2016\u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u2102) / (s - \u03c1)\u2016\n \u2264 \u2211 \u03c1 \u2208 nearZeros s.im, \u2016(zeroMult \u03c1 : \u2102) / (s - \u03c1)\u2016 := norm_sum_le _ _\n _ = \u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u211d) / \u2016s - \u03c1\u2016 := by\n apply Finset.sum_congr rfl\n intro \u03c1 h\u03c1\n rw [norm_div, RCLike.norm_natCast]\n _ \u2264 \u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u211d) * (32 * C0hat (4 * (k : \u211d) + 9 / 2)) := by\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n have hsep := gapCircle_sep_of_mem_nearZeros hk hRlo hgap hs h\u03c1\n rw [show (zeroMult \u03c1 : \u211d) / \u2016s - \u03c1\u2016 = (zeroMult \u03c1 : \u211d) * (1 / \u2016s - \u03c1\u2016) from by ring]\n apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n have h1 : (0 : \u211d) < 1 / (32 * C0hat (4 * (k : \u211d) + 9 / 2)) := by positivity\n have h2 : (0 : \u211d) < \u2016s - \u03c1\u2016 := by linarith [hsep, h1]\n exact (one_div_le_one_div_of_le h2 hsep).trans_eq (one_div_one_div _)\n _ = (32 * C0hat (4 * (k : \u211d) + 9 / 2)) * \u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u211d) := by\n rw [\u2190 Finset.sum_congr rfl (g := fun \u03c1 => (zeroMult \u03c1 : \u211d) *\n (32 * C0hat (4 * (k : \u211d) + 9 / 2))) (fun \u03c1 h\u03c1 => mul_comm _ _), Finset.mul_sum]\n _ \u2264 (32 * C0hat (4 * (k : \u211d) + 9 / 2)) *\n (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) :=\n mul_le_mul_of_nonneg_left nearZeros_count_le (by positivity)\n have hlogmax : Real.log (3 * max |s.im - 1| |s.im + 1| + 5) \u2264 2 * Real.log R := by\n have hmax : max |s.im - 1| |s.im + 1| = |s.im| + 1 := by\n have ht_le : |s.im| \u2264 R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n have h1 : |s.im + 1| \u2264 |s.im| + 1 := abs_add_le _ _\n have h2 : |s.im - 1| \u2264 |s.im| + 1 := by\n have h3 := abs_sub_le_iff.mp (abs_sub_abs_le_abs_sub s.im (-1 : \u211d))\n -- |s.im \u2212 1| \u2264 |s.im| + 1 via the triangle\n have h4 : s.im - 1 = s.im + (-1 : \u211d) := by ring\n rw [h4]\n exact abs_add_le _ _\n apply max_le_iff.mpr\n constructor\n \u00b7 exact h2\n \u00b7 exact h1\n all_goals try exact h1\n rw [hmax]\n have ht_le : |s.im| \u2264 R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n have h1 : Real.log (3 * (|s.im| + 1) + 5) \u2264 Real.log (4 * R) := by\n apply Real.log_le_log (by linarith [abs_nonneg s.im, hRpos])\n linarith [ht_le, hR]\n have h2 : Real.log (4 * R) = Real.log 4 + Real.log R :=\n Real.log_mul (by norm_num : (4 : \u211d) \u2260 0) (by linarith [hRpos] : R \u2260 0)\n have h3 : Real.log 4 \u2264 Real.log R :=\n Real.log_le_log (by norm_num) (by linarith [hR])\n linarith [h1, h2, h3]\n -- the capstone difference\n have hcap : \u2016logDeriv riemannZeta s - \u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u2102) / (s - \u03c1)\u2016\n \u2264 200000 * (Real.log |s.im|) ^ 2 := by\n by_cases hhalf : (1 : \u211d) / 2 \u2264 s.re\n \u00b7 exact logDeriv_riemannZeta_sub_nearZeros_le (t := s.im) ht10 rfl hhalf\n (by linarith [hreg1.le] : s.re \u2264 7 / 2) h\u03b6s\n \u00b7 push Not at hhalf\n exact logDeriv_riemannZeta_sub_nearZeros_le_left (t := s.im) ht10 rfl hreg2\n (by linarith [hhalf] : s.re \u2264 1 / 2) h\u03b6s\n have hlogt : (Real.log |s.im|) ^ 2 \u2264 (Real.log R) ^ 2 := by\n have ht_le : |s.im| \u2264 R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n have h1 : Real.log |s.im| \u2264 Real.log R :=\n Real.log_le_log (by linarith [ht10] : (0 : \u211d) < |s.im|) ht_le\n have h2 : (0 : \u211d) \u2264 Real.log |s.im| :=\n Real.log_nonneg (by linarith [ht10] : (1 : \u211d) \u2264 |s.im|)\n exact pow_le_pow_left\u2080 h2 h1 2\n calc \u2016logDeriv riemannZeta s\u2016\n = \u2016(logDeriv riemannZeta s - \u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u2102) / (s - \u03c1))\n + \u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u2102) / (s - \u03c1)\u2016 := by\n rw [sub_add_cancel]\n _ \u2264 \u2016logDeriv riemannZeta s - \u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u2102) / (s - \u03c1)\u2016\n + \u2016\u2211 \u03c1 \u2208 nearZeros s.im, (zeroMult \u03c1 : \u2102) / (s - \u03c1)\u2016 :=\n norm_add_le _ _\n _ \u2264 200000 * (Real.log |s.im|) ^ 2 +\n 32 * C0hat (4 * (k : \u211d) + 9 / 2) *\n (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) :=\n add_le_add hcap hnear\n _ \u2264 dirichletC2 + 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n have h1 : 32 * C0hat (4 * (k : \u211d) + 9 / 2) *\n (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5))\n \u2264 192 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n have h2 := mul_le_mul_of_nonneg_left hlogmax\n (mul_nonneg (mul_nonneg (by norm_num : (0 : \u211d) \u2264 32) h\u0108pos.le)\n (mul_nonneg (by norm_num : (0 : \u211d) \u2264 3) hA0))\n have h3 : 32 * C0hat (4 * (k : \u211d) + 9 / 2) * (3 * A0count * (2 * Real.log R))\n = 192 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * Real.log R := by ring\n have h4 : 192 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * Real.log R\n \u2264 192 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n apply mul_le_mul_of_nonneg_left _ (mul_nonneg (mul_nonneg (by norm_num) hA0) h\u0108pos.le)\n nlinarith [hlogR, hlogRnn]\n rw [h3] at h2\n exact h2.trans h4\n have h5 : 192 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2\n \u2264 300 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n apply mul_le_mul_of_nonneg_right _ (pow_two_nonneg _)\n apply mul_le_mul_of_nonneg_right _ h\u0108pos.le\n apply mul_le_mul_of_nonneg_right _ hA0\n norm_num\n nlinarith [hlogt, h1, h5, hlogRnn, dirichletC2_nonneg, pow_two_nonneg (Real.log R)]\n \u00b7 -- (iii) the FE route\n push Not at hreg2\n -- pole-avoidance for s/2\n have hpoles : \u2200 m : \u2115, s / 2 \u2260 -(m : \u2102) := by\n intro m hm\n by_cases him : s.im = 0\n \u00b7 -- s real: s = \u2212R, then R/2 = m contradicts the \u2124-clearance\n have hsR : s = (-R : \u211d) := by\n have hnormSq : \u2016s\u2016 ^ 2 = s.re ^ 2 + s.im ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n ring\n rw [him, hs] at hnormSq\n have h1 : s.re ^ 2 = R ^ 2 := by\n have h2 : s.re ^ 2 + (0 : \u211d) ^ 2 = R ^ 2 := by\n have h3 : s.re ^ 2 + s.im ^ 2 = R ^ 2 := hnormSq\n rw [him] at h3\n linarith [h3]\n linarith [h1, h2]\n have h4 : s.re = -R := by\n have h5 : s.re ^ 2 - R ^ 2 = 0 := by linarith [h1]\n have h6 : (s.re - R) * (s.re + R) = 0 := by\n have h7 : s.re ^ 2 - R ^ 2 = (s.re - R) * (s.re + R) := by ring\n rw [h7] at h5\n exact h5\n rcases mul_eq_zero.mp h6 with h8 | h8\n \u00b7 have h9 : s.re = R := by linarith [h8]\n linarith [h9, hreg2]\n \u00b7 linarith [h8]\n apply Complex.ext_iff.mpr\n rw [h4, him]\n simp\n rw [hsR] at hm\n have hm2 : (m : \u211d) = R / 2 := by\n have h1 : (-(R : \u211d) : \u2102) / 2 = -(m : \u2102) := hm\n have h2 : (-(R : \u211d) : \u2102) / 2 = ((-R / 2 : \u211d) : \u2102) := by push_cast; ring\n rw [h2] at h1\n have h3 : (-R / 2 : \u211d) = -(m : \u211d) := by exact_mod_cast h1\n have h4 : (m : \u211d) = R / 2 := by linarith [h3]\n exact h4\n have hgap' := hgapInt (m : \u2124)\n have hcast : ((m : \u2124) : \u211d) = (m : \u211d) := by push_cast; ring\n rw [hcast, \u2190 hm2] at hgap'\n rw [show R / 2 - R / 2 = (0 : \u211d) by ring, abs_zero] at hgap'\n norm_num at hgap'\n \u00b7 exact hm (by\n have h1 : (s / 2).im \u2260 0 := by\n have h2 : (s / 2).im = s.im / 2 := by simp\n rw [h2]\n exact div_ne_zero him (two_ne_zero : (2 : \u211d) \u2260 0)\n have h3 : (-(m : \u2102)).im = 0 := by\n rw [Complex.neg_im, Complex.natCast_im]\n have h4 : (s / 2).im = (-(m : \u2102)).im := congrArg Complex.im hm\n rw [h3] at h4\n exact h1 h4)\n -- the FE identity\n have hG : Complex.Gamma\u211d s \u2260 0 := by\n rw [ne_eq, Complex.Gamma\u211d_eq_zero_iff]\n rintro \u27e8m, hm\u27e9\n have h1 : s / 2 = -(m : \u2102) := by\n rw [hm]\n ring\n exact hpoles m h1\n have hG1 : Complex.Gamma\u211d (1 - s) \u2260 0 := by\n rw [ne_eq, Complex.Gamma\u211d_eq_zero_iff]\n rintro \u27e8m, hm\u27e9\n have hre : ((1 - s) / 2).re = -(m : \u211d) := by\n have h1 : (1 - s) / 2 = -2 * (m : \u2102) / 2 := by rw [hm]; ring\n have h2 : (1 - s) / 2 = -(m : \u2102) := by\n rw [hm]\n ring\n have h3 := congrArg Complex.re h2\n rw [Complex.neg_re, Complex.natCast_re] at h3\n rw [h3]\n simp\n have hpos : (0 : \u211d) < ((1 - s) / 2).re := by\n have h1 : ((1 - s) / 2).re = (1 - s.re) / 2 := by simp [Complex.div_re]\n rw [h1]\n linarith [hreg2]\n rw [hre] at hpos\n have hmn : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg _\n linarith [hpos, hmn]\n have h\u03b61 : riemannZeta (1 - s) \u2260 0 := by\n apply riemannZeta_ne_zero_of_one_le_re\n \u00b7 have h1 : (1 - s).re = 1 - s.re := by simp\n rw [h1]\n linarith [hreg2]\n \u00b7 intro h\n have h2 : s = 0 := by\n have h3 : 1 - s = 1 := h\n have h4 : 1 - s + s = 1 + s := by rw [h3]\n rw [sub_add_cancel] at h4\n rw [h4] at *\n exact h4.symm\n rw [h2, norm_zero] at hs\n linarith [hs, hR]\n have hfe := logDeriv_zeta_fe (fun h => by rw [h, norm_zero] at hs; linarith [hs, hR])\n (fun h => by\n have h1 : s.re = 1 := by rw [h]; simp\n linarith [h1, hreg2])\n hG h\u03b6s (differentiableAt_Gamma\u211d_of_not_neg_nat hpoles)\n (fun h => by\n have h1 : (1 - s) = 0 \u2192 s = 1 := by\n intro h2\n have h3 : 1 - s = 0 := h2\n have h4 : s = 1 := by\n have h5 : 1 - s + s = 0 + s := by rw [h3]\n rw [sub_add_cancel, zero_add] at h5\n exact h5.symm\n exact h4\n exact absurd (h1 h) (fun h6 => by\n have h7 : s.re = 1 := by rw [h6]; simp\n linarith [h7, hreg2]))\n (fun h => by\n have h1 : (1 - s) = 1 \u2192 s = 0 := by\n intro h2\n have h3 : 1 - s = 1 := h2\n have h4 : s = 0 := by\n have h5 : 1 - s + s = 1 + s := by rw [h3]\n rw [sub_add_cancel] at h5\n have h6 : 1 = 1 + s := h5\n have h7 : 1 - 1 = (1 + s) - 1 := by rw [h6]\n rw [sub_self, add_sub_cancel_left] at h7\n exact h7.symm\n exact h4\n exact absurd (h1 h) (fun h6 => by rw [h6, norm_zero] at hs; linarith [hs, hR]))\n hG1 h\u03b61\n (differentiableAt_Gamma\u211d_of_not_neg_nat (fun m hm => by\n have hre : ((1 - s) / 2).re = (1 - s.re) / 2 := by simp [Complex.div_re]\n have h1 : (0 : \u211d) < ((1 - s) / 2).re := by rw [hre]; linarith [hreg2]\n have h2 : (-(m : \u2102)).re = -(m : \u211d) := by\n rw [Complex.neg_re, Complex.natCast_re]\n have h3 := congrArg Complex.re hm\n rw [hre, h2] at h3\n have hmn : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg _\n linarith [h1, h3, hmn]))\n -- the bracket bound\n have hbr1 : logDeriv Complex.Gamma\u211d s\n = -(Real.log Real.pi : \u2102) / 2 + (1 / 2 : \u2102) * Complex.digamma (s / 2) :=\n logDeriv_Gamma\u211d_eq_of_not_neg_nat hpoles\n have hbr2 : logDeriv Complex.Gamma\u211d (1 - s)\n = -(Real.log Real.pi : \u2102) / 2 + (1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2) :=\n logDeriv_Gamma\u211d_eq_of_not_neg_nat (fun m hm => by\n have hre : ((1 - s) / 2).re = (1 - s.re) / 2 := by simp [Complex.div_re]\n have h1 : (0 : \u211d) < ((1 - s) / 2).re := by rw [hre]; linarith [hreg2]\n have h2 : (-(m : \u2102)).re = -(m : \u211d) := by\n rw [Complex.neg_re, Complex.natCast_re]\n have h3 := congrArg Complex.re hm\n rw [hre, h2] at h3\n have hmn : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg _\n linarith [h1, h3, hmn])\n have h\u03c81 : \u2016Complex.digamma (s / 2)\u2016 \u2264 62 + 23 * Real.log (2 + R / 2) :=\n digamma_circle_le hs hgapInt hR\n have h\u03c82 : \u2016Complex.digamma ((1 - s) / 2)\u2016 \u2264 48 + 23 * Real.log R := by\n have hre : ((1 - s) / 2).re = (1 - s.re) / 2 := by simp [Complex.div_re]\n have h1 : (1.75 : \u211d) \u2264 ((1 - s) / 2).re := by rw [hre]; linarith [hreg2]\n have h2 := digamma_right_le h1\n have hnorm : \u2016(1 - s) / 2\u2016 = \u20161 - s\u2016 / 2 := by\n rw [norm_div]\n have h3 : \u2016(2 : \u2102)\u2016 = 2 := by\n rw [show (2 : \u2102) = ((2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h3]\n have hnorm1s : \u20161 - s\u2016 \u2264 1 + R := by\n calc \u20161 - s\u2016 \u2264 \u2016(1 : \u2102)\u2016 + \u2016s\u2016 := norm_sub_le _ _\n _ = 1 + R := by rw [norm_one, hs]\n have hlogle : Real.log (2 + \u2016(1 - s) / 2\u2016) \u2264 Real.log R := by\n apply Real.log_le_log (by positivity)\n rw [hnorm]\n linarith [hnorm1s, hR]\n have hlog2w_nn : (0 : \u211d) \u2264 Real.log (2 + \u2016(1 - s) / 2\u2016) := by\n apply Real.log_nonneg\n have h3 : (0 : \u211d) \u2264 \u2016(1 - s) / 2\u2016 := norm_nonneg _\n linarith [h3]\n linarith [h2, hlogle, hlog2w_nn, hlogRnn]\n -- assemble case (iii)\n have hld1 : \u2016logDeriv riemannZeta (1 - s)\u2016 \u2264 dirichletC2 := by\n apply norm_logDeriv_zeta_le_dirichlet\n have h1 : (1 - s).re = 1 - s.re := by simp\n rw [h1]\n linarith [hreg2]\n rw [hfe]\n have hstep1 : \u2016-logDeriv riemannZeta (1 - s)\n - (logDeriv Complex.Gamma\u211d s + logDeriv Complex.Gamma\u211d (1 - s))\u2016\n \u2264 \u2016logDeriv riemannZeta (1 - s)\u2016 +\n \u2016logDeriv Complex.Gamma\u211d s + logDeriv Complex.Gamma\u211d (1 - s)\u2016 := by\n calc \u2016-logDeriv riemannZeta (1 - s)\n - (logDeriv Complex.Gamma\u211d s + logDeriv Complex.Gamma\u211d (1 - s))\u2016\n \u2264 \u2016-logDeriv riemannZeta (1 - s)\u2016 +\n \u2016logDeriv Complex.Gamma\u211d s + logDeriv Complex.Gamma\u211d (1 - s)\u2016 :=\n norm_sub_le _ _\n _ = \u2016logDeriv riemannZeta (1 - s)\u2016 +\n \u2016logDeriv Complex.Gamma\u211d s + logDeriv Complex.Gamma\u211d (1 - s)\u2016 := by\n rw [norm_neg]\n have hbracket : \u2016logDeriv Complex.Gamma\u211d s + logDeriv Complex.Gamma\u211d (1 - s)\u2016\n \u2264 2 + (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2 := by\n rw [hbr1, hbr2]\n have h1 : -(Real.log Real.pi : \u2102) / 2 + (1 / 2 : \u2102) * Complex.digamma (s / 2) +\n (-(Real.log Real.pi : \u2102) / 2 + (1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2))\n = -(Real.log Real.pi : \u2102) +\n ((1 / 2 : \u2102) * Complex.digamma (s / 2) +\n (1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2)) := by ring\n rw [h1]\n calc \u2016-(Real.log Real.pi : \u2102) +\n ((1 / 2 : \u2102) * Complex.digamma (s / 2) +\n (1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2))\u2016\n \u2264 \u2016(Real.log Real.pi : \u2102)\u2016 +\n \u2016(1 / 2 : \u2102) * Complex.digamma (s / 2) +\n (1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2)\u2016 := by\n have h2 := norm_add_le (-(Real.log Real.pi : \u2102))\n ((1 / 2 : \u2102) * Complex.digamma (s / 2) +\n (1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2))\n rw [norm_neg] at h2\n exact h2\n _ \u2264 2 + ((62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2) := by\n have hlogpi : \u2016(Real.log Real.pi : \u2102)\u2016 \u2264 2 := by\n have h1 := log_pi_le_two\n have hpos : (0 : \u211d) < Real.log Real.pi :=\n Real.log_pos (by linarith [Real.pi_gt_three] : (1 : \u211d) < Real.pi)\n rw [show ((Real.log Real.pi : \u2102)) = ((Real.log Real.pi : \u211d) : \u2102) from rfl,\n Complex.norm_real, Real.norm_eq_abs, abs_of_pos hpos]\n exact h1\n have h\u03c8 : \u2016(1 / 2 : \u2102) * Complex.digamma (s / 2) +\n (1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2)\u2016\n \u2264 (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2 := by\n calc \u2016(1 / 2 : \u2102) * Complex.digamma (s / 2) +\n (1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2)\u2016\n \u2264 \u2016(1 / 2 : \u2102) * Complex.digamma (s / 2)\u2016 +\n \u2016(1 / 2 : \u2102) * Complex.digamma ((1 - s) / 2)\u2016 := norm_add_le _ _\n _ = \u2016Complex.digamma (s / 2)\u2016 / 2 + \u2016Complex.digamma ((1 - s) / 2)\u2016 / 2 := by\n have h1 : \u2016(1 / 2 : \u2102)\u2016 = 1 / 2 := by\n rw [show (1 / 2 : \u2102) = ((1 / 2 : \u211d) : \u2102) by push_cast; ring,\n Complex.norm_real]\n norm_num\n rw [norm_mul, h1, norm_mul, h1]\n ring\n _ \u2264 (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2 := by\n have h1 := div_le_div_of_nonneg_right h\u03c81 (by norm_num : (0 : \u211d) \u2264 2)\n have h2 := div_le_div_of_nonneg_right h\u03c82 (by norm_num : (0 : \u211d) \u2264 2)\n have h3 : \u2016Complex.digamma (s / 2)\u2016 / 2\n \u2264 (62 + 23 * Real.log (2 + R / 2)) / 2 := h1\n have h4 : \u2016Complex.digamma ((1 - s) / 2)\u2016 / 2\n \u2264 (48 + 23 * Real.log R) / 2 := h2\n linarith [h3, h4]\n linarith [hlogpi, h\u03c8]\n _ = 2 + (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2 := by ring\n have hlog2R : Real.log (2 + R / 2) \u2264 Real.log R := by\n apply Real.log_le_log (by linarith [hRpos] : (0 : \u211d) < 2 + R / 2)\n linarith [hR]\n calc \u2016-logDeriv riemannZeta (1 - s)\n - (logDeriv Complex.Gamma\u211d s + logDeriv Complex.Gamma\u211d (1 - s))\u2016\n \u2264 \u2016logDeriv riemannZeta (1 - s)\u2016 +\n \u2016logDeriv Complex.Gamma\u211d s + logDeriv Complex.Gamma\u211d (1 - s)\u2016 := hstep1\n _ \u2264 dirichletC2 + (2 + (62 + 23 * Real.log (2 + R / 2)) / 2 +\n (48 + 23 * Real.log R) / 2) := add_le_add hld1 hbracket\n _ \u2264 dirichletC2 + 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n have h1 : 2 + (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2\n \u2264 100 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n have h2 : 2 + (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2\n \u2264 57 + 23 * Real.log R := by\n have h3 := div_le_div_of_nonneg_right\n (show Real.log (2 + R / 2) \u2264 Real.log R from hlog2R)\n (by norm_num : (0 : \u211d) \u2264 2)\n nlinarith [hlog2R, hlogRnn, Real.log_nonneg (show (1 : \u211d) \u2264 2 + R / 2 from by\n linarith [hRpos])]\n have h4 : (57 : \u211d) + 23 * Real.log R\n \u2264 100 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n have h5 : (1 : \u211d) \u2264 A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2 := by\n have h6 : (81 : \u211d) \u2264 (Real.log R) ^ 2 := by nlinarith [hlogR, hlogRnn]\n have h7 : (2 : \u211d) \u2264 A0count * C0hat (4 * (k : \u211d) + 9 / 2) :=\n le_trans h\u01082 (mul_le_mul_of_nonneg_left (by linarith [h\u01082] :\n (1 : \u211d) \u2264 C0hat (4 * (k : \u211d) + 9 / 2)) hA0)\n nlinarith [h6, h7, hA0, h\u0108pos]\n nlinarith [h5, hlogRnn, hA0, h\u0108pos]\n linarith [h2, h4]\n nlinarith [h1, hnnR, dirichletC2_nonneg]\n\n/-- **The Fexpr circle bound**: \u2016Fexpr s\u2016 \u2264 2\u00b7lowZeroConst +\ndirichletC2 + 400000\u00b7A\u2080\u00b7\u0108\u2080(R+2)\u00b7(log R)\u00b2. -/\ntheorem Fexpr_circle_le {k : \u2115} (hk : 4000 \u2264 k) {R : \u211d}\n (hRlo : 4 * (k : \u211d) + 5 / 2 \u2264 R) (hRhi : R \u2264 4 * (k : \u211d) + 3)\n (hgap : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192\n 1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2)) \u2264 |\u03c1.im - R| \u2228 1 \u2264 |\u03c1.im - R|)\n (hgapInt : \u2200 m : \u2124, 1 / 4 \u2264 |R / 2 - (m : \u211d)|)\n {s : \u2102} (hs : \u2016s\u2016 = R) :\n \u2016Fexpr s\u2016 \u2264 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n classical\n have hsz : \u00ac IsNontrivialZero s :=\n not_isNontrivialZero_on_gapCircle hk hRlo hgap hs\n have h\u01082 : (2 : \u211d) \u2264 C0hat (4 * (k : \u211d) + 9 / 2) := two_le_C0hat (by\n have hkR : (1 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast (by omega : 1 \u2264 k)\n linarith)\n have hR : (16002 : \u211d) \u2264 R := by\n have hkR : (16000 : \u211d) \u2264 4 * (k : \u211d) := by\n have h1 : (4000 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk\n linarith\n linarith [hRlo]\n have hRpos : (0 : \u211d) < R := by linarith [hR]\n have hlogR : (9 : \u211d) \u2264 Real.log R := nine_le_log_of_16002_le hR\n have hlogRnn : (0 : \u211d) \u2264 Real.log R := by linarith [hlogR]\n have hA0 := A0count_pos.le\n have h\u0108R2 : C0hat (4 * (k : \u211d) + 9 / 2) \u2264 C0hat (R + 2) :=\n C0hat_mono (by linarith [hRlo] : (1 : \u211d) \u2264 4 * (k : \u211d) + 9 / 2)\n (by linarith [hRlo] : 4 * (k : \u211d) + 9 / 2 \u2264 R + 2)\n have h\u0108R2pos : (0 : \u211d) < C0hat (R + 2) := by linarith [h\u01082, h\u0108R2]\n -- the pieces\n have hser := seriesFun_norm_le_gapCircle hk hRlo hgap hs\n have hld := logDeriv_circle_le hk hRlo hgap hgapInt hs hsz\n have h\u03c8 := digamma_circle_le hs hgapInt hR\n have h1s := norm_one_div_le_of_norm_eq hs (by linarith [hR] : (1 : \u211d) \u2264 R)\n have h1s1 := norm_one_div_sub_one_le_of_norm_eq hs (by linarith [hR] : (2 : \u211d) \u2264 R)\n have hlogpi := norm_logPi_div_two_le\n -- the norm chain: Fexpr = logDeriv \u03b6 \u2212 seriesFun + 1/s + 1/(s\u22121) \u2212 (log \u03c0)/2 + \u03c8(s/2)/2\n have hchain : \u2016Fexpr s\u2016 \u2264 \u2016logDeriv riemannZeta s\u2016 + \u2016seriesFun s\u2016 +\n \u2016(1 : \u2102) / s\u2016 + \u2016(1 : \u2102) / (s - 1)\u2016 + \u2016(Real.log Real.pi : \u2102) / 2\u2016 +\n \u2016Complex.digamma (s / 2) / 2\u2016 := by\n rw [Fexpr]\n calc \u2016logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\u2016\n \u2264 \u2016logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2\u2016 + \u2016Complex.digamma (s / 2) / 2\u2016 :=\n norm_add_le _ _\n _ \u2264 \u2016logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\u2016\n + \u2016(Real.log Real.pi : \u2102) / 2\u2016 + \u2016Complex.digamma (s / 2) / 2\u2016 :=\n add_le_add_right (norm_sub_le _ _) _\n _ \u2264 \u2016logDeriv riemannZeta s - seriesFun s + 1 / s\u2016 + \u2016(1 : \u2102) / (s - 1)\u2016\n + \u2016(Real.log Real.pi : \u2102) / 2\u2016 + \u2016Complex.digamma (s / 2) / 2\u2016 :=\n add_le_add_right (add_le_add_right (norm_add_le _ _) _) _\n _ \u2264 \u2016logDeriv riemannZeta s - seriesFun s\u2016 + \u2016(1 : \u2102) / s\u2016 + \u2016(1 : \u2102) / (s - 1)\u2016\n + \u2016(Real.log Real.pi : \u2102) / 2\u2016 + \u2016Complex.digamma (s / 2) / 2\u2016 :=\n add_le_add_right (add_le_add_right (add_le_add_right (norm_add_le _ _) _) _) _\n _ \u2264 \u2016logDeriv riemannZeta s\u2016 + \u2016seriesFun s\u2016 + \u2016(1 : \u2102) / s\u2016 + \u2016(1 : \u2102) / (s - 1)\u2016\n + \u2016(Real.log Real.pi : \u2102) / 2\u2016 + \u2016Complex.digamma (s / 2) / 2\u2016 := by\n apply add_le_add_right\n apply add_le_add_right\n apply add_le_add_right\n apply add_le_add_right\n exact norm_sub_le _ _\n -- the \u03c8 term: \u2016\u03c8(s/2)/2\u2016 = \u2016\u03c8(s/2)\u2016/2\n have h\u03c8norm : \u2016Complex.digamma (s / 2) / 2\u2016 = \u2016Complex.digamma (s / 2)\u2016 / 2 := by\n rw [norm_div]\n have h1 : \u2016(2 : \u2102)\u2016 = 2 := by\n rw [show (2 : \u2102) = ((2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h1]\n -- assemble\n have hbig : \u2016logDeriv riemannZeta s\u2016 + \u2016seriesFun s\u2016 + \u2016(1 : \u2102) / s\u2016 +\n \u2016(1 : \u2102) / (s - 1)\u2016 + \u2016(Real.log Real.pi : \u2102) / 2\u2016 + \u2016Complex.digamma (s / 2) / 2\u2016\n \u2264 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have hser2 : \u2016seriesFun s\u2016 \u2264 2 * lowZeroConst +\n 2900 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have h1 : 2900 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2\n \u2264 2900 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 :=\n mul_le_mul_of_nonneg_right\n (mul_le_mul_of_nonneg_left h\u0108R2 hA0) (pow_two_nonneg _)\n linarith [hser, h1]\n have hld2 : \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC2 + 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have h1 : 300 * A0count * C0hat (4 * (k : \u211d) + 9 / 2) * (Real.log R) ^ 2\n \u2264 300 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 :=\n mul_le_mul_of_nonneg_right\n (mul_le_mul_of_nonneg_left h\u0108R2 hA0) (pow_two_nonneg _)\n linarith [hld, h1]\n have h\u03c82 : \u2016Complex.digamma (s / 2) / 2\u2016 \u2264 31 + 12 * Real.log R := by\n rw [h\u03c8norm]\n have hlog2R : Real.log (2 + R / 2) \u2264 Real.log R := by\n apply Real.log_le_log (by linarith [hRpos] : (0 : \u211d) < 2 + R / 2)\n linarith [hR]\n have h1 : (62 + 23 * Real.log (2 + R / 2)) / 2\n \u2264 (62 + 23 * Real.log R) / 2 :=\n div_le_div_of_nonneg_right (add_le_add_left\n (mul_le_mul_of_nonneg_left hlog2R (by norm_num : (0 : \u211d) \u2264 23)) _) (by norm_num)\n have h2 := div_le_div_of_nonneg_right h\u03c8 (by norm_num : (0 : \u211d) \u2264 2)\n linarith [h1, h2, hlogRnn]\n have h1 : 2900 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 +\n (200000 * (Real.log R) ^ 2 + 300 * A0count * C0hat (R + 2) * (Real.log R) ^ 2) +\n ((31 + 12 * Real.log R) + 2)\n \u2264 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have h2 : (2 : \u211d) \u2264 A0count * C0hat (R + 2) :=\n le_trans h\u01082 (le_trans h\u0108R2 (le_refl _))\n have h3 : (81 : \u211d) \u2264 (Real.log R) ^ 2 := by nlinarith [hlogR, hlogRnn]\n have h4 : (1 : \u211d) \u2264 A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n nlinarith [h2, h3, hA0, h\u0108R2pos]\n have h5 : 200000 * (Real.log R) ^ 2\n \u2264 100000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have h6 : (2 : \u211d) \u2264 A0count * C0hat (R + 2) := h2\n nlinarith [h6, pow_two_nonneg (Real.log R)]\n nlinarith [h5, h4, h2, h3, hlogRnn, hA0, h\u0108R2pos]\n linarith [hser2, hld2, h\u03c82, h1s, h1s1, hlogpi, h1, lowZeroConst_nonneg,\n dirichletC2_nonneg]\n exact hchain.trans hbig\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Now c-iii: `logDeriv_circle_le` + `Fexpr_circle_le`.\n\n**logDeriv_circle_le** design:\n```\ntheorem logDeriv_circle_le {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}\n (hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R)\n (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →\n 1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)\n (hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|)\n {s : ℂ} (hs : ‖s‖ = R) (hsz : ¬ IsNontrivialZero s) :\n ‖logDeriv riemannZeta s‖ ≤ dirichletC2 +\n 200000 * (Real.log R) ^ 2 + 192 * C0hat (4 * (k : ℝ) + 9 / 2) * A0count * (Real.log R) ^ 2 +\n 100 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2\n```\nHmm — let me simplify the RHS form: dirichletC2 + 200000·L² + 300·Ĉ₀·A₀·L² (folding 192+100 → 300). Regions:\n(i) 2 ≤ re s: Dirichlet: ‖logDeriv ζ‖ ≤ dirichletC2 ≤ RHS ✓ (rest nonneg).\n(ii) −5/2 ≤ re s ∧ re s ≤ 2: |t| ≥ 10 (auto): capstones + near:\n ‖logDeriv ζ s‖ ≤ ‖logDeriv ζ s − near‖ + ‖near‖ ≤ 200000·(log|t|)² + ‖near‖.\n near: ‖Σ_{ρ ∈ nearZeros t} m/(s−ρ)‖ ≤ Σ ‖m/(s−ρ)‖ = Σ m/‖s−ρ‖ ≤ 32Ĉ₀·(Σ m) ≤ 32Ĉ₀·3A₀·log(3·max|t−1||t+1|+5) ≤ 96·Ĉ₀·A₀·2L = 192·Ĉ₀·A₀·L ≤ 192·Ĉ₀·A₀·L².\n log|t| ≤ log R (|t| ≤ R).\n Sub-split re ≥ 1/2 (5c: 100000) vs re < 1/2 (5d-left: 200000) — uniform 200000.\n Note: the capstones need t = s.im (hsim : s.im = t ✓ rfl with t := s.im) and ζ s ≠ 0 (hsz via... ζ s ≠ 0 ⟸ hsz + re ≥ 1? NO — the capstone takes (hs0 : riemannZeta s ≠ 0): ζ s ≠ 0 from hsz (s not a nontrivial zero) + re s ≥ −5/2: if ζ s = 0: zeta_zero_classification: nontrivial (hsz ✗), 0 (‖s‖ = R > 0 ✗), −2n (re s ≥ −5/2 > −4: −2n with n ≥ 1: −2n ≤ −2: possible for re s ∈ [−5/2, −2]: −2n = −2: s = −2: re = −2 ∈ [−5/2, 2] ✓ POSSIBLE — need to exclude s = −2: ‖s‖ = R ≥ 16002 ≠ 2 ✓ trivially! ‖(−2:ℂ)‖ = 2 ≠ R ✓.) So ζ s ≠ 0 ✓.\n(iii) re s < −5/2: the FE route:\n logDeriv ζ s = −logDeriv ζ(1−s) − (logDeriv ΓR s + logDeriv ΓR(1−s)) via logDeriv_zeta_fe — the 10 hypotheses:\n - hs0' : s ≠ 0 (‖s‖ = R > 0: s = 0 ⟹ ‖s‖ = 0 ✗).\n - hs1' : s ≠ 1 (re < −5/2 < 1: s = 1 ⟹ re = 1 ✗).\n - hG : Gammaℝ s ≠ 0: rw [ne_eq, Complex.Gammaℝ_eq_zero_iff]; rintro ⟨m, hm⟩: s = −2m: s/2 = −m: contradiction with the pole-avoidance hpoles (below).\n - hζ : ζ s ≠ 0: zeta_zero_classification: nontrivial ✗ (hsz); 0 ✗; −2n: s = −2n: s/2 = −n: hpoles ✗.\n - hd : DifferentiableAt Gammaℝ s := differentiableAt_Gammaℝ_of_not_neg_nat hpoles.\n - hpoles : ∀ m : ℕ, s / 2 ≠ -(m : ℂ): split im s = 0 vs ≠ 0:\n - im s ≠ 0: (s/2).im ≠ 0 ⟹ s/2 ≠ −(m:ℂ) (real) ✓.\n - im s = 0: s = re s = −R?? wait — im s = 0 and ‖s‖ = R and re s < −5/2: s = −R (s real, |s| = R, re < 0): (s/2) = −R/2: −R/2 = −m ⟺ R/2 = m: |R/2 − m| = 0 < 1/4 contradicts hgapInt (m : ℤ) ✓.\n - at 1−s: 1−s ≠ 0 (s ≠ 1 ✓); 1−s ≠ 1 (s ≠ 0 ✓); Gammaℝ(1−s) ≠ 0: (1−s)/2 ∉ −ℕ: re((1−s)/2) = (1−re s)/2 > (1+5/2)/2 = 1.75 > 0 ⟹ ≠ −m ✓ (re(−m) = −m ≤ 0 ✗); ζ(1−s) ≠ 0: re(1−s) = 1−re s > 1+5/2 > 1: riemannZeta_ne_zero_of_one_le_re (1 ≤ re(1−s)) (1−s ≠ 1) ✓; DifferentiableAt Gammaℝ(1−s): differentiableAt_Gammaℝ_of_not_neg_nat ((1−s)/2 ∉ −ℕ ✓).\n Then:\n ‖logDeriv ζ s‖ = ‖−logDeriv ζ(1−s) − (bracket)‖ ≤ ‖logDeriv ζ(1−s)‖ + ‖bracket‖ ≤ dirichletC2 + ‖bracket‖ (re(1−s) ≥ 7/2 ≥ 2: Dirichlet ✓).\n bracket := logDeriv ΓR s + logDeriv ΓR(1−s) = −(logπ)/2 + ½ψ(s/2) + (−(logπ)/2 + ½ψ((1−s)/2)) via logDeriv_Gammaℝ_eq_of_not_neg_nat (s/2 ∉ −ℕ ✓ hpoles; (1−s)/2 ∉ −ℕ ✓).\n ‖bracket‖ ≤ log π + ½(‖ψ(s/2)‖ + ‖ψ((1−s)/2)‖): \n - ‖ψ(s/2)‖: two sub-cases: |im(s/2)| ≥ 5: sub-log: 3 + log‖s/2‖ + π ≤ 3 + log(R/2) + 3.15 ≤ 7 + log(R/2) ≤ 62+23·log(2+R/2)·... hmm just bound ≤ 62 + 23·log(2+R/2) uniformly via digamma_circle_le! I have digamma_circle_le (hgapInt) already — use it directly for ALL s ✓: ‖ψ(s/2)‖ ≤ 62 + 23·log(2+R/2) ✓.\n - ‖ψ((1−s)/2)‖: re((1−s)/2) = (1−re s)/2 > 1.75: digamma_right_le: ≤ 48 + 23·log(2+‖(1−s)/2‖): ‖(1−s)/2‖ = ‖1−s‖/2 ≤ (1+R)/2: log(2+‖(1−s)/2‖) ≤ log(2+(1+R)/2) ≤ log(2+R) hmm: 2+(1+R)/2 = (5+R)/2 ≤ R ⟺ 5 ≤ R ✓: ≤ log R = L... or just ≤ log(2+R) ≤ log(2R) = log2+L ≤ 1+L. Let me use log(2+(1+R)/2) ≤ L: 2+(1+R)/2 ≤ R ⟺ 5 ≤ R ✓ so log ≤ L ✓. So ‖ψ((1−s)/2)‖ ≤ 48 + 23·L.\n bracket ≤ 2 + ½(62+23·log(2+R/2)) + ½(48+23·L) ≤ 2 + 31+11.5·L + 24+11.5·L = 57+23L (log(2+R/2) ≤ L ✓ (2+R/2 ≤ R ⟺ 4 ≤ R)).\n So case (iii): ‖logDeriv ζ‖ ≤ dirichletC2 + 57 + 23·L.\n Absorb 57+23L ≤ 100·A₀·Ĉ₀·L² ✓ (A₀ ≥ 1, Ĉ₀ ≥ 2, L ≥ 9: 57 ≤ 57·... 100·A₀Ĉ₀L² ≥ 100·2·81 = 16200 ≥ 57+23L ⟸ 23L ≤ 23·A₀Ĉ₀L² ✓ 57 ≤ 57·A₀Ĉ₀L²/(162)·... 57 ≤ 57/162·A₀Ĉ₀L² ≤ A₀Ĉ₀L²: total ≤ (57/162 + 23)·A₀Ĉ₀L² ≤ 24·A₀Ĉ₀L² ≤ 100·A₀Ĉ₀L² ✓).\n So uniform: ‖logDeriv ζ s‖ ≤ dirichletC2 + max(0, 200000L² + 192Ĉ₀A₀L², 100A₀Ĉ₀L²) — final RHS: dirichletC2 + 200000·L² + 300·A₀·Ĉ₀·L² ✓ (192 ≤ 300, 100 ≤ 300, and region (i) needs just dirichletC2 ≤ RHS ✓ with the others nonneg).\n\n**Fexpr_circle_le**:\n```\ntheorem Fexpr_circle_le {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}\n (hRlo : 4*(k:ℝ)+5/2 ≤ R) (hRhi : R ≤ 4*(k:ℝ)+3)\n (hgap : ...) (hgapInt : ∀ m : ℤ, 1/4 ≤ |R/2 − (m:ℝ)|)\n {s : ℂ} (hs : ‖s‖ = R) :\n ‖Fexpr s‖ ≤ 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2\n```\nAssembly: unfold Fexpr: Fexpr s = logDeriv ζ s − seriesFun s + 1/s + 1/(s−1) − (logπ:ℂ)/2 + digamma (s/2)/2.\nnorm chain:\n‖Fexpr s‖ ≤ ‖logDeriv ζ s‖ + ‖seriesFun s‖ + ‖1/s‖ + ‖1/(s−1)‖ + ‖(logπ)/2‖ + ‖digamma (s/2)/2‖.\nVia successive: ‖a − b + c + d − e + f‖ ≤ ...: \n‖X − seriesFun + Y‖ ≤ ‖X − seriesFun‖ + ‖Y‖ (norm_add_le) hmm — the expression structure: ((((logDeriv − seriesFun) + 1/s) + 1/(s−1)) − c) + ψ: norm ≤ ‖(((logDeriv − seriesFun) + 1/s) + 1/(s−1)) − c‖ + ‖ψ‖ ≤ ‖((logDeriv − seriesFun) + 1/s) + 1/(s−1)‖ + ‖c‖ + ‖ψ‖ ≤ ... chain of norm_add_le/norm_sub_le. ~6 lines.\nPieces:\n- hsz := not_isNontrivialZero_on_gapCircle hk hRlo hgap hs.\n- ‖seriesFun s‖ ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(4k+9/2)·L² ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(R+2)·L² (C0hat_mono: 4k+9/2 ≤ R+2 ⟺ 4k+5/2 ≤ R ✓ hRlo; mono needs 1 ≤ 4k+9/2 ✓).\n- ‖logDeriv ζ s‖ ≤ dirichletC2 + 200000·L² + 300·A₀·Ĉ₀(4k+9/2)·L² ≤ dirichletC2 + 200000·L² + 300·A₀·Ĉ₀(R+2)·L².\n- ψ-elem: ‖digamma (s/2)/2‖ = ‖digamma (s/2)‖/2 ≤ (62+23·log(2+R/2))/2 ≤ 31+12·L ≤ 13·A₀Ĉ₀(R+2)L² (absorbed as computed).\n- 1/s + 1/(s−1) ≤ 2 ≤ (2/162)·A₀Ĉ₀L² ≤ A₀Ĉ₀L².\n- ‖(logπ)/2‖ ≤ 1 ≤ A₀Ĉ₀L².\n- 200000·L² ≤ 100000·A₀Ĉ₀L² (A₀Ĉ₀ ≥ 2).\nTotal: 2·lowZeroConst + dirichletC2 + [2900 + 300 + 13 + 1 + 1 + 100000]·A₀Ĉ₀(R+2)L² = 2·lowZeroConst + dirichletC2 + 103215·A₀Ĉ₀(R+2)L² ≤ 400000·... ✓.\n\nLet me now write c-iii. First logDeriv_circle_le with the three regions. The region (ii) |t| ≥ 10: re s ∈ [−5/2, 2] ⟹ re² ≤ 25/4: im² = R²−re² ≥ R²−25/4: |im| ≥ 10: from R−|im| = re²/(R+|im|) ≤ (25/4)/R: |im| ≥ R−25/(4R) ≥ 10 ⟺ 25/(4R) ≤ R−10 ⟸ R ≥ 16002: linarith: 25/(4R) ≤ 1 ≤ R−10·... 25/(4R) = 6.25/R ≤ 6.25/16002 < 1 ≤ R−10·... R−10 ≥ 15992 ≥ 1 > 25/(4R)·... need |im| ≥ R − 25/(4R) ≥ 10: R − 25/(4R) ≥ 10 ⟺ R − 10 ≥ 25/(4R) ⟸ 25/(4R) ≤ 25/(4·16002) = 0.0004 ≤ 15992 ≤ R−10 ✓.\nThe norm_circle_sub_abs_im_le gives R−|im| ≤ B/R with B := 25/4 (re² ≤ 25/4 ✓): R−|im| ≤ (25/4)/R: |im| ≥ R−(25/4)/R ≥ 10 ✓ linarith.\n\nFor region (ii)'s near-sum:\n```\nhave hnear : ‖∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖\n ≤ 32 * C0hat (4*(k:ℝ)+9/2) * (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) := by\n calc ‖∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖\n ≤ ∑ ρ ∈ nearZeros s.im, ‖(zeroMult ρ : ℂ) / (s - ρ)‖ := norm_sum_le _ _\n _ = ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) / ‖s - ρ‖ := by\n apply Finset.sum_congr rfl\n intro ρ hρ\n rw [norm_div, RCLike.norm_natCast]\n _ ≤ ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) * (32 * C0hat (4*(k:ℝ)+9/2)) := by\n apply Finset.sum_le_sum\n intro ρ hρ\n have hsep := gapCircle_sep_of_mem_nearZeros hk hRlo hgap hs hρ\n -- m/‖s−ρ‖ ≤ m·(32Ĉ₀) ⟸ 1/‖s−ρ‖ ≤ 32Ĉ₀ ⟸ 1/(32Ĉ₀) ≤ ‖s−ρ‖\n rw [show (zeroMult ρ : ℝ) / ‖s - ρ‖ = (zeroMult ρ : ℝ) * (1 / ‖s - ρ‖) from by ring]\n rw [show (zeroMult ρ : ℝ) * (32 * C0hat (4*(k:ℝ)+9/2)) = (zeroMult ρ : ℝ) * (32 * C0hat (4*(k:ℝ)+9/2)) from rfl]\n apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n -- 1/‖s−ρ‖ ≤ 32Ĉ₀ ⟺ 1/(32Ĉ₀) ≤ ‖s−ρ‖ (via one_div_le_one_div_of_le with positive)\n have h1 : (0 : ℝ) < 1 / (32 * C0hat (4*(k:ℝ)+9/2)) := by positivity\n have h2 : (0 : ℝ) < ‖s - ρ‖ := by linarith [hsep, h1]\n rw [one_div_le_one_div_of_le h2 hsep] -- hmm: one_div_le_one_div_of_le (ha : 0 < a) (hb : a ≤ b) : 1/b ≤ 1/a\n -- goal after: 1/‖s−ρ‖ ≤ 32·Ĉ₀ = 1/(1/(32Ĉ₀)): one_div_le_one_div_of_le h2 hsep : 1/‖s−ρ‖ ≤ 1/(1/(32Ĉ₀)): then 1/(1/(32Ĉ₀)) = 32Ĉ₀ (one_div_one_div)\n have h3 : 1 / (1 / (32 * C0hat (4*(k:ℝ)+9/2))) = 32 * C0hat (4*(k:ℝ)+9/2) := one_div_one_div _\n rw [h3] at * — hmm careful; do:\n exact (one_div_le_one_div_of_le h2 hsep).trans_eq (one_div_one_div _)\n _ = (32 * C0hat (4*(k:ℝ)+9/2)) * ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) := by\n rw [Finset.mul_sum] -- hmm: Σ m·(32Ĉ₀) = (32Ĉ₀)·Σm: mul_comm forms: m·c = c·m: sum_congr (mul_comm) then mul_sum\n _ ≤ (32 * C0hat (4*(k:ℝ)+9/2)) * (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) :=\n mul_le_mul_of_nonneg_left nearZeros_count_le (by positivity)\n _ = 32 * C0hat (4*(k:ℝ)+9/2) * (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) := rfl\n```\nThe sum_congr for m·c = c·m: `Finset.sum_congr rfl (fun ρ hρ => mul_comm _ _)`.\n\nHmm — norm_sum_le : ‖∑ x ∈ s, f x‖ ≤ ∑ x ∈ s, ‖f x‖ — `norm_sum_le (s : Finset ι) (f : ι → α) : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖` ✓.\n\nThe capstone application:\n```\nhave hcap : ‖logDeriv riemannZeta s - ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖\n ≤ 200000 * (Real.log |s.im|) ^ 2 := by\n by_cases hhalf : (1 : ℝ) / 2 ≤ s.re\n · have h := logDeriv_riemannZeta_sub_nearZeros_le (t := s.im) ht10 rfl hhalf (by linarith [hσ2] : s.re ≤ 7/2) hζs\n exact h.trans (by ...)\n · push Not at hhalf\n have h := logDeriv_riemannZeta_sub_nearZeros_le_left (t := s.im) ht10 rfl (by linarith [hσ25]) (by linarith [hhalf] : s.re ≤ 1/2) hζs\n exact h\n```\nwith ht10 : 10 ≤ |s.im|, hζs : riemannZeta s ≠ 0, hσ25 : −5/2 ≤ s.re, hσ2 : s.re ≤ 2.\n\nThen region (ii) final:\n```\ncalc ‖logDeriv riemannZeta s‖\n ≤ ‖logDeriv riemannZeta s - ∑ ...‖ + ‖∑ ...‖ := by\n have h1 : logDeriv riemannZeta s = (logDeriv riemannZeta s - ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)) + ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ) := by rw [sub_add_cancel]\n rw [h1]\n exact norm_add_le _ _\n _ ≤ 200000 * (Real.log |s.im|) ^ 2 + (32·Ĉ₀·3A₀·log(...)) := add_le_add hcap hnear\n _ ≤ 200000 * (Real.log R) ^ 2 + 192·Ĉ₀·A₀·L² := ...\n```\nlog|s.im| ≤ log R (|s.im| ≤ R ✓ abs_im_le_norm+hs; log mono, |s.im| ≥ 10 > 0): (Real.log |s.im|)^2 ≤ (Real.log R)^2: both ≥ 0: pow_le_pow_left₀ (Real.log_nonneg (|s.im| ≥ 10 ≥ 1)) (log|s.im| ≤ log R) 2 ✓.\nAnd 32Ĉ₀·3A₀·log(3·max|t−1||t+1|+5) ≤ 192·Ĉ₀·A₀·L: max|t−1||t+1| = |t|+1 ≤ R+1: log(3(R+1)+5) = log(3R+8) ≤ log(4R) ≤ 2L ⟸ 8 ≤ R and log 4 ≤ L ✓. 32·3 = 96: 96Ĉ₀A₀·2L = 192Ĉ₀A₀L ≤ 192Ĉ₀A₀L² (L ≥ 1).\n\nRegion (i) is trivial (Dirichlet + nonneg RHS parts).\n\nRegion (iii): the FE identity + bracket bound — biggest single block (~150 lines).\n\nThen Fexpr_circle_le (~80 lines).\n\nLet me write logDeriv_circle_le first.","signature":""},{"type":"text","text":"Committed. Now c-iii: `logDeriv_circle_le` (three regions) — writing the region structure."},{"type":"tool_use","id":"Edit_198","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 12. The logDeriv circle bound and the Fexpr assembly (5e-v-c-iii)\n\n`logDeriv_circle_le`: three regions — (i) re s ≥ 2: the Dirichlet\nbound; (ii) re s ∈ [−5/2, 2] (automatically |im s| ≥ 10): the 5c/5d\ncapstones + the near sum ≤ 32·Ĉ₀·(near count); (iii) re s < −5/2: the\nFE identity `logDeriv_zeta_fe` + Dirichlet at 1−s + the ΓR bracket\nvia `logDeriv_Gammaℝ_eq_of_not_neg_nat` (which also discharges the\nreal point s = −R). Uniform:\n‖logDeriv ζ s‖ ≤ dirichletC2 + 200000·(log R)² + 300·A₀·Ĉ₀·(log R)².\n\n`Fexpr_circle_le`: ‖Fexpr s‖ ≤ 2·lowZeroConst + dirichletC2 +\n400000·A₀·Ĉ₀(R+2)·(log R)². -/\n\n/-- **The logDeriv bound on the gap circle.** -/\ntheorem logDeriv_circle_le {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}\n (hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R)\n (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →\n 1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)\n (hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|)\n {s : ℂ} (hs : ‖s‖ = R) (hsz : ¬ IsNontrivialZero s) :\n ‖logDeriv riemannZeta s‖ ≤ dirichletC2 +\n 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n classical\n have hĈ2 : (2 : ℝ) ≤ C0hat (4 * (k : ℝ) + 9 / 2) := two_le_C0hat (by\n have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast (by omega : 1 ≤ k)\n linarith)\n have hR : (16002 : ℝ) ≤ R := by\n have hkR : (16000 : ℝ) ≤ 4 * (k : ℝ) := by\n have h1 : (4000 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk\n linarith\n linarith [hRlo]\n have hRpos : (0 : ℝ) < R := by linarith [hR]\n have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR\n have hlogRnn : (0 : ℝ) ≤ Real.log R := by linarith [hlogR]\n have hA0 := A0count_pos.le\n have hĈpos : (0 : ℝ) < C0hat (4 * (k : ℝ) + 9 / 2) := by linarith [hĈ2]\n have hnnR : (0 : ℝ) ≤ 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n apply add_nonneg (mul_nonneg (by norm_num) (pow_two_nonneg _))\n exact mul_nonneg (mul_nonneg (by norm_num) hA0)\n (mul_nonneg hĈpos.le (pow_two_nonneg _))\n -- ζ s ≠ 0 on the whole circle\n have hζs : riemannZeta s ≠ 0 := by\n intro h\n rcases zeta_zero_classification h with hn | h0 | ⟨n, hn, h2n⟩\n · exact hsz hn\n · rw [h0, norm_zero] at hs\n linarith [hs, hR]\n · have hnorm2 : ‖(-2 : ℂ) * (n : ℂ)‖ ≤ 2 * (n : ℝ) := by\n rw [← h2n]\n have h1 : ‖(-2 : ℂ)‖ = 2 := by\n rw [show (-2 : ℂ) = ((-2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [norm_mul, h1, Complex.norm_natCast]\n rw [← h2n] at hnorm2\n have hR2 : R ≤ 2 * (n : ℝ) := by rw [← hs]; exact hnorm2\n have hre : (-2 : ℝ) < -5 / 2 → False := by norm_num\n by_cases hcase : 2 ≤ s.re\n · exact absurd h rfl hsz\n · push Not at hcase\n by_cases hcase2 : -5 / 2 ≤ s.re\n · -- s = −2n with re ∈ [−5/2, 2]: n = 1, s = −2: ‖s‖ = 2 < R\n have hn1 : n = 1 := by\n have hre2 : s.re = -2 * (n : ℝ) := by\n rw [h2n]\n simp [Complex.mul_re, Complex.natCast_re, Complex.ofReal_re]\n have hnn : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hbound : -5 / 2 ≤ -2 * (n : ℝ) ∧ -2 * (n : ℝ) ≤ 2 := by\n rw [← hre2]\n exact ⟨hcase2, hcase⟩\n have h1 : (n : ℝ) < 2 := by linarith [hbound]\n have h2 : (n : ℝ) ≤ 1 := by linarith [h1]\n have h3 : n ≤ 1 := by exact_mod_cast h2\n omega\n rw [hn1] at h2n\n have h4 : ‖s‖ = 2 := by\n rw [h2n]\n rw [show (-2 : ℂ) * ((1 : ℕ) : ℂ) = ((-2 : ℝ) : ℂ) by push_cast; ring,\n Complex.norm_real]\n norm_num\n rw [hs] at h4\n linarith [h4, hR]\n · push Not at hcase2\n exact absurd h rfl hsz\n -- the three regions\n by_cases hreg1 : 2 ≤ s.re\n · -- (i) the Dirichlet bound\n have h1 := norm_logDeriv_zeta_le_dirichlet hreg1\n linarith [h1, hnnR, dirichletC2_nonneg]\n · push Not at hreg1\n by_cases hreg2 : -5 / 2 ≤ s.re\n · -- (ii) the capstones + the near sum\n have ht10 : (10 : ℝ) ≤ |s.im| := by\n have hre25 : s.re ^ 2 ≤ 25 / 4 := by\n have h1 : -5 / 2 ≤ s.re ∧ s.re ≤ 2 := ⟨hreg2, hreg1.le⟩\n nlinarith [sq_nonneg s.re]\n have hRt : R - |s.im| ≤ (25 / 4) / R :=\n norm_circle_sub_abs_im_le hs hRpos hre25\n have h1 : (25 / 4 : ℝ) / R ≤ 1 := by\n rw [div_le_one hRpos]\n linarith [hR]\n have ht_le : |s.im| ≤ R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n linarith [hRt, h1, ht_le, hR]\n -- the near sum\n have hnear : ‖∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖\n ≤ 32 * C0hat (4 * (k : ℝ) + 9 / 2) *\n (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) := by\n calc ‖∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖\n ≤ ∑ ρ ∈ nearZeros s.im, ‖(zeroMult ρ : ℂ) / (s - ρ)‖ := norm_sum_le _ _\n _ = ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) / ‖s - ρ‖ := by\n apply Finset.sum_congr rfl\n intro ρ hρ\n rw [norm_div, RCLike.norm_natCast]\n _ ≤ ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) * (32 * C0hat (4 * (k : ℝ) + 9 / 2)) := by\n apply Finset.sum_le_sum\n intro ρ hρ\n have hsep := gapCircle_sep_of_mem_nearZeros hk hRlo hgap hs hρ\n rw [show (zeroMult ρ : ℝ) / ‖s - ρ‖ = (zeroMult ρ : ℝ) * (1 / ‖s - ρ‖) from by ring]\n apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n have h1 : (0 : ℝ) < 1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2)) := by positivity\n have h2 : (0 : ℝ) < ‖s - ρ‖ := by linarith [hsep, h1]\n exact (one_div_le_one_div_of_le h2 hsep).trans_eq (one_div_one_div _)\n _ = (32 * C0hat (4 * (k : ℝ) + 9 / 2)) * ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℝ) := by\n rw [← Finset.sum_congr rfl (g := fun ρ => (zeroMult ρ : ℝ) *\n (32 * C0hat (4 * (k : ℝ) + 9 / 2))) (fun ρ hρ => mul_comm _ _), Finset.mul_sum]\n _ ≤ (32 * C0hat (4 * (k : ℝ) + 9 / 2)) *\n (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) :=\n mul_le_mul_of_nonneg_left nearZeros_count_le (by positivity)\n have hlogmax : Real.log (3 * max |s.im - 1| |s.im + 1| + 5) ≤ 2 * Real.log R := by\n have hmax : max |s.im - 1| |s.im + 1| = |s.im| + 1 := by\n have ht_le : |s.im| ≤ R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n have h1 : |s.im + 1| ≤ |s.im| + 1 := abs_add_le _ _\n have h2 : |s.im - 1| ≤ |s.im| + 1 := by\n have h3 := abs_sub_le_iff.mp (abs_sub_abs_le_abs_sub s.im (-1 : ℝ))\n -- |s.im − 1| ≤ |s.im| + 1 via the triangle\n have h4 : s.im - 1 = s.im + (-1 : ℝ) := by ring\n rw [h4]\n exact abs_add_le _ _\n apply max_le_iff.mpr\n constructor\n · exact h2\n · exact h1\n all_goals try exact h1\n rw [hmax]\n have ht_le : |s.im| ≤ R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n have h1 : Real.log (3 * (|s.im| + 1) + 5) ≤ Real.log (4 * R) := by\n apply Real.log_le_log (by linarith [abs_nonneg s.im, hRpos])\n linarith [ht_le, hR]\n have h2 : Real.log (4 * R) = Real.log 4 + Real.log R :=\n Real.log_mul (by norm_num : (4 : ℝ) ≠ 0) (by linarith [hRpos] : R ≠ 0)\n have h3 : Real.log 4 ≤ Real.log R :=\n Real.log_le_log (by norm_num) (by linarith [hR])\n linarith [h1, h2, h3]\n -- the capstone difference\n have hcap : ‖logDeriv riemannZeta s - ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖\n ≤ 200000 * (Real.log |s.im|) ^ 2 := by\n by_cases hhalf : (1 : ℝ) / 2 ≤ s.re\n · exact logDeriv_riemannZeta_sub_nearZeros_le (t := s.im) ht10 rfl hhalf\n (by linarith [hreg1.le] : s.re ≤ 7 / 2) hζs\n · push Not at hhalf\n exact logDeriv_riemannZeta_sub_nearZeros_le_left (t := s.im) ht10 rfl hreg2\n (by linarith [hhalf] : s.re ≤ 1 / 2) hζs\n have hlogt : (Real.log |s.im|) ^ 2 ≤ (Real.log R) ^ 2 := by\n have ht_le : |s.im| ≤ R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n have h1 : Real.log |s.im| ≤ Real.log R :=\n Real.log_le_log (by linarith [ht10] : (0 : ℝ) < |s.im|) ht_le\n have h2 : (0 : ℝ) ≤ Real.log |s.im| :=\n Real.log_nonneg (by linarith [ht10] : (1 : ℝ) ≤ |s.im|)\n exact pow_le_pow_left₀ h2 h1 2\n calc ‖logDeriv riemannZeta s‖\n = ‖(logDeriv riemannZeta s - ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ))\n + ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖ := by\n rw [sub_add_cancel]\n _ ≤ ‖logDeriv riemannZeta s - ∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖\n + ‖∑ ρ ∈ nearZeros s.im, (zeroMult ρ : ℂ) / (s - ρ)‖ :=\n norm_add_le _ _\n _ ≤ 200000 * (Real.log |s.im|) ^ 2 +\n 32 * C0hat (4 * (k : ℝ) + 9 / 2) *\n (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5)) :=\n add_le_add hcap hnear\n _ ≤ dirichletC2 + 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n have h1 : 32 * C0hat (4 * (k : ℝ) + 9 / 2) *\n (3 * A0count * Real.log (3 * max |s.im - 1| |s.im + 1| + 5))\n ≤ 192 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n have h2 := mul_le_mul_of_nonneg_left hlogmax\n (mul_nonneg (mul_nonneg (by norm_num : (0 : ℝ) ≤ 32) hĈpos.le)\n (mul_nonneg (by norm_num : (0 : ℝ) ≤ 3) hA0))\n have h3 : 32 * C0hat (4 * (k : ℝ) + 9 / 2) * (3 * A0count * (2 * Real.log R))\n = 192 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * Real.log R := by ring\n have h4 : 192 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * Real.log R\n ≤ 192 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n apply mul_le_mul_of_nonneg_left _ (mul_nonneg (mul_nonneg (by norm_num) hA0) hĈpos.le)\n nlinarith [hlogR, hlogRnn]\n rw [h3] at h2\n exact h2.trans h4\n have h5 : 192 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2\n ≤ 300 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n apply mul_le_mul_of_nonneg_right _ (pow_two_nonneg _)\n apply mul_le_mul_of_nonneg_right _ hĈpos.le\n apply mul_le_mul_of_nonneg_right _ hA0\n norm_num\n nlinarith [hlogt, h1, h5, hlogRnn, dirichletC2_nonneg, pow_two_nonneg (Real.log R)]\n · -- (iii) the FE route\n push Not at hreg2\n -- pole-avoidance for s/2\n have hpoles : ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := by\n intro m hm\n by_cases him : s.im = 0\n · -- s real: s = −R, then R/2 = m contradicts the ℤ-clearance\n have hsR : s = (-R : ℝ) := by\n have hnormSq : ‖s‖ ^ 2 = s.re ^ 2 + s.im ^ 2 := by\n rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n ring\n rw [him, hs] at hnormSq\n have h1 : s.re ^ 2 = R ^ 2 := by\n have h2 : s.re ^ 2 + (0 : ℝ) ^ 2 = R ^ 2 := by\n have h3 : s.re ^ 2 + s.im ^ 2 = R ^ 2 := hnormSq\n rw [him] at h3\n linarith [h3]\n linarith [h1, h2]\n have h4 : s.re = -R := by\n have h5 : s.re ^ 2 - R ^ 2 = 0 := by linarith [h1]\n have h6 : (s.re - R) * (s.re + R) = 0 := by\n have h7 : s.re ^ 2 - R ^ 2 = (s.re - R) * (s.re + R) := by ring\n rw [h7] at h5\n exact h5\n rcases mul_eq_zero.mp h6 with h8 | h8\n · have h9 : s.re = R := by linarith [h8]\n linarith [h9, hreg2]\n · linarith [h8]\n apply Complex.ext_iff.mpr\n rw [h4, him]\n simp\n rw [hsR] at hm\n have hm2 : (m : ℝ) = R / 2 := by\n have h1 : (-(R : ℝ) : ℂ) / 2 = -(m : ℂ) := hm\n have h2 : (-(R : ℝ) : ℂ) / 2 = ((-R / 2 : ℝ) : ℂ) := by push_cast; ring\n rw [h2] at h1\n have h3 : (-R / 2 : ℝ) = -(m : ℝ) := by exact_mod_cast h1\n have h4 : (m : ℝ) = R / 2 := by linarith [h3]\n exact h4\n have hgap' := hgapInt (m : ℤ)\n have hcast : ((m : ℤ) : ℝ) = (m : ℝ) := by push_cast; ring\n rw [hcast, ← hm2] at hgap'\n rw [show R / 2 - R / 2 = (0 : ℝ) by ring, abs_zero] at hgap'\n norm_num at hgap'\n · exact hm (by\n have h1 : (s / 2).im ≠ 0 := by\n have h2 : (s / 2).im = s.im / 2 := by simp\n rw [h2]\n exact div_ne_zero him (two_ne_zero : (2 : ℝ) ≠ 0)\n have h3 : (-(m : ℂ)).im = 0 := by\n rw [Complex.neg_im, Complex.natCast_im]\n have h4 : (s / 2).im = (-(m : ℂ)).im := congrArg Complex.im hm\n rw [h3] at h4\n exact h1 h4)\n -- the FE identity\n have hG : Complex.Gammaℝ s ≠ 0 := by\n rw [ne_eq, Complex.Gammaℝ_eq_zero_iff]\n rintro ⟨m, hm⟩\n have h1 : s / 2 = -(m : ℂ) := by\n rw [hm]\n ring\n exact hpoles m h1\n have hG1 : Complex.Gammaℝ (1 - s) ≠ 0 := by\n rw [ne_eq, Complex.Gammaℝ_eq_zero_iff]\n rintro ⟨m, hm⟩\n have hre : ((1 - s) / 2).re = -(m : ℝ) := by\n have h1 : (1 - s) / 2 = -2 * (m : ℂ) / 2 := by rw [hm]; ring\n have h2 : (1 - s) / 2 = -(m : ℂ) := by\n rw [hm]\n ring\n have h3 := congrArg Complex.re h2\n rw [Complex.neg_re, Complex.natCast_re] at h3\n rw [h3]\n simp\n have hpos : (0 : ℝ) < ((1 - s) / 2).re := by\n have h1 : ((1 - s) / 2).re = (1 - s.re) / 2 := by simp [Complex.div_re]\n rw [h1]\n linarith [hreg2]\n rw [hre] at hpos\n have hmn : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg _\n linarith [hpos, hmn]\n have hζ1 : riemannZeta (1 - s) ≠ 0 := by\n apply riemannZeta_ne_zero_of_one_le_re\n · have h1 : (1 - s).re = 1 - s.re := by simp\n rw [h1]\n linarith [hreg2]\n · intro h\n have h2 : s = 0 := by\n have h3 : 1 - s = 1 := h\n have h4 : 1 - s + s = 1 + s := by rw [h3]\n rw [sub_add_cancel] at h4\n rw [h4] at *\n exact h4.symm\n rw [h2, norm_zero] at hs\n linarith [hs, hR]\n have hfe := logDeriv_zeta_fe (fun h => by rw [h, norm_zero] at hs; linarith [hs, hR])\n (fun h => by\n have h1 : s.re = 1 := by rw [h]; simp\n linarith [h1, hreg2])\n hG hζs (differentiableAt_Gammaℝ_of_not_neg_nat hpoles)\n (fun h => by\n have h1 : (1 - s) = 0 → s = 1 := by\n intro h2\n have h3 : 1 - s = 0 := h2\n have h4 : s = 1 := by\n have h5 : 1 - s + s = 0 + s := by rw [h3]\n rw [sub_add_cancel, zero_add] at h5\n exact h5.symm\n exact h4\n exact absurd (h1 h) (fun h6 => by\n have h7 : s.re = 1 := by rw [h6]; simp\n linarith [h7, hreg2]))\n (fun h => by\n have h1 : (1 - s) = 1 → s = 0 := by\n intro h2\n have h3 : 1 - s = 1 := h2\n have h4 : s = 0 := by\n have h5 : 1 - s + s = 1 + s := by rw [h3]\n rw [sub_add_cancel] at h5\n have h6 : 1 = 1 + s := h5\n have h7 : 1 - 1 = (1 + s) - 1 := by rw [h6]\n rw [sub_self, add_sub_cancel_left] at h7\n exact h7.symm\n exact h4\n exact absurd (h1 h) (fun h6 => by rw [h6, norm_zero] at hs; linarith [hs, hR]))\n hG1 hζ1\n (differentiableAt_Gammaℝ_of_not_neg_nat (fun m hm => by\n have hre : ((1 - s) / 2).re = (1 - s.re) / 2 := by simp [Complex.div_re]\n have h1 : (0 : ℝ) < ((1 - s) / 2).re := by rw [hre]; linarith [hreg2]\n have h2 : (-(m : ℂ)).re = -(m : ℝ) := by\n rw [Complex.neg_re, Complex.natCast_re]\n have h3 := congrArg Complex.re hm\n rw [hre, h2] at h3\n have hmn : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg _\n linarith [h1, h3, hmn]))\n -- the bracket bound\n have hbr1 : logDeriv Complex.Gammaℝ s\n = -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma (s / 2) :=\n logDeriv_Gammaℝ_eq_of_not_neg_nat hpoles\n have hbr2 : logDeriv Complex.Gammaℝ (1 - s)\n = -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2) :=\n logDeriv_Gammaℝ_eq_of_not_neg_nat (fun m hm => by\n have hre : ((1 - s) / 2).re = (1 - s.re) / 2 := by simp [Complex.div_re]\n have h1 : (0 : ℝ) < ((1 - s) / 2).re := by rw [hre]; linarith [hreg2]\n have h2 : (-(m : ℂ)).re = -(m : ℝ) := by\n rw [Complex.neg_re, Complex.natCast_re]\n have h3 := congrArg Complex.re hm\n rw [hre, h2] at h3\n have hmn : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg _\n linarith [h1, h3, hmn])\n have hψ1 : ‖Complex.digamma (s / 2)‖ ≤ 62 + 23 * Real.log (2 + R / 2) :=\n digamma_circle_le hs hgapInt hR\n have hψ2 : ‖Complex.digamma ((1 - s) / 2)‖ ≤ 48 + 23 * Real.log R := by\n have hre : ((1 - s) / 2).re = (1 - s.re) / 2 := by simp [Complex.div_re]\n have h1 : (1.75 : ℝ) ≤ ((1 - s) / 2).re := by rw [hre]; linarith [hreg2]\n have h2 := digamma_right_le h1\n have hnorm : ‖(1 - s) / 2‖ = ‖1 - s‖ / 2 := by\n rw [norm_div]\n have h3 : ‖(2 : ℂ)‖ = 2 := by\n rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h3]\n have hnorm1s : ‖1 - s‖ ≤ 1 + R := by\n calc ‖1 - s‖ ≤ ‖(1 : ℂ)‖ + ‖s‖ := norm_sub_le _ _\n _ = 1 + R := by rw [norm_one, hs]\n have hlogle : Real.log (2 + ‖(1 - s) / 2‖) ≤ Real.log R := by\n apply Real.log_le_log (by positivity)\n rw [hnorm]\n linarith [hnorm1s, hR]\n have hlog2w_nn : (0 : ℝ) ≤ Real.log (2 + ‖(1 - s) / 2‖) := by\n apply Real.log_nonneg\n have h3 : (0 : ℝ) ≤ ‖(1 - s) / 2‖ := norm_nonneg _\n linarith [h3]\n linarith [h2, hlogle, hlog2w_nn, hlogRnn]\n -- assemble case (iii)\n have hld1 : ‖logDeriv riemannZeta (1 - s)‖ ≤ dirichletC2 := by\n apply norm_logDeriv_zeta_le_dirichlet\n have h1 : (1 - s).re = 1 - s.re := by simp\n rw [h1]\n linarith [hreg2]\n rw [hfe]\n have hstep1 : ‖-logDeriv riemannZeta (1 - s)\n - (logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s))‖\n ≤ ‖logDeriv riemannZeta (1 - s)‖ +\n ‖logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s)‖ := by\n calc ‖-logDeriv riemannZeta (1 - s)\n - (logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s))‖\n ≤ ‖-logDeriv riemannZeta (1 - s)‖ +\n ‖logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s)‖ :=\n norm_sub_le _ _\n _ = ‖logDeriv riemannZeta (1 - s)‖ +\n ‖logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s)‖ := by\n rw [norm_neg]\n have hbracket : ‖logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s)‖\n ≤ 2 + (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2 := by\n rw [hbr1, hbr2]\n have h1 : -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma (s / 2) +\n (-(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2))\n = -(Real.log Real.pi : ℂ) +\n ((1 / 2 : ℂ) * Complex.digamma (s / 2) +\n (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2)) := by ring\n rw [h1]\n calc ‖-(Real.log Real.pi : ℂ) +\n ((1 / 2 : ℂ) * Complex.digamma (s / 2) +\n (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2))‖\n ≤ ‖(Real.log Real.pi : ℂ)‖ +\n ‖(1 / 2 : ℂ) * Complex.digamma (s / 2) +\n (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2)‖ := by\n have h2 := norm_add_le (-(Real.log Real.pi : ℂ))\n ((1 / 2 : ℂ) * Complex.digamma (s / 2) +\n (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2))\n rw [norm_neg] at h2\n exact h2\n _ ≤ 2 + ((62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2) := by\n have hlogpi : ‖(Real.log Real.pi : ℂ)‖ ≤ 2 := by\n have h1 := log_pi_le_two\n have hpos : (0 : ℝ) < Real.log Real.pi :=\n Real.log_pos (by linarith [Real.pi_gt_three] : (1 : ℝ) < Real.pi)\n rw [show ((Real.log Real.pi : ℂ)) = ((Real.log Real.pi : ℝ) : ℂ) from rfl,\n Complex.norm_real, Real.norm_eq_abs, abs_of_pos hpos]\n exact h1\n have hψ : ‖(1 / 2 : ℂ) * Complex.digamma (s / 2) +\n (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2)‖\n ≤ (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2 := by\n calc ‖(1 / 2 : ℂ) * Complex.digamma (s / 2) +\n (1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2)‖\n ≤ ‖(1 / 2 : ℂ) * Complex.digamma (s / 2)‖ +\n ‖(1 / 2 : ℂ) * Complex.digamma ((1 - s) / 2)‖ := norm_add_le _ _\n _ = ‖Complex.digamma (s / 2)‖ / 2 + ‖Complex.digamma ((1 - s) / 2)‖ / 2 := by\n have h1 : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by\n rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by push_cast; ring,\n Complex.norm_real]\n norm_num\n rw [norm_mul, h1, norm_mul, h1]\n ring\n _ ≤ (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2 := by\n have h1 := div_le_div_of_nonneg_right hψ1 (by norm_num : (0 : ℝ) ≤ 2)\n have h2 := div_le_div_of_nonneg_right hψ2 (by norm_num : (0 : ℝ) ≤ 2)\n have h3 : ‖Complex.digamma (s / 2)‖ / 2\n ≤ (62 + 23 * Real.log (2 + R / 2)) / 2 := h1\n have h4 : ‖Complex.digamma ((1 - s) / 2)‖ / 2\n ≤ (48 + 23 * Real.log R) / 2 := h2\n linarith [h3, h4]\n linarith [hlogpi, hψ]\n _ = 2 + (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2 := by ring\n have hlog2R : Real.log (2 + R / 2) ≤ Real.log R := by\n apply Real.log_le_log (by linarith [hRpos] : (0 : ℝ) < 2 + R / 2)\n linarith [hR]\n calc ‖-logDeriv riemannZeta (1 - s)\n - (logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s))‖\n ≤ ‖logDeriv riemannZeta (1 - s)‖ +\n ‖logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s)‖ := hstep1\n _ ≤ dirichletC2 + (2 + (62 + 23 * Real.log (2 + R / 2)) / 2 +\n (48 + 23 * Real.log R) / 2) := add_le_add hld1 hbracket\n _ ≤ dirichletC2 + 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n have h1 : 2 + (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2\n ≤ 100 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n have h2 : 2 + (62 + 23 * Real.log (2 + R / 2)) / 2 + (48 + 23 * Real.log R) / 2\n ≤ 57 + 23 * Real.log R := by\n have h3 := div_le_div_of_nonneg_right\n (show Real.log (2 + R / 2) ≤ Real.log R from hlog2R)\n (by norm_num : (0 : ℝ) ≤ 2)\n nlinarith [hlog2R, hlogRnn, Real.log_nonneg (show (1 : ℝ) ≤ 2 + R / 2 from by\n linarith [hRpos])]\n have h4 : (57 : ℝ) + 23 * Real.log R\n ≤ 100 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n have h5 : (1 : ℝ) ≤ A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2 := by\n have h6 : (81 : ℝ) ≤ (Real.log R) ^ 2 := by nlinarith [hlogR, hlogRnn]\n have h7 : (2 : ℝ) ≤ A0count * C0hat (4 * (k : ℝ) + 9 / 2) :=\n le_trans hĈ2 (mul_le_mul_of_nonneg_left (by linarith [hĈ2] :\n (1 : ℝ) ≤ C0hat (4 * (k : ℝ) + 9 / 2)) hA0)\n nlinarith [h6, h7, hA0, hĈpos]\n nlinarith [h5, hlogRnn, hA0, hĈpos]\n linarith [h2, h4]\n nlinarith [h1, hnnR, dirichletC2_nonneg]\n\n/-- **The Fexpr circle bound**: ‖Fexpr s‖ ≤ 2·lowZeroConst +\ndirichletC2 + 400000·A₀·Ĉ₀(R+2)·(log R)². -/\ntheorem Fexpr_circle_le {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}\n (hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R) (hRhi : R ≤ 4 * (k : ℝ) + 3)\n (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →\n 1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)\n (hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|)\n {s : ℂ} (hs : ‖s‖ = R) :\n ‖Fexpr s‖ ≤ 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n classical\n have hsz : ¬ IsNontrivialZero s :=\n not_isNontrivialZero_on_gapCircle hk hRlo hgap hs\n have hĈ2 : (2 : ℝ) ≤ C0hat (4 * (k : ℝ) + 9 / 2) := two_le_C0hat (by\n have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast (by omega : 1 ≤ k)\n linarith)\n have hR : (16002 : ℝ) ≤ R := by\n have hkR : (16000 : ℝ) ≤ 4 * (k : ℝ) := by\n have h1 : (4000 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk\n linarith\n linarith [hRlo]\n have hRpos : (0 : ℝ) < R := by linarith [hR]\n have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR\n have hlogRnn : (0 : ℝ) ≤ Real.log R := by linarith [hlogR]\n have hA0 := A0count_pos.le\n have hĈR2 : C0hat (4 * (k : ℝ) + 9 / 2) ≤ C0hat (R + 2) :=\n C0hat_mono (by linarith [hRlo] : (1 : ℝ) ≤ 4 * (k : ℝ) + 9 / 2)\n (by linarith [hRlo] : 4 * (k : ℝ) + 9 / 2 ≤ R + 2)\n have hĈR2pos : (0 : ℝ) < C0hat (R + 2) := by linarith [hĈ2, hĈR2]\n -- the pieces\n have hser := seriesFun_norm_le_gapCircle hk hRlo hgap hs\n have hld := logDeriv_circle_le hk hRlo hgap hgapInt hs hsz\n have hψ := digamma_circle_le hs hgapInt hR\n have h1s := norm_one_div_le_of_norm_eq hs (by linarith [hR] : (1 : ℝ) ≤ R)\n have h1s1 := norm_one_div_sub_one_le_of_norm_eq hs (by linarith [hR] : (2 : ℝ) ≤ R)\n have hlogpi := norm_logPi_div_two_le\n -- the norm chain: Fexpr = logDeriv ζ − seriesFun + 1/s + 1/(s−1) − (log π)/2 + ψ(s/2)/2\n have hchain : ‖Fexpr s‖ ≤ ‖logDeriv riemannZeta s‖ + ‖seriesFun s‖ +\n ‖(1 : ℂ) / s‖ + ‖(1 : ℂ) / (s - 1)‖ + ‖(Real.log Real.pi : ℂ) / 2‖ +\n ‖Complex.digamma (s / 2) / 2‖ := by\n rw [Fexpr]\n calc ‖logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2‖\n ≤ ‖logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2‖ + ‖Complex.digamma (s / 2) / 2‖ :=\n norm_add_le _ _\n _ ≤ ‖logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)‖\n + ‖(Real.log Real.pi : ℂ) / 2‖ + ‖Complex.digamma (s / 2) / 2‖ :=\n add_le_add_right (norm_sub_le _ _) _\n _ ≤ ‖logDeriv riemannZeta s - seriesFun s + 1 / s‖ + ‖(1 : ℂ) / (s - 1)‖\n + ‖(Real.log Real.pi : ℂ) / 2‖ + ‖Complex.digamma (s / 2) / 2‖ :=\n add_le_add_right (add_le_add_right (norm_add_le _ _) _) _\n _ ≤ ‖logDeriv riemannZeta s - seriesFun s‖ + ‖(1 : ℂ) / s‖ + ‖(1 : ℂ) / (s - 1)‖\n + ‖(Real.log Real.pi : ℂ) / 2‖ + ‖Complex.digamma (s / 2) / 2‖ :=\n add_le_add_right (add_le_add_right (add_le_add_right (norm_add_le _ _) _) _) _\n _ ≤ ‖logDeriv riemannZeta s‖ + ‖seriesFun s‖ + ‖(1 : ℂ) / s‖ + ‖(1 : ℂ) / (s - 1)‖\n + ‖(Real.log Real.pi : ℂ) / 2‖ + ‖Complex.digamma (s / 2) / 2‖ := by\n apply add_le_add_right\n apply add_le_add_right\n apply add_le_add_right\n apply add_le_add_right\n exact norm_sub_le _ _\n -- the ψ term: ‖ψ(s/2)/2‖ = ‖ψ(s/2)‖/2\n have hψnorm : ‖Complex.digamma (s / 2) / 2‖ = ‖Complex.digamma (s / 2)‖ / 2 := by\n rw [norm_div]\n have h1 : ‖(2 : ℂ)‖ = 2 := by\n rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h1]\n -- assemble\n have hbig : ‖logDeriv riemannZeta s‖ + ‖seriesFun s‖ + ‖(1 : ℂ) / s‖ +\n ‖(1 : ℂ) / (s - 1)‖ + ‖(Real.log Real.pi : ℂ) / 2‖ + ‖Complex.digamma (s / 2) / 2‖\n ≤ 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have hser2 : ‖seriesFun s‖ ≤ 2 * lowZeroConst +\n 2900 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have h1 : 2900 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2\n ≤ 2900 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 :=\n mul_le_mul_of_nonneg_right\n (mul_le_mul_of_nonneg_left hĈR2 hA0) (pow_two_nonneg _)\n linarith [hser, h1]\n have hld2 : ‖logDeriv riemannZeta s‖ ≤ dirichletC2 + 200000 * (Real.log R) ^ 2 +\n 300 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have h1 : 300 * A0count * C0hat (4 * (k : ℝ) + 9 / 2) * (Real.log R) ^ 2\n ≤ 300 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 :=\n mul_le_mul_of_nonneg_right\n (mul_le_mul_of_nonneg_left hĈR2 hA0) (pow_two_nonneg _)\n linarith [hld, h1]\n have hψ2 : ‖Complex.digamma (s / 2) / 2‖ ≤ 31 + 12 * Real.log R := by\n rw [hψnorm]\n have hlog2R : Real.log (2 + R / 2) ≤ Real.log R := by\n apply Real.log_le_log (by linarith [hRpos] : (0 : ℝ) < 2 + R / 2)\n linarith [hR]\n have h1 : (62 + 23 * Real.log (2 + R / 2)) / 2\n ≤ (62 + 23 * Real.log R) / 2 :=\n div_le_div_of_nonneg_right (add_le_add_left\n (mul_le_mul_of_nonneg_left hlog2R (by norm_num : (0 : ℝ) ≤ 23)) _) (by norm_num)\n have h2 := div_le_div_of_nonneg_right hψ (by norm_num : (0 : ℝ) ≤ 2)\n linarith [h1, h2, hlogRnn]\n have h1 : 2900 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 +\n (200000 * (Real.log R) ^ 2 + 300 * A0count * C0hat (R + 2) * (Real.log R) ^ 2) +\n ((31 + 12 * Real.log R) + 2)\n ≤ 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have h2 : (2 : ℝ) ≤ A0count * C0hat (R + 2) :=\n le_trans hĈ2 (le_trans hĈR2 (le_refl _))\n have h3 : (81 : ℝ) ≤ (Real.log R) ^ 2 := by nlinarith [hlogR, hlogRnn]\n have h4 : (1 : ℝ) ≤ A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n nlinarith [h2, h3, hA0, hĈR2pos]\n have h5 : 200000 * (Real.log R) ^ 2\n ≤ 100000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have h6 : (2 : ℝ) ≤ A0count * C0hat (R + 2) := h2\n nlinarith [h6, pow_two_nonneg (Real.log R)]\n nlinarith [h5, h4, h2, h3, hlogRnn, hA0, hĈR2pos]\n linarith [hser2, hld2, hψ2, h1s, h1s1, hlogpi, h1, lowZeroConst_nonneg,\n dirichletC2_nonneg]\n exact hchain.trans hbig\n\nend NguyenRH1\n\nend"},"extra_content":null}]