← Session 29 — ii′-5e-v: circle bound (far-tail + series bounds)
thinking (2710 chars)
The proof of `differentiableAt_Gammaℝ_of_im_ne_zero'` uses `Complex.differentiableAt_Gamma _ hhalf` where hhalf : ∀ m : ℕ, s/2 ≠ −(m:ℂ) — the im ≠ 0 hypothesis is ONLY used to get s/2 off the poles! So the SAME proof works for any s with s/2 ∉ −ℕ — i.e. for s = −R with dist(R/2,ℤ) ≥ 1/4. So:
```
theorem differentiableAt_Gammaℝ_of_not_neg_two_nat {s : ℂ} (hs : ∀ m : ℕ, s ≠ -2 * (m : ℂ)) :
DifferentiableAt ℂ Complex.Gammaℝ s := by
have hhalf : ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := by
intro m h
apply hs m
have := congrArg (· * (2 : ℂ)) h
rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at this
rw [this]; ring
... (identical to the im≠0 proof from hhalf on)
```
And similarly (G) at such s — via the pointwise continuity extension, OR actually — now that I have differentiability at the real non-pole points, the continuity-of-equality needs:
- logDeriv ΓR continuous at s₀: (analyticAt: DifferentiableAt → AnalyticAt? No — DifferentiableAt doesn't give AnalyticAt directly... For the CONTINUITY of logDeriv (deriv f / f), I need deriv f continuous at s₀ — deriv of Gammaℝ: is Gammaℝ ANALYTIC at s₀? AnalyticAt follows from DifferentiableAt on an open set... Mathlib: `DifferentiableAt.analyticAt` doesn't exist (banked session 029: "DifferentiableAt.analyticAt does NOT exist (use fun_prop)"). Gammaℝ is analytic off poles: `Complex.analyticAt_Gammaℝ`? hmm — the fun_prop route: analyticAt Gammaℝ s₀ via AnalyticAt.mul of the two factors (both analytic: const_cpow analytic everywhere; Gamma analytic off poles: `Complex.analyticAt_Gamma _ hhalf`? there's differentiableAt_Gamma; analytic version? Mathlib has `Complex.analyticAt_Gamma`?? Let me grep. If differentiable only, then: continuity of logDeriv at s₀ via: logDeriv f = deriv f / f: deriv f continuous at s₀ iff f is C¹ at s₀: analytic ⟹ C¹. For Gamma: analyticAt: Mathlib `Complex.analyticAt_Gamma (s : ℂ) (hs : ∀ m : ℕ, s ≠ -(m:ℂ)) : AnalyticAt ℂ Gamma s`?? I recall `differentiable_Gamma`... Let me grep.
Actually — hold on, maybe simpler: AnalyticAt from AnalyticOnNhd via the identity-principle route for (G)-extension. You know what — let me simplify the whole thing: I'll prove the (G)-extension via the pointwise continuity-of-equality, using:
- logDeriv ΓR continuous at s₀: from DifferentiableAt ℂ (logDeriv Complex.Gammaℝ)? no. From `AnalyticAt ℂ (logDeriv Complex.Gammaℝ) s₀`: logDeriv of an analytic nonvanishing function is analytic: `AnalyticAt.logDeriv`? hmm: logDeriv f = deriv f / f: (analyticAt_f.deriv.div analyticAt_f nonzero): `AnalyticAt.deriv : AnalyticAt ℂ f x → AnalyticAt ℂ (deriv f) x` ✓ exists. Then .div with the nonzero. So I need AnalyticAt ℂ Complex.Gammaℝ s₀.
Grep for analyticAt_Gamma.
The `im ≠ 0` hypothesis was only used for pole-avoidance. Check the analytic Gamma API.
tool: Bash
input
{
"command": "cd \"D:/Python/Quantum/research/lean/NguyenRH1\" && grep -rn \"analyticAt_Gamma\\b\\|theorem analyticAt_Gamma\" ../../../zeta-23-lean/.lake/packages/mathlib/Mathlib/ 2>/dev/null | head -5",
"description": "Search analyticAt_Gamma in Mathlib"
}
raw content_json (database row)
[{"type":"thinking","thinking":"The proof of `differentiableAt_Gammaℝ_of_im_ne_zero'` uses `Complex.differentiableAt_Gamma _ hhalf` where hhalf : ∀ m : ℕ, s/2 ≠ −(m:ℂ) — the im ≠ 0 hypothesis is ONLY used to get s/2 off the poles! So the SAME proof works for any s with s/2 ∉ −ℕ — i.e. for s = −R with dist(R/2,ℤ) ≥ 1/4. So:\n\n```\ntheorem differentiableAt_Gammaℝ_of_not_neg_two_nat {s : ℂ} (hs : ∀ m : ℕ, s ≠ -2 * (m : ℂ)) :\n DifferentiableAt ℂ Complex.Gammaℝ s := by\n have hhalf : ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := by\n intro m h\n apply hs m\n have := congrArg (· * (2 : ℂ)) h\n rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at this\n rw [this]; ring\n ... (identical to the im≠0 proof from hhalf on)\n```\n\nAnd similarly (G) at such s — via the pointwise continuity extension, OR actually — now that I have differentiability at the real non-pole points, the continuity-of-equality needs:\n- logDeriv ΓR continuous at s₀: (analyticAt: DifferentiableAt → AnalyticAt? No — DifferentiableAt doesn't give AnalyticAt directly... For the CONTINUITY of logDeriv (deriv f / f), I need deriv f continuous at s₀ — deriv of Gammaℝ: is Gammaℝ ANALYTIC at s₀? AnalyticAt follows from DifferentiableAt on an open set... Mathlib: `DifferentiableAt.analyticAt` doesn't exist (banked session 029: \"DifferentiableAt.analyticAt does NOT exist (use fun_prop)\"). Gammaℝ is analytic off poles: `Complex.analyticAt_Gammaℝ`? hmm — the fun_prop route: analyticAt Gammaℝ s₀ via AnalyticAt.mul of the two factors (both analytic: const_cpow analytic everywhere; Gamma analytic off poles: `Complex.analyticAt_Gamma _ hhalf`? there's differentiableAt_Gamma; analytic version? Mathlib has `Complex.analyticAt_Gamma`?? Let me grep. If differentiable only, then: continuity of logDeriv at s₀ via: logDeriv f = deriv f / f: deriv f continuous at s₀ iff f is C¹ at s₀: analytic ⟹ C¹. For Gamma: analyticAt: Mathlib `Complex.analyticAt_Gamma (s : ℂ) (hs : ∀ m : ℕ, s ≠ -(m:ℂ)) : AnalyticAt ℂ Gamma s`?? I recall `differentiable_Gamma`... Let me grep.\n\nActually — hold on, maybe simpler: AnalyticAt from AnalyticOnNhd via the identity-principle route for (G)-extension. You know what — let me simplify the whole thing: I'll prove the (G)-extension via the pointwise continuity-of-equality, using:\n- logDeriv ΓR continuous at s₀: from DifferentiableAt ℂ (logDeriv Complex.Gammaℝ)? no. From `AnalyticAt ℂ (logDeriv Complex.Gammaℝ) s₀`: logDeriv of an analytic nonvanishing function is analytic: `AnalyticAt.logDeriv`? hmm: logDeriv f = deriv f / f: (analyticAt_f.deriv.div analyticAt_f nonzero): `AnalyticAt.deriv : AnalyticAt ℂ f x → AnalyticAt ℂ (deriv f) x` ✓ exists. Then .div with the nonzero. So I need AnalyticAt ℂ Complex.Gammaℝ s₀. \n\nGrep for analyticAt_Gamma.","signature":""},{"type":"text","text":"The `im ≠ 0` hypothesis was only used for pole-avoidance. Check the analytic Gamma API."},{"type":"tool_use","id":"Bash_151","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/research/lean/NguyenRH1\" && grep -rn \"analyticAt_Gamma\\b\\|theorem analyticAt_Gamma\" ../../../zeta-23-lean/.lake/packages/mathlib/Mathlib/ 2>/dev/null | head -5","description":"Search analyticAt_Gamma in Mathlib"},"extra_content":null}]