← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
thinking (2572 chars)
I fumbled the hG_an (AnalyticAt Gammaℝ 1) proof and left sorries — that was a mistake, I was overcomplicating. AnalyticAt of Gammaℝ at 1 is much simpler: Gammaℝ is differentiable in a neighborhood — but actually the simplest: use `DifferentiableAt.analyticAt`? Doesn't exist (banked). Alternative: I don't need AnalyticAt of Gammaℝ at 1 — I need ContDiffAt (or just AnalyticAt) of `fun s => logDeriv Gammaℝ (1+s)` at 0.
Simplest robust route: ContDiffAt.congr_of_eventuallyEq with the digamma eventuallyEq (logDeriv_Gammaℝ_one_add holds eventually on 𝓝 0 by LiArchimedean's eventually_Gamma_ne_zero_and_pole_free) and the digamma-side ContDiffAt (hcd pattern from LiArchimedean:208-219).
Does `ContDiffAt.congr_of_eventuallyEq` exist? Let me probe. If yes:
```lean
have hG3 : ContDiffAt ℂ m (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) 0 := by
obtain ⟨hG, hpole⟩ := eventually_Gamma_ne_zero_and_pole_free
have hev : (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) =ᶠ[𝓝 (0 : ℂ)]
(fun s => -(Real.log Real.pi : ℂ) / 2 + (1 / 2) * Complex.digamma ((1 + s) / 2)) := by
filter_upwards [hG, hpole] with s h1 h2
exact logDeriv_Gammaℝ_one_add h1 h2
apply ContDiffAt.congr_of_eventuallyEq hev.symm (?)...
```
hmm direction: ContDiffAt.congr_of_eventuallyEq : f₁ =ᶠ[𝓝 x] f → (ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n f₁ x)? Let me probe the exact form. And the digamma side:
```lean
have hcd0 : ContDiffAt ℂ m (fun s => Complex.digamma ((1 + s) / 2)) 0 := by
have h1 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) := digamma_analyticOn _ dpsiDomain_half
have h2 : AnalyticAt ℂ (fun s : ℂ => (1 + s) / 2) 0 :=
(analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)
have h3 := AnalyticAt.comp_of_eq h1 h2 (by show (1 + (0 : ℂ)) / 2 = 1 / 2; ring)
have heq : (Complex.digamma ∘ (fun s : ℂ => (1 + s) / 2)) =
fun s => Complex.digamma ((1 + s) / 2) := rfl
rw [heq] at h3
exact h3.contDiffAt
exact (contDiff_const (𝕜 := ℂ) (c := -(Real.log Real.pi : ℂ) / 2)).contDiffAt.add
((contDiff_const (𝕜 := ℂ) (c := (1 / 2 : ℂ))).contDiffAt.mul hcd0)
```
plus the defeq assignment to the pointwise-add lambda form.
That avoids the DifferentiableOn-ball mess entirely. Let me probe ContDiffAt.congr_of_eventuallyEq's exact signature first, then rewrite the file portion. Actually — even better: check if it needs the EventuallyEq direction f =ᶠ g with f the target: I'll get the signature from the probe.
Also need `eventually_Gamma_ne_zero_and_pole_free` — it's in LiArchimedean (used at line 196) ✓.
Let me probe.
I left sorries in a fumbled AnalyticAt detour — better route: `ContDiffAt.congr_of_eventuallyEq` with the digamma form. Probing its signature.
tool: Bash
input
{
"command": "cd D:/Python/Quantum/research/lean/NguyenRH1 && cat > Scratch.lean << 'EOF'\nimport Mathlib\n#check @ContDiffAt.congr_of_eventuallyEq\n#check @Filter.EventuallyEq.congr\n#check @add_pow\n#check @Finset.sum_neg_distrib\n#check @mul_left_cancel\u2080\n#check @Nat.cast_ne_zero\n#check @abs_re_le_norm\n#check @eventually_Gamma_ne_zero_and_pole_free\nEOF\nexport PATH=\"$HOME/.elan/bin:$PATH\" && lake env lean Scratch.lean 2>&1 | head -30",
"description": "Probe ContDiffAt congruence + binomial lemmas",
"timeout": 300000
}
raw content_json (database row)
[{"type":"thinking","thinking":"I fumbled the hG_an (AnalyticAt Gammaℝ 1) proof and left sorries — that was a mistake, I was overcomplicating. AnalyticAt of Gammaℝ at 1 is much simpler: Gammaℝ is differentiable in a neighborhood — but actually the simplest: use `DifferentiableAt.analyticAt`? Doesn't exist (banked). Alternative: I don't need AnalyticAt of Gammaℝ at 1 — I need ContDiffAt (or just AnalyticAt) of `fun s => logDeriv Gammaℝ (1+s)` at 0. \n\nSimplest robust route: ContDiffAt.congr_of_eventuallyEq with the digamma eventuallyEq (logDeriv_Gammaℝ_one_add holds eventually on 𝓝 0 by LiArchimedean's eventually_Gamma_ne_zero_and_pole_free) and the digamma-side ContDiffAt (hcd pattern from LiArchimedean:208-219).\n\nDoes `ContDiffAt.congr_of_eventuallyEq` exist? Let me probe. If yes:\n\n```lean\nhave hG3 : ContDiffAt ℂ m (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) 0 := by\n obtain ⟨hG, hpole⟩ := eventually_Gamma_ne_zero_and_pole_free\n have hev : (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) =ᶠ[𝓝 (0 : ℂ)]\n (fun s => -(Real.log Real.pi : ℂ) / 2 + (1 / 2) * Complex.digamma ((1 + s) / 2)) := by\n filter_upwards [hG, hpole] with s h1 h2\n exact logDeriv_Gammaℝ_one_add h1 h2\n apply ContDiffAt.congr_of_eventuallyEq hev.symm (?)...\n```\nhmm direction: ContDiffAt.congr_of_eventuallyEq : f₁ =ᶠ[𝓝 x] f → (ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n f₁ x)? Let me probe the exact form. And the digamma side:\n```lean\n have hcd0 : ContDiffAt ℂ m (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have h1 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) := digamma_analyticOn _ dpsiDomain_half\n have h2 : AnalyticAt ℂ (fun s : ℂ => (1 + s) / 2) 0 :=\n (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)\n have h3 := AnalyticAt.comp_of_eq h1 h2 (by show (1 + (0 : ℂ)) / 2 = 1 / 2; ring)\n have heq : (Complex.digamma ∘ (fun s : ℂ => (1 + s) / 2)) =\n fun s => Complex.digamma ((1 + s) / 2) := rfl\n rw [heq] at h3\n exact h3.contDiffAt\n exact (contDiff_const (𝕜 := ℂ) (c := -(Real.log Real.pi : ℂ) / 2)).contDiffAt.add\n ((contDiff_const (𝕜 := ℂ) (c := (1 / 2 : ℂ))).contDiffAt.mul hcd0)\n```\nplus the defeq assignment to the pointwise-add lambda form.\n\nThat avoids the DifferentiableOn-ball mess entirely. Let me probe ContDiffAt.congr_of_eventuallyEq's exact signature first, then rewrite the file portion. Actually — even better: check if it needs the EventuallyEq direction f =ᶠ g with f the target: I'll get the signature from the probe.\n\nAlso need `eventually_Gamma_ne_zero_and_pole_free` — it's in LiArchimedean (used at line 196) ✓.\n\nLet me probe.","signature":""},{"type":"text","text":"I left sorries in a fumbled AnalyticAt detour — better route: `ContDiffAt.congr_of_eventuallyEq` with the digamma form. Probing its signature."},{"type":"tool_use","id":"Bash_102","name":"Bash","input":{"command":"cd D:/Python/Quantum/research/lean/NguyenRH1 && cat > Scratch.lean << 'EOF'\nimport Mathlib\n#check @ContDiffAt.congr_of_eventuallyEq\n#check @Filter.EventuallyEq.congr\n#check @add_pow\n#check @Finset.sum_neg_distrib\n#check @mul_left_cancel₀\n#check @Nat.cast_ne_zero\n#check @abs_re_le_norm\n#check @eventually_Gamma_ne_zero_and_pole_free\nEOF\nexport PATH=\"$HOME/.elan/bin:$PATH\" && lake env lean Scratch.lean 2>&1 | head -30","description":"Probe ContDiffAt congruence + binomial lemmas","timeout":300000},"extra_content":null}]