← Session 31 — ii′-5f: tight R-bound 10.5/48 (piece 3 + pinch)
thinking (11572 chars)
Committed §17. Now §18 (right tail). Let me write it following §17's structure with the adjustments:
1. farGRight t ρ := if (Nat.floor t + 1 ≤ |ρ.1.im − t| ∧ t ≤ ρ.1.im) then farG t ρ else 0.
Hmm — the condition (⌊t⌋₊+1 ≤ x ∧ t ≤ γ). For the fiber-count, I need the γ-side condition for the window: t ≤ γ.
2. farGRight_nonneg, farGRight_summable.
3. farGRight_term_le : farGRight t ρ ≤ 4.5·farW(⌊x⌋₊)·m — via farG_le_farW_mul (needs x ≥ 1 for nonzero elements).
4. farGRight_fiber_finite (k): the fiber {⌊|ρ.1.im − t|⌋₊ = k} finite.
5. farGRight_fiber_count (k ≥ ⌊t⌋₊+1): ∑_{fiber ∩ {t ≤ γ}} m ≤ C0hat(2k+1) — via zeroWindow (t+k) + hZC + C0hat_mono(t+k+1 ≤ 2k+1) + C0hat_two_mul_add_one_le (k ≥ 11).
6. farGRight_fiber_le (ENNReal per-fiber, if-form: if ⌊t⌋₊+1 ≤ k then 4.5·farW k·C0hat(2k+1) else 0).
7. The combo series: farGRightMaj k := if ⌊t⌋₊+1 ≤ k then 4.5·farW k·C0hat(2k+1) else 0; the combo bound form farGRightMajCombo k := 4.5·(1/(k:ℝ)^2)·[0.433·(log k+0.833)+0.886·(loglog k+0.3475)+2.9] — hmm — 1/k² with k = 0: 1/0 = 0 ✓ nonneg.
Pointwise: farGRightMaj k ≤ farGRightMajCombo k: for k < ⌊t⌋₊+1: 0 ≤ combo (bridge nonneg ✓ need the loglog ≥ −0.37 lemma); for k ≥ ⌊t⌋₊+1: farW k ≤ 1/k² (farW_le_inv_sq, k ≥ 1 ✓) and C0hat(2k+1) ≤ bridge (C0hat_two_mul_add_one_le, k ≥ 11 ✓).
8. The shifted series: ∑' (fun k => farGRightMajCombo (k+11)) — decompose: = 4.5·[0.433·(0.833·W₀+W₁)+0.886·(0.3475·W₀+W₂)+2.9·W₀] via the RW₀/1/2 bricks (paren-grouped!). Need: log(k+11)+0.833 = the RW₁'s log(k+11) — the 0.433·(log(k+11)+0.833)/(k+11)² = 0.433·log(k+11)/(k+11)² + 0.433·0.833/(k+11)² ✓; 0.886·(loglog(k+11)+0.3475)/(k+11)² = 0.886·loglog(k+11)/(k+11)² + 0.886·0.3475/(k+11)² ✓; 2.9/(k+11)² ✓. So farGRightMajCombo (k+11) = 4.5·[(0.433·0.833+0.886·0.3475+2.9)/(k+11)² + 0.433·log(k+11)/(k+11)² + 0.886·loglog(k+11)/(k+11)²] — the combo form ✓ summable via the RW-brick summables (tail11_inv_sq_summable — EXISTS? I have tail11_log_div_sq_summable (standalone ✓); tail11_inv_sq: the antitone machine exists (antitoneOn_one_div_sq + integrableOn_one_div_sq) — make tail11_inv_sq_summable standalone; tail11_loglog: the inline hsumm from RW₂ — make standalone).
9. farGRightMaj_series_le: ∑' farGRightMaj = ∑' (fun k => farGRightMaj (k+11)) (range-11 part = 0 since ⌊t⌋₊ ≥ 10 ⟹ ⌊t⌋₊+1 ≥ 11 ✓) ≤ ∑' (fun k => farGRightMajCombo (k+11)) (pointwise ✓ summable ✓) ≤ 4.5·[0.433·(0.833·W₀+W₁)+0.886·(0.3475·W₀+W₂)+2.9·W₀].
Wait — the pointwise comparison farGRightMaj (k+11) ≤ farGRightMajCombo (k+11): for the shifted family: k+11 ≥ 11 > ⌊t⌋₊?? — NO: k+11 vs ⌊t⌋₊+1: if t = 20, ⌊t⌋₊+1 = 21: for k+11 < 21 (k < 10): farGRightMaj (k+11) = 0 ≤ combo ✓; k+11 ≥ 21: farW ≤ 1/k² + bridge ✓. ✓ pointwise holds for all k.
10. farGRight_le (the outer assembly).
Also the final piece-3 assembly (§19):
```
theorem far_series_le (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t)
{s : ℂ} (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t)
(hζ : riemannZeta s ≠ 0) :
‖∑' ρ, if ρ ∈ nearZerosSub t then (0:ℂ) else seriesDiffTerm s (2+tI) ρ‖
≤ 12.1284 * C0hat (t+1) + 7.2425 := by
-- norm ≤ farG tsum (far_series_norm_le_farG_tsum)
-- tsum split: main + (if ∉ main)
-- (if ∉ main) = farGRight + farGLeft (pointwise, with hNLZ)
-- main ≤ farG_main_le; right ≤ farGRight_le; left ≤ farGLeft_le
-- fold: 4.5·(2C₀+0.55)·1.3476 + Tail_R + Tail_L ≤ 12.1284·C₀ + 7.2425
```
The arithmetic fold: 4.5·(2C₀+0.55)·1.3476 = 12.1284·C₀ + 3.33531 (4.5·0.55·1.3476 = 3.33531); Tail_R = 4.5·[0.433·(0.833·0.1+0.3303)+0.886·(0.3475·0.1+0.1216)+2.9·0.1] = 4.5·[0.433·0.4136+0.886·0.15625+0.29] = 4.5·[0.17909+0.13844+0.29] = 4.5·0.60753 = 2.73389; Tail_L = 4.5·0.26064 = 1.17288. Sum: 3.33531+2.73389+1.17288 = 7.24208 ≤ 7.2425 ✓. And 4.5·2·1.3476 = 12.1284 ✓.
Let me verify Tail_R numerically: 0.433·0.4136 = 0.179088; 0.886·(0.3475·0.1+0.1216) = 0.886·(0.03475+0.1216) = 0.886·0.15635 = 0.138526; sum = 0.179088+0.138526+0.29 = 0.607614; ×4.5 = 2.734263. Tail_L: 0.433·(0.1942/23+0.1687)+0.886·(0.0736/23+0.0621)+2.9/23: 0.1942/23 = 0.0084435; 0.433·0.17694 = 0.076615; 0.0736/23 = 0.0032; 0.886·0.0653 = 0.057856; 2.9/23 = 0.126087; sum = 0.260558; ×4.5 = 1.172511. Total: 3.33531+2.734263+1.172511 = 7.242084 ≤ 7.2425 ✓ (margin 4.2e-4).
Hmm wait — my RW₂ brick is ≤ 0.1216 and I computed 0.886·(0.03475+0.1216) = 0.138526 — and earlier "Tail_R = 2.73393" from the design check — consistent ✓.
Now — the summables I need standalone: tail11_inv_sq_summable + tail11_loglog_div_sq_summable (mirror the tail14 versions). Let me write §18 + §19 (assembly) now. This is the final stretch of piece 3 — then 5f-iii remains (assembly of ALL pieces + pinch + capstone), which is a separate sub-stage.
For §18, careful with:
- The farGRightMajCombo decomposition with PARENS: 0.433·(log(k+11)/(k+11)²) — write 0.433 * (Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2).
- The RW-brick forms: W₀ = ∑' (fun k => 1/((k:ℝ)+11)^2), W₁ = ∑' (fun k => Real.log ((k:ℝ)+11)/((k:ℝ)+11)^2) — hmm the RW₁ brick family is `Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2` — the combo's term `0.433 * (Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2)` ✓ paren ✓.
- W₂ = ∑' (fun k => Real.log (Real.log ((k:ℝ)+11)) / ((k:ℝ)+11)^2) ✓.
farGRightMajComboShift k := 4.5 * ((0.433*0.833+0.886*0.3475+2.9) * (1/(((k:ℝ)+11)^2)) + 0.433 * (Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2) + 0.886 * (Real.log (Real.log ((k:ℝ)+11)) / ((k:ℝ)+11)^2))
Hmm wait — the farGRightMajCombo (k+11) should equal that: 4.5·(1/((k+11):ℝ)²)·[0.433·(log(k+11)+0.833)+0.886·(loglog(k+11)+0.3475)+2.9] — the decomposition: 0.433·(log X+0.833)/X² + 0.886·(loglog X+0.3475)/X² + 2.9/X² with X = (k:ℝ)+11 = 0.433·log X/X² + 0.433·0.833/X² + 0.886·loglog X/X² + 0.886·0.3475/X² + 2.9/X². So farGRightMajCombo (k+11) = 4.5·[(0.433·0.833+0.886·0.3475+2.9)/X² + 0.433·log X/X² + 0.886·loglog X/X²] ✓ — via ring after the paren-forms... The equality needs the div-grouping — prove farGRightMajCombo_eq (k) : farGRightMajCombo (k+11) = 4.5·(combo-sum) via ring (with parens already right, ring is safe).
Hmm — actually farGRightMajCombo is the function of a real k cast — define it as a def:
def farGRightMajCombo (k : ℕ) : ℝ := 4.5 * (1/(k:ℝ)^2) * (0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9)
Then farGRightMajCombo (k+11) — with ((k+11:ℕ):ℝ) = (k:ℝ)+11 bridge ✓.
And the pointwise farGRightMaj k ≤ farGRightMajCombo k:
```
lemma farGRightMaj_le_combo {t : ℝ} (ht : 10 ≤ t) (k : ℕ) :
farGRightMaj t k ≤ farGRightMajCombo k := by
by_cases hk : Nat.floor t + 1 ≤ k
· rw [farGRightMaj, if_pos hk]
-- 4.5·farW k·C0hat(2k+1) ≤ 4.5·(1/k²)·[bridge]
have hk11 : 11 ≤ k := by
have h1 : 10 ≤ Nat.floor t := Nat.floor_mono (by norm_num : (10:ℝ) ≤ t)
... — Nat.floor 10 = 10: Nat.floor_ofNat : ⌊(10:ℝ)⌋₊ = 10 — h1 : ⌊10⌋₊ ≤ ⌊t⌋₊: rw [Nat.floor_ofNat] at h1: 10 ≤ ⌊t⌋₊ ✓ then hk: ⌊t⌋₊+1 ≤ k ⟹ k ≥ 11 ✓ omega.
have h1 := C0hat_two_mul_add_one_le hk11
have h2 := farW_le_inv_sq (by omega : 1 ≤ k)
have hnn : 0 ≤ the-bridge
calc 4.5 * farW k * C0hat (2*(k:ℝ)+1)
≤ 4.5 * (1/(k:ℝ)^2) * (0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9) := by
apply mul_le_mul _ _ _ _
· apply mul_le_mul_of_nonneg_left h2 (by norm_num : (0:ℝ) ≤ 4.5)
· exact h1
· exact bridge-nonneg
· positivity
· rw [farGRightMaj, if_neg hk]
exact farGRightMajCombo_nonneg k
```
The bridge-nonneg lemma:
```
lemma farGRightBridge_nonneg (k : ℕ) :
0 ≤ 0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by
-- log k ≥ 0 (k ≥ 1) or junk 0 (k = 0); loglog k ≥ −0.37
...
```
loglog-nonneg: for k = 0: log 0 = 0 (Real.log_zero), loglog = log 0 = 0 ✓ bridge = 0.433·0.833+0.886·0.3475+2.9 ≥ 0 ✓ norm_num. For k ≥ 1: log k ≥ 0 ✓; loglog k ≥ −0.37: k = 1: loglog 1 = log 0 = 0 ✓; k ≥ 2: log k ≥ log 2 ≥ 0.69314 (log_two_gt_d9): loglog k ≥ log 0.693 ≥ −0.37 (the e^{0.37} argument).
```
lemma loglog_ge_neg_point37 (k : ℕ) (hk : 1 ≤ k) :
-0.37 ≤ Real.log (Real.log k) := by
rcases eq_or_ne k 1 with rfl | hk1
· simp [Real.log_one, Real.log_zero]
· have hk2 : 2 ≤ k := by omega
have h1 : (0.693 : ℝ) ≤ Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)
have h2 : (0.693 : ℝ) ≤ Real.log k := by
have h3 : Real.log 2 ≤ Real.log k := Real.log_le_log (by norm_num) (by exact_mod_cast hk2)
linarith [h1, h3]
have h4 : Real.log 0.693 ≤ Real.log (Real.log k) :=
Real.log_le_log (by norm_num : (0:ℝ) < 0.693) h2
-- log 0.693 ≥ −0.37 ⟺ 0.693 ≥ e^{−0.37} ⟺ e^{0.37} ≥ 0.693⁻¹ = 1.44300
have h5 : Real.log 0.693 ≥ -0.37 := by
have h6 : (1 / 0.693 : ℝ) ≤ Real.exp 0.37 := by
have h7 := Real.sum_le_exp_of_nonneg (show (0:ℝ) ≤ 0.37 by norm_num) 5
rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,
Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h7
norm_num at h7
-- Σ_{k<5} 0.37^k/k! = 1.447671 ≥ 1/0.693 = 1.443002
have h8 : (1 / 0.693 : ℝ) ≤ 1.447671 := by norm_num
linarith [h7, h8]
have h7 : Real.log (1 / 0.693) ≤ 0.37 := by
have h8 := Real.log_le_log (by norm_num : (0:ℝ) < 1/0.693) h6
rwa [Real.log_exp] at h8
rw [Real.log_div (by norm_num : (1:ℝ) ≠ 0) (by norm_num : (0.693:ℝ) ≠ 0)] at h7
-- log(1/0.693) = log 1 − log 0.693 = −log 0.693 ≤ 0.37 ⟹ log 0.693 ≥ −0.37
have h9 : Real.log 0.693 ≥ -0.37 := by
have h10 : Real.log 1 = 0 := Real.log_one
linarith [h7, h10]
exact h9
linarith [h4, h5]
```
Hmm — Real.log_div gives log(1/0.693) = log 1 − log 0.693 ✓ then log 0.693 ≥ −0.37 ✓.
And the nonneg assembly in farGRightBridge_nonneg:
```
by_cases hk0 : k = 0
· rw [hk0]
simp [Real.log_zero]
norm_num
· have hk1 : 1 ≤ k := by omega
have h1 : (0 : ℝ) ≤ Real.log k := Real.log_nonneg (by exact_mod_cast hk1 : (1:ℝ) ≤ (k:ℝ))
have h2 := loglog_ge_neg_point37 k hk1
have h3 : (0.433*0.833 : ℝ) = 0.360889 := by norm_num
have h4 : (0.886*0.3475 : ℝ) = 0.307985 := by norm_num
-- 0.433·(log k + 0.833) ≥ 0.433·0.833; 0.886·(loglog k + 0.3475) ≥ 0.886·(−0.37+0.3475)
nlinarith [h1, h2, Real.log_nonneg (by norm_num : (1:ℝ) ≤ 2.9)]
```
Hmm — nlinarith with products of (log k) atoms: 0.433·(log k+0.833) ≥ 0 needs log k ≥ −0.833 ✓ (log k ≥ 0 for k ≥ 1). And 0.886·(loglog k + 0.3475) ≥ 0.886·(−0.37+0.3475) = 0.886·(−0.0225) = −0.019935: total ≥ 0.433·0.833 + (−0.019935) + 2.9 = 0.360889−0.019935+2.9 = 3.240954 ≥ 0 ✓. linarith with the pieces as atoms: h1 : 0 ≤ log k; h2 : −0.37 ≤ loglog k: 0.433·(log k + 0.833) ≥ 0.433·0.833 (linarith with h1 ✓ linear in atom log k) and 0.886·(loglog k + 0.3475) ≥ 0.886·(−0.0225) (linear ✓): sum ≥ 0.360889−0.019935+2.9 = 3.240954 ≥ 0 ✓ linarith [h1, h2] should do it (linear in the two atoms) ✓.
OK — also the per-fiber machinery mirroring §17. Let me write §18 now (big). And §19 (assembly) after.
One more check — farGRight_fiber_count: for k ≥ ⌊t⌋₊+1, the fiber-filtered set (t ≤ γ): image ⊆ zeroWindow (t+k): γ = t+x with x ∈ [k, k+1) ⟹ γ ∈ [t+k, t+k+1) ✓ (zeroWindow closed [t+k, t+k+1] ✓). count ≤ C0hat(t+k+1) via hZC (t+k ≥ 2: t ≥ 10, k ≥ 0 ✓). Then C0hat(t+k+1) ≤ C0hat(2k+1): C0hat_mono (1 ≤ t+k+1) (t+k+1 ≤ 2k+1 ⟺ t ≤ k ✓ k ≥ ⌊t⌋₊+1 > t ✓). Then C0hat(2k+1) — no further bound needed at the fiber level (the combo-form enters at the series level) ✓ — wait — the per-fiber bound's majorant: 4.5·farW k·C0hat(2k+1) ✓ (the farGRightMaj if-form's value for k ≥ ⌊t⌋₊+1) ✓ consistent.
Now write §18.
Now §18 (3e-ii: the right-tail machine). Writing it with the paren discipline learned.
tool: Edit
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean",
"old_string": " _ \u2264 ENNReal.ofReal (4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23))) :=\n ENNReal.ofReal_le_ofReal farGLeftMaj_series_le\n\nend NguyenRH1\n\nend",
"new_string": " _ \u2264 ENNReal.ofReal (4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23))) :=\n ENNReal.ofReal_le_ofReal farGLeftMaj_series_le\n\n/-! ## 18. Piece 3j: the right-tail machine (\u03b3 > 2t) -/\n\n/-- The right-tail summand: farG restricted to tail zeros (x \u2265 \u230at\u230b\u208a+1)\non the right side (\u03b3 \u2265 t, hence \u03b3 > 2t). -/\ndef farGRight (t : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u211d :=\n if (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im) then farG t \u03c1 else 0\n\nlemma farGRight_nonneg (t : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : (0 : \u211d) \u2264 farGRight t \u03c1 := by\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n exact farG_nonneg t \u03c1\n \u00b7 rw [farGRight, if_neg h]\n\nlemma farGRight_summable {t : \u211d} (ht : 0 \u2264 t) : Summable (farGRight t) := by\n apply Summable.of_norm_bounded (farG_summable ht)\n intro \u03c1\n rw [Real.norm_eq_abs, abs_of_nonneg (farGRight_nonneg t \u03c1)]\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n \u00b7 rw [farGRight, if_neg h]\n exact farG_nonneg t \u03c1\n\n/-- The per-element right-tail bound: farGRight \u2264 4.5\u00b7farW(\u230ax\u230b\u208a)\u00b7m. -/\nlemma farGRight_term_le {t : \u211d} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n farGRight t \u03c1 \u2264 4.5 * farW (Nat.floor |\u03c1.1.im - t|) * (zeroMult \u03c1.1 : \u211d) := by\n classical\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n have hx1 : (1 : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h1 : (1 : \u211d) \u2264 (Nat.floor t : \u211d) + 1 := by\n have h2 : (0 : \u211d) \u2264 (Nat.floor t : \u211d) := Nat.floor_nonneg\n linarith\n have h3 : (Nat.floor t : \u211d) + 1 \u2264 |\u03c1.1.im - t| := by\n have h4 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 |\u03c1.1.im - t| := by exact_mod_cast h.1\n have h5 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h5] at h4\n linarith [h1, h3]\n exact farG_le_farW_mul \u03c1 hx1\n \u00b7 rw [farGRight, if_neg h]\n positivity\n\n/-- The right-tail fiber {\u230ax\u230b\u208a = k} is finite. -/\nlemma farGRight_fiber_finite {t : \u211d} (ht : 0 \u2264 t) (k : \u2115) :\n ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k} :\n Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1}).Finite := by\n apply (finite_subtype_norm_lt (t + (k : \u211d) + 2)).subset\n intro \u03c1 h\u03c1\n show \u2016\u03c1.1\u2016 < t + (k : \u211d) + 2\n have hmem : Nat.floor |\u03c1.1.im - t| = k := h\u03c1\n have h1 : |\u03c1.1.im - t| < (k : \u211d) + 1 := by\n have h2 := Nat.lt_floor_add_one |\u03c1.1.im - t|\n rwa [hmem] at h2\n have hle : \u2016\u03c1.1\u2016 \u2264 |\u03c1.1.re| + |\u03c1.1.im| := Complex.norm_le_abs_re_add_abs_im _\n have hre : |\u03c1.1.re| \u2264 1 := by\n have h3 : 0 < \u03c1.1.re := \u03c1.2.2.1\n have h4 : \u03c1.1.re < 1 := \u03c1.2.2.2\n rw [abs_le]\n constructor <;> linarith\n have him : |\u03c1.1.im| \u2264 t + |\u03c1.1.im - t| := by\n calc |\u03c1.1.im| = |\u03c1.1.im - t + t| := by rw [sub_add_cancel]\n _ \u2264 |\u03c1.1.im - t| + |t| := abs_add_le _ _\n _ = |\u03c1.1.im - t| + t := by rw [abs_of_nonneg ht]\n _ = t + |\u03c1.1.im - t| := by ring\n linarith [hle, hre, him, h1]\n\n/-- **The per-fiber right-tail count**: the mult-weighted count of\nright-tail zeros with bucket k (\u230at\u230b\u208a+1 \u2264 k) is \u2264 C0hat(2k+1). -/\nlemma farGRight_fiber_count (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t)\n {k : \u2115} (hk : Nat.floor t + 1 \u2264 k) :\n \u2211 \u03c1 \u2208 (farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k).toFinset.filter\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im), (zeroMult \u03c1.1 : \u211d)\n \u2264 C0hat (2 * (k : \u211d) + 1) := by\n classical\n set FS := (farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k).toFinset.filter\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im) with hFS\n have hk11 : 11 \u2264 k := by\n have h1 : 10 \u2264 Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : \u211d) \u2264 t)\n rwa [Nat.floor_ofNat] at h2\n omega\n have htk : (2 : \u211d) \u2264 t + (k : \u211d) := by\n have h1 : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith [ht, h1]\n have hcount : ((zeroWindow_finite (t + (k : \u211d))).toFinset.sum fun \u03c1 => zeroMult \u03c1 : \u211d)\n \u2264 C0hat (t + (k : \u211d) + 1) := hZC (t + (k : \u211d)) htk\n have hmono : C0hat (t + (k : \u211d) + 1) \u2264 C0hat (2 * (k : \u211d) + 1) := by\n apply C0hat_mono (by positivity : (1 : \u211d) \u2264 t + (k : \u211d) + 1)\n have h1 : (Nat.floor t : \u211d) + 1 \u2264 (k : \u211d) := by\n have h2 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk\n have h3 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h3] at h2\n have h4 : t \u2264 (k : \u211d) := by\n have h5 : t \u2264 (Nat.floor t : \u211d) + 1 := by\n have h6 := Nat.lt_floor_add_one t\n linarith [h6]\n linarith [h1, h5]\n linarith [h4]\n have hsub : FS.image (fun \u03c1 => \u03c1.1) \u2286 (zeroWindow_finite (t + (k : \u211d))).toFinset := by\n intro z hz\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hz\n rw [hFS, Finset.mem_filter] at h\u03c1\n obtain \u27e8hmem, him\u27e9 := h\u03c1\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := hmem\n have hxk : (k : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h1 := Nat.floor_le (abs_nonneg (\u03c1.1.im - t))\n rwa [hmem2] at h1\n have hxk1 : |\u03c1.1.im - t| < (k : \u211d) + 1 := by\n have h1 := Nat.lt_floor_add_one |\u03c1.1.im - t|\n rwa [hmem2] at h1\n have hx : |\u03c1.1.im - t| = \u03c1.1.im - t := abs_of_nonneg (by linarith [him])\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [hx] at hxk\n linarith [hxk, him]\n \u00b7 rw [hx] at hxk1\n linarith [hxk1, him]\n have hbridge : \u2211 \u03c1 \u2208 FS, (zeroMult \u03c1.1 : \u211d)\n = \u2211 \u03c1 \u2208 FS.image (fun \u03c1 => \u03c1.1), (zeroMult \u03c1 : \u211d) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n calc \u2211 \u03c1 \u2208 FS, (zeroMult \u03c1.1 : \u211d)\n = \u2211 z \u2208 FS.image (fun \u03c1 => \u03c1.1), (zeroMult z : \u211d) := hbridge\n _ \u2264 \u2211 z \u2208 (zeroWindow_finite (t + (k : \u211d))).toFinset, (zeroMult z : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun z _ _ => Nat.cast_nonneg _)\n _ = (((zeroWindow_finite (t + (k : \u211d))).toFinset.sum fun \u03c1 => zeroMult \u03c1) : \u211d) := rfl\n _ \u2264 C0hat (t + (k : \u211d) + 1) := hcount\n _ \u2264 C0hat (2 * (k : \u211d) + 1) := hmono\n\n/-- The per-fiber right-tail bound (ENNReal form). -/\nlemma farGRight_fiber_le (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t) (k : \u2115) :\n \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 ENNReal.ofReal (if Nat.floor t + 1 \u2264 k then 4.5 * farW k * C0hat (2 * (k : \u211d) + 1) else 0) := by\n classical\n have hfin : ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k} :\n Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1}).Finite := farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k\n have htsum : \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n = \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k}).indicator\n (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1)) \u03c1 :=\n tsum_subtype _ (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1))\n rw [htsum]\n rw [tsum_eq_sum (s := hfin.toFinset) (fun \u03c1 h\u03c1 => by\n apply Set.indicator_of_notMem\n rwa [Set.Finite.mem_toFinset] at h\u03c1)]\n rw [Finset.sum_congr rfl (fun \u03c1 h\u03c1 =>\n Set.indicator_of_mem (by rwa [Set.Finite.mem_toFinset] at h\u03c1) _)]\n rw [\u2190 ENNReal.ofReal_sum_of_nonneg (fun \u03c1 _ => farGRight_nonneg t \u03c1)]\n apply ENNReal.ofReal_le_ofReal\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [if_pos hk]\n rw [\u2190 Finset.sum_filter_add_sum_filter_not hfin.toFinset\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im) (farGRight t)]\n have hzero : \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n \u00ac t \u2264 \u03c1.1.im), farGRight t \u03c1 = 0 := by\n apply Finset.sum_eq_zero\n intro \u03c1 h\u03c1\n rw [Finset.mem_filter] at h\u03c1\n rw [farGRight, if_neg (fun h => h\u03c1.2 h.2)]\n rw [hzero, add_zero]\n calc \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n farGRight t \u03c1\n \u2264 \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n (4.5 * farW k) * (zeroMult \u03c1.1 : \u211d) := by\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n have h1 := farGRight_term_le \u03c1\n rw [Finset.mem_filter] at h\u03c1\n obtain \u27e8hmem, _\u27e9 := h\u03c1\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := hmem\n rw [hmem2] at h1\n exact h1\n _ = (4.5 * farW k) *\n \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n (zeroMult \u03c1.1 : \u211d) := by\n rw [Finset.mul_sum]\n _ \u2264 (4.5 * farW k) * C0hat (2 * (k : \u211d) + 1) :=\n mul_le_mul_of_nonneg_left (farGRight_fiber_count hZC ht hk)\n (mul_nonneg (by norm_num : (0 : \u211d) \u2264 4.5) (farW_nonneg k))\n \u00b7 rw [if_neg hk]\n apply le_of_eq\n apply Finset.sum_eq_zero\n intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := h\u03c1\n rw [farGRight, if_neg (fun h => hk (by\n have h1 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 (k : \u211d) := by exact_mod_cast h.1\n have h2 : (Nat.floor t : \u211d) + 1 \u2264 (k : \u211d) := by\n have h3 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h3] at h1\n have h4 : (Nat.floor t : \u211d) + 1 \u2264 |\u03c1.1.im - t| := h1.trans (by\n have h5 : (k : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h6 := Nat.floor_le (abs_nonneg (\u03c1.1.im - t))\n rwa [hmem2] at h6\n exact h5)\n have h7 : |\u03c1.1.im - t| < (Nat.floor t : \u211d) + 1 := by\n have h8 := Nat.lt_floor_add_one |\u03c1.1.im - t|\n rwa [hmem2] at h8\n linarith [h2, h4, h7] : Nat.floor t + 1 \u2264 |\u03c1.1.im - t|))]\n\n/-- loglog k \u2265 \u22120.37 for k \u2265 1 (the bridge nonnegativity input). -/\nlemma loglog_ge_neg_point37 {k : \u2115} (hk : 1 \u2264 k) :\n (-0.37 : \u211d) \u2264 Real.log (Real.log k) := by\n rcases eq_or_ne k 1 with rfl | hk1\n \u00b7 simp [Real.log_one, Real.log_zero]\n \u00b7 have hk2 : 2 \u2264 k := by omega\n have h1 : (0.693 : \u211d) \u2264 Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)\n have h2 : (0.693 : \u211d) \u2264 Real.log k := by\n have h3 : Real.log 2 \u2264 Real.log k :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 2) (by exact_mod_cast hk2)\n linarith [h1, h3]\n have h4 : Real.log 0.693 \u2264 Real.log (Real.log k) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 0.693) h2\n have h5 : (-0.37 : \u211d) \u2264 Real.log 0.693 := by\n have h6 : (1 / 0.693 : \u211d) \u2264 Real.exp 0.37 := by\n have h7 := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 0.37 by norm_num) 5\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h7\n norm_num at h7\n have h8 : (1 / 0.693 : \u211d) \u2264 1.447671 := by norm_num\n linarith [h7, h8]\n have h7 : Real.log (1 / 0.693) \u2264 0.37 := by\n have h8 := Real.log_le_log (by norm_num : (0 : \u211d) < 1 / 0.693) h6\n rwa [Real.log_exp] at h8\n rw [Real.log_div (by norm_num : (1 : \u211d) \u2260 0) (by norm_num : (0.693 : \u211d) \u2260 0),\n Real.log_one] at h7\n linarith [h7]\n linarith [h4, h5]\n\n/-- The right-tail bridge is nonnegative for all k. -/\nlemma farGRightBridge_nonneg (k : \u2115) :\n (0 : \u211d) \u2264 0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by\n by_cases hk0 : k = 0\n \u00b7 rw [hk0]\n simp only [Nat.cast_zero, Real.log_zero, Real.log_one, add_zero]\n norm_num\n \u00b7 have hk1 : 1 \u2264 k := by omega\n have h1 : (0 : \u211d) \u2264 Real.log k := Real.log_nonneg (by exact_mod_cast hk1 : (1 : \u211d) \u2264 (k : \u211d))\n have h2 := loglog_ge_neg_point37 hk1\n have h3 : (0 : \u211d) \u2264 (0.433 : \u211d) * (Real.log k + 0.833) := by\n apply mul_nonneg (by norm_num)\n linarith [h1]\n have h4 : (0.886 : \u211d) * ((-0.37 : \u211d) + 0.3475) \u2264 0.886 * (Real.log (Real.log k) + 0.3475) :=\n mul_le_mul_of_nonneg_left (by linarith [h2] : (-0.37 : \u211d) + 0.3475\n \u2264 Real.log (Real.log k) + 0.3475) (by norm_num)\n have h5 : (0.433 : \u211d) * 0.833 \u2264 0.433 * (Real.log k + 0.833) :=\n mul_le_mul_of_nonneg_left (by linarith [h1] : (0.833 : \u211d) \u2264 Real.log k + 0.833) (by norm_num)\n linarith [h3, h4, h5]\n\n/-- The right-tail majorant series (if-form on \u2115). -/\ndef farGRightMaj (t : \u211d) : \u2115 \u2192 \u211d := fun k =>\n if Nat.floor t + 1 \u2264 k then 4.5 * farW k * C0hat (2 * (k : \u211d) + 1) else 0\n\n/-- The right-tail combo form (the brick decomposition target). -/\ndef farGRightMajCombo : \u2115 \u2192 \u211d := fun k =>\n 4.5 * (1 / (k : \u211d) ^ 2) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9)\n\nlemma farGRightMajCombo_nonneg (k : \u2115) : (0 : \u211d) \u2264 farGRightMajCombo k := by\n rw [farGRightMajCombo]\n have h := farGRightBridge_nonneg k\n have h2 : (0 : \u211d) \u2264 4.5 * (1 / (k : \u211d) ^ 2) := by positivity\n exact mul_nonneg h2 h\n\n/-- The pointwise combo bound for the farGRightMaj. -/\nlemma farGRightMaj_le_combo {t : \u211d} (ht : 10 \u2264 t) (k : \u2115) :\n farGRightMaj t k \u2264 farGRightMajCombo k := by\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [farGRightMaj, if_pos hk, farGRightMajCombo]\n have hk11 : 11 \u2264 k := by\n have h1 : 10 \u2264 Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : \u211d) \u2264 t)\n rwa [Nat.floor_ofNat] at h2\n omega\n have h1 := C0hat_two_mul_add_one_le hk11\n have h2 := farW_le_inv_sq (by omega : 1 \u2264 k)\n have hnn := farGRightBridge_nonneg k\n have hk0 : (0 : \u211d) < (k : \u211d) := by\n have h3 : (1 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast (by omega : 1 \u2264 k)\n linarith\n have h4 : 4.5 * farW k \u2264 4.5 * (1 / (k : \u211d) ^ 2) :=\n mul_le_mul_of_nonneg_left h2 (by norm_num : (0 : \u211d) \u2264 4.5)\n have h5 : C0hat (2 * (k : \u211d) + 1)\n \u2264 0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := h1\n have h6 : (0 : \u211d) \u2264 (k : \u211d) ^ 2 := by positivity\n have h7 : (0 : \u211d) \u2264 1 / (k : \u211d) ^ 2 := by positivity\n calc 4.5 * farW k * C0hat (2 * (k : \u211d) + 1)\n \u2264 (4.5 * (1 / (k : \u211d) ^ 2)) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9) := by\n apply mul_le_mul h4 h5 hnn (by positivity : (0 : \u211d) \u2264 4.5 * (1 / (k : \u211d) ^ 2))\n \u00b7 rw [farGRightMaj, if_neg hk]\n exact farGRightMajCombo_nonneg k\n\n/-- The shifted combo is summable (RW-brick families). -/\nlemma farGRightMajCombo_shift_summable :\n Summable (fun k : \u2115 => farGRightMajCombo (k + 11)) := by\n have hA : Summable (fun k : \u2115 => (1 : \u211d) / ((k : \u211d) + 11) ^ 2) := by\n have h := antitoneOn_one_div_sq.summable_of_integrableOn_Ioi\n integrableOn_one_div_sq (fun t ht => by\n have ht10 : (10 : \u211d) < t := ht\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : \u2115 => (1 : \u211d) / (n : \u211d) ^ 2) 11).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n have hB : Summable (fun k : \u2115 => Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2) :=\n tail11_log_div_sq_summable\n have hC : Summable (fun k : \u2115 =>\n Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2) := by\n apply Summable.of_norm_bounded (tail11_log_div_sq_summable.mul_left (1 / Real.exp 1))\n intro k\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hk1 : (1 : \u211d) \u2264 Real.log ((k : \u211d) + 11) := by\n have h1 := log_eleven_ge\n have h2 : Real.log 11 \u2264 Real.log ((k : \u211d) + 11) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 11) (by\n have h : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith)\n linarith [h1, h2]\n have h3 : (0 : \u211d) \u2264 Real.log (Real.log ((k : \u211d) + 11)) := Real.log_nonneg hk1\n positivity : (0 : \u211d) \u2264 Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)]\n have hk1 : (1 : \u211d) < (k : \u211d) + 11 := by\n have h : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith\n have h4 := log_log_le_div_exp hk1\n have h5 : (0 : \u211d) \u2264 ((k : \u211d) + 11) ^ 2 := by positivity\n have h6 := div_le_div_of_nonneg_right h4 h5\n rw [mul_div_assoc] at h6\n exact h6\n have hAB : Summable (fun k : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)) :=\n (hA.mul_left _).add (hB.mul_left _)\n have hABC : Summable (fun k : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)) :=\n hAB.add (hC.mul_left _)\n have hsum := hABC.mul_left 4.5\n apply Summable.congr hsum\n intro k\n rw [farGRightMajCombo]\n have hcast : ((k + 11 : \u2115) : \u211d) = (k : \u211d) + 11 := by push_cast; ring\n rw [hcast]\n ring\n\n/-- **The right-tail series bound**. -/\nlemma farGRightMaj_series_le {t : \u211d} (ht : 10 \u2264 t) :\n (\u2211' k : \u2115, farGRightMaj t k)\n \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hsumm : Summable (farGRightMaj t) := by\n apply (summable_nat_add_iff (f := farGRightMaj t) 11).mp\n apply Summable.of_norm_bounded farGRightMajCombo_shift_summable\n intro k\n rw [Real.norm_eq_abs, abs_of_nonneg (by\n by_cases hk : Nat.floor t + 1 \u2264 k + 11\n \u00b7 rw [farGRightMaj, if_pos hk]\n have h1 : (1 : \u211d) \u2264 (k : \u211d) + 11 + 1 := by\n have h2 : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith\n have h3 := two_le_C0hat h1\n have h4 : (0 : \u211d) \u2264 4.5 * farW (k + 11) := by positivity\n exact mul_nonneg h4 (by linarith [h3])\n \u00b7 rw [farGRightMaj, if_neg hk] : (0 : \u211d) \u2264 farGRightMaj t (k + 11))]\n exact farGRightMaj_le_combo ht (k + 11)\n have hsplit : (\u2211' k : \u2115, farGRightMaj t k)\n = (\u2211 k \u2208 Finset.range 11, farGRightMaj t k) + \u2211' k : \u2115, farGRightMaj t (k + 11) :=\n (hsumm.sum_add_tsum_nat_add 11).symm\n have hzero : \u2211 k \u2208 Finset.range 11, farGRightMaj t k = 0 := by\n apply Finset.sum_eq_zero\n intro k hk\n rw [Finset.mem_range] at hk\n rw [farGRightMaj, if_neg (by\n have h1 : 10 \u2264 Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : \u211d) \u2264 t)\n rwa [Nat.floor_ofNat] at h2\n omega : \u00acNat.floor t + 1 \u2264 k)]\n -- the shifted series bound via the RW bricks\n have hle := Summable.tsum_le_tsum (fun k => farGRightMaj_le_combo ht (k + 11)) hsumm\n farGRightMajCombo_shift_summable\n have hW0 := tail11_inv_sq_le\n have hW1 := tail11_log_div_sq_le\n have hW2 := tail11_loglog_div_sq_le\n have heval : (\u2211' k : \u2115,\n 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)))\n \u2264 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by\n rw [tsum_mul_left]\n apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 4.5)\n have hdecomp : (\u2211' x : \u2115,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)))\n = (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (\u2211' x : \u2115, (1 / ((x : \u211d) + 11) ^ 2))\n + 0.433 * (\u2211' x : \u2115, (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n + 0.886 * (\u2211' x : \u2115, (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)) := by\n have hA : Summable (fun k : \u2115 => (1 : \u211d) / ((k : \u211d) + 11) ^ 2) := by\n have h := antitoneOn_one_div_sq.summable_of_integrableOn_Ioi\n integrableOn_one_div_sq (fun t ht => by\n have ht10 : (10 : \u211d) < t := ht\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : \u2115 => (1 : \u211d) / (n : \u211d) ^ 2) 11).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n have hB : Summable (fun k : \u2115 => Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2) :=\n tail11_log_div_sq_summable\n have hC : Summable (fun k : \u2115 =>\n Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2) := by\n apply Summable.of_norm_bounded (tail11_log_div_sq_summable.mul_left (1 / Real.exp 1))\n intro k\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hk1 : (1 : \u211d) \u2264 Real.log ((k : \u211d) + 11) := by\n have h1 := log_eleven_ge\n have h2 : Real.log 11 \u2264 Real.log ((k : \u211d) + 11) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 11) (by\n have h : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith)\n linarith [h1, h2]\n have h3 : (0 : \u211d) \u2264 Real.log (Real.log ((k : \u211d) + 11)) := Real.log_nonneg hk1\n positivity : (0 : \u211d) \u2264 Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)]\n have hk1 : (1 : \u211d) < (k : \u211d) + 11 := by\n have h : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith\n have h4 := log_log_le_div_exp hk1\n have h5 : (0 : \u211d) \u2264 ((k : \u211d) + 11) ^ 2 := by positivity\n have h6 := div_le_div_of_nonneg_right h4 h5\n rw [mul_div_assoc] at h6\n exact h6\n have e1 := Summable.tsum_add\n (f := fun x : \u2115 => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n (g := fun x : \u2115 => 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2))\n ((hA.mul_left _).add (hB.mul_left _)) (hC.mul_left _)\n have e2 := Summable.tsum_add\n (f := fun x : \u2115 => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2))\n (g := fun x : \u2115 => 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n (hA.mul_left _) (hB.mul_left _)\n rw [show (\u2211' x : \u2115,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)))\n = \u2211' x : \u2115, ((fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x\n + (fun x : \u2115 => 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)) x)\n from rfl]\n rw [e1]\n rw [show (\u2211' x : \u2115, (fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x)\n = \u2211' x : \u2115, ((fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)) x\n + (fun x : \u2115 => 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x)\n from rfl]\n rw [e2, tsum_mul_left, tsum_mul_left, tsum_mul_left]\n rw [hdecomp]\n have hle1 := mul_le_mul_of_nonneg_left hW0 (by positivity : (0 : \u211d) \u2264\n 0.433 * 0.833 + 0.886 * 0.3475 + 2.9)\n have hle2 := mul_le_mul_of_nonneg_left hW1 (by positivity : (0 : \u211d) \u2264 0.433)\n have hle3 := mul_le_mul_of_nonneg_left hW2 (by positivity : (0 : \u211d) \u2264 0.886)\n linarith [hle1, hle2, hle3]\n calc (\u2211' k : \u2115, farGRightMaj t k)\n = (\u2211 k \u2208 Finset.range 11, farGRightMaj t k) + \u2211' k : \u2115, farGRightMaj t (k + 11) := hsplit\n _ = 0 + \u2211' k : \u2115, farGRightMaj t (k + 11) := by rw [hzero]\n _ \u2264 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by linarith [hle, heval]\n _ = 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by ring\n\n/-- **The right-tail bound** (the ENNReal fiberwise assembly). -/\nlemma farGRight_le (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t) :\n \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, farGRight t \u03c1\n \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hC0 : (0 : \u211d) \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n positivity\n rw [\u2190 ENNReal.ofReal_le_ofReal_iff hC0]\n rw [ENNReal.ofReal_tsum_of_nonneg (fun \u03c1 => farGRight_nonneg t \u03c1)\n (farGRight_summable (by linarith : (0 : \u211d) \u2264 t))]\n rw [\u2190 ENNReal.tsum_fiberwise (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1))\n (fun \u03c1 => Nat.floor |\u03c1.1.im - t|)]\n have hper : \u2200 k : \u2115, \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 ENNReal.ofReal (farGRightMaj t k) := by\n intro k\n have h := farGRight_fiber_le hZC ht k\n rwa [farGRightMaj] at *\n calc \u2211' j : \u2115, \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {j},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 \u2211' j : \u2115, ENNReal.ofReal (farGRightMaj t j) := ENNReal.tsum_le_tsum hper\n _ = ENNReal.ofReal (\u2211' j : \u2115, farGRightMaj t j) := by\n rw [ENNReal.ofReal_tsum_of_nonneg (fun k => by\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [farGRightMaj, if_pos hk]\n have h1 : (1 : \u211d) \u2264 (k : \u211d) + 1 + 1 := by\n have h2 : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith\n have h3 := two_le_C0hat h1\n have h4 : (0 : \u211d) \u2264 4.5 * farW k := by positivity\n exact mul_nonneg h4 (by linarith [h3])\n \u00b7 rw [farGRightMaj, if_neg hk] : (0 : \u211d) \u2264 farGRightMaj t k)\n (by\n have h1 := hsummable_proof_placeholder\n exact h1)]\n _ \u2264 ENNReal.ofReal (4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1)) :=\n ENNReal.ofReal_le_ofReal (farGRightMaj_series_le ht)\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Committed §17. Now §18 (right tail). Let me write it following §17's structure with the adjustments:\n\n1. farGRight t ρ := if (Nat.floor t + 1 ≤ |ρ.1.im − t| ∧ t ≤ ρ.1.im) then farG t ρ else 0.\n Hmm — the condition (⌊t⌋₊+1 ≤ x ∧ t ≤ γ). For the fiber-count, I need the γ-side condition for the window: t ≤ γ.\n2. farGRight_nonneg, farGRight_summable.\n3. farGRight_term_le : farGRight t ρ ≤ 4.5·farW(⌊x⌋₊)·m — via farG_le_farW_mul (needs x ≥ 1 for nonzero elements).\n4. farGRight_fiber_finite (k): the fiber {⌊|ρ.1.im − t|⌋₊ = k} finite.\n5. farGRight_fiber_count (k ≥ ⌊t⌋₊+1): ∑_{fiber ∩ {t ≤ γ}} m ≤ C0hat(2k+1) — via zeroWindow (t+k) + hZC + C0hat_mono(t+k+1 ≤ 2k+1) + C0hat_two_mul_add_one_le (k ≥ 11).\n6. farGRight_fiber_le (ENNReal per-fiber, if-form: if ⌊t⌋₊+1 ≤ k then 4.5·farW k·C0hat(2k+1) else 0).\n7. The combo series: farGRightMaj k := if ⌊t⌋₊+1 ≤ k then 4.5·farW k·C0hat(2k+1) else 0; the combo bound form farGRightMajCombo k := 4.5·(1/(k:ℝ)^2)·[0.433·(log k+0.833)+0.886·(loglog k+0.3475)+2.9] — hmm — 1/k² with k = 0: 1/0 = 0 ✓ nonneg.\n Pointwise: farGRightMaj k ≤ farGRightMajCombo k: for k < ⌊t⌋₊+1: 0 ≤ combo (bridge nonneg ✓ need the loglog ≥ −0.37 lemma); for k ≥ ⌊t⌋₊+1: farW k ≤ 1/k² (farW_le_inv_sq, k ≥ 1 ✓) and C0hat(2k+1) ≤ bridge (C0hat_two_mul_add_one_le, k ≥ 11 ✓).\n8. The shifted series: ∑' (fun k => farGRightMajCombo (k+11)) — decompose: = 4.5·[0.433·(0.833·W₀+W₁)+0.886·(0.3475·W₀+W₂)+2.9·W₀] via the RW₀/1/2 bricks (paren-grouped!). Need: log(k+11)+0.833 = the RW₁'s log(k+11) — the 0.433·(log(k+11)+0.833)/(k+11)² = 0.433·log(k+11)/(k+11)² + 0.433·0.833/(k+11)² ✓; 0.886·(loglog(k+11)+0.3475)/(k+11)² = 0.886·loglog(k+11)/(k+11)² + 0.886·0.3475/(k+11)² ✓; 2.9/(k+11)² ✓. So farGRightMajCombo (k+11) = 4.5·[(0.433·0.833+0.886·0.3475+2.9)/(k+11)² + 0.433·log(k+11)/(k+11)² + 0.886·loglog(k+11)/(k+11)²] — the combo form ✓ summable via the RW-brick summables (tail11_inv_sq_summable — EXISTS? I have tail11_log_div_sq_summable (standalone ✓); tail11_inv_sq: the antitone machine exists (antitoneOn_one_div_sq + integrableOn_one_div_sq) — make tail11_inv_sq_summable standalone; tail11_loglog: the inline hsumm from RW₂ — make standalone).\n9. farGRightMaj_series_le: ∑' farGRightMaj = ∑' (fun k => farGRightMaj (k+11)) (range-11 part = 0 since ⌊t⌋₊ ≥ 10 ⟹ ⌊t⌋₊+1 ≥ 11 ✓) ≤ ∑' (fun k => farGRightMajCombo (k+11)) (pointwise ✓ summable ✓) ≤ 4.5·[0.433·(0.833·W₀+W₁)+0.886·(0.3475·W₀+W₂)+2.9·W₀].\n Wait — the pointwise comparison farGRightMaj (k+11) ≤ farGRightMajCombo (k+11): for the shifted family: k+11 ≥ 11 > ⌊t⌋₊?? — NO: k+11 vs ⌊t⌋₊+1: if t = 20, ⌊t⌋₊+1 = 21: for k+11 < 21 (k < 10): farGRightMaj (k+11) = 0 ≤ combo ✓; k+11 ≥ 21: farW ≤ 1/k² + bridge ✓. ✓ pointwise holds for all k.\n10. farGRight_le (the outer assembly).\n\nAlso the final piece-3 assembly (§19): \n```\ntheorem far_series_le (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t)\n {s : ℂ} (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t)\n (hζ : riemannZeta s ≠ 0) :\n ‖∑' ρ, if ρ ∈ nearZerosSub t then (0:ℂ) else seriesDiffTerm s (2+tI) ρ‖\n ≤ 12.1284 * C0hat (t+1) + 7.2425 := by\n -- norm ≤ farG tsum (far_series_norm_le_farG_tsum)\n -- tsum split: main + (if ∉ main)\n -- (if ∉ main) = farGRight + farGLeft (pointwise, with hNLZ)\n -- main ≤ farG_main_le; right ≤ farGRight_le; left ≤ farGLeft_le\n -- fold: 4.5·(2C₀+0.55)·1.3476 + Tail_R + Tail_L ≤ 12.1284·C₀ + 7.2425\n```\nThe arithmetic fold: 4.5·(2C₀+0.55)·1.3476 = 12.1284·C₀ + 3.33531 (4.5·0.55·1.3476 = 3.33531); Tail_R = 4.5·[0.433·(0.833·0.1+0.3303)+0.886·(0.3475·0.1+0.1216)+2.9·0.1] = 4.5·[0.433·0.4136+0.886·0.15625+0.29] = 4.5·[0.17909+0.13844+0.29] = 4.5·0.60753 = 2.73389; Tail_L = 4.5·0.26064 = 1.17288. Sum: 3.33531+2.73389+1.17288 = 7.24208 ≤ 7.2425 ✓. And 4.5·2·1.3476 = 12.1284 ✓.\n\nLet me verify Tail_R numerically: 0.433·0.4136 = 0.179088; 0.886·(0.3475·0.1+0.1216) = 0.886·(0.03475+0.1216) = 0.886·0.15635 = 0.138526; sum = 0.179088+0.138526+0.29 = 0.607614; ×4.5 = 2.734263. Tail_L: 0.433·(0.1942/23+0.1687)+0.886·(0.0736/23+0.0621)+2.9/23: 0.1942/23 = 0.0084435; 0.433·0.17694 = 0.076615; 0.0736/23 = 0.0032; 0.886·0.0653 = 0.057856; 2.9/23 = 0.126087; sum = 0.260558; ×4.5 = 1.172511. Total: 3.33531+2.734263+1.172511 = 7.242084 ≤ 7.2425 ✓ (margin 4.2e-4).\n\nHmm wait — my RW₂ brick is ≤ 0.1216 and I computed 0.886·(0.03475+0.1216) = 0.138526 — and earlier \"Tail_R = 2.73393\" from the design check — consistent ✓.\n\nNow — the summables I need standalone: tail11_inv_sq_summable + tail11_loglog_div_sq_summable (mirror the tail14 versions). Let me write §18 + §19 (assembly) now. This is the final stretch of piece 3 — then 5f-iii remains (assembly of ALL pieces + pinch + capstone), which is a separate sub-stage.\n\nFor §18, careful with:\n- The farGRightMajCombo decomposition with PARENS: 0.433·(log(k+11)/(k+11)²) — write 0.433 * (Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2).\n- The RW-brick forms: W₀ = ∑' (fun k => 1/((k:ℝ)+11)^2), W₁ = ∑' (fun k => Real.log ((k:ℝ)+11)/((k:ℝ)+11)^2) — hmm the RW₁ brick family is `Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2` — the combo's term `0.433 * (Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2)` ✓ paren ✓.\n- W₂ = ∑' (fun k => Real.log (Real.log ((k:ℝ)+11)) / ((k:ℝ)+11)^2) ✓.\n\nfarGRightMajComboShift k := 4.5 * ((0.433*0.833+0.886*0.3475+2.9) * (1/(((k:ℝ)+11)^2)) + 0.433 * (Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2) + 0.886 * (Real.log (Real.log ((k:ℝ)+11)) / ((k:ℝ)+11)^2))\n\nHmm wait — the farGRightMajCombo (k+11) should equal that: 4.5·(1/((k+11):ℝ)²)·[0.433·(log(k+11)+0.833)+0.886·(loglog(k+11)+0.3475)+2.9] — the decomposition: 0.433·(log X+0.833)/X² + 0.886·(loglog X+0.3475)/X² + 2.9/X² with X = (k:ℝ)+11 = 0.433·log X/X² + 0.433·0.833/X² + 0.886·loglog X/X² + 0.886·0.3475/X² + 2.9/X². So farGRightMajCombo (k+11) = 4.5·[(0.433·0.833+0.886·0.3475+2.9)/X² + 0.433·log X/X² + 0.886·loglog X/X²] ✓ — via ring after the paren-forms... The equality needs the div-grouping — prove farGRightMajCombo_eq (k) : farGRightMajCombo (k+11) = 4.5·(combo-sum) via ring (with parens already right, ring is safe).\n\nHmm — actually farGRightMajCombo is the function of a real k cast — define it as a def:\ndef farGRightMajCombo (k : ℕ) : ℝ := 4.5 * (1/(k:ℝ)^2) * (0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9)\n\nThen farGRightMajCombo (k+11) — with ((k+11:ℕ):ℝ) = (k:ℝ)+11 bridge ✓.\n\nAnd the pointwise farGRightMaj k ≤ farGRightMajCombo k:\n```\nlemma farGRightMaj_le_combo {t : ℝ} (ht : 10 ≤ t) (k : ℕ) :\n farGRightMaj t k ≤ farGRightMajCombo k := by\n by_cases hk : Nat.floor t + 1 ≤ k\n · rw [farGRightMaj, if_pos hk]\n -- 4.5·farW k·C0hat(2k+1) ≤ 4.5·(1/k²)·[bridge]\n have hk11 : 11 ≤ k := by\n have h1 : 10 ≤ Nat.floor t := Nat.floor_mono (by norm_num : (10:ℝ) ≤ t)\n ... — Nat.floor 10 = 10: Nat.floor_ofNat : ⌊(10:ℝ)⌋₊ = 10 — h1 : ⌊10⌋₊ ≤ ⌊t⌋₊: rw [Nat.floor_ofNat] at h1: 10 ≤ ⌊t⌋₊ ✓ then hk: ⌊t⌋₊+1 ≤ k ⟹ k ≥ 11 ✓ omega.\n have h1 := C0hat_two_mul_add_one_le hk11\n have h2 := farW_le_inv_sq (by omega : 1 ≤ k)\n have hnn : 0 ≤ the-bridge\n calc 4.5 * farW k * C0hat (2*(k:ℝ)+1)\n ≤ 4.5 * (1/(k:ℝ)^2) * (0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9) := by\n apply mul_le_mul _ _ _ _\n · apply mul_le_mul_of_nonneg_left h2 (by norm_num : (0:ℝ) ≤ 4.5)\n · exact h1\n · exact bridge-nonneg\n · positivity\n · rw [farGRightMaj, if_neg hk]\n exact farGRightMajCombo_nonneg k\n```\nThe bridge-nonneg lemma:\n```\nlemma farGRightBridge_nonneg (k : ℕ) :\n 0 ≤ 0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by\n -- log k ≥ 0 (k ≥ 1) or junk 0 (k = 0); loglog k ≥ −0.37\n ...\n```\nloglog-nonneg: for k = 0: log 0 = 0 (Real.log_zero), loglog = log 0 = 0 ✓ bridge = 0.433·0.833+0.886·0.3475+2.9 ≥ 0 ✓ norm_num. For k ≥ 1: log k ≥ 0 ✓; loglog k ≥ −0.37: k = 1: loglog 1 = log 0 = 0 ✓; k ≥ 2: log k ≥ log 2 ≥ 0.69314 (log_two_gt_d9): loglog k ≥ log 0.693 ≥ −0.37 (the e^{0.37} argument).\n```\nlemma loglog_ge_neg_point37 (k : ℕ) (hk : 1 ≤ k) :\n -0.37 ≤ Real.log (Real.log k) := by\n rcases eq_or_ne k 1 with rfl | hk1\n · simp [Real.log_one, Real.log_zero]\n · have hk2 : 2 ≤ k := by omega\n have h1 : (0.693 : ℝ) ≤ Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)\n have h2 : (0.693 : ℝ) ≤ Real.log k := by\n have h3 : Real.log 2 ≤ Real.log k := Real.log_le_log (by norm_num) (by exact_mod_cast hk2)\n linarith [h1, h3]\n have h4 : Real.log 0.693 ≤ Real.log (Real.log k) :=\n Real.log_le_log (by norm_num : (0:ℝ) < 0.693) h2\n -- log 0.693 ≥ −0.37 ⟺ 0.693 ≥ e^{−0.37} ⟺ e^{0.37} ≥ 0.693⁻¹ = 1.44300\n have h5 : Real.log 0.693 ≥ -0.37 := by\n have h6 : (1 / 0.693 : ℝ) ≤ Real.exp 0.37 := by\n have h7 := Real.sum_le_exp_of_nonneg (show (0:ℝ) ≤ 0.37 by norm_num) 5\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h7\n norm_num at h7\n -- Σ_{k<5} 0.37^k/k! = 1.447671 ≥ 1/0.693 = 1.443002\n have h8 : (1 / 0.693 : ℝ) ≤ 1.447671 := by norm_num\n linarith [h7, h8]\n have h7 : Real.log (1 / 0.693) ≤ 0.37 := by\n have h8 := Real.log_le_log (by norm_num : (0:ℝ) < 1/0.693) h6\n rwa [Real.log_exp] at h8\n rw [Real.log_div (by norm_num : (1:ℝ) ≠ 0) (by norm_num : (0.693:ℝ) ≠ 0)] at h7\n -- log(1/0.693) = log 1 − log 0.693 = −log 0.693 ≤ 0.37 ⟹ log 0.693 ≥ −0.37\n have h9 : Real.log 0.693 ≥ -0.37 := by\n have h10 : Real.log 1 = 0 := Real.log_one\n linarith [h7, h10]\n exact h9\n linarith [h4, h5]\n```\nHmm — Real.log_div gives log(1/0.693) = log 1 − log 0.693 ✓ then log 0.693 ≥ −0.37 ✓.\n\nAnd the nonneg assembly in farGRightBridge_nonneg:\n```\n by_cases hk0 : k = 0\n · rw [hk0]\n simp [Real.log_zero]\n norm_num\n · have hk1 : 1 ≤ k := by omega\n have h1 : (0 : ℝ) ≤ Real.log k := Real.log_nonneg (by exact_mod_cast hk1 : (1:ℝ) ≤ (k:ℝ))\n have h2 := loglog_ge_neg_point37 k hk1\n have h3 : (0.433*0.833 : ℝ) = 0.360889 := by norm_num\n have h4 : (0.886*0.3475 : ℝ) = 0.307985 := by norm_num\n -- 0.433·(log k + 0.833) ≥ 0.433·0.833; 0.886·(loglog k + 0.3475) ≥ 0.886·(−0.37+0.3475)\n nlinarith [h1, h2, Real.log_nonneg (by norm_num : (1:ℝ) ≤ 2.9)]\n```\nHmm — nlinarith with products of (log k) atoms: 0.433·(log k+0.833) ≥ 0 needs log k ≥ −0.833 ✓ (log k ≥ 0 for k ≥ 1). And 0.886·(loglog k + 0.3475) ≥ 0.886·(−0.37+0.3475) = 0.886·(−0.0225) = −0.019935: total ≥ 0.433·0.833 + (−0.019935) + 2.9 = 0.360889−0.019935+2.9 = 3.240954 ≥ 0 ✓. linarith with the pieces as atoms: h1 : 0 ≤ log k; h2 : −0.37 ≤ loglog k: 0.433·(log k + 0.833) ≥ 0.433·0.833 (linarith with h1 ✓ linear in atom log k) and 0.886·(loglog k + 0.3475) ≥ 0.886·(−0.0225) (linear ✓): sum ≥ 0.360889−0.019935+2.9 = 3.240954 ≥ 0 ✓ linarith [h1, h2] should do it (linear in the two atoms) ✓.\n\nOK — also the per-fiber machinery mirroring §17. Let me write §18 now (big). And §19 (assembly) after.\n\nOne more check — farGRight_fiber_count: for k ≥ ⌊t⌋₊+1, the fiber-filtered set (t ≤ γ): image ⊆ zeroWindow (t+k): γ = t+x with x ∈ [k, k+1) ⟹ γ ∈ [t+k, t+k+1) ✓ (zeroWindow closed [t+k, t+k+1] ✓). count ≤ C0hat(t+k+1) via hZC (t+k ≥ 2: t ≥ 10, k ≥ 0 ✓). Then C0hat(t+k+1) ≤ C0hat(2k+1): C0hat_mono (1 ≤ t+k+1) (t+k+1 ≤ 2k+1 ⟺ t ≤ k ✓ k ≥ ⌊t⌋₊+1 > t ✓). Then C0hat(2k+1) — no further bound needed at the fiber level (the combo-form enters at the series level) ✓ — wait — the per-fiber bound's majorant: 4.5·farW k·C0hat(2k+1) ✓ (the farGRightMaj if-form's value for k ≥ ⌊t⌋₊+1) ✓ consistent.\n\nNow write §18.","signature":""},{"type":"text","text":"Now §18 (3e-ii: the right-tail machine). Writing it with the paren discipline learned."},{"type":"tool_use","id":"Edit_225","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":" _ ≤ ENNReal.ofReal (4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23))) :=\n ENNReal.ofReal_le_ofReal farGLeftMaj_series_le\n\nend NguyenRH1\n\nend","new_string":" _ ≤ ENNReal.ofReal (4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23))) :=\n ENNReal.ofReal_le_ofReal farGLeftMaj_series_le\n\n/-! ## 18. Piece 3j: the right-tail machine (γ > 2t) -/\n\n/-- The right-tail summand: farG restricted to tail zeros (x ≥ ⌊t⌋₊+1)\non the right side (γ ≥ t, hence γ > 2t). -/\ndef farGRight (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ :=\n if (Nat.floor t + 1 ≤ |ρ.1.im - t| ∧ t ≤ ρ.1.im) then farG t ρ else 0\n\nlemma farGRight_nonneg (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (0 : ℝ) ≤ farGRight t ρ := by\n by_cases h : (Nat.floor t + 1 ≤ |ρ.1.im - t| ∧ t ≤ ρ.1.im)\n · rw [farGRight, if_pos h]\n exact farG_nonneg t ρ\n · rw [farGRight, if_neg h]\n\nlemma farGRight_summable {t : ℝ} (ht : 0 ≤ t) : Summable (farGRight t) := by\n apply Summable.of_norm_bounded (farG_summable ht)\n intro ρ\n rw [Real.norm_eq_abs, abs_of_nonneg (farGRight_nonneg t ρ)]\n by_cases h : (Nat.floor t + 1 ≤ |ρ.1.im - t| ∧ t ≤ ρ.1.im)\n · rw [farGRight, if_pos h]\n · rw [farGRight, if_neg h]\n exact farG_nonneg t ρ\n\n/-- The per-element right-tail bound: farGRight ≤ 4.5·farW(⌊x⌋₊)·m. -/\nlemma farGRight_term_le {t : ℝ} (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n farGRight t ρ ≤ 4.5 * farW (Nat.floor |ρ.1.im - t|) * (zeroMult ρ.1 : ℝ) := by\n classical\n by_cases h : (Nat.floor t + 1 ≤ |ρ.1.im - t| ∧ t ≤ ρ.1.im)\n · rw [farGRight, if_pos h]\n have hx1 : (1 : ℝ) ≤ |ρ.1.im - t| := by\n have h1 : (1 : ℝ) ≤ (Nat.floor t : ℝ) + 1 := by\n have h2 : (0 : ℝ) ≤ (Nat.floor t : ℝ) := Nat.floor_nonneg\n linarith\n have h3 : (Nat.floor t : ℝ) + 1 ≤ |ρ.1.im - t| := by\n have h4 : ((Nat.floor t + 1 : ℕ) : ℝ) ≤ |ρ.1.im - t| := by exact_mod_cast h.1\n have h5 : ((Nat.floor t + 1 : ℕ) : ℝ) = (Nat.floor t : ℝ) + 1 := by push_cast; ring\n rwa [h5] at h4\n linarith [h1, h3]\n exact farG_le_farW_mul ρ hx1\n · rw [farGRight, if_neg h]\n positivity\n\n/-- The right-tail fiber {⌊x⌋₊ = k} is finite. -/\nlemma farGRight_fiber_finite {t : ℝ} (ht : 0 ≤ t) (k : ℕ) :\n ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k} :\n Set {ρ : ℂ // IsNontrivialZero ρ}).Finite := by\n apply (finite_subtype_norm_lt (t + (k : ℝ) + 2)).subset\n intro ρ hρ\n show ‖ρ.1‖ < t + (k : ℝ) + 2\n have hmem : Nat.floor |ρ.1.im - t| = k := hρ\n have h1 : |ρ.1.im - t| < (k : ℝ) + 1 := by\n have h2 := Nat.lt_floor_add_one |ρ.1.im - t|\n rwa [hmem] at h2\n have hle : ‖ρ.1‖ ≤ |ρ.1.re| + |ρ.1.im| := Complex.norm_le_abs_re_add_abs_im _\n have hre : |ρ.1.re| ≤ 1 := by\n have h3 : 0 < ρ.1.re := ρ.2.2.1\n have h4 : ρ.1.re < 1 := ρ.2.2.2\n rw [abs_le]\n constructor <;> linarith\n have him : |ρ.1.im| ≤ t + |ρ.1.im - t| := by\n calc |ρ.1.im| = |ρ.1.im - t + t| := by rw [sub_add_cancel]\n _ ≤ |ρ.1.im - t| + |t| := abs_add_le _ _\n _ = |ρ.1.im - t| + t := by rw [abs_of_nonneg ht]\n _ = t + |ρ.1.im - t| := by ring\n linarith [hle, hre, him, h1]\n\n/-- **The per-fiber right-tail count**: the mult-weighted count of\nright-tail zeros with bucket k (⌊t⌋₊+1 ≤ k) is ≤ C0hat(2k+1). -/\nlemma farGRight_fiber_count (hZC : ZeroCountProp) {t : ℝ} (ht : 10 ≤ t)\n {k : ℕ} (hk : Nat.floor t + 1 ≤ k) :\n ∑ ρ ∈ (farGRight_fiber_finite (by linarith : (0 : ℝ) ≤ t) k).toFinset.filter\n (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im), (zeroMult ρ.1 : ℝ)\n ≤ C0hat (2 * (k : ℝ) + 1) := by\n classical\n set FS := (farGRight_fiber_finite (by linarith : (0 : ℝ) ≤ t) k).toFinset.filter\n (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im) with hFS\n have hk11 : 11 ≤ k := by\n have h1 : 10 ≤ Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : ℝ) ≤ t)\n rwa [Nat.floor_ofNat] at h2\n omega\n have htk : (2 : ℝ) ≤ t + (k : ℝ) := by\n have h1 : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith [ht, h1]\n have hcount : ((zeroWindow_finite (t + (k : ℝ))).toFinset.sum fun ρ => zeroMult ρ : ℝ)\n ≤ C0hat (t + (k : ℝ) + 1) := hZC (t + (k : ℝ)) htk\n have hmono : C0hat (t + (k : ℝ) + 1) ≤ C0hat (2 * (k : ℝ) + 1) := by\n apply C0hat_mono (by positivity : (1 : ℝ) ≤ t + (k : ℝ) + 1)\n have h1 : (Nat.floor t : ℝ) + 1 ≤ (k : ℝ) := by\n have h2 : ((Nat.floor t + 1 : ℕ) : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk\n have h3 : ((Nat.floor t + 1 : ℕ) : ℝ) = (Nat.floor t : ℝ) + 1 := by push_cast; ring\n rwa [h3] at h2\n have h4 : t ≤ (k : ℝ) := by\n have h5 : t ≤ (Nat.floor t : ℝ) + 1 := by\n have h6 := Nat.lt_floor_add_one t\n linarith [h6]\n linarith [h1, h5]\n linarith [h4]\n have hsub : FS.image (fun ρ => ρ.1) ⊆ (zeroWindow_finite (t + (k : ℝ))).toFinset := by\n intro z hz\n obtain ⟨ρ, hρ, rfl⟩ := Finset.mem_image.mp hz\n rw [hFS, Finset.mem_filter] at hρ\n obtain ⟨hmem, him⟩ := hρ\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |ρ.1.im - t| = k := hmem\n have hxk : (k : ℝ) ≤ |ρ.1.im - t| := by\n have h1 := Nat.floor_le (abs_nonneg (ρ.1.im - t))\n rwa [hmem2] at h1\n have hxk1 : |ρ.1.im - t| < (k : ℝ) + 1 := by\n have h1 := Nat.lt_floor_add_one |ρ.1.im - t|\n rwa [hmem2] at h1\n have hx : |ρ.1.im - t| = ρ.1.im - t := abs_of_nonneg (by linarith [him])\n rw [Set.Finite.mem_toFinset]\n refine ⟨ρ.2, ?_, ?_⟩\n · rw [hx] at hxk\n linarith [hxk, him]\n · rw [hx] at hxk1\n linarith [hxk1, him]\n have hbridge : ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ)\n = ∑ ρ ∈ FS.image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n calc ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ)\n = ∑ z ∈ FS.image (fun ρ => ρ.1), (zeroMult z : ℝ) := hbridge\n _ ≤ ∑ z ∈ (zeroWindow_finite (t + (k : ℝ))).toFinset, (zeroMult z : ℝ) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun z _ _ => Nat.cast_nonneg _)\n _ = (((zeroWindow_finite (t + (k : ℝ))).toFinset.sum fun ρ => zeroMult ρ) : ℝ) := rfl\n _ ≤ C0hat (t + (k : ℝ) + 1) := hcount\n _ ≤ C0hat (2 * (k : ℝ) + 1) := hmono\n\n/-- The per-fiber right-tail bound (ENNReal form). -/\nlemma farGRight_fiber_le (hZC : ZeroCountProp) {t : ℝ} (ht : 10 ≤ t) (k : ℕ) :\n ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k},\n ENNReal.ofReal (farGRight t b.1)\n ≤ ENNReal.ofReal (if Nat.floor t + 1 ≤ k then 4.5 * farW k * C0hat (2 * (k : ℝ) + 1) else 0) := by\n classical\n have hfin : ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k} :\n Set {ρ : ℂ // IsNontrivialZero ρ}).Finite := farGRight_fiber_finite (by linarith : (0 : ℝ) ≤ t) k\n have htsum : ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k},\n ENNReal.ofReal (farGRight t b.1)\n = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k}).indicator\n (fun ρ => ENNReal.ofReal (farGRight t ρ)) ρ :=\n tsum_subtype _ (fun ρ => ENNReal.ofReal (farGRight t ρ))\n rw [htsum]\n rw [tsum_eq_sum (s := hfin.toFinset) (fun ρ hρ => by\n apply Set.indicator_of_notMem\n rwa [Set.Finite.mem_toFinset] at hρ)]\n rw [Finset.sum_congr rfl (fun ρ hρ =>\n Set.indicator_of_mem (by rwa [Set.Finite.mem_toFinset] at hρ) _)]\n rw [← ENNReal.ofReal_sum_of_nonneg (fun ρ _ => farGRight_nonneg t ρ)]\n apply ENNReal.ofReal_le_ofReal\n by_cases hk : Nat.floor t + 1 ≤ k\n · rw [if_pos hk]\n rw [← Finset.sum_filter_add_sum_filter_not hfin.toFinset\n (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im) (farGRight t)]\n have hzero : ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n ¬ t ≤ ρ.1.im), farGRight t ρ = 0 := by\n apply Finset.sum_eq_zero\n intro ρ hρ\n rw [Finset.mem_filter] at hρ\n rw [farGRight, if_neg (fun h => hρ.2 h.2)]\n rw [hzero, add_zero]\n calc ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im),\n farGRight t ρ\n ≤ ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im),\n (4.5 * farW k) * (zeroMult ρ.1 : ℝ) := by\n apply Finset.sum_le_sum\n intro ρ hρ\n have h1 := farGRight_term_le ρ\n rw [Finset.mem_filter] at hρ\n obtain ⟨hmem, _⟩ := hρ\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |ρ.1.im - t| = k := hmem\n rw [hmem2] at h1\n exact h1\n _ = (4.5 * farW k) *\n ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im),\n (zeroMult ρ.1 : ℝ) := by\n rw [Finset.mul_sum]\n _ ≤ (4.5 * farW k) * C0hat (2 * (k : ℝ) + 1) :=\n mul_le_mul_of_nonneg_left (farGRight_fiber_count hZC ht hk)\n (mul_nonneg (by norm_num : (0 : ℝ) ≤ 4.5) (farW_nonneg k))\n · rw [if_neg hk]\n apply le_of_eq\n apply Finset.sum_eq_zero\n intro ρ hρ\n rw [Set.Finite.mem_toFinset] at hρ\n have hmem2 : Nat.floor |ρ.1.im - t| = k := hρ\n rw [farGRight, if_neg (fun h => hk (by\n have h1 : ((Nat.floor t + 1 : ℕ) : ℝ) ≤ (k : ℝ) := by exact_mod_cast h.1\n have h2 : (Nat.floor t : ℝ) + 1 ≤ (k : ℝ) := by\n have h3 : ((Nat.floor t + 1 : ℕ) : ℝ) = (Nat.floor t : ℝ) + 1 := by push_cast; ring\n rwa [h3] at h1\n have h4 : (Nat.floor t : ℝ) + 1 ≤ |ρ.1.im - t| := h1.trans (by\n have h5 : (k : ℝ) ≤ |ρ.1.im - t| := by\n have h6 := Nat.floor_le (abs_nonneg (ρ.1.im - t))\n rwa [hmem2] at h6\n exact h5)\n have h7 : |ρ.1.im - t| < (Nat.floor t : ℝ) + 1 := by\n have h8 := Nat.lt_floor_add_one |ρ.1.im - t|\n rwa [hmem2] at h8\n linarith [h2, h4, h7] : Nat.floor t + 1 ≤ |ρ.1.im - t|))]\n\n/-- loglog k ≥ −0.37 for k ≥ 1 (the bridge nonnegativity input). -/\nlemma loglog_ge_neg_point37 {k : ℕ} (hk : 1 ≤ k) :\n (-0.37 : ℝ) ≤ Real.log (Real.log k) := by\n rcases eq_or_ne k 1 with rfl | hk1\n · simp [Real.log_one, Real.log_zero]\n · have hk2 : 2 ≤ k := by omega\n have h1 : (0.693 : ℝ) ≤ Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)\n have h2 : (0.693 : ℝ) ≤ Real.log k := by\n have h3 : Real.log 2 ≤ Real.log k :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 2) (by exact_mod_cast hk2)\n linarith [h1, h3]\n have h4 : Real.log 0.693 ≤ Real.log (Real.log k) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 0.693) h2\n have h5 : (-0.37 : ℝ) ≤ Real.log 0.693 := by\n have h6 : (1 / 0.693 : ℝ) ≤ Real.exp 0.37 := by\n have h7 := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.37 by norm_num) 5\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h7\n norm_num at h7\n have h8 : (1 / 0.693 : ℝ) ≤ 1.447671 := by norm_num\n linarith [h7, h8]\n have h7 : Real.log (1 / 0.693) ≤ 0.37 := by\n have h8 := Real.log_le_log (by norm_num : (0 : ℝ) < 1 / 0.693) h6\n rwa [Real.log_exp] at h8\n rw [Real.log_div (by norm_num : (1 : ℝ) ≠ 0) (by norm_num : (0.693 : ℝ) ≠ 0),\n Real.log_one] at h7\n linarith [h7]\n linarith [h4, h5]\n\n/-- The right-tail bridge is nonnegative for all k. -/\nlemma farGRightBridge_nonneg (k : ℕ) :\n (0 : ℝ) ≤ 0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by\n by_cases hk0 : k = 0\n · rw [hk0]\n simp only [Nat.cast_zero, Real.log_zero, Real.log_one, add_zero]\n norm_num\n · have hk1 : 1 ≤ k := by omega\n have h1 : (0 : ℝ) ≤ Real.log k := Real.log_nonneg (by exact_mod_cast hk1 : (1 : ℝ) ≤ (k : ℝ))\n have h2 := loglog_ge_neg_point37 hk1\n have h3 : (0 : ℝ) ≤ (0.433 : ℝ) * (Real.log k + 0.833) := by\n apply mul_nonneg (by norm_num)\n linarith [h1]\n have h4 : (0.886 : ℝ) * ((-0.37 : ℝ) + 0.3475) ≤ 0.886 * (Real.log (Real.log k) + 0.3475) :=\n mul_le_mul_of_nonneg_left (by linarith [h2] : (-0.37 : ℝ) + 0.3475\n ≤ Real.log (Real.log k) + 0.3475) (by norm_num)\n have h5 : (0.433 : ℝ) * 0.833 ≤ 0.433 * (Real.log k + 0.833) :=\n mul_le_mul_of_nonneg_left (by linarith [h1] : (0.833 : ℝ) ≤ Real.log k + 0.833) (by norm_num)\n linarith [h3, h4, h5]\n\n/-- The right-tail majorant series (if-form on ℕ). -/\ndef farGRightMaj (t : ℝ) : ℕ → ℝ := fun k =>\n if Nat.floor t + 1 ≤ k then 4.5 * farW k * C0hat (2 * (k : ℝ) + 1) else 0\n\n/-- The right-tail combo form (the brick decomposition target). -/\ndef farGRightMajCombo : ℕ → ℝ := fun k =>\n 4.5 * (1 / (k : ℝ) ^ 2) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9)\n\nlemma farGRightMajCombo_nonneg (k : ℕ) : (0 : ℝ) ≤ farGRightMajCombo k := by\n rw [farGRightMajCombo]\n have h := farGRightBridge_nonneg k\n have h2 : (0 : ℝ) ≤ 4.5 * (1 / (k : ℝ) ^ 2) := by positivity\n exact mul_nonneg h2 h\n\n/-- The pointwise combo bound for the farGRightMaj. -/\nlemma farGRightMaj_le_combo {t : ℝ} (ht : 10 ≤ t) (k : ℕ) :\n farGRightMaj t k ≤ farGRightMajCombo k := by\n by_cases hk : Nat.floor t + 1 ≤ k\n · rw [farGRightMaj, if_pos hk, farGRightMajCombo]\n have hk11 : 11 ≤ k := by\n have h1 : 10 ≤ Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : ℝ) ≤ t)\n rwa [Nat.floor_ofNat] at h2\n omega\n have h1 := C0hat_two_mul_add_one_le hk11\n have h2 := farW_le_inv_sq (by omega : 1 ≤ k)\n have hnn := farGRightBridge_nonneg k\n have hk0 : (0 : ℝ) < (k : ℝ) := by\n have h3 : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast (by omega : 1 ≤ k)\n linarith\n have h4 : 4.5 * farW k ≤ 4.5 * (1 / (k : ℝ) ^ 2) :=\n mul_le_mul_of_nonneg_left h2 (by norm_num : (0 : ℝ) ≤ 4.5)\n have h5 : C0hat (2 * (k : ℝ) + 1)\n ≤ 0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := h1\n have h6 : (0 : ℝ) ≤ (k : ℝ) ^ 2 := by positivity\n have h7 : (0 : ℝ) ≤ 1 / (k : ℝ) ^ 2 := by positivity\n calc 4.5 * farW k * C0hat (2 * (k : ℝ) + 1)\n ≤ (4.5 * (1 / (k : ℝ) ^ 2)) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9) := by\n apply mul_le_mul h4 h5 hnn (by positivity : (0 : ℝ) ≤ 4.5 * (1 / (k : ℝ) ^ 2))\n · rw [farGRightMaj, if_neg hk]\n exact farGRightMajCombo_nonneg k\n\n/-- The shifted combo is summable (RW-brick families). -/\nlemma farGRightMajCombo_shift_summable :\n Summable (fun k : ℕ => farGRightMajCombo (k + 11)) := by\n have hA : Summable (fun k : ℕ => (1 : ℝ) / ((k : ℝ) + 11) ^ 2) := by\n have h := antitoneOn_one_div_sq.summable_of_integrableOn_Ioi\n integrableOn_one_div_sq (fun t ht => by\n have ht10 : (10 : ℝ) < t := ht\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 2) 11).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n have hB : Summable (fun k : ℕ => Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2) :=\n tail11_log_div_sq_summable\n have hC : Summable (fun k : ℕ =>\n Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2) := by\n apply Summable.of_norm_bounded (tail11_log_div_sq_summable.mul_left (1 / Real.exp 1))\n intro k\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hk1 : (1 : ℝ) ≤ Real.log ((k : ℝ) + 11) := by\n have h1 := log_eleven_ge\n have h2 : Real.log 11 ≤ Real.log ((k : ℝ) + 11) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 11) (by\n have h : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith)\n linarith [h1, h2]\n have h3 : (0 : ℝ) ≤ Real.log (Real.log ((k : ℝ) + 11)) := Real.log_nonneg hk1\n positivity : (0 : ℝ) ≤ Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2)]\n have hk1 : (1 : ℝ) < (k : ℝ) + 11 := by\n have h : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith\n have h4 := log_log_le_div_exp hk1\n have h5 : (0 : ℝ) ≤ ((k : ℝ) + 11) ^ 2 := by positivity\n have h6 := div_le_div_of_nonneg_right h4 h5\n rw [mul_div_assoc] at h6\n exact h6\n have hAB : Summable (fun k : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2)) :=\n (hA.mul_left _).add (hB.mul_left _)\n have hABC : Summable (fun k : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2)) :=\n hAB.add (hC.mul_left _)\n have hsum := hABC.mul_left 4.5\n apply Summable.congr hsum\n intro k\n rw [farGRightMajCombo]\n have hcast : ((k + 11 : ℕ) : ℝ) = (k : ℝ) + 11 := by push_cast; ring\n rw [hcast]\n ring\n\n/-- **The right-tail series bound**. -/\nlemma farGRightMaj_series_le {t : ℝ} (ht : 10 ≤ t) :\n (∑' k : ℕ, farGRightMaj t k)\n ≤ 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hsumm : Summable (farGRightMaj t) := by\n apply (summable_nat_add_iff (f := farGRightMaj t) 11).mp\n apply Summable.of_norm_bounded farGRightMajCombo_shift_summable\n intro k\n rw [Real.norm_eq_abs, abs_of_nonneg (by\n by_cases hk : Nat.floor t + 1 ≤ k + 11\n · rw [farGRightMaj, if_pos hk]\n have h1 : (1 : ℝ) ≤ (k : ℝ) + 11 + 1 := by\n have h2 : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith\n have h3 := two_le_C0hat h1\n have h4 : (0 : ℝ) ≤ 4.5 * farW (k + 11) := by positivity\n exact mul_nonneg h4 (by linarith [h3])\n · rw [farGRightMaj, if_neg hk] : (0 : ℝ) ≤ farGRightMaj t (k + 11))]\n exact farGRightMaj_le_combo ht (k + 11)\n have hsplit : (∑' k : ℕ, farGRightMaj t k)\n = (∑ k ∈ Finset.range 11, farGRightMaj t k) + ∑' k : ℕ, farGRightMaj t (k + 11) :=\n (hsumm.sum_add_tsum_nat_add 11).symm\n have hzero : ∑ k ∈ Finset.range 11, farGRightMaj t k = 0 := by\n apply Finset.sum_eq_zero\n intro k hk\n rw [Finset.mem_range] at hk\n rw [farGRightMaj, if_neg (by\n have h1 : 10 ≤ Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : ℝ) ≤ t)\n rwa [Nat.floor_ofNat] at h2\n omega : ¬Nat.floor t + 1 ≤ k)]\n -- the shifted series bound via the RW bricks\n have hle := Summable.tsum_le_tsum (fun k => farGRightMaj_le_combo ht (k + 11)) hsumm\n farGRightMajCombo_shift_summable\n have hW0 := tail11_inv_sq_le\n have hW1 := tail11_log_div_sq_le\n have hW2 := tail11_loglog_div_sq_le\n have heval : (∑' k : ℕ,\n 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2)))\n ≤ 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by\n rw [tsum_mul_left]\n apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 4.5)\n have hdecomp : (∑' x : ℕ,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2)))\n = (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (∑' x : ℕ, (1 / ((x : ℝ) + 11) ^ 2))\n + 0.433 * (∑' x : ℕ, (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2))\n + 0.886 * (∑' x : ℕ, (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2)) := by\n have hA : Summable (fun k : ℕ => (1 : ℝ) / ((k : ℝ) + 11) ^ 2) := by\n have h := antitoneOn_one_div_sq.summable_of_integrableOn_Ioi\n integrableOn_one_div_sq (fun t ht => by\n have ht10 : (10 : ℝ) < t := ht\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 2) 11).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n have hB : Summable (fun k : ℕ => Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2) :=\n tail11_log_div_sq_summable\n have hC : Summable (fun k : ℕ =>\n Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2) := by\n apply Summable.of_norm_bounded (tail11_log_div_sq_summable.mul_left (1 / Real.exp 1))\n intro k\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hk1 : (1 : ℝ) ≤ Real.log ((k : ℝ) + 11) := by\n have h1 := log_eleven_ge\n have h2 : Real.log 11 ≤ Real.log ((k : ℝ) + 11) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 11) (by\n have h : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith)\n linarith [h1, h2]\n have h3 : (0 : ℝ) ≤ Real.log (Real.log ((k : ℝ) + 11)) := Real.log_nonneg hk1\n positivity : (0 : ℝ) ≤ Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2)]\n have hk1 : (1 : ℝ) < (k : ℝ) + 11 := by\n have h : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith\n have h4 := log_log_le_div_exp hk1\n have h5 : (0 : ℝ) ≤ ((k : ℝ) + 11) ^ 2 := by positivity\n have h6 := div_le_div_of_nonneg_right h4 h5\n rw [mul_div_assoc] at h6\n exact h6\n have e1 := Summable.tsum_add\n (f := fun x : ℕ => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2))\n (g := fun x : ℕ => 0.886 * (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2))\n ((hA.mul_left _).add (hB.mul_left _)) (hC.mul_left _)\n have e2 := Summable.tsum_add\n (f := fun x : ℕ => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2))\n (g := fun x : ℕ => 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2))\n (hA.mul_left _) (hB.mul_left _)\n rw [show (∑' x : ℕ,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2)))\n = ∑' x : ℕ, ((fun x : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)) x\n + (fun x : ℕ => 0.886 * (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2)) x)\n from rfl]\n rw [e1]\n rw [show (∑' x : ℕ, (fun x : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)) x)\n = ∑' x : ℕ, ((fun x : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)) x\n + (fun x : ℕ => 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)) x)\n from rfl]\n rw [e2, tsum_mul_left, tsum_mul_left, tsum_mul_left]\n rw [hdecomp]\n have hle1 := mul_le_mul_of_nonneg_left hW0 (by positivity : (0 : ℝ) ≤\n 0.433 * 0.833 + 0.886 * 0.3475 + 2.9)\n have hle2 := mul_le_mul_of_nonneg_left hW1 (by positivity : (0 : ℝ) ≤ 0.433)\n have hle3 := mul_le_mul_of_nonneg_left hW2 (by positivity : (0 : ℝ) ≤ 0.886)\n linarith [hle1, hle2, hle3]\n calc (∑' k : ℕ, farGRightMaj t k)\n = (∑ k ∈ Finset.range 11, farGRightMaj t k) + ∑' k : ℕ, farGRightMaj t (k + 11) := hsplit\n _ = 0 + ∑' k : ℕ, farGRightMaj t (k + 11) := by rw [hzero]\n _ ≤ 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by linarith [hle, heval]\n _ = 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by ring\n\n/-- **The right-tail bound** (the ENNReal fiberwise assembly). -/\nlemma farGRight_le (hZC : ZeroCountProp) {t : ℝ} (ht : 10 ≤ t) :\n ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farGRight t ρ\n ≤ 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hC0 : (0 : ℝ) ≤ 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n positivity\n rw [← ENNReal.ofReal_le_ofReal_iff hC0]\n rw [ENNReal.ofReal_tsum_of_nonneg (fun ρ => farGRight_nonneg t ρ)\n (farGRight_summable (by linarith : (0 : ℝ) ≤ t))]\n rw [← ENNReal.tsum_fiberwise (fun ρ => ENNReal.ofReal (farGRight t ρ))\n (fun ρ => Nat.floor |ρ.1.im - t|)]\n have hper : ∀ k : ℕ, ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k},\n ENNReal.ofReal (farGRight t b.1)\n ≤ ENNReal.ofReal (farGRightMaj t k) := by\n intro k\n have h := farGRight_fiber_le hZC ht k\n rwa [farGRightMaj] at *\n calc ∑' j : ℕ, ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {j},\n ENNReal.ofReal (farGRight t b.1)\n ≤ ∑' j : ℕ, ENNReal.ofReal (farGRightMaj t j) := ENNReal.tsum_le_tsum hper\n _ = ENNReal.ofReal (∑' j : ℕ, farGRightMaj t j) := by\n rw [ENNReal.ofReal_tsum_of_nonneg (fun k => by\n by_cases hk : Nat.floor t + 1 ≤ k\n · rw [farGRightMaj, if_pos hk]\n have h1 : (1 : ℝ) ≤ (k : ℝ) + 1 + 1 := by\n have h2 : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith\n have h3 := two_le_C0hat h1\n have h4 : (0 : ℝ) ≤ 4.5 * farW k := by positivity\n exact mul_nonneg h4 (by linarith [h3])\n · rw [farGRightMaj, if_neg hk] : (0 : ℝ) ≤ farGRightMaj t k)\n (by\n have h1 := hsummable_proof_placeholder\n exact h1)]\n _ ≤ ENNReal.ofReal (4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1)) :=\n ENNReal.ofReal_le_ofReal (farGRightMaj_series_le ht)\n\nend NguyenRH1\n\nend"},"extra_content":null}]