[{"type":"thinking","thinking":"- `StirlingVert.digamma_stirling hwre (by rw [hvim]; linarith [...])` — the usage pattern ✓.\n- `intervalIntegral.norm_integral_le_integral_norm (h : 0 ≤ a) : ‖∫ x in a..b, f x‖ ≤ ∫ x in a..b, ‖f x‖`? — from LiReflect:834 usage: `(intervalIntegral.norm_integral_le_integral_norm (Nat.cast_nonneg n)).trans ?_` — so norm_integral_le_integral_norm takes the a ≤ b nonneg proof and gives ‖∫ a..b f‖ ≤ ∫ a..b ‖f‖. Then I bound ∫₀¹ ‖δ·z⁻¹‖ ≤ (5/t)·1 by the constant: intervalIntegral.integral_of_le? or since ‖δ·z⁻¹‖ ≤ 5/t pointwise: `intervalIntegral.integral_mono_on`? hmm — ∫₀¹ (5/t) dx = 5/t: `intervalIntegral.integral_const`... the comparison: ∫₀¹ ‖f‖ ≤ ∫₀¹ (5/t) = 5/t: via intervalIntegral.integral_mono_on (h : ∀ x ∈ uIoc, ‖f x‖ ≤ 5/t)? `intervalIntegral.integral_mono_on (hab : a ≤ b) (hf : IntervalIntegrable...) (hg...) (h : ∀ x ∈ uIoc a b, f x ≤ g x) : ∫ a..b f ≤ ∫ a..b g` ✓ standard-ish.\n\nNow write piece 6. Full text:\n\n```lean\n/-! ## 7. Piece 6: the digamma difference -/\n\n/-- The log difference along the constant-imaginary segment: for\ns = σ + it with σ ∈ [−5/2, 3] and t ≥ 10, with w = s/2 and\nw₀ = 1 + (t/2)·I: ‖log (w + 2) − log w₀‖ ≤ 5/t. The segment FTC:\nevery point of [w₀, w+2] has re ≥ 3/4 (slit-plane) and im = t/2. -/\ntheorem log_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n    ‖Complex.log (s / 2 + 2) - Complex.log (1 + (t / 2) * Complex.I)‖ ≤ 5 / t := by\n  have ht0 : (0 : ℝ) < t := by linarith\n  set w : ℂ := s / 2 with hw\n  set w₀ : ℂ := 1 + (t / 2) * Complex.I with hw₀\n  have hwim : w.im = t / 2 := by rw [hw]; simp [him]\n  have hw₀im : w₀.im = t / 2 := by rw [hw₀]; simp\n  have hwre : w.re = s.re / 2 := by rw [hw]; simp\n  have hw₀re : w₀.re = 1 := by rw [hw₀]; simp\n  -- the difference δ = w + 2 − w₀ is real, = σ/2 + 1\n  set δ : ℂ := w + 2 - w₀ with hδ\n  have hδeq : δ = ((s.re / 2 + 1 : ℝ) : ℂ) := by\n    rw [hδ, hw₀]\n    rw [Complex.ext_iff]\n    constructor\n    · simp [hwre]  -- re: w.re + 2 − 1 = s.re/2 + 1\n      ...\n```\nHmm — δ.re: (w + 2 − w₀).re = w.re + 2 − 1 = s.re/2 + 1 ✓ (simp [Complex.sub_re, Complex.add_re, hwre] — the (2:ℂ).re = 2, (1:ℂ).re = 1, ((t/2)·I).re = 0). δ.im: = w.im + 0 − t/2 = 0 ✓. So δ = ((s.re/2 + 1 : ℝ):ℂ) via Complex.ext_iff: the RHS's re: ((x:ℝ):ℂ).re = x (ofReal_re) ✓ and im = 0 ✓. The simp calls need the re/im computation lemmas: `by simp [Complex.sub_re, Complex.add_re, hwre, hw₀re]`-ish. Let me write:\n```lean\n  have hδeq : δ = ((s.re / 2 + 1 : ℝ) : ℂ) := by\n    rw [Complex.ext_iff]\n    constructor\n    · rw [hδ]\n      simp [Complex.sub_re, Complex.add_re, hwre, hw₀re, Complex.ofReal_re]\n      ring? \n```\nHmm — after simp the goal is an arithmetic identity s.re/2 + 2 − 1 = s.re/2 + 1 — simp might leave (s.re/2 + 2 − 1) = (s.re/2+1) — close by linarith? or ring_nf. Let me: `· rw [hδ]; simp [Complex.sub_re, Complex.add_re, hwre, hw₀re]; ring_nf`... risky forms. Alternative robust: compute δ.re and δ.im separately as haves then ext:\n```lean\n  have hδre : δ.re = s.re / 2 + 1 := by\n    rw [hδ]\n    simp [Complex.sub_re, Complex.add_re, hwre, hw₀re]\n    ring_nf  -- hmm — after simp gives w.re + 2 − 1 = ... \n```\nThe simp should evaluate: (w + 2 − w₀).re = w.re + (2:ℂ).re − w₀.re = w.re + 2 − 1 — with rw [hwre] — hmm the simp [hwre] rewrites w.re → s.re/2 ✓. So δ.re = s.re/2 + 2 − 1 = s.re/2 + 1 — the final arithmetic: after simp the goal might be `s.re / 2 + 2 - 1 = s.re / 2 + 1` — linarith/ring closes. Ugh — the exact simp behavior is uncertain. Let me use a more explicit approach:\n\n```lean\n  have hδre : δ.re = s.re / 2 + 1 := by\n    rw [hδ, Complex.sub_re, Complex.add_re, hwre, hw₀re]\n    simp\n    ring_nf\n```\nHmm `(2:ℂ).re`: simp knows (by `Complex.ofNat_re`? or ofReal). Plain `simp` after the rw should evaluate (2:ℂ).re = 2, (1:ℂ).re... and then the goal `s.re / 2 + 2 - 1 = s.re / 2 + 1` — simp doesn't close arithmetic — hmm. The issue: rw [Complex.sub_re] etc transform the LHS of the equation (δ.re = ...): rw at the goal's LHS: (w + 2 − w₀).re → w.re + 2.re − w₀.re — wait sub_re: (a − b).re = a.re − b.re; add_re: (a+b).re = a.re + b.re. So (w+2−w₀).re = (w+2).re − w₀.re = (w.re + (2:ℂ).re) − w₀.re. rw [hwre]: w.re → s.re/2; hw₀re: w₀.re → 1. Goal: s.re/2 + (2:ℂ).re − 1 = s.re/2 + 1. simp evaluates (2:ℂ).re = 2 (via Complex.ofNat_re or ofReal_re — simp handles ✓). Then s.re/2 + 2 − 1 = s.re/2 + 1: `by norm_num`? or linarith. Let me write the whole thing with explicit terminal:\n```lean\n  have hδre : δ.re = s.re / 2 + 1 := by\n    rw [hδ, Complex.sub_re, Complex.add_re, hwre, hw₀re]\n    simp\n    ring_nf\n  have hδim : δ.im = 0 := by\n    rw [hδ, Complex.sub_im, Complex.add_im, hwim, hw₀im]\n    simp\n    ring_nf\n```\nThe `simp` after the rws evaluates the OfNat re/im; ring_nf closes the arithmetic. Hmm — but if simp CLOSES the goal (via deciding), the ring_nf errors \"no goals\". Risk both ways. Alternative bulletproof: \n```lean\n  have hδre : δ.re = s.re / 2 + 1 := by\n    rw [hδ, Complex.sub_re, Complex.add_re, hwre, hw₀re, Complex.ofNat_re]  -- hmm (2:ℂ).re lemma name\n    ring_nf\n```\nThe (2:ℂ).re: the term (2:ℂ) is OfNat; its .re: `Complex.ofNat_re`? or it might just compute via `Complex.re_ofNat`? — risky. The safest known pattern from the codebase: `simp` handles re/im of literals (used all over: `by simp [him]` for (s/2).im etc.). For the arithmetic close, use linarith instead of ring_nf after a NON-closing simp... but if simp closes it, linarith errors. \n\nYou know what — the cleanest: prove δre via a single `simp [...]` + `ring_nf` won't both be needed... Let me look at how the codebase handles e.g. (w + 2).re computations. From LiDigammaLeft:783's hvre — let me check that pattern. Actually from my piece-2 work in this file: `hre : ((2 + t * Complex.I) - ρ.1).re = 2 - ρ.1.re := by simp` — a bare `simp` closed a similar re-computation ✓. So `simp` handles (2:ℂ).re etc. Then the arithmetic: `simp` might fully close `s.re/2 + 2 − 1 = s.re/2 + 1`?? — no, simp doesn't do arithmetic. Plan: `by simp; ring_nf`?? — if simp closes: \"no goals\" error for ring_nf. Ugh.\n\nThe bulletproof pattern used in this codebase (session-033 gotcha): \"congrArg Complex.re + simp is the robust cast-bridge\". And for the arithmetic: `by simp; ring_nf` risks no-goals; `by simp` alone might leave the arithmetic. Let me use: `by simp only [...]; ring_nf`: simp only with specific lemmas NEVER closes the arithmetic goal (only the listed rewrites), leaving it for ring_nf:\n```lean\n  have hδre : δ.re = s.re / 2 + 1 := by\n    rw [hδ]\n    simp only [Complex.sub_re, Complex.add_re, hwre, hw₀re, Complex.ofNat_re, Complex.ofReal_re]\n    ring\n```\nHmm — the (2:ℂ).re — is it Complex.ofNat_re or does it need `(2:ℂ)` as OfNat: simp only [Complex.ofNat_re]? Is there such a lemma? There's `Complex.ofNat_re : (OfNat.ofNat n : ℂ).re = ...`? Hmm — maybe not. The (2:ℂ).re might need `(2:ℂ) = ((2:ℝ):ℂ)` cast + Complex.ofReal_re. Let me use:\n```lean\n  have hδre : δ.re = s.re / 2 + 1 := by\n    have h2re : (2 : ℂ).re = 2 := by simp\n    have h1re : (1 : ℂ).re = 1 := by simp  -- not needed if w₀re given\n    rw [hδ, Complex.sub_re, Complex.add_re, hwre, hw₀re, h2re]\n    ring\n```\n`have h2re : (2:ℂ).re = 2 := by simp` — simp should evaluate (2:ℂ).re (the OfNat re — simp knows via Complex.ofNat_re or norm_cast simp set ✓ plausible — my piece-2 used `by simp` for a similar re computation and it worked ✓). Then the goal: s.re/2 + 2 − 1 = s.re/2 + 1: ring ✓.\n\nThis is getting long. Given it's 2:25 AM and piece 6 is a ~250-line build, let me write it in full carefully and compile-iterate. Actually — let me reconsider the structure to minimize the re/im friction: instead of δ as a complex number with re/im computations, note the segment points: z(y) = w₀ + (y:ℂ)·δ — with δ real-cast: z(y) = w₀ + ((y·(s.re/2+1) : ℝ):ℂ): re = 1 + y·(s.re/2+1), im = t/2. \n\nLet me define things in terms of the real scalar: c := s.re/2 + 1 (real), z(y) := w₀ + ((y·c : ℝ):ℂ). Then:\n- z(y).re = 1 + y·c; z(y).im = t/2.\n- w + 2 = w₀ + ((c:ℝ):ℂ) (since w + 2 = (σ/2 + 2) + (t/2)I and w₀ + c = (1 + c) + (t/2)I = (σ/2 + 2) + (t/2)I ✓).\n- The FTC: g(y) := log(z(y)); HasDerivAt g (z(y)⁻¹ · c) y (chain rule: z(y) = w₀ + (y·c:ℂ) — d/dy = c (real cast): via hasDerivAt_log.comp with the affine map y ↦ w₀ + y·c — the 5d pattern: ((hasDerivAt_id' (x:ℂ)).const_add w) had the form w + y; mine: w₀ + (y:ℂ)·((c:ℝ):ℂ) = w₀ + ((y:ℂ)·c') with c' := ((c:ℝ):ℂ): the deriv is c': (hasDerivAt_id' (x:ℂ)).const_mul c' |>.const_add w₀? — hmm const_mul: HasDerivAt (fun z => z * c') (1 * c') hmm — (hasDerivAt_id' z₀).const_mul c' : HasDerivAt (fun z => z * c') (1 * c' = c') z₀ ✓ then .const_add w₀ : HasDerivAt (fun z => w₀ + z*c') (c') z₀ ✓ then comp with hasDerivAt_log: HasDerivAt (fun z => log (w₀ + z*c')) ((w₀+z₀*c')⁻¹ * c') z₀ ✓ then .comp_ofReal: HasDerivAt (fun y : ℝ => log (w₀ + (y:ℂ)*c')) (((w₀+(x:ℂ)*c')⁻¹ * c')) x ✓.\n- The integral: ∫₀¹ c'·z(y)⁻¹ = g 1 − g 0 = log(w₀ + c') − log w₀ = log(w+2) − log w₀ ✓ (w₀ + 1·c' = w₀ + c' = w+2 — via the h bridge w+2 = w₀ + c').\n- The norm: ‖c'·z(y)⁻¹‖ = |c|·‖z(y)‖⁻¹ ≤ (5/2)·(2/t) = 5/t: |c| = |σ/2 + 1| ≤ 5/2 (σ/2+1 ∈ [−1/4, 5/2] ⟹ |·| ≤ 5/2 ✓); ‖z(y)‖ ≥ |im z(y)| = t/2 ✓.\n- ∫₀¹ 5/t = 5/t: intervalIntegral.integral_const.\n\nThe slit-plane for z(y): re = 1 + yc ≥ 1 − |c|·... c ≥ −1/4: re ≥ 1 + 1·(−1/4)·... y ∈ [0,1]: y·c ≥ min(0, c) = c (if c < 0) ≥ −1/4: re ≥ 1 − 1/4 = 3/4 > 0 ✓. mem_slitPlane_iff: 0 < re ∨ im ≠ 0 — left: re > 0 ✓ (or right: im = t/2 ≠ 0 ✓ — use the RIGHT case, simpler: im z(y) = t/2 ≠ 0 ✓ always!).\n\nOK let me write the whole piece 6. Also note: `intervalIntegral.integral_eq_sub_of_hasDerivAt hanti hconti : ∫ x in a..b, f' x = f b − f a` — the argument order from 5d: hanti (the ∀ x ∈ uIcc, HasDerivAt f (f' x) x) and hconti (IntervalIntegrable f'). ✓\n\nAnd the norm bound: ‖∫₀¹ f'‖ ≤ ∫₀¹ ‖f'‖ via intervalIntegral.norm_integral_le_integral_norm (a ≤ b proof? from the 5d usage: `(intervalIntegral.norm_integral_le_integral_norm (Nat.cast_nonneg n)).trans` — takes (h : 0 ≤ a)-ish... the signature: norm_integral_le_integral_norm (hab : a ≤ b) : ‖∫ x in a..b, f x‖ ≤ ∫ x in a..b, ‖f x‖ — the 5d usage passed (Nat.cast_nonneg n) which is 0 ≤ (n:ℝ) — so the arg is a ≤ b with a = 0: 0 ≤ (n:ℝ) ✓ so signature (hab : a ≤ b). For me: (by norm_num : (0:ℝ) ≤ 1). Then ∫₀¹ ‖f'‖ ≤ ∫₀¹ (5/t) via intervalIntegral.integral_mono_on (h01 : 0 ≤ 1) (hf int) (hg int) (h : ∀ x ∈ uIoc 0 1, ‖f' x‖ ≤ 5/t)? signature check at build. Or simpler: bound via intervalIntegral.norm_integral_le_of_norm_le_const: `intervalIntegral.norm_integral_le_of_norm_le_const (hab : a ≤ b) (h : ∀ x ∈ uIoc a b, ‖f x‖ ≤ C) : ‖∫ x in a..b, f x‖ ≤ C * (b − a)`? Let me check the exact form.","signature":""},{"type":"text","text":"Checking the integral norm-bound lemma name, then writing piece 6 in full."},{"type":"tool_use","id":"Bash_217","name":"Bash","input":{"command":"M=D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib; grep -rn \"theorem norm_integral_le_of_norm_le_const\\|norm_integral_le_of_norm_le_const\" $M/MeasureTheory/Integral/IntervalIntegral*.lean $M/Analysis/**/*.lean 2>/dev/null | head -3; grep -rn \"norm_integral_le_of_norm_le_const\" D:/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/*.lean | head -3","description":"Find norm_integral_le_of_norm_le_const"},"extra_content":null}]