[{"type":"thinking","thinking":"Committed (0829421). Now piece 3c: the far-series machine — the per-term bound, farG + summability, norm reduction. Let me write §15.\n\nPlan:\n1. `farG (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ := if ρ ∈ nearZerosSub t then 0 else 4.5 * (zeroMult ρ.1 : ℝ) / (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t)^2))`\n   Hmm — division: 4.5·m/(x·√(1+x²)) with x = |ρ.im − t|.\n2. farG_nonneg.\n3. farG_summable (t): dominated by C·m/(1+γ²): \n   For ρ far (x ≥ 1): 4.5/(x√(1+x²)) ≤ 4.5/x²; and |γ| ≤ x + t ≤ x + t·x (x ≥ 1... x + t ≤ x(1+t) ⟺ t ≤ tx ⟺ 1 ≤ x for t ≥ 1 ✓): |γ| ≤ (1+t)x ⟹ 1+γ² ≤ 1+(1+t)²x² ≤ 2(1+t)²x²·... wait direction: I want 1/x² ≤ C/(1+γ²): |γ| ≤ (1+t)x ⟹ γ² ≤ (1+t)²x² ⟹ 1+γ² ≤ 1+(1+t)²x² ≤ (1+t)²(1+x²)·... hmm 1+(1+t)²x² vs (1+t)²(1+x²) = (1+t)²+(1+t)²x²: 1+(1+t)²x² ≤ (1+t)²+(1+t)²x² ✓. So 1+γ² ≤ (1+t)²(1+x²) ≤ 2(1+t)²x² (1+x² ≤ 2x² for x ≥ 1 ✓). So 1/x² ≤ 2(1+t)²/(1+γ²) ✓.\n   farG ρ ≤ 4.5·2(1+t)²·m/(1+γ²) = 9(1+t)²·m/(1+γ²) — summable via the LiCircleBound pattern (WeilEF.zero_sum_inv_sq zetaSeam with the normSq(gammaOf) comparison — clone tailTerm_summable's argument: 1+γ² vs 1+normSq(gammaOf ρ): normSq(gammaOf ρ) = im² + (1/2−re)² and 1+normSq ≤ 2(1+im²) — from tailTerm_summable: they showed dominator 2·m/(1+normSq(gammaOf)) works with 1/(1+im²) ≤ 2/(1+normSq(gammaOf)) ✓. So: farG ≤ 9(1+t)²·m/(1+γ²) ≤ 9(1+t)²·2·m/(1+normSq(gammaOf)) = 18(1+t)²·m/(1+normSq(gammaOf)) ✓ summable.\n4. The per-term bound:\n```\nlemma seriesDiffTerm_norm_le_farG {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t)\n    (hζ : riemannZeta s ≠ 0) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    ‖if ρ ∈ nearZerosSub t then (0 : ℂ) else seriesDiffTerm s (2 + t * Complex.I) ρ‖\n      ≤ farG t ρ\n```\nFor ρ near: both 0 ✓. For ρ far (x ≥ 1): ‖seriesDiffTerm‖ = m·‖s₀−s‖/(‖s−ρ‖·‖s₀−ρ‖) ≤ 4.5·m/(x·√(1+x²)):\n- seriesDiffTerm s s₀ ρ = m·(1/(s−ρ) − 1/(s₀−ρ)): algebra 1/(s−ρ) − 1/(s₀−ρ) = (s₀−s)/((s−ρ)(s₀−ρ)): needs s−ρ ≠ 0 (hζ: s = ρ ⟹ ζ s = 0 ✓ contradiction) and s₀−ρ ≠ 0 (s₀ = 2+it: re = 2 ≠ re ρ < 1 ✓).\n- norm: ‖m·(s₀−s)/((s−ρ)(s₀−ρ))‖ = m·‖s₀−s‖/(‖s−ρ‖·‖s₀−ρ‖) (norm_mul, norm_div, norm_natCast-ish: ‖(zeroMult ρ : ℂ)‖ = zeroMult ρ as ℝ ≥ 0).\n- ‖s₀−s‖ ≤ 4.5: s₀−s = (2−s.re:ℝ) (the hdiff from one_div_diff_le ✓ clone).\n- ‖s−ρ‖ ≥ x: |im(s−ρ)| = |t−γ| = x ✓ abs_im_le_norm.\n- ‖s₀−ρ‖ ≥ √(1+x²): ‖s₀−ρ‖² = (2−β)²+(t−γ)² ≥ 1+x² (|2−β| ≥ 1: β < 1). Via Complex.sq_norm or normSq: ‖z‖² = normSq z = re²+im² — `Complex.normSq` : ‖z‖^2 = normSq z? There's `Complex.sq_norm_sub`? Let me use: ‖s₀−ρ‖ ≥ √(1+x²) ⟺ 1+x² ≤ ‖s₀−ρ‖² (Real.le_sqrt (0 ≤ ‖s₀−ρ‖)? — direction: √(1+x²) ≤ ‖s₀−ρ‖ ⟺ 1+x² ≤ ‖s₀−ρ‖² via Real.le_sqrt (0 ≤ ?) hmm: Real.le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ sqrt y ↔ x^2 ≤ y — I want sqrt(1+x²) ≤ ‖s₀−ρ‖: that's `Real.sqrt_le_iff`? or le of sqrt: `Real.sqrt_le_sqrt` no. The form: √A ≤ B ⟺ A ≤ B² (for B ≥ 0): `Real.sqrt_le_iff (hB : 0 ≤ B) : sqrt A ≤ B ↔ A ≤ B^2`? Hmm — earlier I used Real.le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ √y ↔ x² ≤ y — with x = ‖s₀−ρ‖, y = 1+x²: ‖s₀−ρ‖ ≤ √(1+x²) ⟺ ‖s₀−ρ‖² ≤ 1+x² — WRONG direction. I want √(1+x²) ≤ ‖s₀−ρ‖: apply Real.le_sqrt with x := √(1+x²)?? circular. The right lemma: `Real.sqrt_le' ?`— let me think: sqrt A ≤ B ⟺ A ≤ B^2 when B ≥ 0: `Real.sqrt_le_iff (hy : 0 ≤ y) : sqrt x ≤ y ↔ x ≤ y ^ 2`? I believe `Real.sqrt_le_iff (hy : 0 ≤ y) : √x ≤ y ↔ x ≤ y^2`? or `sqrt_le_iff_le_sq`? — use: have := Real.sqrt_le_sqrt (h : 1+x² ≤ ‖s₀−ρ‖²) : √(1+x²) ≤ √(‖s₀−ρ‖²) = ‖s₀−ρ‖ (Real.sqrt_sq_eq_abs + abs_of_nonneg) ✓ — cleaner: \n  ‖s₀−ρ‖² ≥ 1+x² via: ‖s₀−ρ‖² = normSq(s₀−ρ) = (2−β)² + (t−γ)² — `Complex.sq_norm` : ‖z‖^2 = normSq z — `Complex.sq_norm (z) : ‖z‖ ^ 2 = Complex.normSq z`? There's `Complex.normSq_apply` and `Complex.sq_norm_sub`? Hmm — from seriesTerm_norm_eq_div's usage: they used norm_div etc. For normSq: `Complex.sq_norm : ‖z‖^2 = normSq z`? I recall `Complex.sq_norm (z : ℂ) : ‖z‖ ^ 2 = normSq z` might be `Complex.norm_sq_eq_norm_sq`... Let me just compute: \n  ```\n  have hsq : (1 : ℝ) + x ^ 2 ≤ ‖s₀ - ρ.1‖ ^ 2 := by\n    have h1 : ‖s₀ - ρ.1‖ ^ 2 = (s₀ - ρ.1).re ^ 2 + (s₀ - ρ.1).im ^ 2 := by\n      rw [Complex.sq_norm, Complex.normSq_apply]\n    ...\n  ```\n  Check Complex.sq_norm exists: `Complex.sq_norm (z : ℂ) : ‖z‖ ^ 2 = normSq z`? — hmm, there's `Complex.normSq_eq_norm_sq : normSq z = ‖z‖ ^ 2` (probably this direction) ✓ use that: rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply] — then re/im parts: (s₀−ρ).re = 2−β (s₀ = 2+tI: re 2, ρ.re = β: sub_re: 2−β ✓ simp), (s₀−ρ).im = t−γ ✓. Then (2−β)²+(t−γ)² ≥ 1+x²: |2−β| ≥ 1 ⟹ (2−β)² ≥ 1; (t−γ)² = x² (sq_abs: (t−γ)² = |t−γ|² = x² via sq_abs or abs... x := |t−γ|: (t−γ)² = x² via sq_abs: |t−γ|^2 = (t−γ)^2 (sq_abs (t−γ) : |t−γ|^2 = (t−γ)^2 ✓).\n  |2−β| ≥ 1: β < 1 ⟹ 2−β > 1 ✓ abs_of_pos.\n- The assembly: m·‖s₀−s‖/(‖s−ρ‖·‖s₀−ρ‖) ≤ 4.5·m/(x·√(1+x²)):\n  numerator: ‖s₀−s‖ ≤ 4.5 ✓ (m ≥ 0).\n  denominator: ‖s−ρ‖·‖s₀−ρ‖ ≥ x·√(1+x²) (mul_le_mul of the two, pos).\n  division: div_le_div: m·‖s₀−s‖/(‖s−ρ‖‖s₀−ρ‖) ≤ m·4.5/(x√(1+x²)) — via div_le_div (num ≤) (den ≥) (nonneg) (pos): div_le_div (h₁ : a ≤ b) (h₂ : c ≤ d) (hc : 0 ≤ c) (hd : 0 < d)?? — the signature issue again (div_le_div didn't exist). Use: div_le_div_iff₀? or: a/c ≤ b/d ⟺ a·d ≤ b·c: div_le_div_iff (hc : 0 < c)? (hd : 0 < d)? Let me do it manually:\n  ```\n  rw [div_le_div_iff₀ hpos1 hpos2]  -- a/c ≤ b/d ↔ a*d ≤ b*c\n  ```\n  with c = ‖s−ρ‖·‖s₀−ρ‖ > 0 (x ≥ 1 > 0, √(1+x²) > 0) and d = x·√(1+x²) > 0: a·d ≤ b·c: m·‖s₀−s‖·(x√(1+x²)) ≤ m·4.5·(‖s−ρ‖‖s₀−ρ‖): via mul_le_mul (m·‖s₀−s‖ ≤ m·4.5) (x√(1+x²) ≤ ‖s−ρ‖‖s₀−ρ‖) ✓.\n  div_le_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b ✓ (used before ✓).\n\n5. The norm-tsum reduction:\n```\nlemma far_series_norm_le_farG_tsum (ht) {s} (hσlo)(hσhi)(him)(hζ) :\n    ‖∑' ρ, if ρ ∈ nearZerosSub t then (0 : ℂ) else seriesDiffTerm s (2+tI) ρ‖\n      ≤ ∑' ρ, farG t ρ := by\n  have h1 : ‖∑' ρ, ...‖ ≤ ∑' ρ, ‖if ρ ∈ nearZerosSub t then (0:ℂ) else seriesDiffTerm s (2+tI) ρ‖ :=\n    norm_tsum_le_tsum_norm <summable-norm>\n  -- the norm family summable: of_norm_bounded by farG (pointwise via seriesDiffTerm_norm_le_farG + farG nonneg)\n  have h2 : ∑' ρ, ‖...‖ ≤ ∑' ρ, farG t ρ :=\n    Summable.tsum_le_tsum (fun ρ => seriesDiffTerm_norm_le_farG ht hσlo hσhi him hζ ρ) <norm-summable> farG_summable\n  exact h1.trans h2\n```\n`norm_tsum_le_tsum_norm : Summable (fun i => ‖f i‖) → ‖∑' i, f i‖ ≤ ∑' i, ‖f i‖` — check name: `norm_tsum_le_tsum_norm (hf : Summable fun i => ‖f i‖) : ‖∑' i, f i‖ ≤ ∑' i, ‖f i‖` ✓ I believe.\nThe norm-summable: Summable (fun ρ => ‖if ... ‖): of_norm_bounded farG_summable (fun ρ => by rw [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg...)] hmm — ‖(x : ℂ)‖ vs farG: ‖‖x‖‖ = ‖x‖ (norm_norm): the of_norm_bounded condition: ‖f ρ‖ ≤ farG ρ where f ρ = the ℂ if-term: ‖f ρ‖_ℝ = ‖f ρ‖ (Real.norm of the complex norm: ‖(‖z‖ : ℝ)‖ = ‖z‖ via Real.norm_eq_abs + abs_of_nonneg (norm_nonneg z) ✓). Then seriesDiffTerm_norm_le_farG gives ‖if-term‖ ≤ farG ρ ✓.\n\nThen the SPLIT into main + tail (for 3d/3e):\n- mainFinset t := (finite_subtype_norm_lt (2t+1)).toFinset.filter (fun ρ => 1 ≤ |ρ.1.im − t| ∧ |ρ.1.im − t| ≤ t):\n  Wait — the bucket index k(ρ) = ⌊x⌋₊ ≤ ⌊t⌋₊: the main finset: far zeros (x ≥ 1) with k(ρ) ≤ ⌊t⌋₊ ⟺ x < ⌊t⌋₊+1: since x < ⌊t⌋₊+1 ≤ t+1: |γ| ≤ t+x < 2t+1 ✓ ball. Filter condition: 1 ≤ x ∧ x ≤ t (x ≤ t ⟹ k ≤ ⌊t⌋₊ ✓; and k ≤ ⌊t⌋₊ ⟹ x < ⌊t⌋₊+1 ≤ t+1: x could be in (t, t+1) — NOT covered by x ≤ t!! Hmm: k(ρ) ≤ ⌊t⌋₊ ⟺ ⌊x⌋₊ ≤ ⌊t⌋₊ ⟺ x < ⌊t⌋₊+1 — x ∈ (t, ⌊t⌋₊+1) possible when t not integer (x ∈ (t, t+1)): those zeros have k = ⌊t⌋₊ (main bucket) but x > t — my filter (x ≤ t) EXCLUDES them wrongly. Fix the filter: 1 ≤ x ∧ x < ⌊t⌋₊+1 (as a real): x < (⌊t⌋₊ : ℝ)+1. Hmm — but then the bucket-count proof: bucket k ≤ ⌊t⌋₊'s right window [t+k, t+k+1] — for x ∈ (t, ⌊t⌋₊+1) with k = ⌊t⌋₊: γ ∈ [t+⌊t⌋₊, t+⌊t⌋₊+1) ⊆ zeroWindow(t+⌊t⌋₊) ✓ fine.\n  Simpler filter: 1 ≤ x ∧ x < (Nat.floor t : ℝ) + 1. Hmm — Nat.floor t = ⌊t⌋₊. Fine.\n- tsum split: ∑' farG = ∑_{mainFinset} farG + ∑' (if ∉ mainFinset then farG else 0) via tsum_split_finset (LiCircleBound's, ℝ version ✓).\n- The tail: ∑' (if ∉ main then farG else 0): zeros not in main: near (farG = 0 ✓) or x ≥ ⌊t⌋₊+1 > t: γ > 2t or γ < 0. Split further: = ∑' (fun ρ => if ρ.1.im > 2t then farG ρ else 0) + ∑' (fun ρ => if ρ.1.im < 0 then farG ρ else 0)?? — via Summable.tsum_add + tsum_congr: for ρ ∉ main with farG ρ ≠ 0: x ≥ ⌊t⌋₊+1 > t ⟹ γ > 2t ∨ γ < 0 (exclusive) ✓; and for ρ in main or near: all three are 0 ✓. The tsum_congr pointwise: (if ∉ main then farG else 0) = (if γ > 2t then farG else 0) + (if γ < 0 then farG else 0): case analysis on (near/in-main, γ>2t, γ<0) ✓.\n  Both tails summable by of_norm_bounded (farG).\n- Then 3d: main ≤ 4.5·(2C₀+0.55)·S₃-ish ≤ ... and 3e: the two tail machines.\n\nActually — wait, for the tail tsum split I realize there's redundancy: the tail zeros are x > t ⟹ γ > 2t or γ < 0 — and farG for γ < 0 has x = t+|γ|. The left/right tail machines then work on their respective if-forms.\n\nLet me also reconsider — do I even need the mainFinset as a subtype finset with the ball? The main sum: ∑_{mainFinset} farG — bounded by the bucket-family machine (unit_family_le) which takes FS + bucket index + per-bucket counts. FS = mainFinset. The bucket index k(ρ) := Nat.floor x = ⌊|ρ.1.im − t|⌋₊. Bucket range: 1 ≤ k ≤ ⌊t⌋₊. Per-element: farG ρ ≤ 4.5·m·W(k) with W(k) = 1/(k√(1+k²)) = farW k (x ≥ k ⟹ x√(1+x²) ≥ k√(1+k²) ⟹ farG ≤ 4.5·m/(k√(1+k²)) = 4.5·m·farW k ✓). Per-bucket count: ≤ 2C₀+0.55 (the two-window bridge).\n\nThen: main ≤ Σ_{k ∈ Ico 1 (⌊t⌋₊+1)} (4.5·farW k)·(2C₀+0.55) = 4.5·(2C₀+0.55)·Σ farW ≤ 4.5·(2C₀+0.55)·1.3476 (farW_Ico_le ✓).\n\nLet me now write §15 (3c). Then §16 (3d: unit_family_le + main). Then §17 (3e: the two tails). Then §18 (assembly + the far_series_le statement).\n\nFor §15, write:\n\n```lean\n/-! ## 15. Piece 3g: the farG majorant, its summability, and the norm reduction -/\n\ndef farG (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ :=\n  if ρ ∈ nearZerosSub t then (0 : ℝ)\n  else 4.5 * (zeroMult ρ.1 : ℝ) / (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2))\n\nlemma farG_nonneg (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (0 : ℝ) ≤ farG t ρ := by\n  classical\n  by_cases h : ρ ∈ nearZerosSub t <;> simp [farG, h]\n  · positivity\n\nlemma farG_summable (t : ℝ) : Summable (farG t) := by\n  classical\n  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (18 * (1 + t) ^ 2) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))) :=\n    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left _\n  apply Summable.of_norm_bounded hbase\n  intro ρ\n  rw [farG]\n  by_cases h : ρ ∈ nearZerosSub t\n  · rw [if_pos h, norm_zero]\n    positivity\n  · rw [if_neg h]\n    -- x := |ρ.1.im - t| ≥ 1 (far)\n    have hx1 : (1 : ℝ) ≤ |ρ.1.im - t| := by\n      have h' := mem_nearZerosSub.not.mp ... -- h : ρ ∉ nearZerosSub t: ¬(|ρ.im − t| < 1) ⟹ 1 ≤ |...|\n      ...\n    ...\n```\nCareful: h : ρ ∉ nearZerosSub t — mem_nearZerosSub : ρ ∈ nearZerosSub t ↔ |ρ.1.im − t| < 1: so ¬(|ρ.im−t| < 1) ⟹ 1 ≤ |ρ.im−t| (not_lt + abs_nonneg: le_of_not_lt ✓ but mem_nearZerosSub's statement — from the file: `mem_nearZerosSub : ρ ∈ nearZerosSub t ↔ |ρ.1.im - t| < 1` ✓. So hx1 := le_of_not_lt (fun hlt => h (mem_nearZerosSub.mpr hlt)).\n\nThe comparison: farG ρ = 4.5·m/(x√(1+x²)) with x ≥ 1: ≤ 4.5·m/x² (x√(1+x²) ≥ x² ⟹ 1/(x√(1+x²)) ≤ 1/x²: x·√(1+x²) ≥ x·x: √ ≥ x for x ≥ 0: √(1+x²) ≥ √x² = x (x ≥ 1 > 0)): then 4.5·m/x² ≤ 4.5·m·2(1+t)²/(1+γ²) via 1/x² ≤ 2(1+t)²/(1+γ²): from |γ| ≤ (1+t)·x: \n```\n    have hgam : |ρ.1.im| ≤ (1 + t) * |ρ.1.im - t| := by\n      -- |γ| ≤ x + t ≤ x + t·x = (1+t)·x (x ≥ 1, t ≥ 10 — actually t ≥ 0 suffices for t·x ≥ t when x ≥ 1)\n      have h1 : |ρ.1.im| ≤ |ρ.1.im - t| + 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 (by linarith [ht] : (0:ℝ) ≤ t)]\n      -- t ≤ t·x (x ≥ 1, t ≥ 0)\n      have h2 : t ≤ t * |ρ.1.im - t| := by\n        have h3 : t * 1 ≤ t * |ρ.1.im - t| := mul_le_mul_of_nonneg_left hx1 (by linarith [ht] : (0:ℝ) ≤ t)\n        rwa [mul_one] at h3\n      linarith [h1, h2]\n```\nHmm — farG_summable needs t ≥ 0 (for |t| = t and t ≥ 0) — state with (ht : 0 ≤ t) — the far bound: 1+γ² ≤ (1+t)²·2·x²:\n```\n    have h4 : 1 + ρ.1.im ^ 2 ≤ 2 * (1 + t) ^ 2 * (|ρ.1.im - t|) ^ 2 := by\n      have h5 : ρ.1.im ^ 2 ≤ ((1 + t) * |ρ.1.im - t|) ^ 2 := by\n        have h6 : |ρ.1.im| ≤ (1 + t) * |ρ.1.im - t| := hgam\n        have h7 : (0 : ℝ) ≤ (1 + t) * |ρ.1.im - t| := by positivity\n        calc ρ.1.im ^ 2 = |ρ.1.im| ^ 2 := by rw [sq_abs]\n          _ ≤ ((1 + t) * |ρ.1.im - t|) ^ 2 := pow_le_pow_left₀ (abs_nonneg _) h6 2\n      -- 1 + γ² ≤ 1 + (1+t)²x² ≤ (1+t)²x² + (1+t)²x²?? no: 1 ≤ (1+t)²x² (t ≥ 0, x ≥ 1: (1+t)² ≥ 1, x² ≥ 1)\n      have h8 : (1 : ℝ) ≤ (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := by\n        have h9 : (1 : ℝ) ≤ (1 + t) ^ 2 := by\n          have h10 : (1 : ℝ) ≤ 1 + t := by linarith [ht]\n          nlinarith [h10]\n        have h11 : (1 : ℝ) ≤ |ρ.1.im - t| ^ 2 := by\n          have h12 := pow_le_pow_left₀ (by norm_num : (0:ℝ) ≤ 1) hx1 2\n          rwa [one_pow] at h12\n        calc (1 : ℝ) = 1 * 1 := by ring\n          _ ≤ (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := mul_le_mul h9 h11 (by positivity) (by positivity)\n      -- assemble: 1 + γ² ≤ (1+t)²x² + (1+t)²x² = 2(1+t)²x²\n      have h13 : ((1 + t) * |ρ.1.im - t|) ^ 2 = (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := by ring\n      rw [h13] at h5\n      linarith [h5, h8]\n```\nThen 1/x² ≤ 2(1+t)²/(1+γ²): div form: 1/x² ≤ 2(1+t)²/(1+γ²) ⟺ 1+γ² ≤ 2(1+t)²x² ✓ (h4) via div_le_div_iff₀-ish or one_div_le_one_div_of_le: 1/x² ≤ 2(1+t)²/(1+γ²): hmm — one_div_le_one_div_of_le (0 < x²) (x² ≤ ...)? no — the forms differ (2(1+t)² factor). Use: \n```\n    have h14 : 1 / |ρ.1.im - t| ^ 2 ≤ (2 * (1 + t) ^ 2) / (1 + ρ.1.im ^ 2) := by\n      rw [div_le_div_iff₀ (by positivity : (0:ℝ) < 1 + ρ.1.im^2) (by positivity : (0:ℝ) < |ρ.1.im - t|^2)]\n      -- 1 * (x²) ≤ 2(1+t)² * (1+γ²)?? no — div_le_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a/b ≤ c/d ↔ a*d ≤ c*b\n      -- a = 1, b = 1+γ², c = 2(1+t)², d = x²: 1*x² ≤ 2(1+t)²*(1+γ²)?? WRONG DIRECTION — h4 says 1+γ² ≤ 2(1+t)²x²\n```\nhmm: 1/x² ≤ 2(1+t)²/(1+γ²) ⟺ 1·(1+γ²) ≤ 2(1+t)²·x²·... — cross multiply: 1+γ² ≤ 2(1+t)²x² — YES that's h4 ✓: div_le_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a/b ≤ c/d ↔ a*d ≤ c*b: with a = 1, b = x², c = 2(1+t)², d = 1+γ²: 1·(1+γ²) ≤ 2(1+t)²·x² ✓ h4 ✓.\nThen farG = 4.5·m/(x√(1+x²)) ≤ 4.5·m/x² = 4.5·m·(1/x²) ≤ 4.5·m·2(1+t)²/(1+γ²) = 9(1+t)²·m/(1+γ²).\nThen the normSq(gammaOf) comparison (clone tailTerm_summable's hcmp): 1+normSq(gammaOf ρ) ≤ 2(1+γ²) ⟹ m/(1+γ²) ≤ 2·m/(1+normSq) ⟹ farG ≤ 18(1+t)²·m/(1+normSq(gammaOf)) ✓ the hbase dominator ✓.\n\nHmm — the norm management: of_norm_bounded needs ‖farG ρ‖ ≤ hbase ρ: ‖farG ρ‖ = farG ρ (nonneg ✓ abs_of_nonneg) and hbase ρ = 18(1+t)²·(m/(1+normSq)) — nonneg ✓.\n\nThis is getting long — let me just write it. For the per-term bound, the if-form: \n\nActually — cleaner: prove the per-term bound as TWO lemmas: (a) the norm identity for seriesDiffTerm (m·‖s₀−s‖/(‖s−ρ‖‖s₀−ρ‖)), (b) the bound chain. Then the if-wrapper in far_series_norm_le_farG_tsum directly (both sides 0 when near).\n\nLet me write §15 now.","signature":""},{"type":"text","text":"Now §15 (3c: farG + summability + per-term bound + norm reduction)."},{"type":"tool_use","id":"Edit_145","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":"  show (analyticOrderAt riemannZeta ((starRingEnd ℂ) ρ)).toNat\n      = (analyticOrderAt riemannZeta ρ).toNat\n  rw [analyticOrderAt_riemannZeta_conj hρ1]\n\nend NguyenRH1\n\nend","new_string":"  show (analyticOrderAt riemannZeta ((starRingEnd ℂ) ρ)).toNat\n      = (analyticOrderAt riemannZeta ρ).toNat\n  rw [analyticOrderAt_riemannZeta_conj hρ1]\n\n/-! ## 15. Piece 3g: the farG majorant and the norm reduction -/\n\n/-- The far-term majorant: 4.5·m/(x√(1+x²)) with x = |γ − t| (0 for near\nzeros). -/\ndef farG (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ :=\n  if ρ ∈ nearZerosSub t then (0 : ℝ)\n  else 4.5 * (zeroMult ρ.1 : ℝ) / (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2))\n\nlemma farG_nonneg (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (0 : ℝ) ≤ farG t ρ := by\n  classical\n  by_cases h : ρ ∈ nearZerosSub t\n  · rw [farG, if_pos h]\n  · rw [farG, if_neg h]\n    positivity\n\n/-- The absolute-value estimate: |γ| ≤ (1+t)·x for x = |γ−t| ≥ 1, t ≥ 0. -/\nlemma abs_im_le_one_add_mul {t : ℝ} (ht : 0 ≤ t) {γ : ℝ} (hx : 1 ≤ |γ - t|) :\n    |γ| ≤ (1 + t) * |γ - t| := by\n  have h1 : |γ| ≤ |γ - t| + t := by\n    calc |γ| = |γ - t + t| := by rw [sub_add_cancel]\n      _ ≤ |γ - t| + |t| := abs_add_le _ _\n      _ = |γ - t| + t := by rw [abs_of_nonneg ht]\n  have h2 : t ≤ t * |γ - t| := by\n    have h3 : t * 1 ≤ t * |γ - t| := mul_le_mul_of_nonneg_left hx ht\n    rwa [mul_one] at h3\n  linarith [h1, h2]\n\n/-- farG is summable (dominated by 18(1+t)²·m/(1+‖γ‖²)). -/\nlemma farG_summable {t : ℝ} (ht : 0 ≤ t) : Summable (farG t) := by\n  classical\n  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (18 * (1 + t) ^ 2) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))))) :=\n    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left _\n  apply Summable.of_norm_bounded hbase\n  intro ρ\n  rw [Real.norm_eq_abs, abs_of_nonneg (farG_nonneg t ρ)]\n  rw [farG]\n  by_cases h : ρ ∈ nearZerosSub t\n  · rw [if_pos h]\n    positivity\n  · rw [if_neg h]\n    have hx1 : (1 : ℝ) ≤ |ρ.1.im - t| :=\n      le_of_not_lt (fun hlt => h (mem_nearZerosSub.mpr hlt))\n    -- the normSq(gammaOf) comparison (the tailTerm_summable pattern)\n    have hgam : Complex.normSq (gammaOf (ρ : ℂ))\n        = (ρ : ℂ).im ^ 2 + (1 / 2 - (ρ : ℂ).re) ^ 2 := by\n      rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n      ring\n    have hcmp : 1 + Complex.normSq (gammaOf (ρ : ℂ)) ≤ 2 * (1 + (ρ : ℂ).im ^ 2) := by\n      rw [hgam]\n      have hre : ((ρ : ℂ).re - 1 / 2) ^ 2 ≤ 1 / 4 := by\n        have h0 := ρ.2.2.1\n        have h1 := ρ.2.2.2\n        nlinarith [sq_nonneg ((ρ : ℂ).re - 1 / 2)]\n      nlinarith [sq_nonneg (ρ : ℂ).im]\n    -- the (1+t)²x² comparison\n    have hγbound : |ρ.1.im| ≤ (1 + t) * |ρ.1.im - t| := abs_im_le_one_add_mul ht hx1\n    have h4 : 1 + ρ.1.im ^ 2 ≤ 2 * (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := by\n      have h5 : ρ.1.im ^ 2 ≤ (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := by\n        calc ρ.1.im ^ 2 = |ρ.1.im| ^ 2 := by rw [sq_abs]\n          _ ≤ ((1 + t) * |ρ.1.im - t|) ^ 2 :=\n              pow_le_pow_left₀ (abs_nonneg _) hγbound 2\n          _ = (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := by ring\n      have h8 : (1 : ℝ) ≤ (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := by\n        have h9 : (1 : ℝ) ≤ (1 + t) ^ 2 := by\n          have h10 : (1 : ℝ) ≤ 1 + t := by linarith [ht]\n          nlinarith [h10]\n        have h11 : (1 : ℝ) ≤ |ρ.1.im - t| ^ 2 := by\n          have h12 := pow_le_pow_left₀ (by norm_num : (0 : ℝ) ≤ 1) hx1 2\n          rwa [one_pow] at h12\n        calc (1 : ℝ) = 1 * 1 := by ring\n          _ ≤ (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 :=\n              mul_le_mul h9 h11 (by positivity) (by positivity)\n      linarith [h5, h8]\n    -- 1/(x√(1+x²)) ≤ 1/x² ≤ 2(1+t)²/(1+γ²)\n    have h6 : 1 / (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2))\n        ≤ 1 / |ρ.1.im - t| ^ 2 := by\n      have h7 : |ρ.1.im - t| * |ρ.1.im - t|\n          ≤ |ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2) := by\n        apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)\n        calc |ρ.1.im - t| = Real.sqrt ((ρ.1.im - t) ^ 2) := by\n            rw [Real.sqrt_sq_eq_abs]\n          _ ≤ Real.sqrt (1 + (ρ.1.im - t) ^ 2) :=\n            Real.sqrt_le_sqrt (by linarith [sq_nonneg (ρ.1.im - t)])\n      have h8 : (0 : ℝ) < |ρ.1.im - t| * |ρ.1.im - t| := by positivity\n      have h9 := one_div_le_one_div_of_le h8 h7\n      rwa [pow_two] at h9\n    have h10 : 1 / |ρ.1.im - t| ^ 2 ≤ (2 * (1 + t) ^ 2) / (1 + ρ.1.im ^ 2) := by\n      rw [div_le_div_iff₀ (by positivity : (0 : ℝ) < 1 + ρ.1.im ^ 2)\n        (by positivity : (0 : ℝ) < |ρ.1.im - t| ^ 2)]\n      calc (1 : ℝ) * |ρ.1.im - t| ^ 2 = |ρ.1.im - t| ^ 2 := by ring\n        _ ≤ 1 + ρ.1.im ^ 2 := by nlinarith [sq_nonneg ρ.1.im]\n        _ ≤ 2 * (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := h4\n        _ = (2 * (1 + t) ^ 2) * (1 + ρ.1.im ^ 2) - (2 * (1 + t) ^ 2) * (ρ.1.im ^ 2)\n            + (2 * (1 + t) ^ 2) * (ρ.1.im ^ 2) - (2 * (1 + t) ^ 2) * |ρ.1.im - t| ^ 2\n            + (2 * (1 + t) ^ 2) * |ρ.1.im - t| ^ 2 := by ring\n    -- hmm, the above calc is wrong; replace below\n    have h10' : 1 / |ρ.1.im - t| ^ 2 ≤ (2 * (1 + t) ^ 2) / (1 + ρ.1.im ^ 2) := by\n      rw [div_le_div_iff₀ (by positivity : (0 : ℝ) < 1 + ρ.1.im ^ 2)\n        (by positivity : (0 : ℝ) < |ρ.1.im - t| ^ 2)]\n      have h11 : (1 : ℝ) * |ρ.1.im - t| ^ 2 = |ρ.1.im - t| ^ 2 := by ring\n      rw [h11]\n      have h12 : (2 * (1 + t) ^ 2) * (1 + ρ.1.im ^ 2)\n          = 2 * (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 * (1 / |ρ.1.im - t| ^ 2)\n            * (1 + ρ.1.im ^ 2) := by\n        field_simp\n        ring\n      rw [h12]\n      apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : ℝ) ≤ 2 * (1 + t) ^ 2)\n      rw [show (1 / |ρ.1.im - t| ^ 2) * (1 + ρ.1.im ^ 2)\n          = (1 + ρ.1.im ^ 2) / |ρ.1.im - t| ^ 2 from by ring]\n      rw [div_le_iff₀ (by positivity : (0 : ℝ) < |ρ.1.im - t| ^ 2)]\n      calc 1 + ρ.1.im ^ 2 ≤ 2 * (1 + t) ^ 2 * |ρ.1.im - t| ^ 2 := h4\n        _ = 1 * (2 * (1 + t) ^ 2 * |ρ.1.im - t| ^ 2) := by ring\n    -- m/(1+γ²) ≤ 2·m/(1+normSq)\n    have hpos1 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by\n      have h := Complex.normSq_nonneg (gammaOf (ρ : ℂ)); linarith\n    have hpos2 : (0 : ℝ) < 1 + (ρ : ℂ).im ^ 2 := by positivity\n    have hfrac : 1 / (1 + (ρ : ℂ).im ^ 2) ≤ 2 / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n      rw [div_le_div_iff₀ hpos2 hpos1]\n      nlinarith [hcmp]\n    have hm : (0 : ℝ) ≤ (zeroMult ρ : ℝ) := Nat.cast_nonneg _\n    -- assemble\n    calc 4.5 * (zeroMult ρ : ℝ) / (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2))\n        = (4.5 * (zeroMult ρ : ℝ)) * (1 / (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2))) := by\n          rw [div_eq_mul_inv]\n      _ ≤ (4.5 * (zeroMult ρ : ℝ)) * ((2 * (1 + t) ^ 2) / (1 + ρ.1.im ^ 2)) :=\n          mul_le_mul_of_nonneg_left (h6.trans h10')\n            (mul_nonneg (by norm_num : (0 : ℝ) ≤ 4.5) hm)\n      _ = (9 * (1 + t) ^ 2) * ((zeroMult ρ : ℝ) * (1 / (1 + ρ.1.im ^ 2))) := by ring\n      _ ≤ (9 * (1 + t) ^ 2) * ((zeroMult ρ : ℝ) * (2 / (1 + Complex.normSq (gammaOf (ρ : ℂ))))) := by\n          apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : ℝ) ≤ 9 * (1 + t) ^ 2)\n          rw [show (zeroMult ρ : ℝ) * (2 / (1 + Complex.normSq (gammaOf (ρ : ℂ))))\n              = (zeroMult ρ : ℝ) * 2 * (1 / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) from by ring]\n          rw [show (zeroMult ρ : ℝ) * (1 / (1 + ρ.1.im ^ 2))\n              = (zeroMult ρ : ℝ) / (1 + ρ.1.im ^ 2) from by ring]\n          have h13 : (zeroMult ρ : ℝ) / (1 + ρ.1.im ^ 2)\n              ≤ (zeroMult ρ : ℝ) * (2 / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) := by\n            rw [show (zeroMult ρ : ℝ) / (1 + ρ.1.im ^ 2)\n                = (zeroMult ρ : ℝ) * (1 / (1 + ρ.1.im ^ 2)) from by ring]\n            exact mul_le_mul_of_nonneg_left hfrac hm\n          exact h13\n      _ = (18 * (1 + t) ^ 2) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))) := by\n          ring\n\n/-- The per-term norm identity for the far difference term. -/\nlemma seriesDiffTerm_norm_eq {s s₀ : ℂ} (ρ : {ρ : ℂ // IsNontrivialZero ρ})\n    (hs : s ≠ ρ.1) (hs₀ : s₀ ≠ ρ.1) :\n    ‖seriesDiffTerm s s₀ ρ‖\n      = (zeroMult ρ.1 : ℝ) * ‖s₀ - s‖ / (‖s - ρ.1‖ * ‖s₀ - ρ.1‖) := by\n  have h1 : seriesDiffTerm s s₀ ρ\n      = (zeroMult ρ.1 : ℂ) * ((s₀ - s) / ((s - ρ.1) * (s₀ - ρ.1))) := by\n    rw [seriesDiffTerm]\n    have h2 : 1 / (s - ρ.1) - 1 / (s₀ - ρ.1)\n        = (s₀ - s) / ((s - ρ.1) * (s₀ - ρ.1)) := by\n      field_simp [sub_ne_zero.mpr hs, sub_ne_zero.mpr hs₀]\n      ring\n    rw [h2]\n  rw [h1, norm_mul, norm_div, norm_mul]\n  have h3 : ‖(zeroMult ρ.1 : ℂ)‖ = (zeroMult ρ.1 : ℝ) := by\n    rw [show (zeroMult ρ.1 : ℂ) = ((zeroMult ρ.1 : ℝ) : ℂ) by push_cast; ring,\n      Complex.norm_real]\n    exact abs_of_nonneg (Nat.cast_nonneg _)\n  rw [h3]\n\n/-- The per-term far bound: the far difference term is bounded by farG. -/\nlemma seriesDiffTerm_norm_le_farG {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t)\n    (hζ : riemannZeta s ≠ 0) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    ‖if ρ ∈ nearZerosSub t then (0 : ℂ) else seriesDiffTerm s (2 + t * Complex.I) ρ‖\n      ≤ farG t ρ := by\n  classical\n  by_cases h : ρ ∈ nearZerosSub t\n  · rw [if_pos h, norm_zero, farG, if_pos h]\n  · rw [if_neg h, farG, if_neg h]\n    have hx1 : (1 : ℝ) ≤ |ρ.1.im - t| :=\n      le_of_not_lt (fun hlt => h (mem_nearZerosSub.mpr hlt))\n    -- s ≠ ρ and s₀ ≠ ρ\n    have hs : s ≠ ρ.1 := by\n      intro hbad\n      apply hζ\n      rw [hbad]\n      exact ρ.2.1\n    have hs₀ : (2 + t * Complex.I) ≠ ρ.1 := by\n      intro hbad\n      have hre := ρ.2.2.2\n      have h1 : (2 + t * Complex.I).re = ρ.1.re := by rw [hbad]\n      simp at h1\n      linarith [h1, hre]\n    rw [seriesDiffTerm_norm_eq ρ hs hs₀]\n    -- the three factors\n    have hdiff : (2 + t * Complex.I) - s = ((2 - s.re : ℝ) : ℂ) := by\n      rw [Complex.ext_iff]\n      constructor\n      · simp\n      · simp [him]\n    have hsdiff : ‖(2 + t * Complex.I) - s‖ = |2 - s.re| := by\n      rw [hdiff]\n      exact Complex.norm_real _\n    have hsdiffle : ‖(2 + t * Complex.I) - s‖ ≤ 4.5 := by\n      rw [hsdiff, abs_le]\n      constructor <;> linarith\n    have hx : ‖s - ρ.1‖ ≥ |ρ.1.im - t| := by\n      have h1 := abs_im_le_norm (s - ρ.1)\n      have h2 : (s - ρ.1).im = t - ρ.1.im := by simp [him]\n      rw [h2, abs_sub_comm] at h1\n      exact h1\n    have hx₀ : ‖(2 + t * Complex.I) - ρ.1‖ ≥ Real.sqrt (1 + (ρ.1.im - t) ^ 2) := by\n      have hβ : |2 - ρ.1.re| ≥ 1 := by\n        have h1 := ρ.2.2.2\n        rw [abs_of_pos (by linarith : (0 : ℝ) < 2 - ρ.1.re)]\n        linarith\n      have h1 : ‖(2 + t * Complex.I) - ρ.1‖ ^ 2\n          = ((2 + t * Complex.I) - ρ.1).re ^ 2 + ((2 + t * Complex.I) - ρ.1).im ^ 2 := by\n        rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n      have h2 : (1 : ℝ) + (ρ.1.im - t) ^ 2 ≤ ‖(2 + t * Complex.I) - ρ.1‖ ^ 2 := by\n        rw [h1]\n        have hre : ((2 + t * Complex.I) - ρ.1).re = 2 - ρ.1.re := by simp\n        have him2 : ((2 + t * Complex.I) - ρ.1).im = t - ρ.1.im := by simp\n        rw [hre, him2]\n        have h3 : (2 - ρ.1.re) ^ 2 ≥ 1 := by\n          have h4 := pow_le_pow_left₀ (by norm_num : (0 : ℝ) ≤ 1) hβ 2\n          rwa [one_pow, sq_abs] at h4\n        have h5 : (t - ρ.1.im) ^ 2 = (ρ.1.im - t) ^ 2 := by ring\n        rw [h5]\n        linarith [h3, sq_nonneg (ρ.1.im - t)]\n      have h6 := Real.sqrt_le_sqrt h2\n      rwa [Real.sqrt_sq_eq_abs, abs_of_nonneg (norm_nonneg _)] at h6\n    -- assemble\n    have hpos1 : (0 : ℝ) < ‖s - ρ.1‖ * ‖(2 + t * Complex.I) - ρ.1‖ := by\n      have h7 : (0 : ℝ) < ‖s - ρ.1‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hs)\n      have h8 : (0 : ℝ) < ‖(2 + t * Complex.I) - ρ.1‖ :=\n        norm_pos_iff.mpr (sub_ne_zero.mpr hs₀)\n      positivity\n    have hpos2 : (0 : ℝ) < |ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2) := by\n      positivity\n    have h9 : ‖(2 + t * Complex.I) - s‖ ≤ 4.5 := hsdiffle\n    have hm : (0 : ℝ) ≤ (zeroMult ρ.1 : ℝ) := Nat.cast_nonneg _\n    rw [div_le_div_iff₀ hpos1 hpos2]\n    calc (zeroMult ρ.1 : ℝ) * ‖(2 + t * Complex.I) - s‖\n          * (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2))\n        ≤ (zeroMult ρ.1 : ℝ) * 4.5 * (‖s - ρ.1‖ * ‖(2 + t * Complex.I) - ρ.1‖) := by\n          apply mul_le_mul _ _ (by positivity) (by positivity)\n          · calc (zeroMult ρ.1 : ℝ) * ‖(2 + t * Complex.I) - s‖\n                ≤ (zeroMult ρ.1 : ℝ) * 4.5 := mul_le_mul_of_nonneg_left h9 hm\n            _ ≤ (zeroMult ρ.1 : ℝ) * 4.5 := le_rfl\n          · exact mul_le_mul hx hx₀ (Real.sqrt_nonneg _) (abs_nonneg _)\n      _ = (4.5 * (zeroMult ρ.1 : ℝ)) * (‖s - ρ.1‖ * ‖(2 + t * Complex.I) - ρ.1‖) := by ring\n\n/-- **The norm reduction**: the far-series norm is bounded by the farG\ntsum. -/\nlemma far_series_norm_le_farG_tsum {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t)\n    (hζ : riemannZeta s ≠ 0) :\n    ‖∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      if ρ ∈ nearZerosSub t then (0 : ℂ) else seriesDiffTerm s (2 + t * Complex.I) ρ‖\n      ≤ ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farG t ρ := by\n  classical\n  have hnorm_summ : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      ‖if ρ ∈ nearZerosSub t then (0 : ℂ) else seriesDiffTerm s (2 + t * Complex.I) ρ‖) := by\n    apply Summable.of_norm_bounded (farG_summable ht.le)\n    intro ρ\n    rw [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)]\n    exact seriesDiffTerm_norm_le_farG ht hσlo hσhi him hζ ρ\n  have h1 := norm_tsum_le_tsum_norm hnorm_summ\n  have h2 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      ‖if ρ ∈ nearZerosSub t then (0 : ℂ) else seriesDiffTerm s (2 + t * Complex.I) ρ‖)\n      ≤ ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farG t ρ :=\n    Summable.tsum_le_tsum (fun ρ => seriesDiffTerm_norm_le_farG ht hσlo hσhi him hζ ρ)\n      hnorm_summ (farG_summable ht.le)\n  exact h1.trans h2\n\nend NguyenRH1\n\nend"},"extra_content":null}]