← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (9124 chars)
`deriv_zpow (m : ℤ) (x) : deriv (fun x => x ^ m) x = m * x ^ (m - 1)` ✓ exists. For the composition (w−1)^m: use the comp or `deriv.comp`. Or directly: deriv (fun w => (w − 1) ^ m) w = deriv ((fun x => x ^ m) ∘ (fun w => w - 1)) w — via deriv.comp: deriv_zpow at (w−1) · deriv (w−1) = m·(w−1)^{m−1}·1 ✓.
Now let me write the full assembly section and append to LiPrincipal.lean.
```lean
/-! ## 3. The principal part and its integral -/
/-- The principal-part coefficients: A_i = F^{(n+1−i)}(1)/(n+1−i)!,
F(w) = (wⁿ−(w−1)ⁿ)·hLi(w). -/
def Acoeff (n i : ℕ) : ℂ :=
iteratedDeriv (n + 1 - i) (fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w) 1 / (n + 1 - i)!
lemma Acoeff_one (n : ℕ) : Acoeff n 1 = ResW1 n := by
rw [Acoeff, ResW1, show n + 1 - 1 = n from by omega]
/-- The principal part of J at w = 1: P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i. -/
def ppart (n : ℕ) (w : ℂ) : ℂ :=
∑ i ∈ Finset.Icc 1 (n + 1), Acoeff n i / (w - 1) ^ i
/-- The tail primitive G(w) = −Σ_{i=2}^{n+1} (A_i/(i−1))·(w−1)^{−(i−1)}. -/
def Gprim (n : ℕ) (w : ℂ) : ℂ :=
∑ i ∈ Finset.Icc 2 (n + 1), -(Acoeff n i / ((i : ℂ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1))
lemma deriv_Gprim {n : ℕ} {w : ℂ} (hw : w ≠ 1) :
deriv (Gprim n) w = ∑ i ∈ Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i := by
rw [Gprim, deriv_sum]
apply Finset.sum_congr rfl
intro i hi
rw [Finset.mem_Icc] at hi
have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw
-- term: f_i(w) = -(A_i/(i−1))·(w−1)^{−(i−1)}
have hterm : deriv (fun w => -(Acoeff n i / ((i : ℂ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1))) w
= Acoeff n i / (w - 1) ^ i := by
have h1 : HasDerivAt (fun w => (w - 1) ^ (-((i : ℤ) - 1)))
(((-((i : ℤ) - 1)) : ℂ) * (w - 1) ^ (-((i : ℤ) - 1) - 1)) w := by
have h := hasDerivAt_zpow (-((i : ℤ) - 1)) (w - 1) (Or.inl hw1)
-- compose with (w − 1): chain rule gives · 1
have hcomp := h.comp w (hasDerivAt_id w |>.sub_const 1)
-- hmm need the right comp form
simpa using hcomp
...
```
Hmm — deriv_zpow is for (fun x => x^m) at x; composing with (w−1): `HasDerivAt.comp` with h₂ = (·^m) over ℂ, h = (·−1): HasDerivAt ((·^m) ∘ (·−1)) (m·(w−1)^{m−1} * 1) w. Via `HasDerivAt.comp`:
```
have h1 : HasDerivAt (fun w => (w - 1) ^ (-((i : ℤ) - 1)))
((-((i : ℤ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1) - 1) * 1) w := by
have h2 : HasDerivAt (fun x : ℂ => x ^ (-((i : ℤ) - 1)))
((-((i : ℤ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1) - 1)) (w - 1) :=
hasDerivAt_zpow _ _ (Or.inl hw1)
have h3 : HasDerivAt (fun w : ℂ => w - 1) 1 w := by
simpa using (hasDerivAt_id w).sub_const 1
exact h2.comp w h3
```
Wait — hasDerivAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) : HasDerivAt (fun x => x ^ m) (m * x ^ (m - 1)) x ✓ — the derivative value m * x^(m−1) ✓. comp: h2.comp w h3 : HasDerivAt ((fun x => x^m) ∘ (fun w => w−1)) ((m·(w−1)^{m−1}) * 1) w ✓ — the function composition: (fun x => x^m) ∘ (fun w => w−1) = fun w => (w−1)^m ✓ defeq.
Then the full term: deriv (−(A_i/(i−1))·(w−1)^{−(i−1)}) = −(A_i/(i−1))·[−(i−1)]·(w−1)^{−(i−1)−1}·1:
with m = −(i−1) = 1−i: derivative = (1−i)·(w−1)^{(1−i)−1} = (1−i)·(w−1)^{−i}.
So term derivative = −(A_i/(i−1))·(1−i)·(w−1)^{−i} = A_i·(i−1)/(i−1)·(w−1)^{−i} = A_i·(w−1)^{−i} — and I want A_i/(w−1)^i — zpow vs pow: (w−1)^{−i} (zpow, i : ℤ) = (w−1)^{−i}... and 1/(w−1)^i = (w−1)^{−(i:ℤ)} ✓ zpow_neg... For i ≥ 2: −i ≤ −2 < 0: (w−1)^{(−(i:ℤ))} = 1/(w−1)^i ✓ via `zpow_neg` and `zpow_natCast`.
The constant multiplication: deriv (c·f) = c·deriv f ✓ `deriv_const_mul` (needs f differentiable: have it via h1.hasDerivAt.differentiableAt).
Also the negation: deriv (−c·f)... my term is `-(Acoeff n i / ((i:ℂ) − 1)) * (w−1)^m` — treat as `(-(A_i/(i−1))) * (w−1)^m`: deriv = (-(A_i/(i−1))) * (m·(w−1)^{m−1}·1) ✓ deriv_const_mul.
Then sum: deriv_sum — `deriv_sum (h : ∀ i ∈ s, DifferentiableAt ℂ (f i) x) : deriv (∑ i ∈ s, f i) x = ∑ i ∈ s, deriv (f i) x` ✓ exists.
The final equality to A_i/(w−1)^i: algebra: −(A_i/(i−1))·(1−i)·(w−1)^{−i} = A_i·(w−1)^{−i}·((i−1)/(i−1)) — with (i−1 : ℂ) ≠ 0 (i ≥ 2 ⟹ i−1 ≥ 1 ✓): field_simp + ring, then (w−1)^{−i} (zpow) = 1/(w−1)^i: `zpow_neg, zpow_natCast`: (w−1)^(−(i:ℤ)) = ((w−1)^(i:ℤ))⁻¹ = ((w−1)^i)⁻¹ ✓. So A_i·(w−1)^{−i} = A_i/((w−1)^i) ✓.
Hmm wait — the zpow exponent arithmetic: m = −((i:ℤ) − 1) = 1 − i; m − 1 = −i ✓.
Then the telescoping at the goal: A_i/(w−1)^i ✓ matches the sum.
For ppart_eq:
```
lemma ppart_eq_deriv_add {n : ℕ} {w : ℂ} (hw : w ≠ 1) :
ppart n w = Acoeff n 1 / (w - 1) + deriv (Gprim n) w := by
rw [ppart, deriv_Gprim hw]
have : Finset.Icc 1 (n + 1) = {1} ∪ Finset.Icc 2 (n + 1) := by
ext j
simp [Finset.mem_Icc]
omega
rw [this, Finset.sum_union (by simp)]
simp [pow_one]
```
Finset.sum_union needs disjoint {1} ∩ Icc 2 (n+1) = ∅ ✓ simp.
Then integrabilities + holomorphicity:
- (fun s => Acoeff n 1 / (s - 1)): HolomorphicOn on Rectangle \ {1} ✓ (rational, pole only at 1).
- deriv (Gprim n): holomorphic on Rectangle \ {1}: Gprim holomorphic there (finite sum of zpow terms ✓) ⟹ deriv holomorphic (DifferentiableOn.deriv on open set? — deriv of a holomorphic-on-open function: `DifferentiableOn.deriv (hd : DifferentiableOn ℂ f s) (ho : IsOpen s) : DifferentiableOn ℂ (deriv f) s`? I believe `DifferentiableOn.deriv` exists ✓. Rectangle \ {1} open ✓ (Rectangle closed — Rectangle \ {1} open? Rectangle is CLOSED (it's a product of closed intervals) — minus a point is NOT open! Hmm — use a larger open set: Gprim is holomorphic on ℂ \ {1} (open ✓) — DifferentiableOn.deriv on ℂ \ {1} ✓ then restrict to Rectangle \ {1} via mono. Similarly for A/(s−1).
- rectInt_deriv_eq_zero for Gprim: hG : DifferentiableAt G at every border point: border avoids 1 (1 interior ⟹ not on border via not_mem_rectangleBorder_of_rectangle_mem_nhds ✓): Gprim differentiable at w ≠ 1 ✓ (sum of differentiable terms). hGc : ContinuousAt (deriv G) at border points: deriv (Gprim n) = the tail sum (deriv_Gprim) — continuous off {1} ✓ (sum of continuous rational terms, all fine off 1).
The final theorem:
```
theorem rectInt'_ppart {n : ℕ} {z w : ℂ}
(hre : z.re ≤ w.re) (him : z.im ≤ w.im) (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ)) :
RectangleIntegral' (ppart n) z w = ResW1 n := by
have h1not : (1 : ℂ) ∉ RectangleBorder z w := not_mem_rectangleBorder_of_rectangle_mem_nhds h1
have hdecomp : Set.EqOn (ppart n) (fun w => Acoeff n 1 / (w - 1) + deriv (Gprim n) w)
(RectangleBorder z w) := by
intro s hs
have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)
exact ppart_eq_deriv_add hs1
rw [RectangleIntegral'_congr hdecomp]
have hAint : RectangleBorderIntegrable (fun w => Acoeff n 1 / (w - 1)) z w := by
apply HolomorphicOn.rectangleBorderIntegrable' _ h1
intro s hs
have hs1 : s ≠ 1 := hs.2
exact (differentiableAt_const.div (differentiableAt_id.sub (differentiableAt_const 1)) (sub_ne_zero.mpr hs1)).differentiableWithinAt
have hGint : RectangleBorderIntegrable (deriv (Gprim n)) z w := by
apply HolomorphicOn.rectangleBorderIntegrable' _ h1
intro s hs
have hs1 : s ≠ 1 := hs.2
-- deriv of Gprim is differentiable off 1 (Gprim holomorphic on ℂ \ {1})
...
rw [RectangleIntegral'_add _ _ hAint hGint]
rw [ResidueTheoremInRectangle hre him h1]
have hzero : RectangleIntegral (deriv (Gprim n)) z w = 0 := by
apply rectInt_deriv_eq_zero
· intro s hs
have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)
-- Gprim differentiable at s ≠ 1
exact Gprim_differentiableAt hs1
· intro s hs
have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)
-- deriv Gprim continuous at s ≠ 1
rw [deriv_Gprim hs1]
-- the tail sum is continuous off 1
exact tail_continuousAt hs1
rw [RectangleIntegral', hzero]
rw [Acoeff_one]
simp
```
Wait — RectangleIntegral' f z w = (1/(2πI)) • RectangleIntegral f z w — the additivity gave RectangleIntegral' (A/(w−1) + deriv G) = RectangleIntegral' (A/(w−1)) + RectangleIntegral' (deriv G) = Acoeff + (1/(2πI))•0 = Acoeff ✓.
Let me also handle ResidueTheoremInRectangle's exact statement: `theorem ResidueTheoremInRectangle (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : Rectangle z w ∈ 𝓝 p) : RectangleIntegral' (fun s => c / (s - p)) z w = c` ✓ with c := Acoeff n 1, p := 1 ✓.
For Gprim differentiability + deriv continuity, define helper lemmas:
```
lemma Gprim_differentiableAt {n : ℕ} {w : ℂ} (hw : w ≠ 1) :
DifferentiableAt ℂ (Gprim n) w := by
apply DifferentiableAt.sum
intro i hi
apply DifferentiableAt.mul (differentiableAt_const _)
-- (w−1)^m differentiable at w ≠ 1 (zpow with negative exponent, base ≠ 0)
exact (differentiableAt_zpow ... ) hmm — `differentiableAt_zpow (m : ℤ) (x) (h : x ≠ 0 ∨ 0 ≤ m)`? from the grep: hasDerivAt_zpow m x H with H : x ≠ 0 ∨ 0 ≤ m ⟹ differentiableAt. For (w−1): compose.
```
And deriv_Gprim continuity: deriv (Gprim n) w = tail-sum (by deriv_Gprim) — the tail sum of rational terms, each continuous off {1} ✓ (sum of continuous functions, needs w ≠ 1 for denominators).
OK — let me write the whole section 3 and append. This is another ~150 lines. Let me write it in one go and compile.
All pieces confirmed. Writing the assembly section (Acoeff/ppart/Gprim + the integral theorem).
tool: Bash
input
{
"command": "cat >> /d/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiPrincipal.lean << 'EOF'\n\n/-! ## 3. The principal part and its integral -/\n\n/-- The principal-part coefficients: A_i = F^{(n+1\u2212i)}(1)/(n+1\u2212i)!,\nF(w) = (w\u207f\u2212(w\u22121)\u207f)\u00b7hLi(w). -/\ndef Acoeff (n i : \u2115) : \u2102 :=\n iteratedDeriv (n + 1 - i) (fun w : \u2102 => (w ^ n - (w - 1) ^ n) * hLi w) 1 / (n + 1 - i)!\n\nlemma Acoeff_one (n : \u2115) : Acoeff n 1 = ResW1 n := by\n rw [Acoeff, ResW1, show n + 1 - 1 = n from by omega]\n\n/-- The principal part of J at w = 1: P(w) = \u03a3_{i=1}^{n+1} A_i/(w\u22121)^i. -/\ndef ppart (n : \u2115) (w : \u2102) : \u2102 :=\n \u2211 i \u2208 Finset.Icc 1 (n + 1), Acoeff n i / (w - 1) ^ i\n\n/-- The tail primitive G(w) = \u2212\u03a3_{i=2}^{n+1} (A_i/(i\u22121))\u00b7(w\u22121)^{\u2212(i\u22121)}. -/\ndef Gprim (n : \u2115) (w : \u2102) : \u2102 :=\n \u2211 i \u2208 Finset.Icc 2 (n + 1), -(Acoeff n i / ((i : \u2102) - 1)) * (w - 1) ^ (-((i : \u2124) - 1))\n\nlemma Gprim_differentiableAt {n : \u2115} {w : \u2102} (hw : w \u2260 1) :\n DifferentiableAt \u2102 (Gprim n) w := by\n rw [Gprim]\n apply DifferentiableAt.sum\n intro i hi\n apply DifferentiableAt.mul (differentiableAt_const _)\n have hw1 : w - 1 \u2260 0 := sub_ne_zero.mpr hw\n exact (hasDerivAt_zpow _ (w - 1) (Or.inl hw1)).differentiableAt.comp w\n ((hasDerivAt_id w).sub_const 1)\n\nlemma deriv_Gprim {n : \u2115} {w : \u2102} (hw : w \u2260 1) :\n deriv (Gprim n) w = \u2211 i \u2208 Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i := by\n rw [Gprim, deriv_sum (fun i hi => ?_)]\n \u00b7 apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_Icc] at hi\n have hw1 : w - 1 \u2260 0 := sub_ne_zero.mpr hw\n have hi1 : ((i : \u2102) - 1) \u2260 0 := by\n have : 1 < (i : \u211d) := by exact_mod_cast (by omega : 1 < i)\n intro heq\n rw [sub_eq_zero] at heq\n have : (i : \u211d) = 1 := by exact_mod_cast heq\n linarith\n have hd : deriv (fun w => (w - 1) ^ (-((i : \u2124) - 1))) w\n = ((-((i : \u2124) - 1)) : \u2102) * (w - 1) ^ (-((i : \u2124) - 1) - 1) := by\n have h2 : HasDerivAt (fun x : \u2102 => x ^ (-((i : \u2124) - 1)))\n ((-((i : \u2124) - 1)) * (w - 1) ^ (-((i : \u2124) - 1) - 1)) (w - 1) :=\n hasDerivAt_zpow _ _ (Or.inl hw1)\n have h3 : HasDerivAt (fun w : \u2102 => w - 1) 1 w := by\n simpa using (hasDerivAt_id w).sub_const 1\n have hcomp := h2.comp w h3\n rw [Function.comp_apply, mul_one] at hcomp\n exact hcomp.deriv\n rw [deriv_const_mul _ (by\n have hw1' : w - 1 \u2260 0 := sub_ne_zero.mpr hw\n exact (hasDerivAt_zpow _ (w - 1) (Or.inl hw1')).differentiableAt.comp w\n ((hasDerivAt_id w).sub_const 1)), hd]\n have hm : (-((i : \u2124) - 1) - 1 : \u2124) = -(i : \u2124) := by omega\n rw [hm]\n have hzi : ((-(i : \u2124)) : \u2102) = -((i : \u2102)) := by simp\n rw [hzi]\n field_simp [hw1, hi1]\n rw [zpow_neg, zpow_natCast]\n field_simp [hw1]\n ring\n \u00b7 intro i hi\n apply DifferentiableAt.mul (differentiableAt_const _)\n have hw1 : w - 1 \u2260 0 := sub_ne_zero.mpr hw\n exact (hasDerivAt_zpow _ (w - 1) (Or.inl hw1)).differentiableAt.comp w\n ((hasDerivAt_id w).sub_const 1)\n\nlemma tail_continuousAt {n : \u2115} {w : \u2102} (hw : w \u2260 1) :\n ContinuousAt (\u2211 i \u2208 Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i) w := by\n apply ContinuousAt.sum\n intro i hi\n rw [Finset.mem_Icc] at hi\n have hw1 : w - 1 \u2260 0 := sub_ne_zero.mpr hw\n apply ContinuousAt.div (continuousAt_const)\n exact (continuousAt_id.sub continuousAt_const).pow hw1.ne' |> fun h => h.continuousAt\n \u00b7 exact pow_ne_zero _ hw1\n\nlemma ppart_eq_deriv_add {n : \u2115} {w : \u2102} (hw : w \u2260 1) :\n ppart n w = Acoeff n 1 / (w - 1) + deriv (Gprim n) w := by\n rw [ppart, deriv_Gprim hw]\n have hsplit : Finset.Icc 1 (n + 1) = {1} \u222a Finset.Icc 2 (n + 1) := by\n ext j\n simp [Finset.mem_Icc]\n omega\n rw [hsplit, Finset.sum_union (by simp)]\n simp [pow_one]\n\n/-- The principal-part integral: on any rectangle with 1 in its interior,\nRectangleIntegral' (ppart n) z w = ResW1 n. -/\ntheorem rectInt'_ppart {n : \u2115} {z w : \u2102}\n (hre : z.re \u2264 w.re) (him : z.im \u2264 w.im) (h1 : Rectangle z w \u2208 \ud835\udcdd (1 : \u2102)) :\n RectangleIntegral' (ppart n) z w = ResW1 n := by\n have h1not : (1 : \u2102) \u2209 RectangleBorder z w := not_mem_rectangleBorder_of_rectangle_mem_nhds h1\n have hdecomp : Set.EqOn (ppart n) (fun w => Acoeff n 1 / (w - 1) + deriv (Gprim n) w)\n (RectangleBorder z w) := by\n intro s hs\n have hs1 : s \u2260 1 := fun heq => h1not (heq \u25b8 hs)\n exact ppart_eq_deriv_add hs1\n rw [RectangleIntegral'_congr hdecomp]\n have hAint : RectangleBorderIntegrable (fun w => Acoeff n 1 / (w - 1)) z w := by\n apply HolomorphicOn.rectangleBorderIntegrable' _ h1\n intro s hs\n have hs1 : s \u2260 1 := hs.2\n exact (differentiableAt_const.div ((differentiableAt_id.sub (differentiableAt_const 1)))\n (sub_ne_zero.mpr hs1)).differentiableWithinAt\n have hGint : RectangleBorderIntegrable (deriv (Gprim n)) z w := by\n apply HolomorphicOn.rectangleBorderIntegrable' _ h1\n intro s hs\n have hs1 : s \u2260 1 := hs.2\n rw [deriv_Gprim hs1]\n exact (tail_continuousAt hs1).differentiableAt.continuousWithinAt\n rw [RectangleIntegral'_add _ _ hAint hGint]\n rw [ResidueTheoremInRectangle hre him h1]\n have hzero : RectangleIntegral (deriv (Gprim n)) z w = 0 := by\n apply rectInt_deriv_eq_zero\n \u00b7 intro s hs\n have hs1 : s \u2260 1 := fun heq => h1not (heq \u25b8 hs)\n exact Gprim_differentiableAt hs1\n \u00b7 intro s hs\n have hs1 : s \u2260 1 := fun heq => h1not (heq \u25b8 hs)\n rw [deriv_Gprim hs1]\n exact tail_continuousAt hs1\n rw [RectangleIntegral', hzero]\n rw [Acoeff_one]\n simp\nEOF\ncd /d/Python/Quantum/research/lean/NguyenRH1 && export PATH=\"$HOME/.elan/bin:$PATH\" && lake env lean NguyenRH1/LiPrincipal.lean 2>&1 | head -40",
"description": "Append assembly section and compile",
"timeout": 420000
}
raw content_json (database row)
[{"type":"thinking","thinking":"`deriv_zpow (m : ℤ) (x) : deriv (fun x => x ^ m) x = m * x ^ (m - 1)` ✓ exists. For the composition (w−1)^m: use the comp or `deriv.comp`. Or directly: deriv (fun w => (w − 1) ^ m) w = deriv ((fun x => x ^ m) ∘ (fun w => w - 1)) w — via deriv.comp: deriv_zpow at (w−1) · deriv (w−1) = m·(w−1)^{m−1}·1 ✓.\n\nNow let me write the full assembly section and append to LiPrincipal.lean.\n\n```lean\n/-! ## 3. The principal part and its integral -/\n\n/-- The principal-part coefficients: A_i = F^{(n+1−i)}(1)/(n+1−i)!,\nF(w) = (wⁿ−(w−1)ⁿ)·hLi(w). -/\ndef Acoeff (n i : ℕ) : ℂ :=\n iteratedDeriv (n + 1 - i) (fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w) 1 / (n + 1 - i)!\n\nlemma Acoeff_one (n : ℕ) : Acoeff n 1 = ResW1 n := by\n rw [Acoeff, ResW1, show n + 1 - 1 = n from by omega]\n\n/-- The principal part of J at w = 1: P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i. -/\ndef ppart (n : ℕ) (w : ℂ) : ℂ :=\n ∑ i ∈ Finset.Icc 1 (n + 1), Acoeff n i / (w - 1) ^ i\n\n/-- The tail primitive G(w) = −Σ_{i=2}^{n+1} (A_i/(i−1))·(w−1)^{−(i−1)}. -/\ndef Gprim (n : ℕ) (w : ℂ) : ℂ :=\n ∑ i ∈ Finset.Icc 2 (n + 1), -(Acoeff n i / ((i : ℂ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1))\n\nlemma deriv_Gprim {n : ℕ} {w : ℂ} (hw : w ≠ 1) :\n deriv (Gprim n) w = ∑ i ∈ Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i := by\n rw [Gprim, deriv_sum]\n apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_Icc] at hi\n have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw\n -- term: f_i(w) = -(A_i/(i−1))·(w−1)^{−(i−1)}\n have hterm : deriv (fun w => -(Acoeff n i / ((i : ℂ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1))) w\n = Acoeff n i / (w - 1) ^ i := by\n have h1 : HasDerivAt (fun w => (w - 1) ^ (-((i : ℤ) - 1)))\n (((-((i : ℤ) - 1)) : ℂ) * (w - 1) ^ (-((i : ℤ) - 1) - 1)) w := by\n have h := hasDerivAt_zpow (-((i : ℤ) - 1)) (w - 1) (Or.inl hw1)\n -- compose with (w − 1): chain rule gives · 1\n have hcomp := h.comp w (hasDerivAt_id w |>.sub_const 1)\n -- hmm need the right comp form\n simpa using hcomp\n ...\n```\n\nHmm — deriv_zpow is for (fun x => x^m) at x; composing with (w−1): `HasDerivAt.comp` with h₂ = (·^m) over ℂ, h = (·−1): HasDerivAt ((·^m) ∘ (·−1)) (m·(w−1)^{m−1} * 1) w. Via `HasDerivAt.comp`:\n```\n have h1 : HasDerivAt (fun w => (w - 1) ^ (-((i : ℤ) - 1)))\n ((-((i : ℤ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1) - 1) * 1) w := by\n have h2 : HasDerivAt (fun x : ℂ => x ^ (-((i : ℤ) - 1)))\n ((-((i : ℤ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1) - 1)) (w - 1) :=\n hasDerivAt_zpow _ _ (Or.inl hw1)\n have h3 : HasDerivAt (fun w : ℂ => w - 1) 1 w := by\n simpa using (hasDerivAt_id w).sub_const 1\n exact h2.comp w h3\n```\nWait — hasDerivAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) : HasDerivAt (fun x => x ^ m) (m * x ^ (m - 1)) x ✓ — the derivative value m * x^(m−1) ✓. comp: h2.comp w h3 : HasDerivAt ((fun x => x^m) ∘ (fun w => w−1)) ((m·(w−1)^{m−1}) * 1) w ✓ — the function composition: (fun x => x^m) ∘ (fun w => w−1) = fun w => (w−1)^m ✓ defeq.\n\nThen the full term: deriv (−(A_i/(i−1))·(w−1)^{−(i−1)}) = −(A_i/(i−1))·[−(i−1)]·(w−1)^{−(i−1)−1}·1:\nwith m = −(i−1) = 1−i: derivative = (1−i)·(w−1)^{(1−i)−1} = (1−i)·(w−1)^{−i}.\nSo term derivative = −(A_i/(i−1))·(1−i)·(w−1)^{−i} = A_i·(i−1)/(i−1)·(w−1)^{−i} = A_i·(w−1)^{−i} — and I want A_i/(w−1)^i — zpow vs pow: (w−1)^{−i} (zpow, i : ℤ) = (w−1)^{−i}... and 1/(w−1)^i = (w−1)^{−(i:ℤ)} ✓ zpow_neg... For i ≥ 2: −i ≤ −2 < 0: (w−1)^{(−(i:ℤ))} = 1/(w−1)^i ✓ via `zpow_neg` and `zpow_natCast`.\n\nThe constant multiplication: deriv (c·f) = c·deriv f ✓ `deriv_const_mul` (needs f differentiable: have it via h1.hasDerivAt.differentiableAt).\n\nAlso the negation: deriv (−c·f)... my term is `-(Acoeff n i / ((i:ℂ) − 1)) * (w−1)^m` — treat as `(-(A_i/(i−1))) * (w−1)^m`: deriv = (-(A_i/(i−1))) * (m·(w−1)^{m−1}·1) ✓ deriv_const_mul.\n\nThen sum: deriv_sum — `deriv_sum (h : ∀ i ∈ s, DifferentiableAt ℂ (f i) x) : deriv (∑ i ∈ s, f i) x = ∑ i ∈ s, deriv (f i) x` ✓ exists.\n\nThe final equality to A_i/(w−1)^i: algebra: −(A_i/(i−1))·(1−i)·(w−1)^{−i} = A_i·(w−1)^{−i}·((i−1)/(i−1)) — with (i−1 : ℂ) ≠ 0 (i ≥ 2 ⟹ i−1 ≥ 1 ✓): field_simp + ring, then (w−1)^{−i} (zpow) = 1/(w−1)^i: `zpow_neg, zpow_natCast`: (w−1)^(−(i:ℤ)) = ((w−1)^(i:ℤ))⁻¹ = ((w−1)^i)⁻¹ ✓. So A_i·(w−1)^{−i} = A_i/((w−1)^i) ✓.\n\nHmm wait — the zpow exponent arithmetic: m = −((i:ℤ) − 1) = 1 − i; m − 1 = −i ✓.\n\nThen the telescoping at the goal: A_i/(w−1)^i ✓ matches the sum.\n\nFor ppart_eq:\n```\nlemma ppart_eq_deriv_add {n : ℕ} {w : ℂ} (hw : w ≠ 1) :\n ppart n w = Acoeff n 1 / (w - 1) + deriv (Gprim n) w := by\n rw [ppart, deriv_Gprim hw]\n have : Finset.Icc 1 (n + 1) = {1} ∪ Finset.Icc 2 (n + 1) := by\n ext j\n simp [Finset.mem_Icc]\n omega\n rw [this, Finset.sum_union (by simp)]\n simp [pow_one]\n```\nFinset.sum_union needs disjoint {1} ∩ Icc 2 (n+1) = ∅ ✓ simp.\n\nThen integrabilities + holomorphicity:\n- (fun s => Acoeff n 1 / (s - 1)): HolomorphicOn on Rectangle \\ {1} ✓ (rational, pole only at 1).\n- deriv (Gprim n): holomorphic on Rectangle \\ {1}: Gprim holomorphic there (finite sum of zpow terms ✓) ⟹ deriv holomorphic (DifferentiableOn.deriv on open set? — deriv of a holomorphic-on-open function: `DifferentiableOn.deriv (hd : DifferentiableOn ℂ f s) (ho : IsOpen s) : DifferentiableOn ℂ (deriv f) s`? I believe `DifferentiableOn.deriv` exists ✓. Rectangle \\ {1} open ✓ (Rectangle closed — Rectangle \\ {1} open? Rectangle is CLOSED (it's a product of closed intervals) — minus a point is NOT open! Hmm — use a larger open set: Gprim is holomorphic on ℂ \\ {1} (open ✓) — DifferentiableOn.deriv on ℂ \\ {1} ✓ then restrict to Rectangle \\ {1} via mono. Similarly for A/(s−1).\n- rectInt_deriv_eq_zero for Gprim: hG : DifferentiableAt G at every border point: border avoids 1 (1 interior ⟹ not on border via not_mem_rectangleBorder_of_rectangle_mem_nhds ✓): Gprim differentiable at w ≠ 1 ✓ (sum of differentiable terms). hGc : ContinuousAt (deriv G) at border points: deriv (Gprim n) = the tail sum (deriv_Gprim) — continuous off {1} ✓ (sum of continuous rational terms, all fine off 1).\n\nThe final theorem:\n```\ntheorem rectInt'_ppart {n : ℕ} {z w : ℂ}\n (hre : z.re ≤ w.re) (him : z.im ≤ w.im) (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ)) :\n RectangleIntegral' (ppart n) z w = ResW1 n := by\n have h1not : (1 : ℂ) ∉ RectangleBorder z w := not_mem_rectangleBorder_of_rectangle_mem_nhds h1\n have hdecomp : Set.EqOn (ppart n) (fun w => Acoeff n 1 / (w - 1) + deriv (Gprim n) w)\n (RectangleBorder z w) := by\n intro s hs\n have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)\n exact ppart_eq_deriv_add hs1\n rw [RectangleIntegral'_congr hdecomp]\n have hAint : RectangleBorderIntegrable (fun w => Acoeff n 1 / (w - 1)) z w := by\n apply HolomorphicOn.rectangleBorderIntegrable' _ h1\n intro s hs\n have hs1 : s ≠ 1 := hs.2\n exact (differentiableAt_const.div (differentiableAt_id.sub (differentiableAt_const 1)) (sub_ne_zero.mpr hs1)).differentiableWithinAt\n have hGint : RectangleBorderIntegrable (deriv (Gprim n)) z w := by\n apply HolomorphicOn.rectangleBorderIntegrable' _ h1\n intro s hs\n have hs1 : s ≠ 1 := hs.2\n -- deriv of Gprim is differentiable off 1 (Gprim holomorphic on ℂ \\ {1})\n ...\n rw [RectangleIntegral'_add _ _ hAint hGint]\n rw [ResidueTheoremInRectangle hre him h1]\n have hzero : RectangleIntegral (deriv (Gprim n)) z w = 0 := by\n apply rectInt_deriv_eq_zero\n · intro s hs\n have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)\n -- Gprim differentiable at s ≠ 1\n exact Gprim_differentiableAt hs1\n · intro s hs\n have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)\n -- deriv Gprim continuous at s ≠ 1\n rw [deriv_Gprim hs1]\n -- the tail sum is continuous off 1\n exact tail_continuousAt hs1\n rw [RectangleIntegral', hzero]\n rw [Acoeff_one]\n simp\n```\nWait — RectangleIntegral' f z w = (1/(2πI)) • RectangleIntegral f z w — the additivity gave RectangleIntegral' (A/(w−1) + deriv G) = RectangleIntegral' (A/(w−1)) + RectangleIntegral' (deriv G) = Acoeff + (1/(2πI))•0 = Acoeff ✓.\n\nLet me also handle ResidueTheoremInRectangle's exact statement: `theorem ResidueTheoremInRectangle (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : Rectangle z w ∈ 𝓝 p) : RectangleIntegral' (fun s => c / (s - p)) z w = c` ✓ with c := Acoeff n 1, p := 1 ✓.\n\nFor Gprim differentiability + deriv continuity, define helper lemmas:\n```\nlemma Gprim_differentiableAt {n : ℕ} {w : ℂ} (hw : w ≠ 1) :\n DifferentiableAt ℂ (Gprim n) w := by\n apply DifferentiableAt.sum\n intro i hi\n apply DifferentiableAt.mul (differentiableAt_const _)\n -- (w−1)^m differentiable at w ≠ 1 (zpow with negative exponent, base ≠ 0)\n exact (differentiableAt_zpow ... ) hmm — `differentiableAt_zpow (m : ℤ) (x) (h : x ≠ 0 ∨ 0 ≤ m)`? from the grep: hasDerivAt_zpow m x H with H : x ≠ 0 ∨ 0 ≤ m ⟹ differentiableAt. For (w−1): compose.\n```\n\nAnd deriv_Gprim continuity: deriv (Gprim n) w = tail-sum (by deriv_Gprim) — the tail sum of rational terms, each continuous off {1} ✓ (sum of continuous functions, needs w ≠ 1 for denominators).\n\nOK — let me write the whole section 3 and append. This is another ~150 lines. Let me write it in one go and compile.","signature":""},{"type":"text","text":"All pieces confirmed. Writing the assembly section (Acoeff/ppart/Gprim + the integral theorem)."},{"type":"tool_use","id":"Bash_259","name":"Bash","input":{"command":"cat >> /d/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiPrincipal.lean << 'EOF'\n\n/-! ## 3. The principal part and its integral -/\n\n/-- The principal-part coefficients: A_i = F^{(n+1−i)}(1)/(n+1−i)!,\nF(w) = (wⁿ−(w−1)ⁿ)·hLi(w). -/\ndef Acoeff (n i : ℕ) : ℂ :=\n iteratedDeriv (n + 1 - i) (fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w) 1 / (n + 1 - i)!\n\nlemma Acoeff_one (n : ℕ) : Acoeff n 1 = ResW1 n := by\n rw [Acoeff, ResW1, show n + 1 - 1 = n from by omega]\n\n/-- The principal part of J at w = 1: P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i. -/\ndef ppart (n : ℕ) (w : ℂ) : ℂ :=\n ∑ i ∈ Finset.Icc 1 (n + 1), Acoeff n i / (w - 1) ^ i\n\n/-- The tail primitive G(w) = −Σ_{i=2}^{n+1} (A_i/(i−1))·(w−1)^{−(i−1)}. -/\ndef Gprim (n : ℕ) (w : ℂ) : ℂ :=\n ∑ i ∈ Finset.Icc 2 (n + 1), -(Acoeff n i / ((i : ℂ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1))\n\nlemma Gprim_differentiableAt {n : ℕ} {w : ℂ} (hw : w ≠ 1) :\n DifferentiableAt ℂ (Gprim n) w := by\n rw [Gprim]\n apply DifferentiableAt.sum\n intro i hi\n apply DifferentiableAt.mul (differentiableAt_const _)\n have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw\n exact (hasDerivAt_zpow _ (w - 1) (Or.inl hw1)).differentiableAt.comp w\n ((hasDerivAt_id w).sub_const 1)\n\nlemma deriv_Gprim {n : ℕ} {w : ℂ} (hw : w ≠ 1) :\n deriv (Gprim n) w = ∑ i ∈ Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i := by\n rw [Gprim, deriv_sum (fun i hi => ?_)]\n · apply Finset.sum_congr rfl\n intro i hi\n rw [Finset.mem_Icc] at hi\n have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw\n have hi1 : ((i : ℂ) - 1) ≠ 0 := by\n have : 1 < (i : ℝ) := by exact_mod_cast (by omega : 1 < i)\n intro heq\n rw [sub_eq_zero] at heq\n have : (i : ℝ) = 1 := by exact_mod_cast heq\n linarith\n have hd : deriv (fun w => (w - 1) ^ (-((i : ℤ) - 1))) w\n = ((-((i : ℤ) - 1)) : ℂ) * (w - 1) ^ (-((i : ℤ) - 1) - 1) := by\n have h2 : HasDerivAt (fun x : ℂ => x ^ (-((i : ℤ) - 1)))\n ((-((i : ℤ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1) - 1)) (w - 1) :=\n hasDerivAt_zpow _ _ (Or.inl hw1)\n have h3 : HasDerivAt (fun w : ℂ => w - 1) 1 w := by\n simpa using (hasDerivAt_id w).sub_const 1\n have hcomp := h2.comp w h3\n rw [Function.comp_apply, mul_one] at hcomp\n exact hcomp.deriv\n rw [deriv_const_mul _ (by\n have hw1' : w - 1 ≠ 0 := sub_ne_zero.mpr hw\n exact (hasDerivAt_zpow _ (w - 1) (Or.inl hw1')).differentiableAt.comp w\n ((hasDerivAt_id w).sub_const 1)), hd]\n have hm : (-((i : ℤ) - 1) - 1 : ℤ) = -(i : ℤ) := by omega\n rw [hm]\n have hzi : ((-(i : ℤ)) : ℂ) = -((i : ℂ)) := by simp\n rw [hzi]\n field_simp [hw1, hi1]\n rw [zpow_neg, zpow_natCast]\n field_simp [hw1]\n ring\n · intro i hi\n apply DifferentiableAt.mul (differentiableAt_const _)\n have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw\n exact (hasDerivAt_zpow _ (w - 1) (Or.inl hw1)).differentiableAt.comp w\n ((hasDerivAt_id w).sub_const 1)\n\nlemma tail_continuousAt {n : ℕ} {w : ℂ} (hw : w ≠ 1) :\n ContinuousAt (∑ i ∈ Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i) w := by\n apply ContinuousAt.sum\n intro i hi\n rw [Finset.mem_Icc] at hi\n have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw\n apply ContinuousAt.div (continuousAt_const)\n exact (continuousAt_id.sub continuousAt_const).pow hw1.ne' |> fun h => h.continuousAt\n · exact pow_ne_zero _ hw1\n\nlemma ppart_eq_deriv_add {n : ℕ} {w : ℂ} (hw : w ≠ 1) :\n ppart n w = Acoeff n 1 / (w - 1) + deriv (Gprim n) w := by\n rw [ppart, deriv_Gprim hw]\n have hsplit : Finset.Icc 1 (n + 1) = {1} ∪ Finset.Icc 2 (n + 1) := by\n ext j\n simp [Finset.mem_Icc]\n omega\n rw [hsplit, Finset.sum_union (by simp)]\n simp [pow_one]\n\n/-- The principal-part integral: on any rectangle with 1 in its interior,\nRectangleIntegral' (ppart n) z w = ResW1 n. -/\ntheorem rectInt'_ppart {n : ℕ} {z w : ℂ}\n (hre : z.re ≤ w.re) (him : z.im ≤ w.im) (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ)) :\n RectangleIntegral' (ppart n) z w = ResW1 n := by\n have h1not : (1 : ℂ) ∉ RectangleBorder z w := not_mem_rectangleBorder_of_rectangle_mem_nhds h1\n have hdecomp : Set.EqOn (ppart n) (fun w => Acoeff n 1 / (w - 1) + deriv (Gprim n) w)\n (RectangleBorder z w) := by\n intro s hs\n have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)\n exact ppart_eq_deriv_add hs1\n rw [RectangleIntegral'_congr hdecomp]\n have hAint : RectangleBorderIntegrable (fun w => Acoeff n 1 / (w - 1)) z w := by\n apply HolomorphicOn.rectangleBorderIntegrable' _ h1\n intro s hs\n have hs1 : s ≠ 1 := hs.2\n exact (differentiableAt_const.div ((differentiableAt_id.sub (differentiableAt_const 1)))\n (sub_ne_zero.mpr hs1)).differentiableWithinAt\n have hGint : RectangleBorderIntegrable (deriv (Gprim n)) z w := by\n apply HolomorphicOn.rectangleBorderIntegrable' _ h1\n intro s hs\n have hs1 : s ≠ 1 := hs.2\n rw [deriv_Gprim hs1]\n exact (tail_continuousAt hs1).differentiableAt.continuousWithinAt\n rw [RectangleIntegral'_add _ _ hAint hGint]\n rw [ResidueTheoremInRectangle hre him h1]\n have hzero : RectangleIntegral (deriv (Gprim n)) z w = 0 := by\n apply rectInt_deriv_eq_zero\n · intro s hs\n have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)\n exact Gprim_differentiableAt hs1\n · intro s hs\n have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)\n rw [deriv_Gprim hs1]\n exact tail_continuousAt hs1\n rw [RectangleIntegral', hzero]\n rw [Acoeff_one]\n simp\nEOF\ncd /d/Python/Quantum/research/lean/NguyenRH1 && export PATH=\"$HOME/.elan/bin:$PATH\" && lake env lean NguyenRH1/LiPrincipal.lean 2>&1 | head -40","description":"Append assembly section and compile","timeout":420000},"extra_content":null}]