[{"type":"thinking","thinking":"I see — my earlier Edit accidentally pasted my ANALYSIS TEXT (lines 827–860, including markdown code fences and commentary) into the Lean file! That's terrible. I need to replace lines 779–860 (the broken hnorm_eq through the analysis text) with the clean final §6 tail, keeping §5 capstone (862+) intact.\n\nThe clean replacement for the broken region (from \"  -- the B̃₁ remainder bound\" at 779 through the analysis text ending at line 860, just before the §5 comment at 862):\n\nComplete §6 tail:\n- hn1 (norm equality)\n- hnsq (norm square)\n- hnsq_inv\n- hgnorm_cont\n- hB1int\n- hrem_integrable (direct statement form)\n- hmono'\n- hrem\n- hboundary\n- hmid\n- hshift', hsumC\n- hv1 (StirlingVert at v)\n- final calc\n\nNote: hnorm_eq as previously written (line 780-785) has issues: rw [hderiv_eq] leaves beta-redex; then the norm chain. Let me write the whole tail fresh. Also hnsq's simp: goal after rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]: normSq expressed... wait direction: goal ‖w + ↑x‖^2 = (x + w.re)^2 + |w.im|^2: rw [← Complex.normSq_eq_norm_sq]: LHS becomes ↑(normSq (w+↑x))?? — normSq_eq_norm_sq : (normSq z : ℝ) = ‖z‖^2 — so ← direction rewrites ‖z‖^2 → ↑(normSq z): goal ↑(normSq (w+↑x)) = (x+w.re)^2 + |w.im|^2; then Complex.normSq_apply : normSq z = z.re*z.re + z.im*z.im — rw [Complex.normSq_apply]: ↑((w+↑x).re*(w+↑x).re + (w+↑x).im*(w+↑x).im) = ...: simp [add_re, ofReal_re, add_im, ofReal_im]: (w.re + x)*(w.re+x) + (w.im)*(w.im)... with the ofReal cast ↑(a + b) → ↑a + ↑b push_cast handles: hmm — ↑(re*re + im*im) vs RHS real expression: need push_cast to split the coe. Let me write:\n```\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    have h1 : (w + (x : ℂ)).re = w.re + x := by simp [Complex.add_re, Complex.ofReal_re]\n    have h2 : (w + (x : ℂ)).im = w.im := by simp [Complex.add_im, Complex.ofReal_im]\n    rw [h1, h2, sq_abs |w.im|...]\n```\nhmm: after rw [h1, h2]: goal ↑((w.re + x)*(w.re+x) + w.im*w.im) = (x+w.re)^2 + |w.im|^2: push_cast: LHS → (w.re+x)*(w.re+x) + w.im*w.im; then |w.im|^2 = w.im^2: rw [sq_abs]; ring ✓.\nSo: rw [h1, h2]; push_cast; rw [sq_abs]; ring. Order: push_cast first splits coe, then sq_abs rewrites |w.im|^2 → w.im^2, then ring ✓.\n\nLet me write the whole replacement now. Also remember hv1's norm12 requirement and the various pieces.\n\nOne more check on hsum/hEM beta: I'll add `simp only [] at hEM` after the B1 rws. And the f a * ↑(B1 a) terms: after hB10 rw: f 0 * ↑(−1/2)?? the rw [hB10] at hEM rewrites B1 0 → −1/2 giving f 0 * ↑(−1/2 : ℝ) with the RCLike coe — hmm actually the EM statement: f a * B1 a — with 𝕜 := ℂ and B1 : ℝ → ℝ the elaborated term is f a * ↑(B1 a) (RCLike coe) or f a * (B1 a : ℂ)... After rw [hB10] at hEM: f 0 * ((−1/2 : ℝ) : ℂ). And in linear_combination hEM − hconv, ring_nf normalizes ((−1/2:ℝ):ℂ) → −(1/2:ℂ)? via ofReal_neg/ofReal_div ✓ should be handled.\n\nAlso — the summand atoms: hEM's Ioc-sum after simp only [] at hEM: ∑ k ∈ Ioc 0 n, (w + (↑k:ℂ))⁻¹ — wait f ↑k with f := (fun y : ℝ => (w + (y:ℂ))⁻¹): beta: (w + (↑(↑k : ℕ → ℝ):ℂ))⁻¹ — the inner cast (↑k : ℝ) then ofReal: ((↑k:ℝ):ℂ) — matches hconv's ((k:ℝ):ℂ) ✓ syntactically identical ✓.\n\nAnd hsum's statement uses (w + ((j:ℝ):ℂ))⁻¹ — matches ✓. The integrals: hEM's ∫ t in 0..↑n, (fun y..) t — simp only [] at hEM beta-reduces to ∫ t, (w+↑t)⁻¹ — matches hsum's ∫ x, (w + (x:ℂ))⁻¹ (alpha-equiv ✓ same de Bruijn) ✓. The deriv integral: ∫ t, deriv (fun y => (w+↑y)⁻¹) t * ↑(B1 t) — matches hsum's ✓.\n\nNow write the replacement. I'll replace from line 779 to line 860 (the analysis text end), keeping §5 intact.","signature":""},{"type":"text","text":"My earlier edit accidentally pasted analysis notes into the file (lines 827–860). Replacing the whole broken tail with the clean §6 completion."},{"type":"tool_use","id":"Edit_110","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiReflect.lean","old_string":"  -- 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.","new_string":"  -- the B̃₁ remainder bound\n  have hderiv_eq2 : ∀ x : ℝ, deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x\n      = -(((w + (x : ℂ)) ^ 2)⁻¹) := fun x => (hder x).deriv\n  have hn1 : ∀ x : ℝ, ‖-(((w + (x : ℂ)) ^ 2)⁻¹)‖ = ‖(w + (x : ℂ))⁻¹‖ ^ 2 := by\n    intro x\n    simp only [norm_neg, norm_inv, norm_pow, inv_pow]\n  have hnorm_eq : (fun x : ℝ => ‖deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖)\n      = fun x : ℝ => ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖ := by\n    funext x\n    rw [hderiv_eq2 x, norm_mul, Complex.norm_real, hn1 x]\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    have h1 : (w + (x : ℂ)).re = w.re + x := by simp [Complex.add_re, Complex.ofReal_re]\n    have h2 : (w + (x : ℂ)).im = w.im := by simp [Complex.add_im, Complex.ofReal_im]\n    rw [h1, h2]\n    push_cast\n    rw [sq_abs]\n    ring\n  have hnsq_inv : ∀ x : ℝ, ‖(w + (x : ℂ))⁻¹‖ ^ 2 = ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹ := by\n    intro x\n    rw [norm_inv, inv_pow, hnsq x]\n  have hgnorm_cont : Continuous fun x : ℝ => ‖(w + (x : ℂ))⁻¹‖ ^ 2 :=\n    ((Continuous.inv₀ (continuous_const.add Complex.continuous_ofReal) hne_all).norm).pow 2\n  have hB1int : IntervalIntegrable (fun x : ℝ => ‖B1 x‖) volume 0 (n : ℝ) := by\n    rw [intervalIntegrable_iff']\n    apply MeasureTheory.Measure.integrableOn_of_bounded (by simp)\n      aestronglyMeasurable_B1.norm (M := 1 / 2)\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 (norm_nonneg _), Real.norm_eq_abs]\n    exact abs_B1_le_half hx.1\n  have hrem_integrable : IntervalIntegrable\n      (fun x : ℝ => ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖) volume 0 (n : ℝ) :=\n    hB1int.continuousOn_mul hgnorm_cont.continuousOn\n  have hmono : ∫ x in (0 : ℝ)..(n : ℝ), ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖\n      ≤ ∫ x in (0 : ℝ)..(n : ℝ), (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) := by\n    refine 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    show ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖ ≤ (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹)\n    rw [hnsq_inv x, Real.norm_eq_abs]\n    have hB : |B1 x| ≤ 1 / 2 := abs_B1_le_half hx.1\n    have hpos : (0 : ℝ) ≤ ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹ := inv_nonneg.mpr (by positivity)\n    calc (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) * |B1 x|\n        ≤ (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) * (1 / 2) :=\n          mul_le_mul_of_nonneg_left hB hpos\n      _ = (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) := by ring\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    calc ∫ x in (0 : ℝ)..(n : ℝ), ‖deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ)‖\n        = ∫ x in (0 : ℝ)..(n : ℝ), ‖(w + (x : ℂ))⁻¹‖ ^ 2 * ‖B1 x‖ := by\n          rw [hnorm_eq]\n      _ ≤ ∫ x in (0 : ℝ)..(n : ℝ), (1 / 2) * (((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹) := hmono\n      _ = (1 / 2) * ∫ x in (0 : ℝ)..(n : ℝ), ((x + w.re) ^ 2 + |w.im| ^ 2)⁻¹ := by\n          rw [intervalIntegral.integral_mul_const]\n      _ ≤ (1 / 2) * (Real.pi / |w.im|) :=\n          mul_le_mul_of_nonneg_left harctan (by norm_num)\n  -- the boundary term\n  have hboundary : ‖((w + ((0 : ℝ) : ℂ))⁻¹ - (w + ((n : ℝ) : ℂ))⁻¹) / 2‖ ≤ 1 / 2 := by\n    have h1 : ‖(w + ((0 : ℝ) : ℂ))⁻¹‖ ≤ 1 / 2 := by\n      have hw0 : (w : ℂ) + ((0 : ℝ) : ℂ) = w := by simp\n      rw [hw0, norm_inv, show (1 / 2 : ℝ) = (2 : ℝ)⁻¹ by norm_num]\n      exact (inv_le_inv₀ (by linarith [hwnorm] : (0 : ℝ) < ‖w‖)\n        (by norm_num : (0 : ℝ) < 2)).mpr hwnorm\n    have h2 : ‖(w + ((n : ℝ) : ℂ))⁻¹‖ ≤ 1 / 2 := by\n      have hvn : (w : ℂ) + ((n : ℝ) : ℂ) = v := by rw [hv]; simp\n      rw [hvn, norm_inv, show (1 / 2 : ℝ) = (2 : ℝ)⁻¹ by norm_num]\n      exact (inv_le_inv₀ (by linarith [hvnorm] : (0 : ℝ) < ‖v‖)\n        (by norm_num : (0 : ℝ) < 2)).mpr hvnorm\n    have h2c : ‖((2 : ℂ))‖ = 2 := by\n      rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by norm_num, Complex.norm_real, Real.norm_eq_abs,\n        abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)]\n    have hsum12 : ‖(w + ((0 : ℝ) : ℂ))⁻¹ - (w + ((n : ℝ) : ℂ))⁻¹‖ ≤ 1 :=\n      (norm_sub_le _ _).trans (by linarith [h1, h2])\n    calc ‖((w + ((0 : ℝ) : ℂ))⁻¹ - (w + ((n : ℝ) : ℂ))⁻¹) / 2‖\n        = ‖(w + ((0 : ℝ) : ℂ))⁻¹ - (w + ((n : ℝ) : ℂ))⁻¹‖ / 2 := by rw [norm_div, h2c]\n      _ ≤ 1 / 2 := by\n          rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)]\n          nlinarith [hsum12]\n  -- the middle piece: sum minus log-difference\n  have hmid : ‖(∑ j ∈ Finset.range n, (w + ((j : ℝ) : ℂ))⁻¹)\n        - (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        = ((w + ((0 : ℝ) : ℂ))⁻¹ - (w + ((n : ℝ) : ℂ))⁻¹) / 2\n          + ∫ x in (0 : ℝ)..(n : ℝ), deriv (fun y : ℝ => (w + (y : ℂ))⁻¹) x * (B1 x : ℂ) := by\n      rw [hsum, hint]\n      ring\n    rw [halg]\n    exact (norm_add_le _ _).trans (add_le_add hboundary hrem)\n  -- StirlingVert at v = w + 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    have hnorm12 : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by\n      rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,\n        Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 2)]\n    have hsq : (4 : ℝ) ≤ v.im ^ 2 := by\n      rw [hvim]\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    calc ‖Complex.digamma v - Complex.log v‖\n        = ‖(Complex.digamma v - Complex.log v + (1 / 2 : ℂ) / v) - (1 / 2 : ℂ) / v‖ := by\n          congr 1; ring\n      _ ≤ ‖Complex.digamma v - Complex.log v + (1 / 2 : ℂ) / v‖ + ‖(1 / 2 : ℂ) / v‖ :=\n          norm_sub_le _ _\n      _ ≤ 3 / v.im ^ 2 + 1 / 4 := by\n          apply add_le_add hst\n          rw [norm_div, hnorm12, div_le_iff₀ (by linarith [hvnorm] : (0 : ℝ) < ‖v‖)]\n          nlinarith [hvnorm]\n      _ ≤ 3 / 4 + 1 / 4 := by\n          apply add_le_add_right\n          rw [div_le_div_iff₀ (by linarith [hsq] : (0 : ℝ) < v.im ^ 2) (by norm_num)]\n          nlinarith [hsq]\n      _ ≤ 1 := by norm_num\n  -- final assembly\n  have hshift' : Complex.digamma v\n      = Complex.digamma w + ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ := by\n    rw [hv]\n    exact digamma_add_natCast him n\n  have hsumC : (∑ j ∈ Finset.range n, (w + ((j : ℝ) : ℂ))⁻¹)\n      = ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ :=\n    Finset.sum_congr rfl fun j _ => hcast j\n  calc ‖Complex.digamma w - Complex.log w‖\n      = ‖(Complex.digamma v - Complex.log v)\n          - ((∑ j ∈ Finset.range n, (w + ((j : ℝ) : ℂ))⁻¹)\n            - (Complex.log v - Complex.log w))‖ := by\n        congr 1\n        rw [hshift', ← hsumC]\n        ring\n    _ ≤ ‖Complex.digamma v - Complex.log v‖\n          + ‖(∑ j ∈ Finset.range n, (w + ((j : ℝ) : ℂ))⁻¹)\n            - (Complex.log v - Complex.log w)‖ :=\n        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          rw [div_le_div_left Real.pi_pos hc0 (by norm_num : (0 : ℝ) < 2)]\n          exact hw\n        nlinarith [hpc, Real.pi_lt_d2.le]\n\n/-! ## 5. The left-half loose R-bound (ii′-5d capstone) -/"},"extra_content":null}]