[{"type":"thinking","thinking":"`Complex.ofReal_ratCast (q : ℚ) : ofReal ↑q = ↑q := rfl` — it's `rfl`! So ((q:ℝ):ℂ) = (q:ℂ) definitionally — the casts are defeq. So `Complex.norm_real` can apply through the defeq? For the norm: ‖(↑q : ℂ)‖ where the term is a direct ℚ→ℂ cast: since ((q:ℝ):ℂ) = (q:ℂ) by rfl, I can use `show ‖(((harmonic (n-1) : ℚ) : ℝ) : ℂ)‖ = _` — the show with the double-cast form is defeq ✓ then norm_real etc. Or simpler: keep everything in ℂ and avoid the ℝ detour: bound ‖−(γ:ℂ) + (↑H:ℂ)‖ directly via norm_sub_le? no — I want the exact real-abs form for the tight sign analysis... actually I don't need tight: ‖−(γ:ℂ) + (↑H:ℂ)‖ ≤ γ + H via: norm: ‖(↑x:ℂ)‖ = |x| for x real — the term −(γ:ℂ) + (↑H:ℂ) = ((−γ + H : ℝ) : ℂ) up to defeq (ofReal_neg/ofReal_add are rfl-ish simp): `show ‖((-Real.eulerMascheroniConstant + (harmonic (n-1) : ℚ) : ℝ) : ℂ)‖ ≤ _` — is the double-cast sum defeq to the goal's term? goal term: −(γ:ℂ) + (↑(harmonic..):ℂ): the components: (γ:ℂ) = ((γ:ℝ):ℂ) defeq ✓ (ofReal... γ is Real.eulerMascheroniConstant : ℝ; (γ:ℂ) is ℝ→ℂ ✓ direct); (↑(harmonic (n−1) : ℚ):ℂ) vs (((harmonic..):ℚ):ℝ):ℂ — defeq by ofReal_ratCast (rfl) ✓. So the show-form: ‖((−γ + ↑(harmonic (n−1)) : ℝ):ℂ)‖ — is −(γ:ℂ) + (↑H:ℂ) defeq to ↑((−γ + ↑H : ℝ))? ofReal_add : ((a+b:ℝ):ℂ) = (a:ℂ)+(b:ℂ) — is it rfl-defeq? ofReal is a RingHom application... the coe (↑(a+b)) vs (↑a + ↑b): these are defeq? Complex.ofReal is defined as a function; ↑(a+b) = ↑a + ↑b requires the ring-hom property — NOT rfl-defeq in general (it's a simp/norm_cast lemma). The `ofReal_ratCast (q) : ofReal ↑q = ↑q := rfl` IS rfl because both are the same underlying cast paths (Rat.cast to ℂ is defined via ofReal∘Rat.cast to ℝ probably). Hmm — risky. SAFEST: convert the goal term to the real-sum form via push_cast?? push_cast on ‖X‖ with X the complex sum: push_cast rewrites (↑(−γ+↑H))-type coercions outward: the goal ‖−(γ:ℂ) + (↑H:ℂ)‖ = |(−γ + ↑H : ℝ)|... push_cast doesn't produce the norm-real form. \n\nCleanest robust: prove the real-sub-level bound then transfer:\n```\n    have hreal : |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ)|\n        ≤ Real.eulerMascheroniConstant + (1 + Real.log (n - 1)) := by\n      have hH0 : (0 : ℝ) ≤ ((harmonic (n - 1) : ℚ) : ℝ) := by positivity\n      have hHbound : ((harmonic (n - 1) : ℚ) : ℝ) ≤ 1 + Real.log (n - 1) := harmonic_le_one_add_log (n - 1)\n      have h1 : (-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ)\n          ≤ Real.eulerMascheroniConstant + (1 + Real.log (n - 1)) := by\n        linarith [hγ0, hHbound]  -- −γ + H ≤ γ + (1+log) ⟺ H − (1+log) ≤ 2γ ✓ (H ≤ 1+log, γ ≥ 0)\n      have h2 : -(Real.eulerMascheroniConstant + (1 + Real.log (n - 1)))\n          ≤ (-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ) := by\n        -- −γ − (1+log) ≤ −γ + H ⟺ −(1+log) ≤ H: H ≥ 0 and −(1+log(n−1)) ≤ 0 ✓ hmm need log(n−1) ≥ ... for n = 2: log 1 = 0: 1 + log ≥ 1 > 0 ✓ for n ≥ 2: log(n−1) ≥ log 1 = 0 ✓: so −(1+log) ≤ 0 ≤ H ✓:\n        have hlog0 : (0 : ℝ) ≤ Real.log (n - 1) := by\n          apply Real.log_nonneg\n          have h1 : (1 : ℝ) ≤ ((n - 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ n - 1)\n          ... hmm (n−1 : ℕ) cast to ℝ: ((n−1:ℕ):ℝ) ≥ 1 for n ≥ 2 ✓\n        linarith [hH0, hlog0, hγ0]\n      exact abs_le.mpr ⟨h2, h1⟩\n    -- transfer to the complex norm\n    have hnrm : ‖-(Real.eulerMascheroniConstant : ℂ) + ((harmonic (n - 1) : ℚ) : ℂ)‖\n        = |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ)| := by\n      rw [← Complex.ofReal_ratCast?]... \n```\nFor the norm transfer: the goal-side term: −(γ:ℂ) + ((H:ℚ):ℂ). I'll show it equals (((−γ + (H:ℝ)) : ℝ) : ℂ) via push_cast?? The casts: (γ:ℂ) is ℝ→ℂ ✓; ((H:ℚ):ℂ) is ℚ→ℂ. push_cast normalizes mixed casts: ((H:ℚ):ℂ) — push_cast might rewrite to ((H:ℝ):ℂ) via ofReal_ratCast (it's norm_cast tagged ✓ per the grep: @[simp, norm_cast]). So: \n```\n    have hnrm : ‖-(Real.eulerMascheroniConstant : ℂ) + ((harmonic (n - 1) : ℚ) : ℂ)‖\n        = |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ)| := by\n      rw [← Complex.ofReal_neg, ← Complex.ofReal_add, ← Complex.ofReal_ratCast, Complex.norm_real,\n        Real.norm_eq_abs]\n```\nHmm — the ofReal_ratCast : ofReal ↑q = ↑q — the ← direction: ↑q → ofReal ↑q: rewrites ((harmonic..):ℚ):ℂ) → (((harmonic..):ℚ):ℝ):ℂ) ✓. Then ofReal_neg/ofReal_add ←: −(γ:ℂ) + (((H:ℝ)):ℂ) → ↑(−γ) + ↑(H:ℝ) → ↑((−γ + H:ℝ)): ✓ then norm_real : ‖(x:ℂ)‖ = ‖x‖_ℝ and Real.norm_eq_abs. Order matters: first ← ofReal_ratCast (converting the ℚ→ℂ cast to ℚ→ℝ→ℂ), then ← ofReal_add needs the args to be ℝ-casts: −(γ:ℂ) = −(↑(γ:ℝ))... ← ofReal_neg : −↑a → ↑(−a) ✓; then ← ofReal_add : ↑(−γ) + ↑(H) → ↑(−γ + H) ✓. So the rw chain: [← Complex.ofReal_ratCast, ← Complex.ofReal_neg, ← Complex.ofReal_add, Complex.norm_real, Real.norm_eq_abs]. Hmm — Complex.norm_real : ‖(r : ℂ)‖ = ‖r‖ — with r := (−γ + H : ℝ) ✓; Real.norm_eq_abs : ‖r‖ = |r| ✓.\n\nOK. Now the MAIN series case. Let me write it complete:\n\n```\n  · -- the series case: w not an integer\n    have hcomp : w ∈ Complex.integerComplement := hwint  -- mem iff: ¬∃ n:ℤ, ↑n = w — hwint's form after by_cases: ¬∃ m : ℤ, (↑m:ℂ) = w — mem_integerComplement_iff : x ∈ ℂ_ℤ ↔ ¬∃ n : ℤ, ↑n = x: the by_cases gives hwint : ¬(∃ m : ℤ, (↑m:ℂ) = w) directly — and membership is Iff.rfl — so exact hwint works? the membership x ∈ ℂ_ℤ unfolds to the negation by rfl ✓: `exact hwint`.\n    rw [DigammaSeries.digamma_series hcomp]\n    set A := w.re with hA_def\n    set N := ⌈w.re⌉₊ with hN_def\n    have hA0 : (0 : ℝ) < A := by linarith [hwre]\n    have hNA : A ≤ (N : ℝ) := by rw [hN_def]; exact Nat.le_ceil _\n    have hNA1 : (N : ℝ) ≤ A + 1 := by\n      have h := Nat.ceil_lt_add_one (show (0 : ℝ) ≤ w.re by linarith [hwre])\n      have h2 : ((⌈w.re⌉₊ : ℕ) : ℝ) < w.re + 1 := by exact_mod_cast h\n      rw [hN_def]; linarith [h2]\n    have hN1 : 1 ≤ N := by\n      have h1 := Nat.ceil_mono hwre  -- hmm Nat.ceil_mono : a ≤ b → ⌈a⌉₊ ≤ ⌈b⌉₊ — hwre : 2 ≤ w.re: ⌈(2:ℝ)⌉₊ ≤ ⌈w.re⌉₊\n      rwa [hN_def, Nat.ceil_ofNat] at h1  -- Nat.ceil_ofNat : ⌈(n:ℝ)⌉₊ = n: ⌈(2:ℝ)⌉₊ = 2: h1 : 2 ≤ ⌈w.re⌉₊; goal 1 ≤ N with N := ⌈w.re⌉₊: h1 gives 2 ≤ ... ⟹ 1 ≤: rwa... let me: have h1 : (2:ℕ) ≤ N := by rw [hN_def]; ... ; exact Nat.one_le_iff... no: omega from h1... simplest: have h1 : 2 ≤ N := by rw [hN_def]; exact Nat.ceil_mono hwre |>.trans_eq'?? — ugh. Write:\n      have h1 : (2 : ℕ) ≤ N := by\n        rw [hN_def]\n        have h2 := Nat.ceil_mono hwre  -- ⌈(2:ℝ)⌉₊ ≤ ⌈w.re⌉₊\n        rwa [Nat.ceil_ofNat] at h2\n      omega\n    -- the series summability + norm bound\n    have hterm_summ : Summable (fun n : ℕ => ‖1 / ((n : ℂ) + 1) - 1 / (w + n + 1)‖) :=\n      Summable.of_nonneg_of_le (fun n => norm_nonneg _) (fun n => norm_digamma_term_le hwre n)\n        (summable_digamma_majorant hwre)\n    -- the kernel analysis\n    have hker_summ : Summable (fun n : ℕ => (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹) := by\n      have h1 : Summable (fun n : ℕ => (((n : ℝ) + 1) ^ 2)⁻¹) := by\n        ... (clone from summable_digamma_majorant's proof — factor it as its own lemma? it's inline there. Let me factor `summable_nat_add_one_sq_inv : Summable (fun n : ℕ => (((n:ℝ)+1)^2)⁻¹)` as a standalone helper before summable_digamma_majorant and reuse.)\n      refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ h1\n      intro n\n      rw [inv_le_inv₀ (by positivity) (by positivity)]\n      -- goal ((n:ℝ)+1)^2 ≤ ((n:ℝ)+1)*(A+n+1)\n      rw [sq]\n      apply mul_le_mul_of_nonneg_left _ (by positivity)\n      have h2 := Nat.cast_nonneg n\n      linarith [hA0, h2]\n    ...\n```\nLet me factor the (n+1)⁻² summability as a helper `summable_nat_add_one_sq_inv` and use in both. \n\nThen the split:\n```\n    have hsplit : (∑' n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹)\n        = ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n          + ∑' n : ℕ, (((n : ℝ) + (N : ℝ) + 1) * (A + ((n : ℝ) + (N : ℝ)) + 1))⁻¹ := by\n      have h := hker_summ.sum_add_tsum_nat_add N  -- (∑ range N f) + ∑' (f (n+N)) = ∑' f\n      rw [← h]  -- goal becomes the sum form: need to match f (n+N) with my ((↑n + ↑N)+1)... — the shifted function: f (n+N) = (((↑(n+N):ℝ)+1)*(A+↑(n+N)+1))⁻¹ = (((↑n+↑N)+1)*(A+(↑n+↑N)+1))⁻¹ — my form has (↑n + ↑N) — push_cast difference. For the `rw [← h]` to close, the forms must match syntactically — they won't (↑(n+N) vs ↑n+↑N). So DON'T rw; instead:\n      rw [← h]\n      congr 1  -- hmm: goal ∑ range N f + ∑' n, myshift n = ∑ range N f + ∑' n, f (n+N): congr 1 reduces to the tsum equality: apply tsum_congr; intro n; push_cast; ring_nf?? — the inv arguments equal: congr 1; push_cast; ring — the forms ((↑n+↑N)+1)*(A+(↑n+↑N)+1) vs (↑(n+N)+1)*(A+↑(n+N)+1): push_cast turns ↑(n+N) → ↑n+↑N then both sides identical — but these are inside ⁻¹: congr 1 to reduce to the base equality: \n      refine tsum_congr fun n => ?_\n      push_cast\n      ring_nf\n```\nHmm — tsum_congr : (∀ i, f i = g i) → ∑' f = ∑' g ✓ exists. The per-term: (((↑n+↑N)+1)*(A+(↑n+↑N)+1))⁻¹ = (((↑(n+N):ℝ)+1)*(A+↑(n+N)+1))⁻¹: congr 1: (↑n+↑N+1)*(A+(↑n+↑N)+1) = (↑(n+N)+1)*(A+↑(n+N)+1): push_cast; ring ✓. But wait — after `rw [← h]` the goal is `∑ range N f + ∑' n, myshift n = ∑ range N f + ∑' n, f (n+N)` — congr 1 gives TWO goals (the finite sums equal — rfl) and the tsums: hmm congr 1 on a + b = c + d gives a = c and b = d: the finite sums are syntactically equal ⟹ closed by rfl automatically? congr 1 might leave `∑ range N f = ∑ range N f` (closed) and the tsum goal. Then tsum_congr per-term. But actually the per-term forms: myshift n vs f (n+N): my hsplit's statement writes the shifted term as (((n:ℝ) + (N:ℝ) + 1) * (A + ((n:ℝ) + (N:ℝ)) + 1))⁻¹ — to make the congruence `push_cast; ring` work the base expressions must be ring-equal after cast normalization ✓.\n\nHmm — actually simpler: state hsplit's shifted term EXACTLY as f (n+N): (((↑(n+N) : ℝ) + 1) * (A + ↑(n+N) + 1))⁻¹ — then rw [← h] closes definitionally ✓ and handle the cast-normalization in the TAIL bound step (where I compare with the telescope): tail: ∑' n, f (n+N) ≤ ∑' n, (1/(↑n+↑N) − 1/(↑n+↑N+1)): per-term: f (n+N) = ((↑(n+N)+1)(A+↑(n+N)+1))⁻¹ ≤ 1/(↑n+↑N) − 1/(↑n+↑N+1): the RHS = 1/((↑n+↑N)(↑n+↑N+1)) [field]: and the LHS ≤ that ⟺ (↑n+↑N)(↑n+↑N+1) ≤ (↑(n+N)+1)(A+↑(n+N)+1): with ↑(n+N) = ↑n+↑N (push_cast): (x)(x+1) vs (x+1)(A+x+1) with x = ↑n+↑N: ⟺ x ≤ A+x+1 ⟺ 0 ≤ A+1 ✓. So per-term:\n```\n    have htail_term : ∀ n : ℕ, (((↑(n + N) : ℝ) + 1) * (A + ↑(n + N) + 1))⁻¹\n        ≤ 1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1) := by\n      intro n\n      have hN0 : (0 : ℝ) < (n : ℝ) + N := by\n        have h1 := Nat.cast_nonneg n\n        have h2 : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN1\n        linarith [h1, h2]\n      have htelesplit : (1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)\n          = (((n : ℝ) + N) * ((n : ℝ) + N + 1))⁻¹ := by\n        field_simp [hN0.ne']  -- 1/x − 1/(x+1) = 1/(x(x+1)): field_simp then ring — careful field_simp may close... write: field_simp [hN0.ne', (hN0.trans... (x+1 ≠ 0)]; ring — risk gotcha. Alternative: rw [div_sub_div _ _ hN0.ne' (by positivity... (x+1) ≠ 0)]; then ring_nf? div_sub_div (a b) (ha : c ≠ 0) (hb : d ≠ 0) : a/c − b/d = (a*d − b*c)/(c*d): then (1*(x+1) − 1*x)/(x*(x+1)) = 1/(x(x+1)): ring_nf normalize? The LHS (x+1−x)/(x(x+1)) = 1/(x(x+1)): div_eq: field_simp safest: \n        rw [div_sub_div _ _ hN0.ne' (by positivity : ((n : ℝ) + N + 1) ≠ 0)]\n        rw [div_eq_iff (by positivity : (0:ℝ) < ((n:ℝ)+N)*((n:ℝ)+N+1))]  -- hmm goal (1*(x+1) − 1*x)/(x*(x+1)) = (x*(x+1))⁻¹: div_eq_iff (hb : b ≠ 0): a/b = c ↔ a = c*b: (x*(x+1))⁻¹ as c: rw [div_eq_iff ...]: 1*(x+1) − 1*x = (x*(x+1))⁻¹ * (x*(x+1)): RHS = 1 (inv_mul_cancel₀): rw [inv_mul_cancel₀ (by positivity : (x*(x+1)) ≠ 0)]; ring (1*(x+1) − 1*x = 1: ring ✓)\n        ...\n      rw [htelesplit]\n      -- goal ((↑(n+N)+1)(A+↑(n+N)+1))⁻¹ ≤ ((x)(x+1))⁻¹ with x = ↑n+↑N: inv_le_inv₀ (pos) (the ≤): \n      apply inv_le_inv₀ (by positivity)  -- hmm inv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a: goal LHS⁻¹ ≤ RHS⁻¹ ⟺ RHS-denom ≤ LHS-denom: (x)(x+1) ≤ (↑(n+N)+1)(A+↑(n+N)+1): \n      · -- the ≤\n        push_cast [Nat.cast_add]  -- normalize ↑(n+N) → ↑n + ↑N\n        have h1 := Nat.cast_nonneg n\n        nlinarith [hA0, h1, hN0]  -- (x+1)(A+x+1) − x(x+1) = (x+1)(A+1) ≥ 0\n      · -- positivity of the RHS denom\n        positivity?? (0:ℝ) < (↑n+↑N)*(↑n+↑N+1): mul_pos hN0 (by linarith [hN0]) — hmm after push_cast ordering... let me put the positivity first. \n```\nOK — I'll manage these at compile time. The tail sum:\n```\n    have htail : ∑' n : ℕ, (((↑(n + N) : ℝ) + 1) * (A + ↑(n + N) + 1))⁻¹ ≤ 1 / (N : ℝ) := by\n      have h1 : Summable (fun n : ℕ => (((↑(n + N) : ℝ) + 1) * (A + ↑(n + N) + 1))⁻¹) :=\n        (summable_nat_add_iff N).mpr hker_summ  -- summable_nat_add_iff (k) : Summable (fun n => f (n + k)) ↔ Summable f ✓\n      calc ∑' n : ℕ, (((↑(n + N) : ℝ) + 1) * (A + ↑(n + N) + 1))⁻¹\n          ≤ ∑' n : ℕ, (1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)) :=\n            tsum_le_tsum htail_term h1 (tsum_one_div_sub_telescope N hN1 ▸ ...).summable?? — the telescope's summability: (tsum_one_div_sub_telescope N hN1) is an equality; the Summable: HasSum (from the hasSum_iff_tendsto route) — hmm my tsum_one_div_sub_telescope returns the tsum equality, not HasSum. Get summability: `Summable.of...`: the telescope sequence has a tsum (= 1/N) ⟹ Summable: `summable_of_...`: from the equality: Summable f iff ∃ a, HasSum f a: I have HasSum inside the proof... restate tsum_one_div_sub_telescope to also give the HasSum: add `hasSum_one_div_sub_telescope : HasSum (...) (1/N)` as the main and derive the tsum version from it. Let me restructure §1 to expose the HasSum version.\n            (hasSum_one_div_sub_telescope N hN1).summable\n        _ = 1 / (N : ℝ) := hasSum_one_div_sub_telescope N hN1 |>.tsum_eq\n```\nOK — restructure §1: `hasSum_one_div_sub_telescope` (the HasSum) + `tsum_one_div_sub_telescope` (derived). I already have the HasSum inline (hHasSum) — just make it standalone.\n\nHead bound:\n```\n    have hhead : ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n        ≤ (1 + Real.log (N : ℝ)) / A := by\n      calc ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n          ≤ ∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹ / A := by\n            apply Finset.sum_le_sum\n            intro n _\n            -- ((n+1)(A+n+1))⁻¹ ≤ (n+1)⁻¹/A ⟺ (n+1)*A ≤ (n+1)(A+n+1): \n            rw [div_eq_mul_inv, inv_le_inv₀ (by positivity) (by positivity)]\n            -- goal A*(n+1) ≤ (n+1)*(A+n+1): ring-normalize: nlinarith\n            have h2 := Nat.cast_nonneg n\n            nlinarith [hA0, h2]\n        _ = (1 + Real.log (N : ℝ)) / A := by\n            -- ∑ (n+1)⁻¹/A = (1/A)·∑(n+1)⁻¹·... per-term: (↑n+1)⁻¹/A = (1/A)·(↑n+1)⁻¹ hmm: (n+1)⁻¹/A = (1/(n+1))/A ✓ div_div: = 1/(A(n+1)): then ∑ 1/(A(n+1)) = (1/A)∑1/(n+1): via Finset.mul_sum backwards:\n            rw [← Finset.mul_sum]  -- hmm: Finset.mul_sum : a * ∑ f = ∑ a * f: ← direction turns ∑ (1/A)·... — the per-term form must match a * f n: (1/A) * (1/(↑n+1)): my terms are (↑n+1)⁻¹/A: convert: \n            rw [show (1 + Real.log (N:ℝ)) / A = (1/A) * (1 + Real.log (N:ℝ)) by rw [div_eq_mul_inv, mul_comm]]\n            rw [← Finset.mul_sum]\n            apply Finset.sum_congr rfl\n            intro n _\n            rw [div_eq_mul_inv, mul_inv, one_div]  -- (↑n+1)⁻¹/A → (↑n+1)⁻¹ * A⁻¹; goal: (↑n+1)⁻¹ * A⁻¹ = (1/A) * (↑n+1)⁻¹: mul_comm... \n            ring\n      -- then the harmonic bound\n      have hS := sum_one_div_le_one_add_log N\n      ... (the (1/A) * Σ ≤ (1/A)(1+log N) via mul_le_mul_of_nonneg_left + the form shuffle)\n```\nHmm wait — my calc's first step target `(↑n+1)⁻¹/A` per-term and second step converts to (1/A)(1+log N)/... Let me restructure the head as a direct chain:\n```\n    have hhead : ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n        ≤ (1 + Real.log (N : ℝ)) / A := by\n      have hS := sum_one_div_le_one_add_log N\n      have hper : ∀ n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n          ≤ (1 / A) * (1 / ((n : ℝ) + 1)) := by\n        intro n\n        have h1 : (0 : ℝ) < (n : ℝ) + 1 := by positivity\n        have h2 := Nat.cast_nonneg n\n        rw [div_eq_mul_inv, mul_inv, one_div, one_div]  -- hmm LHS ((n+1)(A+n+1))⁻¹ vs (A⁻¹)*((n+1)⁻¹): inv_le_inv₀ forms... \n        -- goal: ((n+1)(A+n+1))⁻¹ ≤ A⁻¹ * (n+1)⁻¹ ⟺ same as (A(n+1))⁻¹ ≤ ... : since (A(n+1)) ≤ ((n+1)(A+n+1)): inv flips: ((n+1)(A+n+1))⁻¹ ≤ (A(n+1))⁻¹ = A⁻¹(n+1)⁻¹: \n        rw [show (1 / A) * (1 / ((n : ℝ) + 1)) = (A * ((n : ℝ) + 1))⁻¹ by\n          rw [one_div, one_div, ← mul_inv]]  -- (A*(n+1))⁻¹ = A⁻¹*(n+1)⁻¹ ✓ mul_inv\n        apply inv_le_inv₀ (by positivity)  -- goal: A*(n+1) ≤ (n+1)*(A+n+1): \n        nlinarith [hA0, h2]\n      calc ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n          ≤ ∑ n ∈ Finset.range N, (1 / A) * (1 / ((n : ℝ) + 1)) := Finset.sum_le_sum fun n _ => hper n\n        _ = (1 / A) * ∑ n ∈ Finset.range N, (1 / ((n : ℝ) + 1)) := Finset.mul_sum.symm  -- mul_sum : a * ∑ = ∑ a*f: Finset.mul_sum.symm : ∑ (a * f i) = a * ∑ f — hmm the name: `Finset.mul_sum : a * (∑ i, f i) = ∑ i, a * f i` — so .symm : ∑ a*f = a*∑ ✓ but the per-term form: my terms (1/A)*(1/(↑n+1)) with f n := 1/(↑n+1): matches ✓. Hmm — Finset.mul_sum signature: `Finset.mul_sum (s) (f) (a) : a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i`? arg order varies by version. Use rw [Finset.mul_sum] at the right spot or exact (Finset.mul_sum ...).symm — iterate at build.\n        _ ≤ (1 + Real.log (N : ℝ)) / A := by\n            rw [div_eq_mul_inv]  -- RHS → (1+log N)*A⁻¹\n            rw [mul_comm (1 / A)]  -- hmm LHS (1/A) * Σ = (A⁻¹)*Σ: 1/A = A⁻¹: one_div: rw [one_div]: LHS A⁻¹ * Σ; goal A⁻¹*Σ ≤ (1+log N)*A⁻¹: \n            rw [mul_comm (1 + Real.log (N : ℝ)) (A⁻¹)]  -- ugh A⁻¹ as a term — after one_div rewrite... \n```\nThese mul_comm shuffles are error-prone to predict. ROBUST ALTERNATIVE: use `gcongr`!! gcongr handles a * x ≤ a * y with side goal Σ ≤ 1+log N: \n```\n        _ ≤ (1 + Real.log (N : ℝ)) / A := by\n            rw [div_eq_mul_inv, one_div]  -- hmm\n            gcongr  -- (1/A)*Σ ≤ (1+log N)*A⁻¹: gcongr should match A⁻¹ * Σ ≤ (1+log N) * A⁻¹: the factors: A⁻¹ vs (1+log N) are the varying ones... gcongr compares products component-wise: A⁻¹ ≤ 1+log N?? no — the pattern: a₁*b₁ ≤ a₂*b₂ — gcongr tries a₁ ≤ a₂ and b₁ ≤ b₂ — that's wrong (I want a₁ = a₂ = A⁻¹ and Σ ≤ 1+log N). gcongr with the equal first factor: it recognizes a * x ≤ a * y patterns: side goal Σ ≤ 1+log N ✓. The forms must match: LHS (1/A)*Σ and RHS (1+log N)/A: after rw [div_eq_mul_inv, one_div]: LHS A⁻¹*Σ; RHS (1+log N)*A⁻¹ — commuted! gcongr might still match (it's robust to comm? gcongr uses the ordered-multiplication lemmas which need same-order). Fix by rewriting RHS as A⁻¹*(1+log N): rw [div_eq_mul_inv, mul_comm ((1 + Real.log ↑N)) (A⁻¹)]?? the A⁻¹ atom naming... ugh. Use: have hA0' : (0:ℝ) < A := ...; rw [div_eq_mul_inv]; exact mul_le_mul_of_nonneg_left hS (inv_nonneg.mpr hA0'.le) — mul_le_mul_of_nonneg_left (h : b ≤ c) (ha : 0 ≤ a) : a * b ≤ a * c: with a := A⁻¹, b := Σ, c := 1+log N: gives A⁻¹*Σ ≤ A⁻¹*(1+log N): the goal after rw [div_eq_mul_inv]: (1/A)*Σ ≤ (1+log N)*A⁻¹ — the LHS (1/A)*Σ: is 1/A elaborated as A⁻¹ already? div_eq_mul_inv : a/b = a * b⁻¹: so 1/A = 1 * A⁻¹?? — 1/A parses as OfNat.ofNat 1 / A: div_eq_mul_inv gives 1 * A⁻¹ — NOT A⁻¹ syntactically (extra 1*). one_mul needed. UGH. \n\nOK — definitive robust pattern avoiding all this: state the head bound as `∑ ... ≤ (1 + Real.log N) / A` and prove via `div_le_iff₀`:\n```\n      rw [div_le_iff₀ hA0']  -- goal: ∑ (...) ≤ (1 + log N) * A?? NO — div_le_iff₀ (hc : 0 < c) : a/c ≤ b ↔ a ≤ b*c: my goal ∑ ≤ (1+log N)/A has the form X ≤ b/c: use `le_div_iff₀ (hc : 0 < c) : a ≤ b/c ↔ a * c ≤ b` ✓ (journal-024 banked le_div_iff₀? they banked div_le_iff₀ — le_div_iff₀ presumably exists too): rw [le_div_iff₀ hA0']: goal (∑ ...)*A ≤ 1 + log N:\n      calc (∑ n ∈ range N, ...) * A ≤ ((1/A) * ∑ 1/(n+1)) * A := by gcongr (per-term hper)?? — still the per-term...\n```\nFINE. Let me stop trying to predict the exact tactic sequence and just write a reasonable first attempt, then fix what the compiler says. The mul/div micro-algebra will take a couple of iterations; that's normal for this codebase (every session's journal has these).\n\nGiven the volume, let me write §2's main theorem now in full as an Edit-append (via matching the file's current last lines), accepting it'll need 3-5 compile iterations. To reduce the commutation pain, I'll use `field_simp`-free explicit two-step haves with `calc` and accept verbosity.\n\nActually — a cleaner trick for the head: per-term ((n+1)(A+n+1))⁻¹ ≤ (n+1)⁻¹ * A⁻¹ via the inv comparison, then:\n∑ ≤ ∑ (n+1)⁻¹ * A⁻¹ = (∑ (n+1)⁻¹) * A⁻¹ [Finset.sum_mul] ≤ (1+log N) * A⁻¹ [mul_le_mul_of_nonneg_right hS (inv_nonneg...)] = (1+log N)/A [div_eq_mul_inv.symm]. The Finset.sum_mul : (∑ i, f i) * a = ∑ i, f i * a — so ← Finset.sum_mul turns ∑ (f i * a) into (∑ f) * a ✓. Per-term: (n+1)⁻¹ * A⁻¹ = f n * A⁻¹ ✓ matches Finset.sum_mul's pattern. So:\n```\n      calc ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n          ≤ ∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹ * A⁻¹ := Finset.sum_le_sum fun n _ => hper n\n        _ = (∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹) * A⁻¹ := by rw [← Finset.sum_mul]\n        _ ≤ (1 + Real.log (N : ℝ)) * A⁻¹ :=\n            mul_le_mul_of_nonneg_right hS' (inv_nonneg.mpr hA0.le)\n        _ = (1 + Real.log (N : ℝ)) / A := by rw [div_eq_mul_inv]\n```\nwhere hper n : ((n+1)(A+n+1))⁻¹ ≤ (n+1)⁻¹ * A⁻¹: \n```\n    have hper : ∀ n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹ ≤ ((n : ℝ) + 1)⁻¹ * A⁻¹ := by\n      intro n\n      rw [← mul_inv]  -- RHS → (n+1)⁻¹ * A⁻¹ = ((n+1)*A)⁻¹: ← mul_inv : a⁻¹ * b⁻¹ = (a*b)⁻¹ ✓\n      apply inv_le_inv₀ (by positivity)  -- goal: (n+1)*A ≤ (n+1)*(A+n+1)\n      · -- the ≤: (n+1)*A ≤ (n+1)*(A+n+1) ⟺ 0 ≤ (n+1)(n+1)·: mul_le_mul_of_nonneg_left (A ≤ A+n+1) (0 ≤ n+1):\n        apply mul_le_mul_of_nonneg_left _ (by positivity)\n        have h2 := Nat.cast_nonneg n\n        linarith [hA0, h2]\n      · -- hmm inv_le_inv₀'s second arg: 0 < the other side: (0:ℝ) < ((n+1)*(A+n+1)): positivity? knows A = w.re... A is set — positivity needs 0 < A: not visible. Give explicitly:\n```\ninv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a — the apply inv_le_inv₀ leaves TWO goals? No — inv_le_inv₀ is an iff: use (inv_le_inv₀ ha hb).mpr h — term-mode: `(inv_le_inv₀ (by positivity : (0:ℝ) < (n+1)*A) (by ...)).mpr ?_` with the second positivity needing A > 0 explicitly:\n```\n      have h1 : (0 : ℝ) < ((n : ℝ) + 1) * A := by positivity  -- hmm positivity needs 0 < A: A is set to w.re: positivity can't see hwre. Provide: mul_pos (by positivity) hA0 — but A is the set var: hA0 : 0 < A ✓ in context: mul_pos (by positivity : (0:ℝ) < (n:ℝ)+1) hA0 ✓\n      have h2 : (0 : ℝ) < ((n : ℝ) + 1) * (A + (n : ℝ) + 1) := by\n        apply mul_pos (by positivity)\n        have h3 := Nat.cast_nonneg n\n        linarith [hA0, h3]\n      apply (inv_le_inv₀ h1 h2).mpr\n      -- goal: (n+1)*(A+n+1) ≤ (n+1)*A?? NO — inv_le_inv₀ h1 h2 : ((n+1)*A)⁻¹ ≤ ((n+1)(A+n+1))⁻¹ ↔ ((n+1)(A+n+1)) ≤ ((n+1)*A) — WRONG DIRECTION! I want ((n+1)(A+n+1))⁻¹ ≤ ((n+1)A)⁻¹ ⟺ (n+1)A ≤ (n+1)(A+n+1): so inv_le_inv₀ with a := (n+1)(A+n+1), b := (n+1)*A: (inv_le_inv₀ h2 h1).mpr (the ≤ : (n+1)*A ≤ (n+1)(A+n+1)): \n      apply (inv_le_inv₀ h2 h1).mpr\n      apply mul_le_mul_of_nonneg_left _ (by positivity)\n      have h3 := Nat.cast_nonneg n\n      linarith [hA0, h3]\n```\n✓. And hS' : ∑ (n+1)⁻¹ ≤ 1 + log N — my sum_one_div_le_one_add_log is stated with 1/(↑n+1) — the (n+1)⁻¹ form: one_div bridge: hS : ∑ 1/(↑n+1) ≤ 1+log N; my sum here: ∑ (↑n+1)⁻¹: convert: simp only [one_div] to unify: add a variant or state hS with one_div at use:\n```\n      have hS' : (∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹) ≤ 1 + Real.log (N : ℝ) := by\n        have h := sum_one_div_le_one_add_log N\n        simpa [one_div] using h\n```\n✓.\n\nOK. I've spent a lot on planning — time to WRITE and let the compiler guide. Writing §2's main theorem as an Edit append now, complete, then compile.","signature":""},{"type":"text","text":"Writing §2's main theorem via Edit-append, complete (compiler will guide the micro-algebra)."},{"type":"tool_use","id":"Edit_268","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean","old_string":"    rw [Rat.cast_inv, Rat.cast_natCast, one_div]\n  rw [h1]\n  exact harmonic_le_one_add_log N","new_string":"    rw [Rat.cast_inv, Rat.cast_natCast, one_div]\n  rw [h1]\n  exact harmonic_le_one_add_log N\n\n/-- **The right-half-plane digamma bound (B)**: for re w ≥ 2, |im w| ≤ 5,\n‖ψ(w)‖ ≤ 20·log(2+‖w‖). Weierstrass series + split at N = ⌈re w⌉₊;\npositive integers via the harmonic identity. -/\ntheorem norm_digamma_le_of_two_le_re {w : ℂ} (hwre : 2 ≤ w.re) (hwim : |w.im| ≤ 5) :\n    ‖Complex.digamma w‖ ≤ 20 * Real.log (2 + ‖w‖) := by\n  have hw_norm_ge : 2 ≤ ‖w‖ := by\n    have h1 := Complex.abs_re_le_norm w\n    rwa [abs_of_nonneg (by linarith [hwre])] at h1\n  have hlog4 : (5 : ℝ) / 3 ≤ 19 * Real.log (2 + ‖w‖) := by\n    have h1 : Real.log 4 ≤ Real.log (2 + ‖w‖) :=\n      Real.log_le_log (by norm_num) (by linarith [hw_norm_ge])\n    have h2 : (1 : ℝ) < Real.log 4 := by\n      have h3 := Real.log_two_lt_d9.le\n      have h4 := Real.log_two_gt_d9.le\n      have h5 : Real.log 4 = 2 * Real.log 2 := by\n        rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]\n        push_cast\n        ring\n      linarith [h3, h4, h5]\n    nlinarith [h1, h2]\n  by_cases hwint : ∃ m : ℤ, (m : ℂ) = w\n  · -- the positive-integer case: w = ↑n, n ≥ 2\n    obtain ⟨m, hm⟩ := hwint\n    have hmre : w.re = (m : ℝ) := by rw [← hm]; simp\n    have hm2 : 2 ≤ m := by\n      by_contra h\n      push Not at h\n      have h1 : (m : ℝ) ≤ 1 := by exact_mod_cast (show m ≤ 1 by omega)\n      linarith [hwre, hmre, h1]\n    have hn2 : 2 ≤ m.toNat := by\n      have h1 : (2 : ℤ).toNat ≤ m.toNat := Int.toNat_mono hm2\n      have h2 : (2 : ℤ).toNat = 2 := by decide\n      rwa [h2] at h1\n    set n := m.toNat with hn_def\n    have hwn : w = (n : ℂ) := by\n      rw [← hm, hn_def]\n      exact_mod_cast Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ m)\n    rw [hwn, digamma_natCast_eq n (by omega)]\n    have hγ0 : (0 : ℝ) ≤ Real.eulerMascheroniConstant :=\n      Real.one_half_lt_eulerMascheroniConstant.le.trans (by norm_num)\n    have hreal : |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ)|\n        ≤ Real.eulerMascheroniConstant + (1 + Real.log (n - 1)) := by\n      have hH0 : (0 : ℝ) ≤ ((harmonic (n - 1) : ℚ) : ℝ) := by positivity\n      have hHbound : ((harmonic (n - 1) : ℚ) : ℝ) ≤ 1 + Real.log (n - 1) :=\n        harmonic_le_one_add_log (n - 1)\n      have hlog0 : (0 : ℝ) ≤ Real.log ((n : ℝ) - 1) := by\n        apply Real.log_nonneg\n        have h1 : (1 : ℝ) ≤ ((n - 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ n - 1)\n        have h2 : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by\n          rw [Nat.cast_sub (by omega : 1 ≤ n)]\n          push_cast\n          ring\n        linarith [h1, h2]\n      apply abs_le.mpr\n      constructor <;> linarith [hγ0, hH0, hHbound, hlog0]\n    have hnrm : ‖-(Real.eulerMascheroniConstant : ℂ) + ((harmonic (n - 1) : ℚ) : ℂ)‖\n        = |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : ℚ) : ℝ)| := by\n      rw [← Complex.ofReal_ratCast, ← Complex.ofReal_neg, ← Complex.ofReal_add,\n        Complex.norm_real, Real.norm_eq_abs]\n    rw [hnrm]\n    have hlogn1 : Real.log ((n : ℝ) - 1) ≤ Real.log (2 + ‖w‖) := by\n      apply Real.log_le_log (by\n        have h1 : (1 : ℝ) ≤ ((n - 1 : ℕ) : ℝ) := by exact_mod_cast (by omega : 1 ≤ n - 1)\n        have h2 : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by\n          rw [Nat.cast_sub (by omega : 1 ≤ n)]\n          push_cast\n          ring\n        linarith [h1, h2])\n      have hwnorm : ‖w‖ = (n : ℝ) := by rw [hwn, RCLike.norm_natCast]\n      rw [hwnorm]\n      have h3 : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by\n        rw [Nat.cast_sub (by omega : 1 ≤ n)]\n        push_cast\n        ring\n      linarith [h3]\n    -- |−γ + H| ≤ γ + 1 + log(n−1) ≤ 2/3 + 1 + log(2+‖w‖) and fold\n    have hγ1 : Real.eulerMascheroniConstant ≤ 1 :=\n      Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)\n    have h1 : Real.log (2 + ‖w‖) ≤ Real.log (2 + ‖w‖) := le_rfl\n    linarith [hreal, hγ1, hlogn1, hlog4]\n  · -- the series case: w off the integers\n    have hcomp : w ∈ Complex.integerComplement := hwint\n    rw [DigammaSeries.digamma_series hcomp]\n    set A := w.re with hA_def\n    set N := ⌈w.re⌉₊ with hN_def\n    have hA0 : (0 : ℝ) < A := by linarith [hwre]\n    have hNA : A ≤ (N : ℝ) := by rw [hN_def]; exact Nat.le_ceil _\n    have hNA1 : (N : ℝ) ≤ A + 1 := by\n      have h := Nat.ceil_lt_add_one (show (0 : ℝ) ≤ w.re by linarith [hwre])\n      have h2 : ((⌈w.re⌉₊ : ℕ) : ℝ) < w.re + 1 := by exact_mod_cast h\n      rw [hN_def]\n      linarith [h2]\n    have hN1 : 1 ≤ N := by\n      have h1 : (2 : ℕ) ≤ N := by\n        rw [hN_def]\n        have h2 := Nat.ceil_mono hwre\n        rwa [Nat.ceil_ofNat] at h2\n      omega\n    have hterm_summ : Summable (fun n : ℕ => ‖1 / ((n : ℂ) + 1) - 1 / (w + n + 1)‖) :=\n      Summable.of_nonneg_of_le (fun n => norm_nonneg _) (fun n => norm_digamma_term_le hwre n)\n        (summable_digamma_majorant hwre)\n    -- the kernel: summable, split bound\n    have hker_summ : Summable (fun n : ℕ => (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹) := by\n      have h1 : Summable (fun n : ℕ => (((n : ℝ) + 1) ^ 2)⁻¹) := by\n        have h2 : Summable (fun n : ℕ => (((n : ℝ)) ^ 2)⁻¹) := by\n          have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : ℝ) < 2)\n          have heq : (fun n : ℕ => ((n : ℝ) ^ (2 : ℝ))⁻¹)\n              = fun n : ℕ => (((n : ℝ)) ^ 2)⁻¹ := by\n            funext n\n            rw [show ((2 : ℝ)) = ((2 : ℕ) : ℝ) by norm_num, Real.rpow_natCast]\n          rwa [heq] at h3\n        have h4 := (summable_nat_add_iff 1).mpr h2\n        simpa [add_comm] using h4\n      refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ h1\n      intro n\n      apply (inv_le_inv₀ (by positivity) (by positivity)).mpr\n      rw [sq]\n      apply mul_le_mul_of_nonneg_left _ (by positivity)\n      have h2 := Nat.cast_nonneg n\n      linarith [hA0, h2]\n    have hsplit : (∑' n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹)\n        = ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n          + ∑' n : ℕ, ((((n + N : ℕ) : ℝ) + 1) * (A + ((n + N : ℕ) : ℝ) + 1))⁻¹ := by\n      rw [← hker_summ.sum_add_tsum_nat_add N]\n    -- the head bound\n    have hhead : ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n        ≤ (1 + Real.log (N : ℝ)) / A := by\n      have hper : ∀ n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n          ≤ ((n : ℝ) + 1)⁻¹ * A⁻¹ := by\n        intro n\n        have h1 : (0 : ℝ) < ((n : ℝ) + 1) * A := mul_pos (by positivity) hA0\n        have h2 : (0 : ℝ) < ((n : ℝ) + 1) * (A + (n : ℝ) + 1) := by\n          apply mul_pos (by positivity)\n          have h3 := Nat.cast_nonneg n\n          linarith [hA0, h3]\n        rw [← mul_inv]\n        apply (inv_le_inv₀ h2 h1).mpr\n        apply mul_le_mul_of_nonneg_left _ (by positivity)\n        have h3 := Nat.cast_nonneg n\n        linarith [hA0, h3]\n      have hS' : (∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹) ≤ 1 + Real.log (N : ℝ) := by\n        have h := sum_one_div_le_one_add_log N\n        simpa [one_div] using h\n      calc ∑ n ∈ Finset.range N, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹\n          ≤ ∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹ * A⁻¹ :=\n            Finset.sum_le_sum fun n _ => hper n\n        _ = (∑ n ∈ Finset.range N, ((n : ℝ) + 1)⁻¹) * A⁻¹ := by rw [← Finset.sum_mul]\n        _ ≤ (1 + Real.log (N : ℝ)) * A⁻¹ :=\n            mul_le_mul_of_nonneg_right hS' (inv_nonneg.mpr hA0.le)\n        _ = (1 + Real.log (N : ℝ)) / A := by rw [div_eq_mul_inv]\n    -- the tail bound\n    have htail : (∑' n : ℕ, ((((n + N : ℕ) : ℝ) + 1) * (A + ((n + N : ℕ) : ℝ) + 1))⁻¹)\n        ≤ 1 / (N : ℝ) := by\n      have h1 : Summable (fun n : ℕ => ((((n + N : ℕ) : ℝ) + 1) * (A + ((n + N : ℕ) : ℝ) + 1))⁻¹) :=\n        (summable_nat_add_iff N).mpr hker_summ\n      have hterm : ∀ n : ℕ, ((((n + N : ℕ) : ℝ) + 1) * (A + ((n + N : ℕ) : ℝ) + 1))⁻¹\n          ≤ 1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1) := by\n        intro n\n        have hN0 : (0 : ℝ) < (n : ℝ) + N := by\n          have h2 := Nat.cast_nonneg n\n          have h3 : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN1\n          linarith [h2, h3]\n        have htele : (1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)\n            = (((n : ℝ) + N) * ((n : ℝ) + N + 1))⁻¹ := by\n          rw [div_sub_div _ _ hN0.ne' (by positivity)]\n          rw [div_eq_iff (by positivity : (0 : ℝ) < ((n : ℝ) + N) * ((n : ℝ) + N + 1))]\n          rw [inv_mul_cancel₀ (by positivity : ((n : ℝ) + N) * ((n : ℝ) + N + 1) ≠ 0)]\n          ring\n        rw [htele]\n        have h2 : (0 : ℝ) < ((n : ℝ) + N) * ((n : ℝ) + N + 1) := by positivity\n        have h3 : (0 : ℝ) < (((n + N : ℕ) : ℝ) + 1) * (A + ((n + N : ℕ) : ℝ) + 1) := by\n          apply mul_pos (by positivity)\n          have h4 := Nat.cast_nonneg n\n          have h5 : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN1\n          push_cast\n          linarith [hA0, h4, h5]\n        apply (inv_le_inv₀ h3 h2).mpr\n        push_cast\n        have h4 := Nat.cast_nonneg n\n        nlinarith [hA0, h4, hN0]\n      calc (∑' n : ℕ, ((((n + N : ℕ) : ℝ) + 1) * (A + ((n + N : ℕ) : ℝ) + 1))⁻¹)\n          ≤ ∑' n : ℕ, (1 / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)) :=\n            tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable\n        _ = 1 / (N : ℝ) := (hasSum_one_div_sub_telescope N hN1).tsum_eq\n    -- assemble the series bound\n    have hN0R : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN1\n    have hkernel_bound : (∑' n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹)\n        ≤ (2 + Real.log (A + 1)) / A := by\n      rw [hsplit]\n      have h1 : (1 + Real.log (N : ℝ)) / A ≤ (1 + Real.log (A + 1)) / A := by\n        apply div_le_div_of_nonneg_left _ hA0\n        have h2 : Real.log (N : ℝ) ≤ Real.log (A + 1) :=\n          Real.log_le_log hN0R hNA1\n        linarith [h2]\n      have h2 : (1 : ℝ) / (N : ℝ) ≤ 1 / A := one_div_le_one_div_of_le hA0 hNA\n      linarith [h1, h2, hhead, htail]\n    -- the norm of the series\n    have hser : ‖∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (w + n + 1))‖\n        ≤ (‖w‖ / A) * (2 + Real.log (A + 1)) := by\n      calc ‖∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (w + n + 1))‖\n          ≤ ∑' n : ℕ, ‖1 / ((n : ℂ) + 1) - 1 / (w + n + 1)‖ :=\n            norm_tsum_le_tsum_norm hterm_summ\n        _ ≤ ∑' n : ℕ, ‖w‖ / (((n : ℝ) + 1) * (A + (n : ℝ) + 1)) :=\n            tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ\n              (summable_digamma_majorant hwre)\n        _ = ‖w‖ * ∑' n : ℕ, (((n : ℝ) + 1) * (A + (n : ℝ) + 1))⁻¹ := by\n            rw [tsum_mul_left]\n            apply tsum_congr\n            intro n\n            rw [div_eq_mul_inv]\n        _ ≤ ‖w‖ * ((2 + Real.log (A + 1)) / A) :=\n            mul_le_mul_of_nonneg_left hkernel_bound (norm_nonneg _)\n        _ = (‖w‖ / A) * (2 + Real.log (A + 1)) := by ring\n    -- the ratio ‖w‖/A ≤ 3\n    have hratio : ‖w‖ / A ≤ 3 := by\n      have h1 : ‖w‖ ≤ 3 * A := by\n        have hnormsq : ‖w‖ ^ 2 = w.re ^ 2 + w.im ^ 2 := by\n          rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n          ring\n        have him5 : w.im ^ 2 ≤ 25 := by\n          calc w.im ^ 2 = |w.im| ^ 2 := by rw [sq_abs]\n            _ ≤ 5 ^ 2 := pow_le_pow_left₀ (abs_nonneg _) hwim _\n            _ = 25 := by norm_num\n        have h2 : ‖w‖ ^ 2 ≤ (3 * A) ^ 2 := by\n          rw [hnormsq]\n          have hA2 : 2 ≤ A := hwre\n          nlinarith [him5, hA2]\n        exact le_of_pow_le_pow_left₀ (two_ne_zero) (by positivity) h2\n      rw [div_le_iff₀ hA0]\n      linarith [h1]\n    -- the final assembly\n    have hlogA : Real.log (A + 1) ≤ Real.log (‖w‖ + 1) := by\n      apply Real.log_le_log (by linarith [hA0])\n      have h1 : w.re ≤ ‖w‖ := by\n        have h2 := Complex.abs_re_le_norm w\n        rwa [abs_of_nonneg (by linarith [hwre])] at h2\n      linarith [h1]\n    have hγ1 : Real.eulerMascheroniConstant ≤ 1 :=\n      Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)\n    have h1w : ‖(1 : ℂ) / w‖ ≤ 1 := by\n      rw [norm_div, norm_one]\n      rw [div_le_one (by linarith [hw_norm_ge] : (0 : ℝ) < ‖w‖)]\n      exact hw_norm_ge\n    calc ‖-(Real.eulerMascheroniConstant : ℂ) - 1 / w\n          + ∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (w + n + 1))‖\n        ≤ Real.eulerMascheroniConstant + ‖(1 : ℂ) / w‖\n          + ‖∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (w + n + 1))‖ := by\n          refine (norm_add_le _ _).trans ?_\n          refine add_le_add_right ?_ _\n          refine (norm_sub_le _ _).trans ?_\n          rw [norm_neg]\n          exact add_le_add_left (by\n            rw [show ((Real.eulerMascheroniConstant : ℂ))\n              = ((Real.eulerMascheroniConstant : ℝ) : ℂ) from rfl, Complex.norm_real,\n              Real.norm_eq_abs, abs_of_nonneg\n                (Real.one_half_lt_eulerMascheroniConstant.le.trans (by norm_num))]) _\n      _ ≤ 1 + 1 + (‖w‖ / A) * (2 + Real.log (A + 1)) := by\n          gcongr\n          · exact hγ1\n          · exact h1w\n          · exact hser\n      _ ≤ 20 * Real.log (2 + ‖w‖) := by\n          have h2 : (‖w‖ / A) * (2 + Real.log (A + 1)) ≤ 3 * (2 + Real.log (‖w‖ + 1)) := by\n            apply mul_le_mul hratio (by linarith [hlogA]) (by positivity) (by positivity)\n          have h3 : Real.log (‖w‖ + 1) ≤ Real.log (2 + ‖w‖) :=\n            Real.log_le_log (by positivity) (by linarith)\n          nlinarith [h2, h3, hlog4, Real.log_nonneg (show (1 : ℝ) ≤ 2 + ‖w‖ by linarith [hw_norm_ge])]\n\nend NguyenRH1\n\nend"},"extra_content":null}]