[{"type":"thinking","thinking":"§0–§5 done and green. Now §6: the left-plane uniform digamma bound. Let me write it. Recall the plan:\n\n```lean\n/-! ## 6. The left-plane uniform digamma bound (ii′-5e input) -/\n\ntheorem digamma_add_natCast {w : ℂ} (hw : w.im ≠ 0) (n : ℕ) :\n    Complex.digamma (w + n) = Complex.digamma w + ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹\n\ntheorem norm_digamma_sub_log_le_of_two_le_abs_im {w : ℂ} (hw : 2 ≤ |w.im|) :\n    ‖Complex.digamma w - Complex.log w‖ ≤ 3\n```\n\nThe second proof structure:\n1. n := ⌈|w.re|⌉₊ + 2; v := w + ↑n; re v = w.re + n ≥ 2 > 0.\n2. hshift: digamma v = digamma w + Σ_{j ∈ range n} (w + ↑j)⁻¹.\n3. EM for f x = (w + ↑x)⁻¹ on [0, n]: Σ_{range n} f j = ∫₀ⁿ f + (f 0 − f n)/2 + ∫₀ⁿ f' B1.\n4. ∫₀ⁿ f = log v − log w (FTC via comp_ofReal + hasDerivAt_log).\n5. remainder ‖∫ f' B1‖ ≤ (1/2)∫₀ⁿ ((x+a)²+c²)⁻¹ dx ≤ (1/2)(π/c) (arctan FTC).\n6. StirlingVert at v: ‖ψ v − log v‖ ≤ 3/(im v)² + 1/(2‖v‖) ≤ 3/4 + 1/4 = 1.\n7. boundary ‖(f 0 − f n)/2‖ ≤ (1/2)(1/2 + 1/2) = 1/2.\n8. assemble: ψ w − log w = (ψ v − log v) − (Σ f − (log v − log w)); ≤ 1 + (1/2 + (1/2)(π/2)) ≤ 1 + 1/2 + π/4 ≤ 3.\n\nDetails to get right:\n- The EM lemma name: `sum_eq_integral_add_integral_deriv` (root namespace? It was in EulerMaclaurin.lean — is it in a namespace? The file had `open Finset Interval MeasureTheory` and `variable {𝕜}` — no namespace seen in the head. Let me double check there's no `namespace` line... From my earlier read: after the imports, `open Finset Interval MeasureTheory`, `variable {𝕜 : Type*} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ}`, then defs. I didn't see a namespace declaration. B1 is used unqualified in LiRBound ✓. So root namespace ✓.\n- The exact statement (from the read): \n```\ntheorem sum_eq_integral_add_integral_deriv (ha : 0 ≤ a) (hab : a ≤ b)\n    (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t)\n    (h_cont : ContinuousOn (deriv f) [[a, b]]) :\n    ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f k =\n      f a * B1 a - f b * B1 b + (∫ t in a..b, f t) + ∫ t in a..b, deriv f t * B1 t\n```\nwith f : ℝ → 𝕜, B1 : ℝ → ℝ — so f a * B1 a : the B1 a is coerced to 𝕜 via RCLike coe. `[[a,b]]` = Set.uIcc a b (Interval notation — the file opened Interval; in my file I have `open ... MeasureTheory` — need `Set.uIcc` or open Interval. LiRBound used [[a,b]]? They wrote `Set.uIcc_of_le hab` in EulerMaclaurin... For my file I'll write Set.uIcc explicitly.\n\n- f k with k : ℕ: f (↑k : ℝ) — the sum is ∑ k ∈ Ioc .., f ↑k (Nat.cast to ℝ) ✓.\n\nNow the cast juggling between (j : ℂ) in digamma_add_natCast's sum and f (↑j : ℝ) = (w + ((↑j : ℝ) : ℂ))⁻¹: ((↑j : ℝ):ℂ) = (↑j : ℂ): `Complex.ofReal_natCast`? Hmm exact name — there's `Complex.ofReal_natCast (n : ℕ) : ((↑n : ℝ) : ℂ) = ↑n`? I believe `Complex.ofReal_natCast` exists as simp lemma ✓ (ofReal_natCast? it's `Complex.ofReal_natCast : ((n : ℝ) : ℂ) = n` — I'll use `by simp` or `by push_cast` bridges where needed).\n\n- The HasDerivAt for the antiderivative: F y = Complex.log (w + ↑y), derivative (w + ↑x)⁻¹:\n```\n  have hanti : ∀ x ∈ Set.uIcc 0 (n : ℝ), HasDerivAt (fun y : ℝ => Complex.log (w + (y : ℂ))) ((w + (x : ℂ))⁻¹) x := by\n    intro x _\n    have hne : w + (x : ℂ) ≠ 0 := hne_all x\n    have hslit : w + (x : ℂ) ∈ Complex.slitPlane := by\n      rw [Complex.mem_slitPlane_iff]\n      right\n      rw [Complex.add_im, Complex.ofReal_im, add_zero]  -- (w + ↑x).im = w.im + 0 = w.im\n      exact him\n    have h1 : HasDerivAt (fun z : ℂ => Complex.log (w + z)) ((w + (x : ℂ))⁻¹) (x : ℂ) := by\n      have h2 := (Complex.hasDerivAt_log hslit).comp (x : ℂ) ((hasDerivAt_id' (x : ℂ)).const_add w)\n      -- h2 : HasDerivAt (log ∘ (w + ·)) ((w+↑x)⁻¹ * 1) ↑x\n      simpa [Function.comp_def] using h2\n    exact h1.comp_ofReal\n```\nCareful: (hasDerivAt_id' z).const_add w : HasDerivAt (fun z => w + z) 1 z? `HasDerivAt.const_add (c) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => c + f x) f' x` ✓ with f = fun z => z, f' = 1: HasDerivAt (fun z => w + z) 1 z ✓. comp: HasDerivAt (log ∘ fun z => w + z) ((w+z)⁻¹ * 1) z — wait HasDerivAt.comp: (hh : HasDerivAt h h' (f x)) (hf : HasDerivAt f f' x) : HasDerivAt (h ∘ f) (h' * f') x: h' * f' = (w+↑x)⁻¹ * 1 ✓. simpa [Function.comp_def]: turns (h' * 1) into h' and the comp into the lambda ✓ (mul_one via simp).\n\nHmm — one concern: `Complex.hasDerivAt_log hslit : HasDerivAt Complex.log (w+↑x)⁻¹ (w+↑x)` — wait hasDerivAt_log {z} (hz : z ∈ slitPlane) : HasDerivAt log z⁻¹ z — the derivative at z=w+↑x is (w+↑x)⁻¹ ✓ and the point is w+↑x ✓. comp with const_add at (x:ℂ): the inner evaluates to w + ↑x ✓ matches.\n\ncomp_ofReal : (hf : HasDerivAt e e' ↑z) → HasDerivAt (fun y : ℝ => e ↑y) e' z — from RealDeriv.lean: `theorem HasDerivAt.comp_ofReal (hf : HasDerivAt e e' ↑z) : HasDerivAt (fun y : ℝ => e ↑y) e' z` ✓. So h1.comp_ofReal : HasDerivAt (fun y : ℝ => (fun z => Complex.log (w + z)) ↑y) ((w+↑x)⁻¹) x — the function fun y => Complex.log (w + ↑y) ✓ defeq.\n\n- hne_all : ∀ x : ℝ, w + (x : ℂ) ≠ 0:\n```\n  have hne_all : ∀ x : ℝ, w + (x : ℂ) ≠ 0 := by\n    intro x h\n    apply him\n    have := congrArg Complex.im h\n    simp [Complex.add_im] at this  -- (w + ↑x).im = w.im + (↑x).im = w.im: simp gives this : w.im = 0 ✓ exact this\n    exact this\n```\nHmm: this : (w + ↑x).im = (0:ℂ).im; simp [Complex.add_im] — (↑x : ℂ).im = 0 via ofReal_im ✓ and RHS (0:ℂ).im = 0 via zero_im (is it simp? unsure) — `simpa [Complex.add_im] using this` should produce w.im = 0. Let me write:\n```\n    have h2 : (w + (x : ℂ)).im = 0 := by rw [h]; simp\n    rw [Complex.add_im, Complex.ofReal_im, add_zero] at h2\n    exact him h2\n```\nCleaner ✓.\n\n- hf_diff: ∀ t ∈ Set.Icc 0 (n:ℝ), DifferentiableAt ℝ f t: from hder: \n```\n  have hder : ∀ x : ℝ, HasDerivAt f (-(((w + (x : ℂ)) ^ 2)⁻¹)) x := by\n    intro x\n    have hne := hne_all x\n    have h1 : HasDerivAt (fun z : ℂ => (w + z)⁻¹) (-(((w + (x : ℂ)) ^ 2)⁻¹)) (x : ℂ) := by\n      have h2 := ((hasDerivAt_id' (x : ℂ)).const_add w).inv hne\n      -- HasDerivAt.inv (hf : HasDerivAt f f' x) (hx : f x ≠ 0) : HasDerivAt (fun x => (f x)⁻¹) (-f' / f x ^ 2) x\n      -- h2 : HasDerivAt (fun z => (w+z)⁻¹) (-1 / (w+↑x)^2) ↑x\n      convert h2 using 1  -- −1/u² = −(u²)⁻¹\n      rw [neg_div, one_mul, inv_pow]  -- hmm: −1/(w+↑x)^2 = −((w+↑x)^2)⁻¹: div_eq_mul_inv: 1/u² = (u²)⁻¹: one_mul... −1/u² = −(1 * (u²)⁻¹) = −(u²)⁻¹: rw [neg_div, one_div, inv_pow]?? 1/u² = (u²)⁻¹: one_div (u^2) : 1/(u^2) = (u^2)⁻¹ ✓. So: −1/(u^2) = −(u^2)⁻¹ by rw [neg_div, one_div] ✓.\n    exact h1.comp_of_real... wait comp_ofReal\n    exact h1.comp_ofReal\n```\nHmm wait: HasDerivAt.inv's exact value: `HasDerivAt.inv (hf : HasDerivAt f f' x) (hx : f x ≠ 0) : HasDerivAt (fun x => (f x)⁻¹) (-(f x ^ 2)⁻¹ * f') x`? or (−f' / (f x)^2)? Two candidate forms. With f' = 1: −(u²)⁻¹ * 1 = −(u²)⁻¹ or −1/u² = −(u²)⁻¹ after one_div. To be safe use convert/simpa. I'll write `simpa using ((hasDerivAt_id' (x:ℂ)).const_add w).inv hne` and see; the target value −((w+↑x)^2)⁻¹ vs whatever comes out — simpa with [neg_div, one_div, one_mul, mul_one] should bridge. Actually let me define hder with target `(−1 / (w + (x:ℂ)) ^ 2)` — no wait, I need deriv f x for the norm: ‖deriv f x‖ = ‖w+↑x‖⁻² — any of the equal forms works since I take norm. Let me set the target as whatever HasDerivAt.inv produces and then show its norm. Cleanest: \n```\n  have hder : ∀ x : ℝ, HasDerivAt f (-(((w + (x:ℂ)) ^ 2)⁻¹)) x\n```\nand convert via: −(u²)⁻¹ = −(1/u²) = −1/u². If HasDerivAt.inv gives −f'/(f x)^2 = −1/u²: rw [neg_div, one_div] hmm: −1/u² = −(1/u²) by neg_div (a/b form: −1/u² parses as −(1/u²)? −1/u^2 = (−1)/(u^2) = −(1/u^2) ✓ same). Then 1/u² = (u²)⁻¹ (one_div). So target −(u²)⁻¹ = −(1/u²): rw [inv_eq_one_div?]... I'll use `convert h2 using 1; rw [neg_div, one_div]` — the convert produces goal −(u²)⁻¹ = −1/u^2 or −1/u^2 = −(u²)⁻¹ depending direction; then rw [one_div] hmm... Let me just use `simpa [neg_div, one_div] using h2` — simp normalizes both sides. OK.\n\nActually — even simpler: I don't need HasDerivAt's exact value at all! I need: (a) DifferentiableAt for hf_diff — can get from the formula's continuity: f = fun x => (w + ↑x)⁻¹ is differentiable since the denominator never vanishes: `DifferentiableAt.inv₀`? hmm — for ℝ → ℂ: differentiableAt of (fun x => (w+↑x)⁻¹): it's (e ∘ ofReal) with e = (w + ·)⁻¹: differentiable via comp_ofReal chain as above — but there's a slicker path: f is CONTINUOUS with continuous derivative formula... I need deriv f explicitly for the EM lemma (h_cont : ContinuousOn (deriv f)). The EM lemma uses `deriv f` (the actual deriv function!) — so I MUST know deriv f = the formula (for h_cont and for the integrand norm bound). So hder with the exact value is needed. Fine — go with HasDerivAt.inv + simpa.\n\n- hcont: ContinuousOn (deriv f) (Set.uIcc 0 ↑n): \n```\n  have hderiv_eq : deriv f = fun x : ℝ => -(((w + (x:ℂ)) ^ 2)⁻¹) := funext fun x => (hder x).deriv\n  have hcont : ContinuousOn (deriv f) (Set.uIcc 0 (n:ℝ)) := by\n    rw [hderiv_eq]\n    apply Continuous.continuousOn\n    apply Continuous.neg\n    apply Continuous.inv₀ _ (fun x => pow_ne_zero 2 (hne_all x))\n    exact (continuous_const.add Complex.continuous_ofReal).pow 2\n```\nContinuous.inv₀ (hf : Continuous f) (h : ∀ x, f x ≠ 0) : Continuous (fun x => (f x)⁻¹): signature `Continuous.inv₀ (hf : Continuous f) (h : ∀ x, f x ≠ 0)`? hmm — Continuous.inv₀ : Continuous f → (∀ x, f x ≠ 0) → Continuous f⁻¹? I think `Continuous.inv₀ (hf : Continuous f) (h : ∀ x, f x ≠ 0) : Continuous fun x => (f x)⁻¹` ✓ exists.\n\n- The EM application:\n```\n  have hEM := sum_eq_integral_add_integral_deriv (f := f) (a := 0) (b := (n : ℝ)) le_rfl (Nat.cast_nonneg _)\n    (fun t ht => (hder t).differentiableAt) hcont\n  rw [Nat.floor_zero, Nat.floor_natCast] at hEM\n  -- B1 values\n  have hB10 : B1 0 = -1 / 2 := by unfold B1; simp\n  have hB1n : B1 (n : ℝ) = -1 / 2 := by unfold B1; rw [Nat.floor_natCast]; simp\n  rw [hB10, hB1n] at hEM\n```\nWait — B1 def: `noncomputable def B1 (x : ℝ) : ℝ := x - ⌊x⌋₊ - 1 / 2` — unfold B1: (0:ℝ) − ⌊(0:ℝ)⌋₊ − 1/2: simp [Nat.floor_zero]: 0 − 0 − 1/2 = −1/2 ✓. For ↑n: ↑n − ⌊↑n⌋₊ − 1/2: Nat.floor_natCast : ⌊(↑n : ℝ)⌋₊ = n: then ↑n − ↑n − 1/2 = −1/2: simp ✓.\n\nHmm — but hEM's term is `f 0 * ↑(B1 0)` with the RCLike coe — after rw [hB10] at hEM: f 0 * ↑(-1/2 : ℝ)... The coercion ((−1/2 : ℝ) : ℂ): fine for algebra.\n\n- Sum conversion:\n```\n  have hIoc : Finset.Ioc 0 n = (Finset.range (n + 1)).erase 0 := by\n    ext x\n    simp only [Finset.mem_Ioc, Finset.mem_erase, Finset.mem_range]\n    omega\n  have hconv : ∑ k ∈ Finset.Ioc 0 n, f (k : ℝ) = ∑ j ∈ Finset.range n, f (j : ℝ) - f 0 + f (n : ℝ) := by\n    rw [hIoc]\n    have h0mem : 0 ∈ Finset.range (n + 1) := Finset.mem_range.mpr (Nat.succ_pos n)\n    have h1 := Finset.add_sum_erase (Finset.range (n + 1)) (fun k => f (k : ℝ)) h0mem\n    -- h1 : f 0 + ∑ x ∈ erase 0 (range (n+1)), f x = ∑ x ∈ range (n+1), f x\n    rw [Finset.sum_range_succ] at h1\n    -- h1 : f 0 + Σ_erase = Σ_range_n + f n\n    linarith-free: pure algebra on ℂ — use linear_combination? or:\n    linear_combination h1\n```\nhconv goal: Σ_erase = Σ_range_n − f 0 + f n. h1 : f 0 + Σ_erase = Σ_range_n + f n. linear_combination h1 ✓ (ℂ comm ring).\n\nWait — Finset.add_sum_erase signature: `Finset.add_sum_erase (s : Finset α) (h : a ∈ s) : f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x`? hmm might need (f := ...). Write: `Finset.add_sum_erase _ _ h0mem`? The signature: `theorem Finset.add_sum_erase (s : Finset α) (f : α → β) (h : a ∈ s) : f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x` — args (s f h) ✓.\n\n- Then hsum:\n```\n  have hsum : ∑ j ∈ Finset.range n, f (j : ℝ)\n      = (∫ x in (0:ℝ)..(n:ℝ), f x) + (f 0 - f (n:ℝ)) / 2 + ∫ x in (0:ℝ)..(n:ℝ), deriv f x * (B1 x : ℂ) := by\n    linear_combination hEM + hconv  -- check: hEM: Σ_Ioc = f0·↑(−1/2) − fn·↑(−1/2) + ∫f + ∫f'B1; hconv: Σ_Ioc = Σ_range − f0 + fn. Goal: Σ_range = ∫f + (f0−fn)/2 + ∫f'B1.\n```\nlinear_combination hEM + hconv: hEM.l−r + hconv.l−r = (Σ_Ioc − [−f0/2 + fn/2 + ∫f + ∫f']) + (Σ_Ioc − Σ_range + f0 − fn) = 2Σ_Ioc − Σ_range + f0 − fn + f0/2 − fn/2 − ∫f − ∫f'. Goal l−r: Σ_range − ∫f − (f0−fn)/2 − ∫f'. Setting equal: need Σ_range − ∫f − (f0−fn)/2 − ∫f' = 2Σ_Ioc − Σ_range + (3/2)f0 − (3/2)fn − ∫f − ∫f' — no. Solve properly: variables: S = Σ_range, I = Σ_Ioc, A = f0, B = fn, J = ∫f, R = ∫f'B1.\nhEM: I = −A/2 + B/2 + J + R (with ↑(−1/2) casts — hmm the coe: f 0 * ↑(B1 0) = A * ↑(−1/2) = −A/2 in ℂ — linear_combination normalizes casts? push_cast needed. The term f 0 * ((-1/2 : ℝ):ℂ) — linear_combination uses ring_nf which handles ofReal casts ✓ probably).\nhconv: I = S − A + B.\nGoal: S = J + (A−B)/2 + R.\nFrom hconv: I = S − A + B. Sub into hEM: S − A + B = −A/2 + B/2 + J + R ⟹ S = A/2 − B/2 + J + R = J + (A−B)/2 + R ✓. linear_combination hEM − hconv: (hEM.l − hEM.r) − (hconv.l − hconv.r) = (−A/2+B/2+J+R ... let me just trust linear_combination to find it if I give hEM + hconv with signs: try `linear_combination hEM - hconv`: l−r combination: (I − (−A/2+B/2+J+R)) − (I − (S−A+B)) = I + A/2 − B/2 − J − R − I + S − A + B = S − A/2 + B/2 − J − R. Goal l−r = S − J − (A−B)/2 − R = S − A/2 + B/2 − J − R ✓ MATCH. So `linear_combination hEM - hconv` ✓.\n\n- The FTC integral hint:\n```\n  have hint : ∫ x in (0:ℝ)..(n:ℝ), f x = Complex.log v - Complex.log w := by\n    have hconti : IntervalIntegrable f volume 0 (n : ℝ) := by\n      apply ContinuousOn.intervalIntegrable\n      -- f continuous on uIcc\n      apply Continuous.continuousOn\n      apply Continuous.inv₀ _ hne_all\n      exact continuous_const.add Complex.continuous_ofReal\n    have hFTC := intervalIntegral.integral_eq_sub_of_hasDerivAt hanti hconti\n    -- hFTC : ∫ x in 0..↑n, (w+↑x)⁻¹ = (fun y => log (w+↑y)) ↑n − (fun y => log (w+↑y)) 0\n    rw [hFTC]\n    simp [hv]  -- log (w + ↑↑n) − log (w + ↑0) = log v − log w: (↑(↑n:ℝ):ℂ) = ↑n: ofReal_natCast? simp should know (Complex.ofReal_natCast is simp?); w + 0: ofReal_zero? ↑0 = 0: simp\n```\nHmm — intervalIntegral.integral_eq_sub_of_hasDerivAt signature: (hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f' ... ) — I wrote hanti with uIcc membership ✓. But note the f in the integral is `f` (my set function) vs the FTC's f': the integral ∫ x in 0..↑n, f x where f x = (w+↑x)⁻¹ ✓ and hanti gives HasDerivAt (antiderivative) ((w+↑x)⁻¹) x — the derivative value must match f x: (w + ↑x)⁻¹ = f x by rfl of the set-def — since f is `set ... with hf`, occurrences of f won't automatically unfold. Might need `simp only [hf]` bridges. To reduce friction, DON'T use `set` for f — just use let-free plain functions and repeat. Hmm, `set f := fun x : ℝ => (w + (x:ℂ))⁻¹ with hf` — then f x needs `rw [hf]` or simp only [hf] to unfold. The EM lemma application with (f := f) — the lemma's f is a variable, my set-f is a local def — fine. The congruences: ∫ x, f x = ∫ x, (w+↑x)⁻¹ needs f x ≡ (w+↑x)⁻¹ definitionally ✓ (set introduces f as a local definition with hf : f = fun x => ...; the FTC produces terms about (fun y => log (w+↑y)); my hint statement is about ∫ f and log v − log w — after rw [hFTC]?? hmm hFTC : ∫ x in 0..↑n, (fun y => (w+↑y)⁻¹)... wait no — hconti : IntervalIntegrable f... and hanti : HasDerivAt (fun y => log (w+↑y)) ((w+↑x)⁻¹) x — for integral_eq_sub_of_hasDerivAt, the integrand is given by hanti's derivative VALUES: (fun x => (w+↑x)⁻¹) — but my goal's integral is over f. These differ syntactically (f vs the lambda). Since f is a local `set` definition, f x is defeq to (w+↑x)⁻¹ but the integral's function ∫ x, f x vs ∫ x, (w+↑x)⁻¹: the FTC conclusion: ∫ x in a..b, (fun x => (w+↑x)⁻¹) x?? The lemma: integral_eq_sub_of_hasDerivAt (hf : ∀ x ∈ uIcc, HasDerivAt F (F' x) x) (hi : IntervalIntegrable F' ..) : ∫ x in a..b, F' x = F b − F a — F' is implicit, unified with hanti's derivative family (fun x => (w+↑x)⁻¹)... actually hanti : ∀ x ∈ uIcc, HasDerivAt F ((w+↑x)⁻¹) x — the derivative is the TERM (w+↑x)⁻¹, so F' := fun x => (w+↑x)⁻¹ by unification? The HasDerivAt's second arg is the value (w+↑x)⁻¹ — for the lemma to see a family F' it needs to abstract: Lean does this via the unifier: ∀ x ∈ uIcc, HasDerivAt F (?F' x) x with ?F' x := (w+↑x)⁻¹ — higher-order: ?F' := fun x => (w+↑x)⁻¹ ✓ (pattern unification works here). So hFTC : ∫ x in 0..↑n, (fun x => (w+↑x)⁻¹) x = ... hmm or ∫ x, ?F' x with ?F' assigned — the conclusion shows F' x with the lambda applied or not. In practice the conclusion is ∫ x in a..b, (w+↑x)⁻¹ = F ↑n − F 0 with F = fun y => log (w+↑y). Then hint's LHS ∫ x, f x: with set-f, `f` is a local hypothesis-bound function; ∫ x, f x = ∫ x, (w+↑x)⁻¹ needs simp only [hf] on the goal first: goal ∫ x, f x = log v − log w: simp only [hf] turns f into the lambda everywhere (also in the sum hsum etc.). To minimize pain: skip `set` for f; write the function explicitly everywhere (verbose but robust). I'll define it via plain `let`-free repetition: use (fun x : ℝ => (w + (x:ℂ))⁻¹) in the EM application with (f := fun x : ℝ => (w + (x:ℂ))⁻¹) and write all integrals/sums with the explicit lambda. Hmm — the sums: ∑ j ∈ range n, f ↑j appears in hconv/hsum/hshift; hshift (digamma_add_natCast) has (w + (↑j:ℂ))⁻¹. If everything is explicit lambda-free terms: digamma sum: (w + (↑j:ℂ))⁻¹; EM sum: (w + ((↑j : ℝ):ℂ))⁻¹ — need the cast bridge ((↑j:ℝ):ℂ) = (↑j:ℂ): Complex.ofReal_natCast — is it simp? `Complex.ofReal_natCast (n : ℕ) : ((↑n : ℝ) : ℂ) = ↑n`? I think the simp lemma name is `Complex.ofReal_natCast` ✓ (RCLike.ofReal_natCast exists: `RCLike.ofReal_natCast`? hmm). Let me use push_cast to bridge: (w + ((↑j : ℝ):ℂ))⁻¹ = (w + (↑j : ℂ))⁻¹ by push_cast ring_nf? For a term-level congruence: `by push_cast; ring`? pushes ofReal_natCast ✓ then ring closes if syntactically equal... they're equal after cast push ✓. I'll keep a helper:\n```\n  have hcast : ∀ j : ℕ, (w + ((j : ℝ) : ℂ))⁻¹ = (w + (j : ℂ))⁻¹ := by\n    intro j\n    push_cast\n    ring_nf  -- or congr 1; push_cast; ring\n```\nHmm push_cast on the goal (w + ↑(↑j:ℝ))⁻¹ = (w + ↑j)⁻¹: rewrites ↑(↑j:ℝ) → ↑j ✓ then both sides identical — closes by rfl? push_cast leaves `rfl` goal which it closes? push_cast doesn't close rfl automatically... add `ring` won't hurt. Actually simplest: `by simp` — simp set includes ofReal_natCast presumably: (w + ((↑j:ℝ):ℂ))⁻¹ = (w + ↑j)⁻¹: simp rewrites LHS ((↑j:ℝ):ℂ) to ↑j via ofReal_natCast (if simp) then rfl ✓.\n\nTo avoid death by a thousand cast cuts, let me define f explicitly as a top-level... no — w is a bound variable. OK let me just carefully write with explicit terms and bridge casts as needed.\n\n- The remainder bound hrem:\n```\n  have hrem : ‖∫ x in (0:ℝ)..(n:ℝ), deriv (fun y : ℝ => (w + (y:ℂ))⁻¹) x * (B1 x : ℂ)‖\n      ≤ (1 / 2) * (Real.pi / c) := by\n    have h1 : ‖∫ x in (0:ℝ)..(n:ℝ), deriv (fun y : ℝ => (w + (y:ℂ))⁻¹) x * (B1 x : ℂ)‖\n        ≤ ∫ x in (0:ℝ)..(n:ℝ), ‖deriv (fun y : ℝ => (w + (y:ℂ))⁻¹) x * (B1 x : ℂ)‖ :=\n      intervalIntegral.norm_integral_le_integral_norm (Nat.cast_nonneg n)\n    refine h1.trans ?_\n    have h2 : ∫ x in (0:ℝ)..(n:ℝ), ‖deriv (fun y : ℝ => (w + (y:ℂ))⁻¹) x * (B1 x : ℂ)‖\n        ≤ ∫ x in (0:ℝ)..(n:ℝ), (1/2) * (((x + a)^2 + c^2)⁻¹) := by\n      apply intervalIntegral.integral_mono_on (Nat.cast_nonneg n) hint1 hint2\n      intro x hx\n      -- pointwise\n      rw [hderiv_eq]  -- deriv value — but hderiv_eq is about deriv f with f set... handle\n      ...\n```\nHmm — deriv (fun y => (w+↑y)⁻¹) x: I have hder x : HasDerivAt (fun y => (w+↑y)⁻¹) (−((w+↑x)²)⁻¹) x (if I skip set-f). Then (hder x).deriv : deriv (fun y => (w+↑y)⁻¹) x = −((w+↑x)²)⁻¹ ✓ pointwise rewrite via `rw [(hder x).deriv]`.\n\nThe pointwise bound: ‖(−((w+↑x)²)⁻¹) * ↑(B1 x)‖ = ‖w+↑x‖⁻² * |B1 x| ≤ ‖w+↑x‖⁻² * (1/2) = (1/2) * ((x+a)² + c²)⁻¹:\n```\n      have hB : |B1 x| ≤ 1 / 2 := abs_B1_le_half (Set.mem_Icc.mp hx).1  -- hx : x ∈ Icc 0 ↑n: (0:ℝ) ≤ x\n      -- wait hx from integral_mono_on: x ∈ Set.Icc 0 ↑n? or uIcc? `intervalIntegral.integral_mono_on (hab : a ≤ b) (hf) (hg) (h : ∀ x ∈ Set.Icc a b, f x ≤ g x)` — I think Icc ✓.\n      have hnorm : ‖(-(((w + (x:ℂ)) ^ 2)⁻¹)) * (B1 x : ℂ)‖ = ‖w + (x:ℂ)‖ ^ 2 ⁻¹ * |B1 x| := by\n        rw [norm_mul, norm_neg, norm_inv, norm_pow]\n        -- ‖↑(B1 x)‖ = |B1 x|: Complex.norm_real + Real.norm_eq_abs? norm_real : ‖(r:ℂ)‖ = ‖r‖_ℝ = |r| via Real.norm_eq_abs: rw [Complex.norm_real, Real.norm_eq_abs]\n        rw [Complex.norm_real, Real.norm_eq_abs]\n      -- ‖w+↑x‖^2 = (x + a)^2 + c^2\n      have hnsq : ‖w + (x:ℂ)‖ ^ 2 = (x + a)^2 + c^2 := by\n        rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n        simp [Complex.add_re, Complex.ofReal_re, Complex.add_im, Complex.ofReal_im]\n        -- goal: (w.re + x)*(w.re+x) + w.im*w.im = (x+a)^2 + c^2 — with a := w.re (set), c := |w.im|\n        rw [sq_abs]  -- hmm c is set to |w.im|: c^2 = |w.im|^2: `sq_abs w.im : |w.im|^2 = w.im^2`? sq_abs (a) : |a|^2 = a^2 ✓\n        ring\n      rw [(hder x).deriv, hnorm, hnsq]\n      -- goal: ((x+a)^2+c^2)⁻¹ * |B1 x| ≤ (1/2) * ((x+a)^2+c^2)⁻¹\n      have hpos : (0:ℝ) < (x + a)^2 + c^2 := by nlinarith [sq_nonneg (x+a), hc0]\n      rw [ge_iff_le, ← mul_comm (1/2) _]?? — just: \n      calc ((x+a)^2+c^2)⁻¹ * |B1 x| ≤ ((x+a)^2+c^2)⁻¹ * (1/2) := mul_le_mul_of_nonneg_left hB (inv_nonneg.mpr hpos.le)\n        _ = (1/2) * ((x+a)^2+c^2)⁻¹ := by ring\n```\nCareful with normSq_apply form (re*re + im*im vs ^2) — ring/nlinarith handles.\n\nThe set variables a := w.re, c := |w.im| introduced via `set a := w.re with ha` — set rewrites occurrences in the goal but NOT in hypotheses unless... it does rewrite in all? `set a := w.re with ha` replaces w.re by a in goal and context? It adds ha : a = w.re and replaces in the goal only by default; hypotheses keep w.re. To avoid confusion, skip `set` for a, c — just use w.re and |w.im| directly with local haves. Actually with explicit w.re/|w.im| the ring steps need the right forms — fine.\n\n- The arctan integral bound:\n```\n  have harctan : ∫ x in (0:ℝ)..(n:ℝ), ((x + w.re)^2 + |w.im|^2)⁻¹ ≤ Real.pi / |w.im| := by\n    have hc0 : (0:ℝ) < |w.im| := by linarith [hw]  -- |w.im| ≥ 2 > 0\n    have hanti2 : ∀ x ∈ Set.uIcc 0 (n:ℝ),\n        HasDerivAt (fun y : ℝ => (1/|w.im|) * Real.arctan ((y + w.re)/|w.im|))\n          (((x + w.re)^2 + |w.im|^2)⁻¹) x := by\n      intro x _\n      have h1 : HasDerivAt (fun y : ℝ => (y + w.re)/|w.im|) (1/|w.im|) x :=\n        ((hasDerivAt_id x).add_const w.re).div_const |w.im|\n      have h2 := h1.arctan  -- Real.HasDerivAt.arctan\n      have h3 := h2.const_mul (1/|w.im|)\n      -- h3 : HasDerivAt (fun y => (1/|w.im|) * arctan ((y+w.re)/|w.im|)) ((1/|w.im|) * (1/(1+((x+w.re)/|w.im|)^2) * (1/|w.im|))) x\n      convert h3 using 1\n      -- value equality: (1/c) * (1/(1+((x+a)/c)^2) * (1/c)) = ((x+a)^2+c^2)⁻¹\n      field_simp [hc0.ne']\n      ring\n    have hconti2 : IntervalIntegrable (fun x : ℝ => ((x + w.re)^2 + |w.im|^2)⁻¹) volume 0 (n:ℝ) := by\n      apply ContinuousOn.intervalIntegrable\n      apply Continuous.continuousOn\n      apply Continuous.inv₀ _ (fun x => by nlinarith [sq_nonneg (x + w.re), hc0] : ∀ x, (x + w.re)^2 + |w.im|^2 ≠ 0)\n      · continuity: ((continuous_id.add continuous_const).pow 2).add continuous_const\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti2 hconti2]\n    -- = (1/c)(arctan((↑n + a)/c) − arctan((0+a)/c)) ≤ π/c\n    have h1 : Real.arctan ((↑n + w.re)/|w.im|) - Real.arctan ((0 + w.re)/|w.im|) ≤ Real.pi := by\n      have hu := Real.arctan_lt_pi_div_two ((↑n + w.re)/|w.im|)\n      have hv := Real.arctan_lt_pi_div_two (-((0 + w.re)/|w.im|))\n      rw [Real.arctan_neg] at hv\n      linarith [Real.pi_pos, hv]\n    -- final: (1/c)*u − (1/c)*v = (1/c)*(u−v) ≤ (1/c)*π = π/c\n    have hc0' : (0:ℝ) < |w.im| := hc0\n    rw [show (0:ℝ) + w.re = w.re by ring]  -- hmm: (0 + w.re)/c — just leave; ring_nf handles\n    rw [div_le_iff??]... the goal after rw FTC: (1/c)*arctan(...) − (1/c)*arctan(...) ≤ π/c:\n    calc (1/|w.im|) * Real.arctan ((↑n + w.re)/|w.im|) - (1/|w.im|) * Real.arctan ((0 + w.re)/|w.im|)\n        = (1/|w.im|) * (Real.arctan ((↑n + w.re)/|w.im|) - Real.arctan ((0 + w.re)/|w.im|)) := by ring\n      _ ≤ (1/|w.im|) * Real.pi := by\n        apply mul_le_mul_of_nonneg_left h1 (by positivity)\n      _ = Real.pi / |w.im| := by ring\n```\nReal.HasDerivAt.arctan : `Real.HasDerivAt.arctan (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x` ✓ I'm fairly confident (Real.HasDerivAt.arctan exists).\n`Real.arctan_neg : arctan (−x) = −arctan x` ✓.\n\nFor hconti2's continuity: Continuous fun x => ((x + w.re)^2 + |w.im|^2)⁻¹: Continuous.inv₀ (((continuous_id.add continuous_const).pow 2).add continuous_const) (fun x => ne_of_gt (by nlinarith [sq_nonneg (x + w.re), hc0])). Note `continuous_id` for ℝ ✓.\n\n- StirlingVert at v: hv1:\n```\n  have hv1 : ‖Complex.digamma v - Complex.log v‖ ≤ 1 := by\n    have hst := StirlingVert.digamma_stirling hvre (by rw [hvim]; linarith [hw])\n    -- hst : ‖digamma v − log v + (1/2)/v‖ ≤ 3 / v.im^2\n    have hvnorm : 2 ≤ ‖v‖ := by\n      have h := Complex.abs_im_le_norm v\n      rw [hvim] at h  -- |w.im| ≤ ‖v‖\n      linarith [hw]\n    calc ‖Complex.digamma v - Complex.log v‖\n        = ‖(Complex.digamma v - Complex.log v + (1/2:ℂ)/v) - (1/2:ℂ)/v‖ := by congr 1; ring\n      _ ≤ ‖Complex.digamma v - Complex.log v + (1/2:ℂ)/v‖ + ‖(1/2:ℂ)/v‖ := norm_sub_le _ _\n      _ ≤ 3 / v.im^2 + 1/4 := by\n        apply add_le_add hst\n        rw [norm_div]\n        have h12 : ‖(1/2 : ℂ)‖ = 1/2 := ... (same pattern)\n        rw [h12]\n        rw [div_le_iff₀ (by linarith [hvnorm] : (0:ℝ) < ‖v‖)]  -- (1/2) ≤ (1/4)*‖v‖ ⟺ 2 ≤ ‖v‖ ✓\n        nlinarith [hvnorm]\n      _ ≤ 1 := by\n        -- 3/v.im² ≤ 3/4: v.im² = w.im² ≥ 4\n        have hsq : (4:ℝ) ≤ v.im^2 := by\n          rw [hvim]  -- wait v.im = w.im: v.im^2 = w.im^2 ≥ |w.im|^2 ≥ 4\n          calc (4:ℝ) = (2:ℝ)^2 := by norm_num\n            _ ≤ |w.im|^2 := pow_le_pow_left₀ (by norm_num) hw _\n            _ = w.im^2 := by rw [sq_abs]\n        have h34 : 3 / v.im^2 ≤ 3 / 4 := by\n          rw [div_le_div_iff (by linarith [hsq] : (0:ℝ) < v.im^2) (by norm_num)]  -- 3*4 ≤ 3*v.im² ⟺ 4 ≤ v.im² ✓\n          nlinarith [hsq]\n        linarith [h34]\n```\ndiv_le_div_iff — journal-024: \"div_le_div_iff₀ (hb hd) : a/b ≤ c/d ↔ a*d ≤ c*b (GroupWithZero/Basic); the 4-arg div_le_div does NOT exist\". So use div_le_div_iff₀ hsqpos (by norm_num : (0:ℝ) < 4) : 3/v.im² ≤ 3/4 ↔ 3*4 ≤ 3*v.im² ✓ nlinarith [hsq].\n\n- Boundary hboundary:\n```\n  have hboundary : ‖((w + (0:ℝ):ℂ)⁻¹ - (w + ((n:ℝ):ℂ))⁻¹) / 2‖ ≤ 1 / 2 := by\n    -- f 0 − f ↑n over 2\n    have hwnorm : 2 ≤ ‖w‖ := (Complex.abs_im_le_norm w).trans' hw  -- hmm: |w.im| ≤ ‖w‖ and 2 ≤ |w.im| ⟹ 2 ≤ ‖w‖: hw.trans (Complex.abs_im_le_norm w) ✓\n    have hvnorm : 2 ≤ ‖v‖ := ...\n    have h1 : ‖(w + (0:ℝ):ℂ)⁻¹‖ ≤ 1/2 := by\n      rw [show w + ((0:ℝ):ℂ) = w by simp, norm_inv]\n      rw [div_le_iff₀?...]: ‖w‖⁻¹ ≤ 1/2 ⟺ 1 ≤ ‖w‖/2 ⟺ 2 ≤ ‖w‖: inv_le_iff? Use: ‖w‖⁻¹ ≤ 1/2 ⟺ (2 ≤ ‖w‖): `inv_le_of_inv_le₀`? simplest: rw [inv_le_iff₀?]... journal-024 banked div_le_iff₀. (‖w‖)⁻¹ = 1/‖w‖: one_div... Let me: rw [norm_inv, inv_le_iff₀ (by linarith [hwnorm] : (0:ℝ) < ‖w‖) (by norm_num : (0:ℝ) < 2)]?? inv_le_iff₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a — hmm that gives ‖w‖⁻¹ ≤ (1/2) = (2)⁻¹ ⟺ 2 ≤ ‖w‖ ✓: `inv_le_iff₀` might be `inv_le_inv₀`. Alternatives: one_div: (1/2 : ℝ) = 2⁻¹ hmm (1/2) = 2⁻¹ by one_div... `inv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a` ✓ I'm fairly confident inv_le_inv₀ exists with that form. So: ‖w‖⁻¹ ≤ 1/2: rw [show (1/2 : ℝ) = (2:ℝ)⁻¹ by norm_num]; exact (inv_le_inv₀ (by linarith) (by norm_num)).mpr hwnorm ✓.\n    ... same for v ...\n    calc ‖((w + ↑(0:ℝ))⁻¹ - (w + ↑(n:ℝ))⁻¹)/2‖ \n        ≤ (‖(w + ↑(0:ℝ))⁻¹‖ + ‖(w + ↑(n:ℝ))⁻¹‖)/2 := by\n          rw [norm_div]; gcongr; exact norm_sub_le _ _  -- hmm norm_div: ‖X/2‖ = ‖X‖/‖2‖: need ‖(2:ℂ)‖ = 2\n      _ ≤ (1/2 + 1/2)/2 := by gcongr (both h1 h2)\n      _ = 1/2 := by norm_num\n```\nWait — (w + ↑(↑n:ℝ))⁻¹ vs v = w + (↑n:ℂ): cast bridge needed: ((↑n:ℝ):ℂ) = (↑n:ℂ) via ofReal_natCast-simp. Since v is `set v := w + (↑n:ℂ)`, the term (w + ↑(↑n:ℝ))⁻¹ — simp [Complex.ofReal_natCast?] then rw [← hv]... Let me handle: `show ‖((w:ℂ) + ... )‖` ugh. Let me make the boundary cleaner: note f 0 = w⁻¹ (w + 0) and f ↑n = v⁻¹ up to cast. I'll write the whole assembly with explicit normalization helpers:\n\nhfn : (w : ℂ) + ((n:ℝ):ℂ) = v: by rw [hv]; simp [Complex.ofReal_natCast?]... — let me just check whether `Complex.ofReal_natCast` exists as simp. It's `RCLike.ofReal_natCast (K) (n) : ((↑n : ℝ) : K) = ↑n`? I recall `Complex.ofReal_natCast (n : ℕ) : (↑(↑n : ℝ) : ℂ) = ↑n` exists as a simp lemma (in Data/Complex/Basic or RCLike). I'll trust `by simp` or `by push_cast` to close such cast goals; test at build.\n\n- hmid (the Σf − (log v − log w) bound):\n```\n  have hmid : ‖(∑ j ∈ Finset.range n, (w + ((j:ℝ):ℂ))⁻¹) - (Complex.log v - Complex.log w)‖\n      ≤ 1/2 + (1/2) * (Real.pi / |w.im|) := by\n    have halg : (∑ j ∈ Finset.range n, (w + ((j:ℝ):ℂ))⁻¹) - (Complex.log v - Complex.log w)\n        = (f 0 - f ↑n)/2 + ∫ x in 0..↑n, deriv f x * (B1 x : ℂ) := by\n      rw [hsum, hint]; ring\n    rw [halg]\n    exact (norm_add_le _ _).trans (add_le_add hboundary hrem)\n```\nwhere hsum's LHS is ∑ j ∈ range n, (w + ↑↑j)⁻¹ with f explicit. So hsum should be stated with the explicit lambda-free summand: ∑ j ∈ Finset.range n, (w + ((j:ℝ):ℂ))⁻¹ = ∫ x in 0..↑n, (w + (x:ℂ))⁻¹ dx + ((w + ↑(0:ℝ))⁻¹ − (w + ↑(↑n:ℝ))⁻¹)/2 + ∫ x, deriv (fun y => (w+↑y)⁻¹) x * ↑(B1 x). That's hEM + hconv combined with the lambda explicit. The EM's ∑ k ∈ Ioc .., f ↑k — with f := fun y : ℝ => (w + (y:ℂ))⁻¹: the summand f ↑k = (w + (↑k:ℂ))⁻¹ ✓ beta — the statement shows (fun y => ...) ↑k — beta redex; rw/simp only [] to beta-reduce: `simp only []`? Use `beta_reduce`? In Lean4 Mathlib, `simp only []` does beta. OK.\n\n- Final assembly:\n```\n  calc ‖Complex.digamma w - Complex.log w‖\n      = ‖(Complex.digamma v - Complex.log v)\n          - ((∑ j ∈ Finset.range n, (w + ((j:ℝ):ℂ))⁻¹) - (Complex.log v - Complex.log w))‖ := by\n        congr 1\n        -- digamma w = digamma v − Σ (from hshift, cast-bridged)\n        rw [hshift']  -- digamma v = digamma w + Σ (j:ℂ)-form — need the sum in (j:ℝ)-cast form... \n        ring\n    _ ≤ ‖Complex.digamma v - Complex.log v‖ + ‖...‖ := norm_sub_le _ _\n    _ ≤ 1 + (1/2 + (1/2) * (Real.pi / |w.im|)) := add_le_add hv1 hmid\n    _ ≤ 3 := by\n      have hpc : Real.pi / |w.im| ≤ Real.pi / 2 := by\n        apply div_le_div_of_nonneg_left Real.pi_nonneg hc0 hw  -- check direction: π/c ≤ π/2 with c ≥ 2: div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c) : a/c ≤ a/b ✓\n      nlinarith [hpc, Real.pi_lt_d2.le]\n```\nhshift relates digamma (w + ↑n) = digamma w + Σ_{j} (w + (↑j:ℂ))⁻¹ (ℕ-cast). The hmid sum uses (j:ℝ)-cast. Bridge: the sums are equal by sum_congr with the cast lemma. Let me define hsumC : ∑ j ∈ range n, (w + ((j:ℝ):ℂ))⁻¹ = ∑ j ∈ range n, (w + (j:ℂ))⁻¹ := Finset.sum_congr rfl (fun j _ => by simp). Then in the congr-1 algebra: digamma w − log w = (digamma v − log v) − (Σ_ℝ − (log v − log w)) with digamma v = digamma w + Σ_ℕ: rw [hshift, ← hsumC]; ring ✓.\n\n- hv1's hvim : v.im = w.im: rw [hv]; simp [Complex.add_im, Complex.natCast_im] — natCast_im : (↑n : ℂ).im = 0 — exists as simp? `Complex.natCast_im : (↑n : ℂ).im = 0`? I believe yes (used in zeroDisc_isNontrivial's simp call — they had natCast_re? they used `simp [neg_re, mul_re]` for −2*↑n... which needs mul_re, neg_re, natCast_re, natCast_im — it worked, so those exist ✓).\n- hvre : 0 < v.re: v.re = w.re + ↑n: simp [Complex.add_re, Complex.natCast_re] then need 0 < w.re + ↑n: from Nat.le_ceil: |w.re| ≤ ↑⌈|w.re|⌉₊ and n = ⌈|w.re|⌉₊ + 2: (↑n : ℝ) = ↑⌈..⌉₊ + 2 (push_cast): w.re + ↑n ≥ w.re + |w.re| + 2 ≥ 2: neg_abs_le w.re : −|w.re| ≤ w.re ⟹ w.re + |w.re| ≥ 0 ✓:\n```\n  have hnv : (0:ℝ) < w.re + (n : ℝ) := by\n    have h1 : (n : ℝ) = (⌈|w.re|⌉₊ : ℝ) + 2 := by rw [hn]; push_cast; ring\n    have h2 : |w.re| ≤ (⌈|w.re|⌉₊ : ℝ) := Nat.le_ceil _\n    have h3 : 0 ≤ w.re + |w.re| := by linarith [neg_abs_le w.re]\n    nlinarith [h1, h2, h3]\n```\nn is `set n := ⌈|w.re|⌉₊ + 2 with hn` — hn : n = ⌈|w.re|⌉₊ + 2 ✓.\n\n- The hanti's IntervalIntegrable (for the log FTC): integrand (w+↑x)⁻¹ continuous ✓.\n- integral_eq_sub_of_hasDerivAt: signature `(hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' volume a b) : ∫ x in a..b, f' x = f b − f a` ✓.\n\nOne more: hsum uses hEM which needs `Set.Icc` for hf_diff and `Set.uIcc` ([[a,b]]) for h_cont — the lemma states hf_diff on Set.Icc a b and h_cont on [[a,b]] = uIcc ✓ match my haves.\n\nAlso `abs_B1_le_half {x : ℝ} (hx : 0 ≤ x) : |B1 x| ≤ 1/2` ✓ root namespace.\n\nAlso `intervalIntegral.integral_mono_on` — check name/signature: `intervalIntegral.integral_mono_on (h : a ≤ b) (hf : IntervalIntegrable f volume a b) (hg : IntervalIntegrable g volume a b) (hfg : ∀ x ∈ Set.Icc a b, f x ≤ g x) : ∫ x in a..b, f x ≤ ∫ x in a..b, g x`? I think it's `integral_mono_on (h : a ≤ b) (hf : IntervalIntegrable f ...) (hg : ...) (hfg : ∀ᵐ x ∂(μ.restrict (Set.Icc a b)), f x ≤ g x)`? or the plain ∀ version `intervalIntegral.integral_mono_on (hab : a ≤ b) (hf) (hg) (h : ∀ x ∈ Set.Icc a b, f x ≤ g x)`? hmm. There are two: integral_mono (ae) and integral_mono_on (Icc). I'll adapt at build. The integrability side: hint1 : IntervalIntegrable (fun x => ‖deriv .. x * ↑(B1 x)‖) volume 0 ↑n: Continuous on Icc: deriv = −(w+↑x)²⁻¹ continuous ✓, B1 bounded measurable... ‖deriv * B1‖: B1 is not continuous but bounded+AEStronglyMeasurable (Zeta23 has aestronglyMeasurable_B1 + abs_B1_le_half): product continuous·measurable: IntervalIntegrable via ContinuousOn.intervalIntegrable? norm of product: (continuous_norm.comp...) — the function x ↦ ‖deriv x * ↑(B1 x)‖ = ‖deriv x‖ * |B1 x|: product of continuous with bounded-ae-measurable: use `IntervalIntegrable.continuousOn_mul`? hmm that was for the ℂ-valued: Zeta23's intervalIntegrable_deriv_mul_B1 handles deriv f * B1 integrability ✓ — for the NORM version: ‖deriv f x * ↑(B1 x)‖ ≤ ‖deriv f x‖ * (1/2) pointwise and the norm function is Continuous.mul (B1 measurable...) — simplest: IntegrableOn of bounded ae-measurable on finite measure: `MeasureTheory.Measure.integrableOn_of_bounded (hμ : μ s < ∞) (hmeas : AEStronglyMeasurable f μ) (hM : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ M)`? The Zeta23 intervalIntegrable_deriv_mul_B1 used exactly this pattern (Measure.integrableOn_of_bounded (by simp) (by fun_prop) (M := 1/2) with the ae bound). For my norm function: AEStronglyMeasurable (fun x => ‖deriv x * ↑(B1 x)‖): from aestronglyMeasurable_B1 and the continuous deriv: (aestronglyMeasurable.comp... — via (continuous_norm.comp_continuous...).aestronglyMeasurable mul AEStrongly... There's `AEStronglyMeasurable.mul`? For ℝ≥0... Let me instead bound the norm integral differently — AVOID integral_mono_on for the norm: use a two-step: \n‖∫ F‖ ≤ ∫ ‖F‖ (norm_integral_le_integral_norm) then ∫ ‖F‖ ≤ ∫ G where ‖F‖ ≤ G pointwise ae: `intervalIntegral.integral_mono_ae`? Also needs integrability of ‖F‖. Hmm same issue.\n\nAlternative cleaner: bound ‖F(x)‖ pointwise ≤ H(x) where H continuous, and use: ∫ ‖F‖ ≤ ∫ H via... still needs ‖F‖ integrable. OK let me just build the integrability: \nfun x => ‖deriv f x * ↑(B1 x)‖: write as (fun x => ‖deriv f x‖ * |B1 x|) via norm_mul/norm_real funext... measurable: |B1| = (B1) with abs: aestronglyMeasurable_B1 : AEStronglyMeasurable B1 — .norm? there's `AEStronglyMeasurable.norm : AEStronglyMeasurable f → AEStronglyMeasurable (fun x => ‖f x‖)` ✓. And for the coercion ↑(B1 x): RCLike ofReal: continuous_ofReal.comp aestrongly... `(Complex.continuous_ofReal.comp_aestronglyMeasurable aestronglyMeasurable_B1)` — Continuous.comp_aestronglyMeasurable ✓ exists. Then mul: `AEStronglyMeasurable.mul`? for normed... `AEStronglyMeasurable.mul (hf : AEStronglyMeasurable f) (hg : AEStronglyMeasurable g) : AEStronglyMeasurable (f * g)` ✓ exists (for normed ring-ish targets ✓ ℂ). Then .norm again. Then integrableOn_of_bounded with M := (max of ‖deriv‖ on Icc)·(1/2): need a uniform bound: ‖deriv f x‖ = ‖w+↑x‖⁻² ≤ 1/4 (‖w+↑x‖ ≥ |im| ≥ 2 ⟹ ‖·‖⁻² ≤ 1/4): so ‖deriv * B1‖ ≤ (1/4)(1/2) = 1/8 pointwise (not just ae). With IntervalIntegrable from Measure.integrableOn_of_bounded (μ [a,b] < ∞) (aestronglyMeasurable) (ae ∀ᵐ bound 1/8) then intervalIntegrable_iff' ... that's what Zeta23's helper does — I can MIMIC: actually simpler: since I need BOTH the EM's own integrability (which the lemma handles internally? no — the EM lemma sum_eq_integral_add_integral_deriv has hypotheses hf_diff + h_cont only; its internal proof uses intervalIntegrable_deriv_mul_B1) — the integral ∫ deriv f * B1 EXISTS by the lemma. For my norm bound: \nhint_norm : IntervalIntegrable (fun x => ‖deriv f x * ↑(B1 x)‖) volume 0 ↑n:\n  IntervalIntegrable.continuousOn_mul? hmm — no. Let me use: the function equals (fun x => ‖deriv f x‖ * |B1 x|) ae... equal everywhere actually (norm_mul, Complex.norm_real? ‖(r:ℂ)‖ = |r|: Complex.norm_real gives ‖(r:ℂ)‖ = ‖r‖ and Real.norm_eq_abs: ‖r‖ = |r| ✓ so pointwise equal). Then IntervalIntegrable of (‖deriv‖ · |B1|): continuous ‖deriv‖ times bounded ae-measurable |B1|: `IntervalIntegrable.mul_bdd...`? There might be `IntervalIntegrable.continuousOn_mul` is for two continuous... The pattern in Zeta23: `IntervalIntegrable.continuousOn_mul ?_ h_cont` where ?_ : IntervalIntegrable B1-ish via integrableOn_of_bounded — i.e., continuousOn_mul (h_bdd_integrable) (h_cont): signature `IntervalIntegrable.continuousOn_mul (h1 : IntervalIntegrable f μ a b) (h2 : ContinuousOn g [[a,b]]) : IntervalIntegrable (fun t => f t * g t)`? In EulerMaclaurin it's used as `IntervalIntegrable.continuousOn_mul ?_ h_cont` giving IntervalIntegrable (fun t => deriv f t * B1 t) with ?_ the B1 integrability and h_cont the deriv continuity — so continuousOn_mul (hf_integrable) (hg_continuousOn) : f * g integrable. So for my norm version: f := fun x => |B1 x| (bounded, ae-measurable ⟹ integrable on finite interval via integrableOn_of_bounded), g := fun x => ‖deriv .. x‖ (continuousOn): IntervalIntegrable (fun x => |B1 x| * ‖deriv x‖) ✓ then rewrite to my norm function via pointwise equality (funext + mul_comm + norm_mul): \n```\n  have hnorm_eq : (fun x : ℝ => ‖deriv .. x * ↑(B1 x)‖) = fun x : ℝ => |B1 x| * ‖deriv .. x‖ := by\n    funext x\n    rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, Real.norm_eq_abs]  -- ‖↑(B1 x)‖ = |B1 x|; ‖deriv‖ stays ‖·‖ (normed field norm = abs for ℝ? ‖deriv..‖ is ℂ-norm — the function is ℝ-valued after outer norm: ‖d‖ * |B1|: order swap via mul_comm)\n    ring\n```\nHmm: ‖d * ↑(B1 x)‖ = ‖d‖ * ‖↑(B1 x)‖ = ‖d‖ * |B1 x| = |B1 x| * ‖d‖ (mul_comm) ✓. And |B1 x| as ℝ: |B1 x| = ‖(B1 x : ℝ)‖ via Real.norm_eq_abs.symm. OK.\n\nThis is getting heavy but it's all standard. Total §6 estimate ~350 lines. Let me now also prepare the integrability for the arctan side and (1/2)((x+a)²+c²)⁻¹ (continuous ✓ easy).\n\nActually — hmm, wait. Let me reconsider: is there an EASIER route to ∫ ‖F‖ ≤ bound that avoids the ae-measurability plumbing? YES: use `intervalIntegral.norm_integral_le_of_norm_le` : `intervalIntegral.norm_integral_le_of_norm_le (hab : a ≤ b) (hf : IntervalIntegrable f ...) (hM : ∀ x ∈ Set.Icc a b, ‖f x‖ ≤ M)`? hmm that's for CONSTANT M. There's `intervalIntegral.norm_integral_le_of_norm_le (hab) (hf : IntervalIntegrable f volume a b) (h : ∀ x ∈ Set.uIcc a b, ‖f x‖ ≤ C) : ‖∫ x in a..b, f x‖ ≤ C * (b - a)`? — constant only; C·n too big. \n\nWhat about: `intervalIntegral.norm_integral_le_integral_norm` then bound ∫ ‖F x‖ via comparing with the CONTINUOUS majorant G(x) = (1/2)((x+a)²+c²)⁻¹ using integral_mono_on — needs ‖F‖ integrable: ‖F‖ = ‖deriv‖·|B1| as shown. The plumbing is needed but it's ~10 lines via the Zeta23 pattern. Fine.\n\nLet me also double-check `intervalIntegral.integral_mono_on` exists with the Icc-pointwise form... In Mathlib: `intervalIntegral.integral_mono_on (h : a ≤ b) (hf : IntervalIntegrable f volume a b) (hg : IntervalIntegrable g volume a b) (hfg : ∀ x ∈ Set.Icc a b, f x ≤ g x) : ∫ x in a..b, f x ≤ ∫ x in a..b, g x` — I believe this exact one exists (integral_mono_on with Ioc version too). OK.\n\nNow write §6. Also the final constant check: 1 + (1/2 + (1/2)(π/c)) ≤ 3 with π/c ≤ π/2 < 1.575: 1 + 1/2 + 0.7875 = 2.2875 ≤ 3 ✓ nlinarith [hpc, Real.pi_lt_d2.le]: need (1/2)*(π/c) ≤ (1/2)*(3.15/2)... nlinarith with hpc : π/c ≤ π/2 and pi < 3.15: 1 + 1/2 + (1/2)(π/c) ≤ 1.5 + 0.5·(π/2) ≤ 1.5 + π/4 ≤ 1.5 + 0.7875 = 2.2875 ≤ 3 ✓.\n\nWriting §6 now. Note: digamma_add_natCast needs the induction with the ∀ m hypothesis at each step. Let me write:\n\n```\ntheorem digamma_add_natCast {w : ℂ} (hw : w.im ≠ 0) (n : ℕ) :\n    Complex.digamma (w + n) = Complex.digamma w + ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ := by\n  have hne : ∀ j : ℕ, ∀ m : ℕ, w + (j : ℂ) ≠ -(m : ℂ) := by\n    intro j m h\n    apply hw\n    have h2 : (w + (j : ℂ)).im = 0 := by rw [h]; simp\n    rw [Complex.add_im, Complex.natCast_im, add_zero] at h2\n    exact h2\n  induction n with\n  | zero => simp\n  | succ k ih =>\n    have h1 := Complex.digamma_apply_add_one (w + (k : ℂ)) (hne k)\n    rw [show w + ((k + 1 : ℕ) : ℂ) = (w + (k : ℂ)) + 1 by push_cast; ring, h1, ih,\n      Finset.sum_range_succ]\n    ring  -- hmm: (digamma w + Σ_{j<k}) + (w+↑k)⁻¹ = digamma w + Σ_{j<k+1}: sum_range_succ already applied... let me check: after rw [..., h1, ih, Finset.sum_range_succ]: goal digamma w + Σ_{j<k} + (w+↑k)⁻¹ = digamma w + (Σ_{j<k} + (w+↑k)⁻¹): ring closes? Or it's already closed by rw rfl. Let me drop the ring and see; safer keep `rw [...]` then `ring` — if rw closes, ring errors \"no goals\"... journal-024 gotcha: check. Use `rw [...]; ` and if unsolved add ring. I'll write `rw [...]` then `ring_nf`? risky either way; use `exact` with calc? Simplest: after the rw chain, add `ring` and remove if \"no goals\" error. Actually since sum_range_succ rewrites the RHS Σ_{j<k+1}: goal after all rws: (digamma w + Σ_{j<k}) + (w+↑k)⁻¹ = digamma w + (Σ_{j<k} + (w+↑k)⁻¹)?? — the LHS form: h1 : digamma (w+↑k+1) = digamma (w+↑k) + (w+↑k)⁻¹; after rw [show ..., h1]: goal LHS becomes digamma (w+↑k) + (w+↑k)⁻¹; then rw [ih]: digamma (w+↑k) → digamma w + Σ_{j<k}: goal: (digamma w + Σ_{j<k}) + (w+↑k)⁻¹ = digamma w + Σ_{j<k+1}; rw [Finset.sum_range_succ] rewrites Σ_{j<k+1} → Σ_{j<k} + (w+↑k)⁻¹ hmm — sum_range_succ : ∑ i ∈ range (n+1), f i = ∑ i ∈ range n, f i + f n ✓ rewrites the occurrence. Then both sides: (digamma w + Σ) + term vs digamma w + (Σ + term) — NOT syntactically equal (assoc) — ring closes ✓. Keep the ring.\n```\n\nWait — actually, digamma_apply_add_one : digamma (s + 1) = digamma s + s⁻¹. My rw [show w + ↑(k+1) = (w + ↑k) + 1 ...] — the direction: goal LHS has digamma (w + ↑(k+1)); the show rewrites it to digamma ((w+↑k)+1); then rw [h1] : digamma (w+↑k+1)... hold on h1 : digamma (w + ↑k + 1) = ... — is `w + ↑k + 1` the same term as `(w + ↑k) + 1`? Yes (+ is left-assoc) ✓.\n\nCast note: (w + (k:ℂ)) with k : ℕ — digamma_apply_add_one's s := w + ↑k, hypothesis ∀ m, w + ↑k ≠ −↑m = hne k ✓.\n\nOK writing the full §6 now. Also need `Set.mem_Icc`/`Set.uIcc` handling: hanti : ∀ x ∈ Set.uIcc 0 ↑n — intro x _ fine.\n\nFor hcont (ContinuousOn (deriv f) [[0, ↑n]]): [[a,b]] notation needs `open Interval` — I'll write Set.uIcc 0 (↑n) explicitly.\n\nThe EM lemma's h_cont expects `ContinuousOn (deriv f) [[a, b]]` where [[a,b]] is uIcc notation from `open Interval` in EulerMaclaurin — but the STATEMENT's type has Set.uIcc a b after elaboration regardless ✓ so providing Set.uIcc works.\n\nAlso `sum_eq_integral_add_integral_deriv` — root namespace ✓ (no namespace in the file).\n\nOne more: my f is (fun x : ℝ => (w + (x:ℂ))⁻¹); the EM sum's summand f ↑k with k : ℕ — the cast (↑k : ℝ). After applying, terms show (fun x => (w + ↑x)⁻¹) ↑k — beta redexes; use `simp only []` to beta-reduce or write the application with beta-reduced form via `show`. I'll add `simp only []` after the EM rw if needed — or `beta_reduce`. In Lean4 Mathlib: `simp only []` performs beta/eta. OK.\n\nLet me also prepare hne_all, hanti, hconti, hder, hderiv_eq, hcont as top-level haves in the main theorem before EM.\n\nLength concern — fine, write it.","signature":""},{"type":"text","text":"§0–§5 green. Now §6 — the left-plane uniform digamma bound (the 5e input)."},{"type":"tool_use","id":"Edit_103","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiReflect.lean","old_string":"/-! ## 5. The left-half loose R-bound (ii′-5d capstone) -/","new_string":"/-! ## 5.5. The digamma recurrence over a natural shift -/\n\n/-- ψ(w + n) = ψ(w) + Σ_{j<n} (w + j)⁻¹ (iterated `digamma_apply_add_one`;\nthe off-real hypothesis keeps every step away from the poles). -/\ntheorem digamma_add_natCast {w : ℂ} (hw : w.im ≠ 0) (n : ℕ) :\n    Complex.digamma (w + n) = Complex.digamma w + ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ := by\n  have hne : ∀ j : ℕ, ∀ m : ℕ, w + (j : ℂ) ≠ -(m : ℂ) := by\n    intro j m h\n    apply hw\n    have h2 : (w + (j : ℂ)).im = 0 := by rw [h]; simp\n    rw [Complex.add_im, Complex.natCast_im, add_zero] at h2\n    exact h2\n  induction n with\n  | zero => simp\n  | succ k ih =>\n    have h1 := Complex.digamma_apply_add_one (w + (k : ℂ)) (hne k)\n    rw [show w + ((k + 1 : ℕ) : ℂ) = (w + (k : ℂ)) + 1 by push_cast; ring, h1, ih,\n      Finset.sum_range_succ]\n    ring\n\n/-! ## 6. The left-plane uniform digamma bound (ii′-5e input) -/\n\n/-- **The left-plane uniform digamma bound**: for `2 ≤ |im w|` (away from the\npoles), `‖ψ(w) − log w‖ ≤ 3`. Route (D-067 §6): shift `w` by\n`n = ⌈|re w|⌉₊ + 2` into the right half-plane (StirlingVert there), and\ncompare the reciprocal sum with the log difference by first-order\nEuler–Maclaurin (`sum_eq_integral_add_integral_deriv`); the B̃₁ remainder is\nbounded by the arctan integral `∫ dx/((x+a)²+c²) ≤ π/c ≤ π/2`. The constants\nare uniform in the chain length — this is what makes the bound usable on the\nγ-gap circles of ii′-5e. -/\ntheorem norm_digamma_sub_log_le_of_two_le_abs_im {w : ℂ} (hw : 2 ≤ |w.im|) :\n    ‖Complex.digamma w - Complex.log w‖ ≤ 3 := by\n  -- setup\n  have him : w.im ≠ 0 := by\n    intro h\n    rw [h, abs_zero] at hw\n    norm_num at hw\n  have hc0 : (0 : ℝ) < |w.im| := by linarith [hw]\n  set n := ⌈|w.re|⌉₊ + 2 with hn\n  have hcast : ∀ j : ℕ, (w + ((j : ℝ) : ℂ))⁻¹ = (w + (j : ℂ))⁻¹ := by\n    intro j\n    simp\n  set v := w + (n : ℂ) with hv\n  have hnv : (0 : ℝ) < w.re + (n : ℝ) := by\n    have h1 : (n : ℝ) = (⌈|w.re|⌉₊ : ℝ) + 2 := by rw [hn]; push_cast; ring\n    have h2 : |w.re| ≤ (⌈|w.re|⌉₊ : ℝ) := Nat.le_ceil _\n    have h3 : 0 ≤ w.re + |w.re| := by linarith [neg_abs_le w.re]\n    nlinarith [h1, h2, h3]\n  have hvre : 0 < v.re := by\n    rw [hv]\n    simp [Complex.add_re, Complex.natCast_re]\n    exact hnv\n  have hvim : v.im = w.im := by\n    rw [hv]\n    simp [Complex.add_im, Complex.natCast_im]\n  have hvnorm : 2 ≤ ‖v‖ := by\n    have h := Complex.abs_im_le_norm v\n    rw [hvim] at h\n    linarith [hw, h]\n  have hwnorm : 2 ≤ ‖w‖ := hw.trans (Complex.abs_im_le_norm w)\n  have hne_all : ∀ x : ℝ, w + (x : ℂ) ≠ 0 := by\n    intro x h\n    apply him\n    have h2 : (w + (x : ℂ)).im = 0 := by rw [h]; simp\n    rw [Complex.add_im, Complex.ofReal_im, add_zero] at h2\n    exact h2\n  -- the derivative family of f y = (w + ↑y)⁻¹\n  have hder : ∀ x : ℝ, HasDerivAt (fun y : ℝ => (w + (y : ℂ))⁻¹) (-(((w + (x : ℂ)) ^ 2)⁻¹)) x := by\n    intro x\n    have hne := hne_all x\n    have h1 : HasDerivAt (fun z : ℂ => (w + z)⁻¹) (-(((w + (x : ℂ)) ^ 2)⁻¹)) (x : ℂ) := by\n      have h2 := ((hasDerivAt_id' (x : ℂ)).const_add w).inv hne\n      simpa [neg_div, one_div] using h2\n    exact h1.comp_ofReal\n  have hderiv_eq : deriv (fun y : ℝ => (w + (y : ℂ))⁻¹)\n      = fun x : ℝ => -(((w + (x : ℂ)) ^ 2)⁻¹) := funext fun x => (hder x).deriv\n  have hcont : ContinuousOn (deriv (fun y : ℝ => (w + (y : ℂ))⁻¹)) (Set.uIcc 0 (n : ℝ)) := by\n    rw [hderiv_eq]\n    apply Continuous.continuousOn\n    apply Continuous.neg\n    apply Continuous.inv₀ _ (fun x => pow_ne_zero 2 (hne_all x))\n    exact (continuous_const.add Complex.continuous_ofReal).pow 2\n  -- Euler–Maclaurin\n  have hEM := sum_eq_integral_add_integral_deriv (f := fun y : ℝ => (w + (y : ℂ))⁻¹)\n    (a := 0) (b := (n : ℝ)) le_rfl (Nat.cast_nonneg _)\n    (fun t _ => (hder t).differentiableAt) hcont\n  rw [Nat.floor_zero, Nat.floor_natCast] at hEM\n  have hB10 : B1 0 = -1 / 2 := by unfold B1; simp\n  have hB1n : B1 (n : ℝ) = -1 / 2 := by unfold B1; rw [Nat.floor_natCast]; simp\n  rw [hB10, hB1n] at hEM\n  have hIoc : Finset.Ioc 0 n = (Finset.range (n + 1)).erase 0 := by\n    ext x\n    simp only [Finset.mem_Ioc, Finset.mem_erase, Finset.mem_range]\n    omega\n  have hconv : ∑ k ∈ Finset.Ioc 0 n, (w + ((k : ℝ) : ℂ))⁻¹\n      = ∑ j ∈ Finset.range n, (w + ((j : ℝ) : ℂ))⁻¹ - (w + ((0 : ℝ) : ℂ))⁻¹\n        + (w + ((n : ℝ) : ℂ))⁻¹ := by\n    rw [hIoc]\n    have h0mem : 0 ∈ Finset.range (n + 1) := Finset.mem_range.mpr (Nat.succ_pos n)\n    have h1 := Finset.add_sum_erase (Finset.range (n + 1))\n      (fun k => (w + ((k : ℝ) : ℂ))⁻¹) h0mem\n    rw [Finset.sum_range_succ] at h1\n    linear_combination h1\n  have hsum : ∑ j ∈ Finset.range n, (w + ((j : ℝ) : ℂ))⁻¹\n      = (∫ x in (0 : ℝ)..(n : ℝ), (w + (x : ℂ))⁻¹)\n        + ((w + ((0 : ℝ) : ℂ))⁻¹ - (w + ((n : ℝ) : ℂ))⁻¹) / 2\n        + ∫ x in (0 : ℝ)..(n : ℝ),\n            deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ) := by\n    linear_combination hEM - hconv\n  -- the log FTC\n  have hanti : ∀ x ∈ Set.uIcc 0 (n : ℝ),\n      HasDerivAt (fun y : ℝ => Complex.log (w + (y : ℂ))) ((w + (x : ℂ))⁻¹) x := by\n    intro x _\n    have hne := hne_all x\n    have hslit : w + (x : ℂ) ∈ Complex.slitPlane := by\n      rw [Complex.mem_slitPlane_iff]\n      right\n      rw [Complex.add_im, Complex.ofReal_im, add_zero]\n      exact him\n    have h1 : HasDerivAt (fun z : ℂ => Complex.log (w + z)) ((w + (x : ℂ))⁻¹) (x : ℂ) := by\n      have h2 := (Complex.hasDerivAt_log hslit).comp (x : ℂ)\n        ((hasDerivAt_id' (x : ℂ)).const_add w)\n      simpa [Function.comp_def] using h2\n    exact h1.comp_ofReal\n  have hconti : IntervalIntegrable (fun y : ℝ => (w + (y : ℂ))⁻¹) volume 0 (n : ℝ) := by\n    apply ContinuousOn.intervalIntegrable\n    apply Continuous.continuousOn\n    apply Continuous.inv₀ _ hne_all\n    exact continuous_const.add Complex.continuous_ofReal\n  have hint : ∫ x in (0 : ℝ)..(n : ℝ), (w + (x : ℂ))⁻¹ = Complex.log v - Complex.log w := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti hconti]\n    simp [hv]\n  -- the arctan comparison integral\n  have hanti2 : ∀ x ∈ Set.uIcc 0 (n : ℝ),\n      HasDerivAt (fun y : ℝ => (1 / |w.im|) * Real.arctan ((y + w.re) / |w.im|))\n        (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) x := by\n    intro x _\n    have h1 : HasDerivAt (fun y : ℝ => (y + w.re) / |w.im|) (1 / |w.im|) x :=\n      ((hasDerivAt_id x).add_const w.re).div_const |w.im|\n    have h2 := h1.arctan\n    have h3 := h2.const_mul (1 / |w.im|)\n    refine h3.congr_deriv ?_\n    field_simp [hc0.ne']\n    ring\n  have hconti2 : IntervalIntegrable (fun x : ℝ => ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹)\n      volume 0 (n : ℝ) := by\n    apply ContinuousOn.intervalIntegrable\n    apply Continuous.continuousOn\n    apply Continuous.inv₀ _ (fun x => by\n      have h1 : (0 : ℝ) < (x + w.re) ^ 2 + |w.im| ^ 2 := by\n        nlinarith [sq_nonneg (x + w.re), hc0]\n      exact ne_of_gt h1)\n    exact (continuous_id.add continuous_const).pow 2 |>.add continuous_const\n  have harctan : ∫ x in (0 : ℝ)..(n : ℝ), ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹\n      ≤ Real.pi / |w.im| := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti2 hconti2]\n    have h1 : Real.arctan (((n : ℝ) + w.re) / |w.im|)\n        - Real.arctan ((0 + w.re) / |w.im|) ≤ Real.pi := by\n      have hu := Real.arctan_lt_pi_div_two (((n : ℝ) + w.re) / |w.im|)\n      have hv2 := Real.arctan_lt_pi_div_two (-((0 + w.re) / |w.im|))\n      rw [Real.arctan_neg] at hv2\n      linarith [Real.pi_pos, hv2]\n    calc (1 / |w.im|) * Real.arctan (((n : ℝ) + w.re) / |w.im|)\n          - (1 / |w.im|) * Real.arctan ((0 + w.re) / |w.im|)\n        = (1 / |w.im|) * (Real.arctan (((n : ℝ) + w.re) / |w.im|)\n            - Real.arctan ((0 + w.re) / |w.im|)) := by ring\n      _ ≤ (1 / |w.im|) * Real.pi :=\n          mul_le_mul_of_nonneg_left h1 (by positivity)\n      _ = Real.pi / |w.im| := by ring\n  -- the B̃₁ remainder bound\n  have hnorm_eq : (fun x : ℝ => ‖deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖)\n      = fun x : ℝ => |B1 x| * ‖(w + (x : ℂ))⁻¹‖ ^ 2 := by\n    funext x\n    rw [hderiv_eq]\n    rw [norm_mul, norm_neg, norm_inv, norm_pow, Complex.norm_real, Real.norm_eq_abs]\n    ring\n  have hnsq : ∀ x : ℝ, ‖w + (x : ℂ)‖ ^ 2 = (x + w.re) ^ 2 + |w.im| ^ 2 := by\n    intro x\n    rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n    simp [Complex.add_re, Complex.ofReal_re, Complex.add_im, Complex.ofReal_im]\n    rw [sq_abs]\n    ring\n  have hrem_integrable : IntervalIntegrable\n      (fun x : ℝ => ‖deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖)\n      volume 0 (n : ℝ) := by\n    rw [hnorm_eq]\n    apply IntervalIntegrable.continuousOn_mul _ ((Continuous.inv₀\n      ((continuous_const.add Complex.continuous_ofReal).pow 2)\n      (fun x => pow_ne_zero 2 (hne_all x))).neg |>.norm |>.continuousOn)\n    rw [intervalIntegrable_iff]\n    apply Measure.integrableOn_of_bounded (M := 1 / 2)\n    · simp\n    · exact (aestronglyMeasurable_B1.norm)\n    · filter_upwards [self_mem_ae_restrict (by measurability)] with x hx\n      rw [Set.uIcc_of_le (Nat.cast_nonneg n), Set.mem_Icc] at hx\n      rw [Real.norm_of_nonneg (abs_nonneg _)]\n      exact abs_B1_le_half hx.1\n  have hrem : ‖∫ x in (0 : ℝ)..(n : ℝ),\n        deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖\n      ≤ (1 / 2) * (Real.pi / |w.im|) := by\n    refine (intervalIntegral.norm_integral_le_integral_norm (Nat.cast_nonneg n)).trans ?_\n    have hmono : ∫ x in (0 : ℝ)..(n : ℝ),\n          ‖deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖\n        ≤ ∫ x in (0 : ℝ)..(n : ℝ), (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) := by\n      apply intervalIntegral.integral_mono_on (Nat.cast_nonneg n) hrem_integrable\n        (hconti2.const_mul _)\n      intro x hx\n      rw [Set.mem_Icc] at hx\n      rw [hnorm_eq, (hder x).deriv]\n      rw [norm_neg, norm_inv, norm_pow]\n      have hB : |B1 x| ≤ 1 / 2 := abs_B1_le_half hx.1\n      have hpos : (0 : ℝ) < (x + w.re) ^ 2 + |w.im| ^ 2 := by\n        nlinarith [sq_nonneg (x + w.re), hc0]\n      rw [hnsq]\n      calc |B1 x| * (((x + w.re) ^ 2 + |w.im| ^ 2) ^ 2)⁻¹\n          ≤ (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2) ^ 2)⁻¹ :=\n            by apply mul_le_mul_of_nonneg_right _ hB ... \n```\nHmm wait — I'm making an error in hnsq/norm application: ‖(w+↑x)⁻¹‖² = (‖w+↑x‖⁻¹)² = (‖w+↑x‖²)⁻¹. Let me redo the pointwise step carefully:\n\ngoal (after rw [hnorm_eq, (hder x).deriv]): |B1 x| * ‖−((w+↑x)²)⁻¹‖^2 ≤ (1/2) * ((x+w.re)²+|w.im|²)⁻¹.\n‖−((w+↑x)²)⁻¹‖ = ‖(w+↑x)²‖⁻¹ = (‖w+↑x‖²)⁻¹. So LHS = |B1 x| * ((‖w+↑x‖²)⁻¹)² — CAREFUL: the outer ^2 in hnorm_eq is on the NORM: ‖(w+↑x)⁻¹‖^2 = (‖w+↑x‖⁻¹)² = (‖w+↑x‖²)⁻¹ ✓ (inv_pow). So hnorm_eq should be stated as |B1 x| * ‖(w + ↑x)⁻¹‖^2 — and then ‖(w+↑x)⁻¹‖^2 = (‖w+↑x‖⁻¹)^2 = ((‖w+↑x‖)^2)⁻¹... Then with hnsq: = (((x+w.re)² + |w.im|²))⁻¹. So the goal becomes |B1 x| * (((x+w.re)²+|w.im|²))⁻¹ ≤ (1/2) * (((x+w.re)²+|w.im|²))⁻¹ — but wait the integrand on the RHS is (1/2) * ((x+w.re)^2 + |w.im|^2)⁻¹ ✓ same. Then mul_le_mul_of_nonneg_left hB (inv_nonneg.mpr hpos.le) : |B1 x| * X ≤ (1/2) * X? mul_le_mul_of_nonneg_left (h : b ≤ c) (ha : 0 ≤ a) : a * b ≤ a * c — so |B1 x| * X ≤ (1/2)*X is mul_le_mul_of_nonneg_RIGHT (h : |B1 x| ≤ 1/2) (hX : 0 ≤ X)?? mul_le_mul_of_nonneg_right (h : b ≤ c) (ha : 0 ≤ a) : b * a ≤ c * a — with a := X: |B1 x| * X ≤ (1/2) * X ✓.\n\nSo the calc:\n```\n      rw [hnorm_eq]\n      rw [show ‖(w + (x:ℂ))⁻¹‖ ^ 2 = (((x + w.re)^2 + |w.im|^2)⁻¹) by\n        rw [norm_inv, inv_pow, hnsq x]  -- (‖w+↑x‖⁻¹)² = (‖w+↑x‖²)⁻¹ = ((x+w.re)²+|w.im|²)⁻¹\n        ]  -- hmm: ‖(w+↑x)⁻¹‖ = ‖w+↑x‖⁻¹ (norm_inv); (‖w+↑x‖⁻¹)^2 = (‖w+↑x‖^2)⁻¹ (inv_pow); hnsq x : ‖w+↑x‖^2 = (x+w.re)^2+|w.im|^2\n      exact mul_le_mul_of_nonneg_right hB (inv_nonneg.mpr hpos.le)\n```\nWait — inv_pow : (a⁻¹)^n = (a^n)⁻¹ ✓. So ‖(w+↑x)⁻¹‖^2 = (‖w+↑x‖⁻¹)^2 [norm_inv] = (‖w+↑x‖^2)⁻¹ [inv_pow] = ((x+w.re)²+|w.im|²)⁻¹ [hnsq] ✓.\n\nAnd drop the (hder x).deriv rewrite since hnorm_eq already has the deriv unfolded? hnorm_eq : (fun x => ‖deriv (fun y => (w+↑y)⁻¹) x * ↑(B1 x)‖) = fun x => |B1 x| * ‖(w+↑x)⁻¹‖^2 — the rw [hderiv_eq] inside hnorm_eq's proof handles the deriv. Then in hmono, after rw [hnorm_eq] — the goal's integrand ‖deriv .. x * ↑(B1 x)‖ — the integral's function is the lambda (fun x => ‖deriv .. x * ↑(B1 x)‖): rw [hnorm_eq] rewrites the lambda ✓ then the pointwise goal after intro x hx: (fun x => |B1 x| * ‖(w+↑x)⁻¹‖^2) x ≤ (fun x => (1/2)*...) x — beta redexes: `simp only []` to beta-reduce, or the integral_mono_on's hfg goal shows the lambdas applied — beta reduce via `show`. Add `simp only []` after intro. Hmm — actually with the rw [hnorm_eq] BEFORE intro, the intervalIntegral.integral_mono_on's remaining goal is ∀ x ∈ Icc, (fun x => |B1 x| * ‖(w+↑x)⁻¹‖^2) x ≤ (fun x => (1/2) * ((x+w.re)^2+|w.im|^2)⁻¹) x. After intro x hx: beta redex goal. `simp only []` beta-reduces. Or `show |B1 x| * ‖(w + (x:ℂ))⁻¹‖^2 ≤ (1/2) * ((x + w.re)^2 + |w.im|^2)⁻¹` — show with defeq ✓ better.\n\nThen:\n```\n    refine hmono.trans ?_\n    rw [← intervalIntegral.integral_mul_const]  -- (1/2) * ∫ = ∫ (1/2)*·: integral_mul_const (c) (f) : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x — direction: rw [← ...] turns ∫ (1/2)*((..)⁻¹) into (1/2) * ∫ (..)⁻¹\n    exact mul_le_mul_of_nonneg_left harctan (by norm_num)  -- (1/2)*∫ ≤ (1/2)*(π/c) ✓\n```\n\nThen hboundary, hmid, final. Also `IntervalIntegrable.const_mul` for hconti2.const_mul ✓ exists.\n\nAlso `aestronglyMeasurable_B1` — root namespace from Zeta23 EulerMaclaurin ✓ (aestronglyMeasurable_B1 : AEStronglyMeasurable B1). .norm : AEStronglyMeasurable (fun x => ‖B1 x‖) — but I need AEStronglyMeasurable (fun x => |B1 x|) — for ℝ: |x| = ‖x‖: Real.norm_eq_abs — the integrableOn_of_bounded's hmeas : AEStronglyMeasurable f μ with f = fun x => |B1 x|: (aestronglyMeasurable_B1.norm) gives fun x => ‖B1 x‖ — ‖·‖ on ℝ is |·| defeq? Real.norm_eq_abs : ‖x‖ = |x| — defeq? Real.norm x := |x| — I think defeq (instNormReal uses abs). The bound: ∀ᵐ x, ‖f x‖ ≤ M with f = |B1 ·|: ‖|B1 x|‖ = |B1 x| (Real.norm_eq_abs, abs of nonneg = itself: Real.norm_of_nonneg (abs_nonneg _)) ✓ as I wrote.\n\nHmm wait — in hrem_integrable I used `IntervalIntegrable.continuousOn_mul _ (...)` — the argument order from EulerMaclaurin: `IntervalIntegrable.continuousOn_mul ?_ h_cont` produced IntervalIntegrable (fun t ↦ deriv f t * B1 t) with ?_ = the B1 integrability and h_cont = deriv continuity — so continuousOn_mul (h_int : IntervalIntegrable f ..) (h_cont : ContinuousOn g ..) : IntervalIntegrable (fun t => f t * g t ..)?? In their use: (fun t ↦ deriv f t * B1 t) — so f := B1 (integrable) and g := deriv f (continuous)?? The product order: deriv f t * B1 t = g t * f t... Their call: IntervalIntegrable.continuousOn_mul ?_ h_cont with ?_ : IntervalIntegrable B1 (via integrableOn_of_bounded (M := 1/2)) and h_cont : ContinuousOn (deriv f) — result (fun t ↦ deriv f t * B1 t) — so the signature is continuousOn_mul (hf : IntervalIntegrable f) (hg : ContinuousOn g) : IntervalIntegrable (g * f)? or (f * g)? Given result deriv * B1 with f := B1, g := deriv: result = g * f. So continuousOn_mul (hf : IntervalIntegrable f μ a b) (hg : ContinuousOn g uIcc) : IntervalIntegrable (fun t => g t * f t)? Hmm can't tell. Let me check the exact statement.\n\nFor my use: I want IntervalIntegrable (fun x => |B1 x| * ‖(w+↑x)⁻¹‖^2): f := |B1| integrable, g := ‖(w+↑x)⁻¹‖^2 continuous. If the signature gives (g * f): (fun x => ‖(w+↑x)⁻¹‖^2 * |B1 x|) — WRONG ORDER for my hnorm_eq... but I can swap hnorm_eq's RHS to ‖(w+↑x)⁻¹‖^2 * |B1 x|... whatever — check the signature first.\n\nActually — wait, in my hrem_integrable above I wrote the product as |B1 x| * ‖(w+↑x)⁻¹‖^2 in hnorm_eq. Let me check EulerMaclaurin's exact continuousOn_mul signature.","replace_all":false},"extra_content":null}]