← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (1660 chars)
`HolomorphicOn.rectangleBorderIntegrable'` is exactly what I need: HolomorphicOn f (Rectangle \ {p}) + Rectangle ∈ 𝓝 p ⟹ RectangleBorderIntegrable f z w.
Now write the assembly. Let me append to LiPrincipal.lean:
1. `Acoeff`, `ppart`, `Gprim` defs.
2. `deriv_Gprim`: needs deriv of zpow terms. Check `deriv_zpow`.
3. `ppart_eq` (off {1}): ppart = A_1/(w−1) + tail = A_1/(w−1) + deriv Gprim.
4. Holomorphicity of both pieces on Rectangle \ {1} (for integrability).
5. rectInt_deriv_eq_zero's hypotheses for Gprim: DifferentiableAt G at each border point (w ≠ 1 there ✓ since 1 interior) + ContinuousAt (deriv G) at border points.
6. `rectInt'_ppart` final.
For deriv_Gprim's term derivative: f_i(w) = c·(w−1)^{−(i−1)} (zpow m = −(i−1)): deriv = c·m·(w−1)^{m−1}: via deriv_zpow? Let me check the exact form. For ℂ: `deriv_zpow (m : ℤ) (x : ℂ) : deriv (fun x => x ^ m) x = m * x ^ (m - 1)`? — I believe there's `deriv_zpow`. The composition with (w−1): deriv (fun w => (w−1)^m) w = m·(w−1)^{m−1}·1 — via `deriv.comp` or a direct lemma `deriv_pow_sub...`? Alternatively use HasDerivAt.zpow + comp... Let me just compute via deriv_const_sub... or actually there's likely `deriv_fun_zpow` or handle via `(deriv_zpow m 1).comp`? Use `deriv.comp`:
deriv (fun w => (w − 1) ^ m) w: = deriv ((· ^ m) ∘ (· − 1)) w = deriv (·^m) (w−1) · deriv (·−1) w = m·(w−1)^{m−1}·1 ✓ via HasDerivAt: `(hasDerivAt_zpow m (w−1)?...` — there's `HasDerivAt.zpow (m : ℤ) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => f x ^ m) (m * f x ^ (m - 1) * f') x`? Something like that exists for zpow. Then deriv via hasDerivAt.deriv.
Let me check deriv_zpow / HasDerivAt.zpow existence quickly.
Checking the zpow derivative lemma before writing the assembly.
tool: Bash
input
{
"command": "cd /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem deriv_zpow\\|lemma deriv_zpow\" Mathlib/ --include=*.lean | head -3; grep -rn \"HasDerivAt.zpow\\|hasDerivAt_zpow\" Mathlib/Analysis/Calculus/Deriv/*.lean 2>/dev/null | head -4",
"description": "Check zpow derivative lemmas"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`HolomorphicOn.rectangleBorderIntegrable'` is exactly what I need: HolomorphicOn f (Rectangle \\ {p}) + Rectangle ∈ 𝓝 p ⟹ RectangleBorderIntegrable f z w.\n\nNow write the assembly. Let me append to LiPrincipal.lean:\n\n1. `Acoeff`, `ppart`, `Gprim` defs.\n2. `deriv_Gprim`: needs deriv of zpow terms. Check `deriv_zpow`.\n3. `ppart_eq` (off {1}): ppart = A_1/(w−1) + tail = A_1/(w−1) + deriv Gprim.\n4. Holomorphicity of both pieces on Rectangle \\ {1} (for integrability).\n5. rectInt_deriv_eq_zero's hypotheses for Gprim: DifferentiableAt G at each border point (w ≠ 1 there ✓ since 1 interior) + ContinuousAt (deriv G) at border points.\n6. `rectInt'_ppart` final.\n\nFor deriv_Gprim's term derivative: f_i(w) = c·(w−1)^{−(i−1)} (zpow m = −(i−1)): deriv = c·m·(w−1)^{m−1}: via deriv_zpow? Let me check the exact form. For ℂ: `deriv_zpow (m : ℤ) (x : ℂ) : deriv (fun x => x ^ m) x = m * x ^ (m - 1)`? — I believe there's `deriv_zpow`. The composition with (w−1): deriv (fun w => (w−1)^m) w = m·(w−1)^{m−1}·1 — via `deriv.comp` or a direct lemma `deriv_pow_sub...`? Alternatively use HasDerivAt.zpow + comp... Let me just compute via deriv_const_sub... or actually there's likely `deriv_fun_zpow` or handle via `(deriv_zpow m 1).comp`? Use `deriv.comp`:\nderiv (fun w => (w − 1) ^ m) w: = deriv ((· ^ m) ∘ (· − 1)) w = deriv (·^m) (w−1) · deriv (·−1) w = m·(w−1)^{m−1}·1 ✓ via HasDerivAt: `(hasDerivAt_zpow m (w−1)?...` — there's `HasDerivAt.zpow (m : ℤ) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => f x ^ m) (m * f x ^ (m - 1) * f') x`? Something like that exists for zpow. Then deriv via hasDerivAt.deriv.\n\nLet me check deriv_zpow / HasDerivAt.zpow existence quickly.","signature":""},{"type":"text","text":"Checking the zpow derivative lemma before writing the assembly."},{"type":"tool_use","id":"Bash_258","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem deriv_zpow\\|lemma deriv_zpow\" Mathlib/ --include=*.lean | head -3; grep -rn \"HasDerivAt.zpow\\|hasDerivAt_zpow\" Mathlib/Analysis/Calculus/Deriv/*.lean 2>/dev/null | head -4","description":"Check zpow derivative lemmas"},"extra_content":null}]