← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (4127 chars)
`AnalyticAt.comp {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (g ∘ f) x` — NOTE: the OUTER function is `g` and the INNER is `f` — so `AnalyticAt.comp (hg : AnalyticAt g (f x)) (hf : AnalyticAt f x)` — the hg is the OUTER (digamma) and hf is the INNER (the affine). So the call should be `AnalyticAt.comp h1 h2` with h1 : AnalyticAt digamma ((fun s => (1+s)/2) 0) — the point must be `(fun s => (1+s)/2) 0` — the APPLICATION form (f x) with f := the affine. The point in h1 must be `(affine) 0` — the application form — h1's point is (1:ℂ)/2 — the application (fun s => (1+s)/2) 0 beta-reduces to (1+0)/2 which displays as... — the unifier needs (f x) with f := the affine, x := 0 — so the point must be `(fun s => (1+s)/2) 0` — as I noted the beta-reduced form (1+0)/2 mis-unified. Fix: make h1's point EXACTLY `(fun s : ℂ => (1 + s) / 2) 0` — unreduced:
```lean
have h1 : AnalyticAt ℂ Complex.digamma ((fun s : ℂ => (1 + s) / 2) 0) := by
have h0 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) :=
digamma_analyticOn _ dpsiDomain_half
have e : ((fun s : ℂ => (1 + s) / 2) 0) = (1 : ℂ) / 2 := by simp -- hmm simp normalizes (1+0)/2 → 1/2? — the point form
rw [e] -- NO — this rewrites h0's point — wrong direction
exact h0 -- h0 : AnalyticAt digamma (1/2) — the goal's point ((fun s => (1+s)/2) 0) — defeq beta ✓ exact should accept!
```
The `exact h0` — h0 : AnalyticAt ℂ digamma (1/2) — goal's point ((fun s => (1+s)/2) 0) — defeq via beta+arithmetic — `exact` checks defeq — (fun s => (1+s)/2) 0 ≡ (1+0)/2 ≡ 1/2 ✓ — exact should work IF Lean's defeq does the beta and the numeral arithmetic — (1+0)/2 vs 1/2 — for ℂ — the numeral division — is (1+0)/2 ≡ 1/2 definitionally? — 1+0 in ℂ — as discussed, NOT defeq for ℂ (the addition of OfNat 1 and OfNat 0 — Complex's addition is a structure operation — (1+0).re = 1.re+0.re = 1+0 (real) — real 1+0 — ℝ's addition — also not defeq...). Hmm — so `exact h0` fails on the point defeq. And `show`-based forms normalize to the mis-unifying form.
SOLUTION: keep the point as the UNREDUCED application and prove h1 via a conversion that doesn't normalize:
```lean
have h1 : AnalyticAt ℂ Complex.digamma ((fun s : ℂ => (1 + s) / 2) 0) := by
have h0 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) :=
digamma_analyticOn _ dpsiDomain_half
have e : ((fun s : ℂ => (1 + s) / 2) 0) = (1 : ℂ) / 2 := by
show (1 + (0 : ℂ)) / 2 = 1 / 2 -- hmm — the LHS is the beta of the application
ring
rw [e] at h0 ⊢ -- wait — rw [e] at h0 ⊢ — no...
```
Hmm — the issue: I want h1's point to STAY as the unreduced application. Prove it as: `exact e ▸ h0`? — with e : ((fun s => (1+s)/2) 0) = 1/2 — then h0 : AnalyticAt digamma (1/2) — and I want AnalyticAt digamma ((fun s => (1+s)/2) 0) — that's e ▸ h0 in the reverse: `e.symm ▸ h0` — the ▸ transport: e.symm : 1/2 = ((fun s => (1+s)/2) 0) — h0 ▸ along it: AnalyticAt digamma ((fun s => (1+s)/2) 0) ✓ — but ▸ is finicky. Alternative: `convert h0` — convert produces the point-equality side goal: ((fun s => (1+s)/2) 0) = 1/2 — closed by `simp` (beta + arithmetic) ✓:
```lean
have h1 : AnalyticAt ℂ Complex.digamma ((fun s : ℂ => (1 + s) / 2) 0) := by
convert digamma_analyticOn _ dpsiDomain_half
simp -- or: show (1+0)/2 = 1/2; ring
have h3 := AnalyticAt.comp h1 h2 -- h1's point is the application form ✓ comp unifies f := affine ✓
```
`convert h0` — h0 : AnalyticAt digamma (1/2) — goal AnalyticAt digamma ((fun s => (1+s)/2) 0) — convert produces the point-eq goal: (1/2) = ((fun s => (1+s)/2) 0)?? or the reverse — then `simp` — the application beta-reduces to (1+0)/2 and simp normalizes to 1/2 ✓ hopefully. If simp's normal form of ((fun s => (1+s)/2) 0) is (1+0)/2 and then... — simp computes (1+0)/2 = 1/2 ✓ (norm_num-ish inside simp? — simp has `add_zero` and numeral division — the (1+0)/2 → 1/2 — simp should handle via add_zero + ... hmm — (1+0)/2 = 1/2 — after add_zero: 1/2 = 1/2 ✓ rfl — simp closes by rfl ✓).
Let me apply this convert approach.
The comp unification needs the point in application form. Using `convert`.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiArchimedean.lean",
"old_string": " have hcd0 : ContDiffAt \u2102 j (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have h1 : AnalyticAt \u2102 Complex.digamma ((1 : \u2102) / 2) :=\n digamma_analyticOn _ dpsiDomain_half\n have h2 : AnalyticAt \u2102 (fun s : \u2102 => (1 + s) / 2) 0 :=\n (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)\n have h3 := AnalyticAt.comp (g := fun s : \u2102 => (1 + s) / 2) h1 h2\n have heq : (Complex.digamma \u2218 (fun s : \u2102 => (1 + s) / 2)) =\n fun s => Complex.digamma ((1 + s) / 2) := rfl\n rw [heq] at h3\n exact h3.contDiffAt",
"new_string": " have hcd0 : ContDiffAt \u2102 j (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have h1 : AnalyticAt \u2102 Complex.digamma ((fun s : \u2102 => (1 + s) / 2) 0) := by\n convert digamma_analyticOn _ dpsiDomain_half\n simp\n have h2 : AnalyticAt \u2102 (fun s : \u2102 => (1 + s) / 2) 0 :=\n (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)\n have h3 := AnalyticAt.comp h1 h2\n have heq : (Complex.digamma \u2218 (fun s : \u2102 => (1 + s) / 2)) =\n fun s => Complex.digamma ((1 + s) / 2) := rfl\n rw [heq] at h3\n exact h3.contDiffAt"
}
result 2026-08-22 11:17:02Z → 2026-08-22 11:17:02Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiArchimedean.lean",
"oldString": " have hcd0 : ContDiffAt \u2102 j (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have h1 : AnalyticAt \u2102 Complex.digamma ((1 : \u2102) / 2) :=\n digamma_analyticOn _ dpsiDomain_half\n have h2 : AnalyticAt \u2102 (fun s : \u2102 => (1 + s) / 2) 0 :=\n (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)\n have h3 := AnalyticAt.comp (g := fun s : \u2102 => (1 + s) / 2) h1 h2\n have heq : (Complex.digamma \u2218 (fun s : \u2102 => (1 + s) / 2)) =\n fun s => Complex.digamma ((1 + s) / 2) := rfl\n rw [heq] at h3\n exact h3.contDiffAt",
"newString": " have hcd0 : ContDiffAt \u2102 j (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have h1 : AnalyticAt \u2102 Complex.digamma ((fun s : \u2102 => (1 + s) / 2) 0) := by\n convert digamma_analyticOn _ dpsiDomain_half\n simp\n have h2 : AnalyticAt \u2102 (fun s : \u2102 => (1 + s) / 2) 0 :=\n (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)\n have h3 := AnalyticAt.comp h1 h2\n have heq : (Complex.digamma \u2218 (fun s : \u2102 => (1 + s) / 2)) =\n fun s => Complex.digamma ((1 + s) / 2) := rfl\n rw [heq] at h3\n exact h3.contDiffAt",
"originalFile": "/-\nNguyenRH1/LiArchimedean.lean \u2014 tier ii\u2032 sub-stage ii\u2032-3a, piece (A)\n(D-066 \u00a74): the archimedean coefficients of the (4.10) split.\n\nTarget (D-066): the Taylor coefficients of s \u21a6 logDeriv Gamma\u211d (1+s) at 0:\n\n (1/j!)\u00b7iteratedDeriv j (fun s => logDeriv Gamma\u211d (1+s)) 0 = (\u22121)^{j+1} a_{j+1},\n\ni.e. `iteratedDeriv j ... 0 = (\u22121)^{j+1}\u00b7j!\u00b7lagariasA (j+1)`.\n\nPart 1 (this file, complete): the Gamma\u211d logDeriv split\n logDeriv Gamma\u211d (1+s) = \u2212(log \u03c0)/2 + (1/2)\u00b7digamma((1+s)/2)\n(`logDeriv_Gamma\u211d_one_add`) and the j = 0 evaluation\n logDeriv Gamma\u211d 1 = \u2212(log 4\u03c0 + \u03b3)/2 = \u2212lagariasA1\n(`logDeriv_Gamma\u211d_one`) \u2014 via Mathlib's `Complex.digamma_one_half`.\n\nPart 2 (next): the digamma series from BohrMollerup's logGammaSeq and the\nj \u2265 1 polygamma values at 1/2, then the odd-m reindexing to lagariasA.\n\nArchive references: D-066 (route \u03b24, piece A), journal-019/020.\n-/\nimport Mathlib\nimport NguyenRH1.LiDigamma\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The Gamma\u211d logDeriv split -/\n\n/-- The cpow factor as an exponential: \u03c0^(\u2212w/2) = exp(\u2212(log \u03c0)/2\u00b7w). -/\nlemma pi_cpow_neg_half_eq_exp (w : \u2102) :\n (\u2191Real.pi : \u2102) ^ (-w / 2) = Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w) := by\n rw [Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero)]\n congr 1\n rw [\u2190 Complex.ofReal_log Real.pi_nonneg]\n ring_nf\n\n/-- The Gamma\u211d logDeriv split: for (1+s)/2 off the poles of \u0393,\n logDeriv Gamma\u211d (1+s) = \u2212(log \u03c0)/2 + (1/2)\u00b7\u03c8((1+s)/2). -/\nlemma logDeriv_Gamma\u211d_one_add {s : \u2102}\n (hs : Complex.Gamma ((1 + s) / 2) \u2260 0)\n (hs2 : \u2200 m : \u2115, ((1 + s) / 2) \u2260 -m) :\n logDeriv Complex.Gamma\u211d (1 + s) =\n -(Real.log Real.pi : \u2102) / 2 + (1 / 2) * Complex.digamma ((1 + s) / 2) := by\n have hfun : Complex.Gamma\u211d = fun w : \u2102 =>\n Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w) * Complex.Gamma (w / 2) := by\n funext w\n show Complex.Gamma\u211d w = _\n rw [Complex.Gamma\u211d_def]\n congr 1\n exact pi_cpow_neg_half_eq_exp w\n rw [hfun]\n have hdif1 : DifferentiableAt \u2102 (fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w))\n (1 + s) := by\n have h1 : DifferentiableAt \u2102 (fun w : \u2102 => -(Real.log Real.pi : \u2102) / 2 * w) (1 + s) :=\n differentiableAt_id.const_mul _\n exact Complex.differentiableAt_exp.comp (1 + s) h1\n have hdif2 : DifferentiableAt \u2102 (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) := by\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => w / 2) (1 + s) :=\n differentiableAt_id.div_const 2\n exact (Complex.differentiableAt_Gamma _ hs2).comp (1 + s) h2\n rw [logDeriv_mul (f := fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w))\n (g := fun w => Complex.Gamma (w / 2)) (1 + s) (Complex.exp_ne_zero _) hs hdif1 hdif2]\n have h1 : logDeriv (fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w)) (1 + s) =\n -(Real.log Real.pi : \u2102) / 2 := by\n rw [logDeriv_apply]\n have hd : deriv (fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w)) (1 + s) =\n Complex.exp (-(Real.log Real.pi : \u2102) / 2 * (1 + s)) * (-(Real.log Real.pi : \u2102) / 2) := by\n have hh1 : HasDerivAt (fun w : \u2102 => -(Real.log Real.pi : \u2102) / 2 * w)\n (-(Real.log Real.pi : \u2102) / 2) (1 + s) := by\n simpa using (hasDerivAt_id (1 + s)).const_mul (-(Real.log Real.pi : \u2102) / 2)\n have hh2 := (Complex.hasDerivAt_exp (-(Real.log Real.pi : \u2102) / 2 * (1 + s))).comp (1 + s) hh1\n have heq : (Complex.exp \u2218 fun w : \u2102 => -(Real.log Real.pi : \u2102) / 2 * w) =\n fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w) := rfl\n rw [heq] at hh2\n exact hh2.deriv\n rw [hd]\n field_simp [Complex.exp_ne_zero (-(Real.log Real.pi : \u2102) / 2 * (1 + s))]\n have h2 : logDeriv (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) =\n (1 / 2) * Complex.digamma ((1 + s) / 2) := by\n rw [logDeriv_apply]\n have hd : deriv (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) =\n deriv Complex.Gamma ((1 + s) / 2) * (1 / 2) := by\n have hh1 : HasDerivAt (fun w : \u2102 => w / 2) (1 / 2) (1 + s) := by\n simpa using (hasDerivAt_id (1 + s)).div_const (2 : \u2102)\n have hh2 := ((Complex.differentiableAt_Gamma _ hs2).hasDerivAt).comp (1 + s) hh1\n have heq : (Complex.Gamma \u2218 fun w : \u2102 => w / 2) = fun w : \u2102 => Complex.Gamma (w / 2) := rfl\n rw [heq] at hh2\n exact hh2.deriv\n rw [hd, Complex.digamma_def, logDeriv_apply]\n field_simp [hs]\n rw [h1, h2]\n\n/-! ## 2. The j = 0 evaluation: \u03c4\u2080 = \u2212a\u2081 -/\n\n/-- log(4\u03c0) = 2\u00b7log 2 + log \u03c0. -/\nlemma log_four_pi : Real.log (4 * Real.pi) = 2 * Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num) (by positivity)]\n congr 1\n rw [show (4 : \u211d) = 2 ^ 2 from by norm_num, Real.log_pow]\n ring\n\n/-- **\u03c4\u2080** (D-066 \u00a74, j = 0): logDeriv Gamma\u211d 1 = \u2212(log 4\u03c0 + \u03b3)/2 = \u2212a\u2081. -/\ntheorem logDeriv_Gamma\u211d_one :\n logDeriv Complex.Gamma\u211d 1 = -(lagariasA1 : \u2102) := by\n have hs : Complex.Gamma ((1 + (0 : \u2102)) / 2) \u2260 0 := by\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e, Complex.Gamma_one_half_eq]\n have hpi : (\u2191Real.pi : \u2102) \u2260 0 := by exact_mod_cast Real.pi_ne_zero\n rw [Complex.cpow_def_of_ne_zero hpi]\n exact Complex.exp_ne_zero _\n have hs2 : \u2200 m : \u2115, ((1 + (0 : \u2102)) / 2) \u2260 -m := by\n intro m hm\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e] at hm\n have hre : ((1 : \u2102) / 2).re = (-(m : \u2102)).re := by rw [hm]\n simp at hre\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n have h := logDeriv_Gamma\u211d_one_add (s := 0) hs hs2\n rw [add_zero] at h\n rw [h]\n rw [Complex.digamma_one_half]\n rw [show Complex.log (2 : \u2102) = (Real.log 2 : \u2102) by\n rw [show (2 : \u2102) = ((2 : \u211d) : \u2102) by simp]\n exact (Complex.ofReal_log (by norm_num : (0 : \u211d) \u2264 2)).symm]\n rw [lagariasA1, log_four_pi]\n push_cast\n ring\n\n/-! ## 3. The full archimedean coefficient evaluation (all j) -/\n\n/-- The split's hypotheses hold on a neighbourhood of 0. -/\nlemma eventually_Gamma_ne_zero_and_pole_free :\n (\u2200\u1da0 s in \ud835\udcdd (0 : \u2102), Complex.Gamma ((1 + s) / 2) \u2260 0) \u2227\n (\u2200\u1da0 s in \ud835\udcdd (0 : \u2102), \u2200 m : \u2115, (1 + s) / 2 \u2260 -(m : \u2102)) := by\n have hcont1 : ContinuousAt (fun s : \u2102 => Complex.Gamma ((1 + s) / 2)) 0 := by\n have haffine : ContinuousAt (fun s : \u2102 => (1 + s) / 2) 0 := by\n have h := (continuousAt_const.add continuousAt_id : ContinuousAt (fun s : \u2102 => 1 + s) 0)\n simpa using h.div_const (2 : \u2102)\n have hG : ContinuousAt Complex.Gamma ((1 + (0 : \u2102)) / 2) := by\n apply Complex.continuousAt_Gamma\n intro m\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e]\n intro hcontra\n have h2 : ((1 : \u2102) / 2).re = (-(m : \u2102)).re := by rw [hcontra]\n simp at h2\n have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n have hcomp := hG.comp 0 haffine\n have heq : (Complex.Gamma \u2218 fun s : \u2102 => (1 + s) / 2) =\n fun s => Complex.Gamma ((1 + s) / 2) := rfl\n rw [heq] at hcomp\n exact hcomp\n have h1 : \u2200\u1da0 s in \ud835\udcdd (0 : \u2102), Complex.Gamma ((1 + s) / 2) \u2260 0 := by\n have hG1 : Complex.Gamma ((1 + (0 : \u2102)) / 2) \u2260 0 := by\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e, Complex.Gamma_one_half_eq]\n have hpi : (\u2191Real.pi : \u2102) \u2260 0 := by exact_mod_cast Real.pi_ne_zero\n rw [Complex.cpow_def_of_ne_zero hpi]\n exact Complex.exp_ne_zero _\n exact hcont1.tendsto.eventually_ne hG1\n have h2 : \u2200\u1da0 s in \ud835\udcdd (0 : \u2102), \u2200 m : \u2115, (1 + s) / 2 \u2260 -(m : \u2102) := by\n have hopen : IsOpen {s : \u2102 | 0 < (((1 + s) / 2).re)} := by\n have hcont : Continuous (fun s : \u2102 => (((1 + s) / 2).re)) := by\n have h1 : Continuous (fun s : \u2102 => (1 + s) / 2) :=\n (continuous_const.add continuous_id).div_const (2 : \u2102)\n exact Complex.continuous_re.comp h1\n exact isOpen_Ioi.preimage hcont\n have hmem : (0 : \u2102) \u2208 {s : \u2102 | 0 < (((1 + s) / 2).re)} := by\n show 0 < (((1 + (0 : \u2102)) / 2).re)\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e]\n simp\n filter_upwards [hopen.mem_nhds hmem] with s hs\n intro m hmeq\n rw [hmeq] at hs\n simp at hs\n have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n exact \u27e8h1, h2\u27e9\n\n/-- **Piece (A), the archimedean Taylor coefficients (D-066 \u00a74)**: for all j,\n iteratedDeriv j (fun s => logDeriv Gamma\u211d (1+s)) 0 = (\u22121)^{j+1}\u00b7j!\u00b7\u2191lagariasA(j+1). -/\ntheorem iteratedDeriv_logDeriv_Gamma\u211d (j : \u2115) :\n iteratedDeriv j (fun s : \u2102 => logDeriv Complex.Gamma\u211d (1 + s)) 0 =\n ((-1 : \u2102)) ^ (j + 1) * (j ! : \u2102) * (lagariasA (j + 1) : \u211d) := by\n rcases Nat.eq_zero_or_pos j with hj0 | hj0\n \u00b7 subst hj0\n rw [iteratedDeriv_zero]\n rw [lagariasA, if_pos rfl]\n simp [logDeriv_Gamma\u211d_one]\n \u00b7 have hj : 1 \u2264 j := hj0\n obtain \u27e8hG, hpole\u27e9 := eventually_Gamma_ne_zero_and_pole_free\n have hev : (fun s : \u2102 => logDeriv Complex.Gamma\u211d (1 + s)) =\u1da0[\ud835\udcdd (0 : \u2102)]\n (fun s => -(Real.log Real.pi : \u2102) / 2 + (1 / 2) * Complex.digamma ((1 + s) / 2)) := by\n filter_upwards [hG, hpole] with s h1 h2\n exact logDeriv_Gamma\u211d_one_add h1 h2\n rw [iteratedDeriv_congr_of_eventuallyEq hev]\n -- the constant dies for j \u2265 1\n have hsplit2 : (fun s : \u2102 => -(Real.log Real.pi : \u2102) / 2 +\n (1 / 2) * Complex.digamma ((1 + s) / 2)) =\n (fun _ : \u2102 => -(Real.log Real.pi : \u2102) / 2) +\n (fun s => (1 / 2) * Complex.digamma ((1 + s) / 2)) := rfl\n rw [hsplit2]\n have hcd0 : ContDiffAt \u2102 j (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have h1 : AnalyticAt \u2102 Complex.digamma ((1 : \u2102) / 2) :=\n digamma_analyticOn _ dpsiDomain_half\n have h2 : AnalyticAt \u2102 (fun s : \u2102 => (1 + s) / 2) 0 :=\n (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)\n have h3 := AnalyticAt.comp (g := fun s : \u2102 => (1 + s) / 2) h1 h2\n have heq : (Complex.digamma \u2218 (fun s : \u2102 => (1 + s) / 2)) =\n fun s => Complex.digamma ((1 + s) / 2) := rfl\n rw [heq] at h3\n exact h3.contDiffAt\n have hcd : ContDiffAt \u2102 j (fun s => (1 / 2) * Complex.digamma ((1 + s) / 2)) 0 :=\n (contDiff_const (\ud835\udd5c := \u2102) (c := (1 / 2 : \u2102))).contDiffAt.mul hcd0\n rw [iteratedDeriv_add contDiff_const.contDiffAt hcd]\n rw [iteratedDeriv_const, if_neg (by omega : j \u2260 0), zero_add]\n rw [iteratedDeriv_const_mul (1 / 2 : \u2102) hcd0]\n rw [iteratedDeriv_one_add_div_two Complex.digamma j (by\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e]\n exact digamma_analyticOn _ dpsiDomain_half) (by\n have hcont : Tendsto (fun s : \u2102 => (1 + s) / 2) (\ud835\udcdd 0) (\ud835\udcdd ((1 + (0 : \u2102)) / 2)) := by\n have hc : ContinuousAt (fun s : \u2102 => (1 + s) / 2) 0 := by\n have h := (continuousAt_const.add continuousAt_id : ContinuousAt (fun s : \u2102 => 1 + s) 0)\n simpa using h.div_const (2 : \u2102)\n exact hc.tendsto\n have h1 : ((1 + (0 : \u2102)) / 2) = 1 / 2 := by ring\n rw [h1] at hcont\n exact hcont.eventually ((digamma_analyticOn _ dpsiDomain_half).eventually_analyticAt))]\n rw [iteratedDeriv_digamma_half_value j hj]\n have h2pow : ((1 : \u2102) / 2) * ((1 : \u2102) / 2) ^ j * (2 : \u2102) ^ (j + 1) = 1 := by\n rw [show ((1 : \u2102) / 2) * ((1 : \u2102) / 2) ^ j = ((1 : \u2102) / 2) ^ (j + 1) from by\n rw [pow_succ]; ring]\n rw [\u2190 mul_pow]\n simp\n have hkey : (1 / 2 : \u2102) * ((1 / 2 : \u2102) ^ j *\n (((-1 : \u2102)) ^ (j + 1) * (j ! : \u2102) * ((2 : \u2102) ^ (j + 1) * (lagariasA (j + 1) : \u211d)))) =\n ((-1 : \u2102)) ^ (j + 1) * (j ! : \u2102) * (lagariasA (j + 1) : \u211d) := by\n rw [show (1 / 2 : \u2102) * ((1 / 2 : \u2102) ^ j * (((-1 : \u2102)) ^ (j + 1) * (j ! : \u2102) *\n ((2 : \u2102) ^ (j + 1) * (lagariasA (j + 1) : \u211d)))) =\n (((1 : \u2102) / 2) * ((1 : \u2102) / 2) ^ j * (2 : \u2102) ^ (j + 1)) *\n (((-1 : \u2102)) ^ (j + 1) * (j ! : \u2102) * (lagariasA (j + 1) : \u211d)) by ring]\n rw [h2pow]\n ring\n exact hkey\n",
"structuredPatch": [
{
"oldStart": 209,
"oldLines": 11,
"newStart": 209,
"newLines": 12,
"lines": [
" (fun s => (1 / 2) * Complex.digamma ((1 + s) / 2)) := rfl",
" rw [hsplit2]",
" have hcd0 : ContDiffAt \u2102 j (fun s => Complex.digamma ((1 + s) / 2)) 0 := by",
"- have h1 : AnalyticAt \u2102 Complex.digamma ((1 : \u2102) / 2) :=",
"- digamma_analyticOn _ dpsiDomain_half",
"+ have h1 : AnalyticAt \u2102 Complex.digamma ((fun s : \u2102 => (1 + s) / 2) 0) := by",
"+ convert digamma_analyticOn _ dpsiDomain_half",
"+ simp",
" have h2 : AnalyticAt \u2102 (fun s : \u2102 => (1 + s) / 2) 0 :=",
" (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)",
"- have h3 := AnalyticAt.comp (g := fun s : \u2102 => (1 + s) / 2) h1 h2",
"+ have h3 := AnalyticAt.comp h1 h2",
" have heq : (Complex.digamma \u2218 (fun s : \u2102 => (1 + s) / 2)) =",
" fun s => Complex.digamma ((1 + s) / 2) := rfl",
" rw [heq] at h3"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"`AnalyticAt.comp {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (g ∘ f) x` — NOTE: the OUTER function is `g` and the INNER is `f` — so `AnalyticAt.comp (hg : AnalyticAt g (f x)) (hf : AnalyticAt f x)` — the hg is the OUTER (digamma) and hf is the INNER (the affine). So the call should be `AnalyticAt.comp h1 h2` with h1 : AnalyticAt digamma ((fun s => (1+s)/2) 0) — the point must be `(fun s => (1+s)/2) 0` — the APPLICATION form (f x) with f := the affine. The point in h1 must be `(affine) 0` — the application form — h1's point is (1:ℂ)/2 — the application (fun s => (1+s)/2) 0 beta-reduces to (1+0)/2 which displays as... — the unifier needs (f x) with f := the affine, x := 0 — so the point must be `(fun s => (1+s)/2) 0` — as I noted the beta-reduced form (1+0)/2 mis-unified. Fix: make h1's point EXACTLY `(fun s : ℂ => (1 + s) / 2) 0` — unreduced:\n```lean\n have h1 : AnalyticAt ℂ Complex.digamma ((fun s : ℂ => (1 + s) / 2) 0) := by\n have h0 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) :=\n digamma_analyticOn _ dpsiDomain_half\n have e : ((fun s : ℂ => (1 + s) / 2) 0) = (1 : ℂ) / 2 := by simp -- hmm simp normalizes (1+0)/2 → 1/2? — the point form\n rw [e] -- NO — this rewrites h0's point — wrong direction\n exact h0 -- h0 : AnalyticAt digamma (1/2) — the goal's point ((fun s => (1+s)/2) 0) — defeq beta ✓ exact should accept!\n```\nThe `exact h0` — h0 : AnalyticAt ℂ digamma (1/2) — goal's point ((fun s => (1+s)/2) 0) — defeq via beta+arithmetic — `exact` checks defeq — (fun s => (1+s)/2) 0 ≡ (1+0)/2 ≡ 1/2 ✓ — exact should work IF Lean's defeq does the beta and the numeral arithmetic — (1+0)/2 vs 1/2 — for ℂ — the numeral division — is (1+0)/2 ≡ 1/2 definitionally? — 1+0 in ℂ — as discussed, NOT defeq for ℂ (the addition of OfNat 1 and OfNat 0 — Complex's addition is a structure operation — (1+0).re = 1.re+0.re = 1+0 (real) — real 1+0 — ℝ's addition — also not defeq...). Hmm — so `exact h0` fails on the point defeq. And `show`-based forms normalize to the mis-unifying form. \n\nSOLUTION: keep the point as the UNREDUCED application and prove h1 via a conversion that doesn't normalize: \n```lean\n have h1 : AnalyticAt ℂ Complex.digamma ((fun s : ℂ => (1 + s) / 2) 0) := by\n have h0 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) :=\n digamma_analyticOn _ dpsiDomain_half\n have e : ((fun s : ℂ => (1 + s) / 2) 0) = (1 : ℂ) / 2 := by\n show (1 + (0 : ℂ)) / 2 = 1 / 2 -- hmm — the LHS is the beta of the application\n ring\n rw [e] at h0 ⊢ -- wait — rw [e] at h0 ⊢ — no...\n```\nHmm — the issue: I want h1's point to STAY as the unreduced application. Prove it as: `exact e ▸ h0`? — with e : ((fun s => (1+s)/2) 0) = 1/2 — then h0 : AnalyticAt digamma (1/2) — and I want AnalyticAt digamma ((fun s => (1+s)/2) 0) — that's e ▸ h0 in the reverse: `e.symm ▸ h0` — the ▸ transport: e.symm : 1/2 = ((fun s => (1+s)/2) 0) — h0 ▸ along it: AnalyticAt digamma ((fun s => (1+s)/2) 0) ✓ — but ▸ is finicky. Alternative: `convert h0` — convert produces the point-equality side goal: ((fun s => (1+s)/2) 0) = 1/2 — closed by `simp` (beta + arithmetic) ✓:\n```lean\n have h1 : AnalyticAt ℂ Complex.digamma ((fun s : ℂ => (1 + s) / 2) 0) := by\n convert digamma_analyticOn _ dpsiDomain_half\n simp -- or: show (1+0)/2 = 1/2; ring\n have h3 := AnalyticAt.comp h1 h2 -- h1's point is the application form ✓ comp unifies f := affine ✓\n```\n`convert h0` — h0 : AnalyticAt digamma (1/2) — goal AnalyticAt digamma ((fun s => (1+s)/2) 0) — convert produces the point-eq goal: (1/2) = ((fun s => (1+s)/2) 0)?? or the reverse — then `simp` — the application beta-reduces to (1+0)/2 and simp normalizes to 1/2 ✓ hopefully. If simp's normal form of ((fun s => (1+s)/2) 0) is (1+0)/2 and then... — simp computes (1+0)/2 = 1/2 ✓ (norm_num-ish inside simp? — simp has `add_zero` and numeral division — the (1+0)/2 → 1/2 — simp should handle via add_zero + ... hmm — (1+0)/2 = 1/2 — after add_zero: 1/2 = 1/2 ✓ rfl — simp closes by rfl ✓).\n\nLet me apply this convert approach.","signature":""},{"type":"text","text":"The comp unification needs the point in application form. Using `convert`."},{"type":"tool_use","id":"Edit_572","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiArchimedean.lean","old_string":" have hcd0 : ContDiffAt ℂ j (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have h1 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) :=\n 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 (g := fun s : ℂ => (1 + s) / 2) h1 h2\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","new_string":" have hcd0 : ContDiffAt ℂ j (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have h1 : AnalyticAt ℂ Complex.digamma ((fun s : ℂ => (1 + s) / 2) 0) := by\n convert digamma_analyticOn _ dpsiDomain_half\n simp\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 h1 h2\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"},"extra_content":null}]