← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (2223 chars)
I'm leaving sorries and guessing names again (`convex_halfspace_re_gt`, `hasDerivAt_b2Integral... .analyticAt`). Let me be careful:
1. The convexity of half-planes in ℂ: exact lemma names: `convex_halfspace_re_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.re}`? Let me check Mathlib: Mathlib/Analysis/Convex/... there's `convex_halfspace_re_gt`? I believe Complex halfspace lemmas exist: `convex_halfspace_re_gt`, `convex_halfspace_im_gt` etc. — need verification.
2. AnalyticAt from HasDerivAt at a point: hasDerivAt gives differentiability AT the point — for analyticity at z I need differentiability in a NEIGHBORHOOD: the B̃₂ integral has HasDerivAt at EVERY point of {re > −1} — so DifferentiableOn {re > −1} ⟹ AnalyticOnNhd via DifferentiableOn.analyticOnNhd (open) — then .analyticAt at z (z ∈ the open set). So:
```lean
have hJ_an : AnalyticOnNhd ℂ (fun s : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) {z | -1 < z.re} := by
apply DifferentiableOn.analyticOnNhd _ (isOpen_lt continuous_const Complex.continuous_re)
intro z hz
exact (hasDerivAt_b2Integral hz).differentiableAt.differentiableWithinAt
```
Then at z ∈ W: (hJ_an.mono (W ⊆ {re > −1})).analyticAt? AnalyticOnNhd ℂ f W → AnalyticAt ℂ f z for z ∈ W (W open — `AnalyticOnNhd.analyticAt (h) (hx : s ∈ 𝓝 z)`? h z hz directly: AnalyticOnNhd f s = ∀ x ∈ s, AnalyticAt f x ✓ so hJ_an_mono z hz directly).
Let me check `DifferentiableOn.analyticOnNhd` arg order: from CauchyIntegral.lean:631: `theorem _root_.DifferentiableOn.analyticOnNhd {s : Set ℂ} {f : ℂ → E} (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) : AnalyticOnNhd ℂ f s`? Let me verify the arg order (hd first or hs first) — earlier I used `(hd.analyticOnNhd Metric.isOpen_ball) (-2) hball` in LiContour ✓ — so hd.analyticOnNhd hs gives AnalyticOnNhd — then applying to a point: `(hd.analyticOnNhd hs) x hx` — wait in LiContour I wrote `(hd.analyticOnNhd Metric.isOpen_ball) (-2) hball`?? AnalyticOnNhd f s = ∀ x, x ∈ s → AnalyticAt f x — applying (−2) hball ✓. Hmm but AnalyticOnNhd is ∀ x ∈ s, AnalyticAt — the membership form. In LiContour it compiled ✓. OK.
3. `convex_halfspace_re_gt`: check existence.
Let me check these names, then write §4 completely and carefully.
Checking the half-plane convexity lemma names before completing §4.
tool: Bash
input
{
"command": "cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"convex_halfspace_re_gt\\|convex_halfspace_im_gt\\|convex_halfspace_re_lt\\|convex_halfspace_im_lt\" Mathlib/Analysis/Complex/Convex.lean Mathlib/Analysis/Complex/*.lean 2>/dev/null | head -6",
"description": "Verify half-plane convexity lemmas"
}
raw content_json (database row)
[{"type":"thinking","thinking":"I'm leaving sorries and guessing names again (`convex_halfspace_re_gt`, `hasDerivAt_b2Integral... .analyticAt`). Let me be careful:\n\n1. The convexity of half-planes in ℂ: exact lemma names: `convex_halfspace_re_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.re}`? Let me check Mathlib: Mathlib/Analysis/Convex/... there's `convex_halfspace_re_gt`? I believe Complex halfspace lemmas exist: `convex_halfspace_re_gt`, `convex_halfspace_im_gt` etc. — need verification.\n\n2. AnalyticAt from HasDerivAt at a point: hasDerivAt gives differentiability AT the point — for analyticity at z I need differentiability in a NEIGHBORHOOD: the B̃₂ integral has HasDerivAt at EVERY point of {re > −1} — so DifferentiableOn {re > −1} ⟹ AnalyticOnNhd via DifferentiableOn.analyticOnNhd (open) — then .analyticAt at z (z ∈ the open set). So:\n```lean\n have hJ_an : AnalyticOnNhd ℂ (fun s : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) {z | -1 < z.re} := by\n apply DifferentiableOn.analyticOnNhd _ (isOpen_lt continuous_const Complex.continuous_re)\n intro z hz\n exact (hasDerivAt_b2Integral hz).differentiableAt.differentiableWithinAt\n```\nThen at z ∈ W: (hJ_an.mono (W ⊆ {re > −1})).analyticAt? AnalyticOnNhd ℂ f W → AnalyticAt ℂ f z for z ∈ W (W open — `AnalyticOnNhd.analyticAt (h) (hx : s ∈ 𝓝 z)`? h z hz directly: AnalyticOnNhd f s = ∀ x ∈ s, AnalyticAt f x ✓ so hJ_an_mono z hz directly).\n\nLet me check `DifferentiableOn.analyticOnNhd` arg order: from CauchyIntegral.lean:631: `theorem _root_.DifferentiableOn.analyticOnNhd {s : Set ℂ} {f : ℂ → E} (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) : AnalyticOnNhd ℂ f s`? Let me verify the arg order (hd first or hs first) — earlier I used `(hd.analyticOnNhd Metric.isOpen_ball) (-2) hball` in LiContour ✓ — so hd.analyticOnNhd hs gives AnalyticOnNhd — then applying to a point: `(hd.analyticOnNhd hs) x hx` — wait in LiContour I wrote `(hd.analyticOnNhd Metric.isOpen_ball) (-2) hball`?? AnalyticOnNhd f s = ∀ x, x ∈ s → AnalyticAt f x — applying (−2) hball ✓. Hmm but AnalyticOnNhd is ∀ x ∈ s, AnalyticAt — the membership form. In LiContour it compiled ✓. OK.\n\n3. `convex_halfspace_re_gt`: check existence.\n\nLet me check these names, then write §4 completely and carefully.","signature":""},{"type":"text","text":"Checking the half-plane convexity lemma names before completing §4."},{"type":"tool_use","id":"Bash_277","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"convex_halfspace_re_gt\\|convex_halfspace_im_gt\\|convex_halfspace_re_lt\\|convex_halfspace_im_lt\" Mathlib/Analysis/Complex/Convex.lean Mathlib/Analysis/Complex/*.lean 2>/dev/null | head -6","description":"Verify half-plane convexity lemmas"},"extra_content":null}]