[{"type":"thinking","thinking":"Committed. Now ii′-1b(ii): the principal-part integral ∮ P = ResW1.\n\nSetup: P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i with A_i = F^{(n+1−i)}(1)/(n+1−i)!, F(w) = (wⁿ−(w−1)ⁿ)hLi(w). The claim: on any rectangle with 1 in its interior, RectangleIntegral' P z w = A_1 = ResW1 n.\n\nWait — actually for the assembly in (iii), I need P to be the FULL principal part of J at 1. The A_i's: A_i = (1/(n+1−i)!)·(d/dw)^{n+1−i}[(w−1)^{n+1}J(w)]|₁. And (w−1)^{n+1}J(w) = [wⁿ−(w−1)ⁿ]hLi(w) =: F(w) near 1 (punctured). So A_i = F^{(n+1−i)}(1)/(n+1−i)! and the residue A_1 = F^{(n)}(1)/n! = ResW1 n ✓ by definition of ResW1.\n\nDefine:\n```\ndef ppart (n : ℕ) (w : ℂ) : ℂ := ∑ i ∈ Finset.Icc 1 (n+1), (Acoeff n i) / (w - 1)^i\ndef Acoeff (n i : ℕ) : ℂ := iteratedDeriv (n + 1 - i) (fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w) 1 / (n + 1 - i)!\n```\nThen ∮ P = Acoeff n 1 = ResW1 n (Acoeff n 1 = iteratedDeriv n F 1 / n! = ResW1 ✓ definitionally).\n\nThe integral: pull to a small square around 1 (RectanglePullToNhdOfPole'') — actually for the FINAL assembly in (iii), the rectangle is the big D-036 one; the residue theorem machinery (residueTheorem_finset) handles the simple-pole parts; for P I need:\nRectangleIntegral' P z w = Acoeff n 1 whenever 1 is interior to the rectangle AND P's only pole (1) is inside.\n\nProof: P = Acoeff n 1/(w−1) + Σ_{i=2}^{n+1} Acoeff n i/(w−1)^i.\n- RectangleIntegral' (fun w => Acoeff n 1/(w−1)) z w = Acoeff n 1 via `ResidueTheoremInRectangle` (needs Rectangle z w ∈ 𝓝 1 = interior ✓).\n- Σ_{i≥2} terms integrate to 0: each term Acoeff n i/(w−1)^i = deriv of G_i(w) := −Acoeff n i/((i−1)(w−1)^{i−1}); G_i differentiable on RectangleBorder-neighborhood (1 off the border since 1 is interior ✓); the rectangle integral of a derivative over the closed boundary = 0 by FTC per side.\n\nFor the FTC per side: HIntegral (G') x₁ x₂ y = G(x₂+iy) − G(x₁+iy): `intervalIntegral.integral_deriv_eq_sub (h : ∀ x ∈ [[x₁,x₂]], HasDerivAt G (G' x) (x + y*I)) (hint : IntervalIntegrable ...)`. The sides parametrized: HIntegral f x₁ x₂ y = ∫ x in x₁..x₂, f (x + y*I). With f = G': = G(x₂+iy) − G(x₁+iy) if (x ↦ G(x+iy))' = G'(x+iy)·1 ✓ chain rule.\n\nVIntegral f x y₁ y₂ = ∫ y in y₁..y₂, f (x + y*I): with f = G': the derivative of (y ↦ G(x+iy)) is G'(x+iy)·I: so ∫ G'(x+iy) dy = (G(x+iy₂) − G(x+iy₁))/I. The RectangleIntegral = H bottom − H top + I·V right − I·V left: summing:\n[G(b) − G(a)] − [G(d) − G(c)] + I·[(G(d) − G(c))/I] − I·[(G(b) − G(a))/I] = 0 ✓ where a,b,c,d corners.\n\nThis is mechanical but needs the parametrization FTC done carefully. Is there a ready Mathlib lemma for \"rectangle integral of a derivative with primitive differentiable on the border\"? Hmm — the vendored `HolomorphicOn.vanishesOnRectangle` : HolomorphicOn f U + Rectangle ⊆ U ⟹ RectangleIntegral f z w = 0 — if G' were holomorphic on a set containing the rectangle... G_i is holomorphic off {1} — and the rectangle CONTAINS 1 — so can't apply directly. BUT — use the pull-to-square first: RectanglePullToNhdOfPole'' reduces to a small square around 1; on the small square, G_i is still singular at center (1) — vanishesOnRectangle doesn't apply either (1 is inside the small square). Hmm — so the primitive-FTC per-side argument is unavoidable... OR use the ML-style trick: A_i/(w−1)^i = (1/(1−i))·deriv(1/(w−1)^{i−1})·... and use `ResidueTheoremOnRectangleWithSimplePole`-style decomposition — no.\n\nAlternative cleaner route for the i ≥ 2 terms: use `RectangleIntegral'_eq_sumResiduesIn`-style... no.\n\nAlternative: use Cauchy's theorem for a function with a primitive: is there a Mathlib lemma `RectangleIntegral f z w = 0` if f has a primitive holomorphic on the rectangle MINUS a point not on the border? The primitive is differentiable ON the border — the standard proof via FTC per side. Let me just do the FTC computation directly — it's about 80–120 lines with the parametrization details.\n\nActually — wait. Simpler: the i ≥ 2 sum has the primitive G(w) = −Σ_{i=2}^{n+1} Acoeff n i/((i−1)(w−1)^{i−1}) which is differentiable on the whole BORDER (1 is interior, not on border). The rectangle integral of G' over the boundary: each side is a straight segment; FTC applies to G on each closed segment (G differentiable on a neighborhood of each point of the segment — since the border avoids 1 and G is meromorphic with pole only at 1, G is holomorphic in a nhd of every border point ✓). So per side: ∫_side G' = G(end) − G(start). Sum around: 0.\n\nIn Lean: HIntegral G' x₁ x₂ y = ∫_{x₁}^{x₂} G'(x + y·I) dx. The integrand: G'(x + yI) = d/dx[G(x+yI)] (chain: HasDerivAt (fun x => G (x + y*I)) (deriv G (x+yI) * 1) x ✓ (HasDerivAt.comp with (fun x => x + yI) derivative 1)). Then `intervalIntegral.integral_deriv_eq_sub (hderiv : ∀ x ∈ [[x₁,x₂]], HasDerivAt (fun x => G (x+yI)) (G' x) x) (hint : IntervalIntegrable (G' ∘ (·+yI)))`: gives ∫ = G(x₂+yI) − G(x₁+yI) ✓. The HasDerivAt for each x on the segment: G is differentiable at x+yI (≠ 1 — border point ≠ 1 ✓ since 1 interior not on border ✓). IntervalIntegrable: G' continuous on the segment ✓ (holomorphic there) ⟹ integrable.\n\nThis is doable. Let me estimate the full ii′-1b(ii): P def + Acoeff + the pull-to-square + the i≥2 vanishing + assemble ≈ 200–300 lines. And then (iii) needs R's holomorphic-at-1 + residueTheorem_finset application ≈ 300+ lines. Session 016 already delivered (i); (ii) now, (iii) likely session 017.\n\nHmm — wait, actually there's a subtlety with the pull-to-square approach: `RectanglePullToNhdOfPole''` gives: RectangleIntegral' f z w = RectangleIntegral' f (small square) for f holomorphic on Rectangle \\ {p} — but P has the pole AT 1 — P is NOT holomorphic on Rectangle \\ {1}?? P IS holomorphic off {1} (rational function with pole only at 1) ✓. So:\nRectangleIntegral' P z w = RectangleIntegral' P (square_c 1) for small c (eventually all c > 0 small).\nThen on the small square: P = A_1/(w−1) + [i≥2 sum]. The [i≥2 sum] integral on the small square: the square's border avoids 1 ✓ and the primitive G works on the border ✓ so FTC gives 0. And A_1/(w−1) via ResidueTheoremInRectangle ✓.\n\nActually — do I even need the pull-to-square? Directly on the big rectangle: P = A_1/(w−1) + G' where G' is the i≥2 sum (with primitive G holomorphic off {1}): RectangleIntegral' (A_1/(w−1) + G') = RectangleIntegral' (A_1/(w−1)) + RectangleIntegral' G' = A_1 + 0 — needs RectangleIntegral'.add (linearity — vendored `RectangleBorderIntegrable.add` + the integral of a sum = sum of integrals — should exist) and the two pieces. So NO pull-to-square needed:\n- RectangleIntegral' (fun w => A_1/(w−1)) z w = A_1 via ResidueTheoremInRectangle (needs 1 interior ✓).\n- RectangleIntegral' G' z w = 0 via the FTC-per-side argument (G differentiable on border ✓ — 1 interior so border avoids 1 ✓).\nBoth on the big rectangle directly. \n\nSo ii′-1b(ii) needs:\n1. `rectInt'_derivative_of_hasDerivOn_border` (generic): if G differentiable on a nhd of each border point, RectangleIntegral' (deriv G) z w = 0. Hmm — more precisely: RectangleIntegral (fun s => deriv G s) z w = 0 (the 2πi factor irrelevant). Via per-side FTC.\n2. Acoeff/ppart defs + P = A_1/(w−1) + G' decomposition.\n3. RectangleIntegral'.add / linearity.\n4. ResidueTheoremInRectangle application.\n5. Assemble: rectInt'_ppart : RectangleIntegral' (ppart n) z w = ResW1 n (when 1 interior).\n\nFor step 1, the per-side FTC — the RectangleIntegral unfolds into HIntegral/VIntegral sums. Let me check the vendored RectangleIntegral def and whether there's FTC for HIntegral/VIntegral already. Let me look at the def.","signature":""},{"type":"text","text":"Continuing with ii′-1b(ii): the principal-part integral. Checking the rectangle integral definition for the FTC-per-side argument."},{"type":"tool_use","id":"Bash_219","name":"Bash","input":{"command":"sed -n '30,80p' /d/Python/Quantum/zeta-23-lean/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean","description":"Read HIntegral/VIntegral/RectangleIntegral definitions"},"extra_content":null}]