← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
thinking (654 chars)
`ContDiffAt.congr_of_eventuallyEq (hf : ContDiffAt 𝕜 n f x) (h : f₁ =ᶠ[𝓝 x] f) : ContDiffAt 𝕜 n f₁ x` — so with f := digamma-form (the smooth one), f₁ := logDeriv Gammaℝ (1+s)-form, h : f₁ =ᶠ f ✓.
`eventually_Gamma_ne_zero_and_pole_free` — unknown in Scratch (it's in NguyenRH1's LiArchimedean, needs the import/open). It's used inside LiArchimedean itself at line 196 ✓ exists in that namespace. My LiCrux imports LiArchimedean + opens NguyenRH1 ✓ will resolve.
`add_pow (x y) (n) : (x+y)^n = ∑ m ∈ range(n+1), x^m * y^(n−m) * ↑(n.choose m)` ✓.
Now rewrite the file — remove the fumbled hG3 sorry block and write the complete file properly in one go.
Signatures confirmed. Rewriting LiCrux.lean completely and properly.
tool: Write
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCrux.lean",
"content": "/-\nLiCrux.lean \u2014 tier ii\u2032-3c: the (4.10-a) assembly and the crux identity\nSf(n) = Res\u2081(n) (D-066 \u00a72; the assembly algebra verified numerically in\nD-064 \u00a73).\n\nThe chain (all k \u2265 1, m := k\u22121):\n- (M) sigmaP k = \u2212gFun^{(m)}(0)/m! [ii\u2032-3b capstone]\n- (FE) gFun^{(m)}(0) = (\u22121)^{m+1}\u00b7gFun^{(m)}(1) [xiL_one_sub]\n- (exp) gFun^{(m)}(1) = (\u22121)^m\u00b7m! \u2212 m!\u00b7lcoeff m\n + (\u22121)^{m+1}\u00b7m!\u00b7a_{m+1} [shift expansion:\n 1/(1+s) + hLiExt + \u0393R\u2032/\u0393R(1+s); pieces (A)/(B) ii\u2032-3a]\n\u27f9 (4.10-a): lcoeff (k\u22121) = (\u22121)^k\u00b7(lagariasA k + sigmaP k) + (\u22121)^{k\u22121}\n\u27f9 the crux: ResW1 n = SInfty n + 1 \u2212 liCoeff n (\u2102), i.e.\n (ResW1 n).re = Sf n, for n \u2265 1.\n\nPerimeter: ZeroCountProp only (inherited via ii\u2032-3b's capstone).\n-/\nimport Mathlib\nimport NguyenRH1.LiMoments\nimport NguyenRH1.LiArchimedean\nimport NguyenRH1.LiZetaCoeff\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The FE relation: gFun^{(m)}(0) = (\u22121)^{m+1}\u00b7gFun^{(m)}(1) -/\n\n/-- The functional equation as a function identity: gFun(1\u2212s) = \u2212gFun(s)\neverywhere (xiL is entire; xiL(1\u2212s) = xiL(s) + chain rule). -/\nlemma gFun_one_sub_fun : (fun s : \u2102 => gFun (1 - s)) = -gFun := by\n have hderiv : \u2200 s : \u2102, deriv xiL (1 - s) = -deriv xiL s := by\n intro s\n have hfun : (fun s : \u2102 => xiL (1 - s)) = xiL := funext xiL_one_sub\n have h2 : deriv (fun s : \u2102 => xiL (1 - s)) s = deriv xiL s := by rw [hfun]\n have h1 : DifferentiableAt \u2102 xiL ((fun s : \u2102 => 1 - s) s) := differentiable_xiL _\n have h2' : DifferentiableAt \u2102 (fun s : \u2102 => 1 - s) s :=\n (differentiableAt_const (1 : \u2102)).sub differentiableAt_id\n have hcomp : deriv (xiL \u2218 fun s : \u2102 => 1 - s) s =\n deriv xiL ((fun s : \u2102 => 1 - s) s) * deriv (fun s : \u2102 => 1 - s) s :=\n deriv_comp s h1 h2'\n have heq : (xiL \u2218 fun s : \u2102 => 1 - s) = fun s : \u2102 => xiL (1 - s) := rfl\n rw [heq] at hcomp\n have hinner : deriv (fun s : \u2102 => 1 - s) s = -1 := by\n have h0' : HasDerivAt (fun s : \u2102 => 1 - s) (0 - 1) s :=\n (hasDerivAt_const s (1 : \u2102)).sub (hasDerivAt_id' s)\n rw [h0'.deriv]\n norm_num\n rw [hinner] at hcomp\n simp at hcomp\n rw [hcomp] at h2\n linear_combination -h2\n funext s\n rw [Pi.neg_apply, gFun, gFun, logDeriv_apply, logDeriv_apply, xiL_one_sub, hderiv s,\n neg_div]\n\n/-- The FE derivative relation (D-066 \u00a72): gFun^{(m)}(0) =\n(\u22121)^{m+1}\u00b7gFun^{(m)}(1), via the unconditional\n`iteratedDeriv_comp_const_sub` + `iteratedDeriv_neg`. -/\nlemma iteratedDeriv_gFun_zero (m : \u2115) :\n iteratedDeriv m gFun 0 = ((-1 : \u2102)) ^ (m + 1) * iteratedDeriv m gFun 1 := by\n have h1 := congr_fun (iteratedDeriv_comp_const_sub m gFun (1 : \u2102)) 0\n rw [sub_zero, smul_eq_mul] at h1\n rw [gFun_one_sub_fun, iteratedDeriv_neg] at h1\n linear_combination -h1\n\n/-! ## 2. The shift expansion: gFun(1+s) = 1/(1+s) + hLiExt s + \u0393R\u2032/\u0393R(1+s) -/\n\n/-- The punctured form of the shift expansion (pure logDeriv algebra at\n1+s, mirroring `gFun_eq_momentB`; no perimeter needed). -/\nlemma gFun_one_add_punctured :\n \u2200\u1da0 s in \ud835\udcdd[\u2260] (0 : \u2102), gFun (1 + s) =\n 1 / (1 + s) + hLiExt s + logDeriv Complex.Gamma\u211d (1 + s) := by\n -- eventually facts on \ud835\udcdd 0\n have hZA : \u2200\u1da0 s in \ud835\udcdd (0 : \u2102), zetaA (1 + s) \u2260 0 := by\n have h1 : Tendsto (fun s : \u2102 => 1 + s) (\ud835\udcdd 0) (\ud835\udcdd (1 + (0 : \u2102))) :=\n (continuousAt_const.add continuousAt_id).tendsto\n rw [add_zero] at h1\n exact h1.eventually zetaA_ne_zero_near_one\n have h\u03931 : \u2200 m : \u2115, (1 : \u2102) / 2 \u2260 -(m : \u2102) := by\n intro m hm\n have e := congrArg Complex.re hm\n have e2 : ((-((m : \u211d) : \u2102))).re = -(m : \u211d) := by simp\n have e3 : ((1 : \u2102) / 2).re = 1 / 2 := by simp\n rw [e3, e2] at e\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n have h\u0393cont : ContinuousAt Complex.Gamma\u211d 1 :=\n (differentiableAt_Gamma\u211d_of_not_neg_nat h\u03931).continuousAt\n have h\u0393 : \u2200\u1da0 s in \ud835\udcdd (0 : \u2102), Complex.Gamma\u211d (1 + s) \u2260 0 := by\n have h1 : Tendsto (fun s : \u2102 => 1 + s) (\ud835\udcdd 0) (\ud835\udcdd (1 + (0 : \u2102))) :=\n (continuousAt_const.add continuousAt_id).tendsto\n rw [add_zero] at h1\n exact h1.eventually ((h\u0393cont.tendsto).eventually_ne (by\n rw [Complex.Gamma\u211d_one]; norm_num))\n have hpole : \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)) :=\n Complex.continuous_re.comp ((continuous_const.add continuous_id).div_const 2)\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 filter_upwards [self_mem_nhdsWithin, hZA.filter_mono nhdsWithin_le_nhds,\n h\u0393.filter_mono nhdsWithin_le_nhds, hpole.filter_mono nhdsWithin_le_nhds,\n (eventually_ne_nhds (show (0 : \u2102) \u2260 -1 by norm_num)).filter_mono nhdsWithin_le_nhds]\n with s hs0 hZAs h\u0393s hpols hs1\n -- point hypotheses\n have hs1' : (1 : \u2102) + s \u2260 1 := by\n intro h\n apply hs0\n linear_combination h\n have hs0' : (1 : \u2102) + s \u2260 0 := by\n intro h\n apply hs1\n linear_combination h\n have h\u03b6s : riemannZeta (1 + s) \u2260 0 := by\n intro h\u03b6\n have e := zetaA_apply hs1'\n rw [h\u03b6, mul_zero] at e\n exact hZAs e\n have h\u0393diff : DifferentiableAt \u2102 Complex.Gamma\u211d (1 + s) :=\n differentiableAt_Gamma\u211d_of_not_neg_nat hpols\n -- the logDeriv algebra at 1+s (the gFun_eq_momentB pattern)\n have hopen : IsOpen ({0}\u1d9c \u2229 {1}\u1d9c : Set \u2102) :=\n isOpen_compl_singleton.inter isOpen_compl_singleton\n have hexp : xiL =\u1da0[\ud835\udcdd (1 + s)]\n (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) := by\n filter_upwards [hopen.mem_nhds \u27e8hs0', hs1'\u27e9] with t ht\n exact xiL_eq_mul ht.1 ht.2\n have h\u039beq : completedRiemannZeta =\u1da0[\ud835\udcdd (1 + s)]\n (fun t => Complex.Gamma\u211d t * riemannZeta t) := by\n filter_upwards [h\u0393diff.continuousAt.eventually_ne h\u0393s, eventually_ne_nhds hs0']\n with t ht\u0393 ht0\n rw [riemannZeta_def_of_ne_zero ht0]\n field_simp [ht\u0393]\n have hlog : logDeriv xiL (1 + s) =\n logDeriv (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) (1 + s) := by\n rw [logDeriv_apply, logDeriv_apply, hexp.deriv_eq, hexp.eq_of_nhds]\n show logDeriv xiL (1 + s) = _\n rw [hlog]\n have hP : DifferentiableAt \u2102 (fun t : \u2102 => t * (t - 1) / 2) (1 + s) :=\n (differentiableAt_id.mul (differentiableAt_id.sub_const 1)).div_const 2\n have h\u039b : DifferentiableAt \u2102 completedRiemannZeta (1 + s) :=\n differentiableAt_completedZeta hs0' hs1'\n have hP0 : (1 + s) * ((1 + s) - 1) / 2 \u2260 0 :=\n div_ne_zero (mul_ne_zero hs0' (sub_ne_zero.mpr hs1')) two_ne_zero\n have h\u039b0 : completedRiemannZeta (1 + s) \u2260 0 := by\n rw [Ne, RvM.completedRiemannZeta_eq_zero_iff]\n rintro h\n exact h\u03b6s h.1\n rw [logDeriv_mul (f := fun t : \u2102 => t * (t - 1) / 2) (g := completedRiemannZeta) _\n hP0 h\u039b0 hP h\u039b]\n have hPlog : logDeriv (fun t : \u2102 => t * (t - 1) / 2) (1 + s) =\n 1 / (1 + s) + 1 / s := by\n rw [logDeriv_apply]\n have hderiv : deriv (fun t : \u2102 => t * (t - 1) / 2) (1 + s) = (1 + s) - 1 / 2 := by\n have h2' : HasDerivAt (fun t : \u2102 => t * (t - 1) / 2)\n ((1 * ((1 + s) - 1) + (1 + s) * 1) / 2) (1 + s) :=\n ((hasDerivAt_id' (1 + s)).mul ((hasDerivAt_id' (1 + s)).sub_const 1)).div_const 2\n rw [h2'.deriv]\n ring\n rw [hderiv, show ((1 : \u2102) + s) - 1 = s by ring]\n field_simp [hs0', hs0]\n ring\n have hlog\u039b : logDeriv completedRiemannZeta (1 + s) =\n logDeriv Complex.Gamma\u211d (1 + s) + logDeriv riemannZeta (1 + s) := by\n have heq : logDeriv completedRiemannZeta (1 + s) =\n logDeriv (fun t => Complex.Gamma\u211d t * riemannZeta t) (1 + s) := by\n rw [logDeriv_apply, logDeriv_apply, h\u039beq.deriv_eq, h\u039beq.eq_of_nhds]\n rw [heq, logDeriv_mul (f := Complex.Gamma\u211d) (g := riemannZeta) _ h\u0393s h\u03b6s h\u0393diff\n (differentiableAt_riemannZeta hs1')]\n rw [hPlog, hlog\u039b]\n -- the hLiExt identity: hLiExt s = 1/s + \u03b6\u2032/\u03b6(1+s)\n have hE : hLiExt s = 1 / s + logDeriv riemannZeta (1 + s) := by\n rw [hLiExt_of_ne hs0]\n have hh : hLi (1 + s) = 1 - s * (deriv zetaA (1 + s) / zetaA (1 + s)) := by\n rw [hLi]\n ring_nf\n rw [hh]\n have hX : (1 - (1 - s * (deriv zetaA (1 + s) / zetaA (1 + s)))) / s =\n deriv zetaA (1 + s) / zetaA (1 + s) := by\n field_simp [hs0]\n rw [hX]\n have hzeq : (fun w : \u2102 => (w - 1) * riemannZeta w) =\u1da0[\ud835\udcdd (1 + s)] zetaA := by\n filter_upwards [eventually_ne_nhds hs1'] with z hz\n exact (zetaA_apply hz).symm\n have hderiv_zetaA : deriv zetaA (1 + s) =\n riemannZeta (1 + s) + s * deriv riemannZeta (1 + s) := by\n rw [\u2190 hzeq.deriv_eq]\n have hsplit : (fun w : \u2102 => (w - 1) * riemannZeta w) =\n (fun w : \u2102 => w - 1) * riemannZeta := rfl\n rw [hsplit, deriv_mul (differentiableAt_id.sub_const 1)\n (differentiableAt_riemannZeta hs1')]\n have h1 : deriv (fun w : \u2102 => w - 1) (1 + s) = 1 := by\n simpa using ((hasDerivAt_id' (1 + s)).sub_const 1).deriv\n rw [h1]\n ring\n rw [hderiv_zetaA, zetaA_apply hs1', logDeriv_apply]\n field_simp [hs0, h\u03b6s]\n ring\n rw [hE]\n ring\n\n/-- The shift expansion on a full neighbourhood of 0 (both sides are\ncontinuous at 0; the point value comes from `eq_of_eventuallyEq_nhd_ne`). -/\nlemma gFun_one_add_eventuallyEq :\n (fun s : \u2102 => gFun (1 + s)) =\u1da0[\ud835\udcdd (0 : \u2102)]\n fun s => 1 / (1 + s) + hLiExt s + logDeriv Complex.Gamma\u211d (1 + s) := by\n have hp := gFun_one_add_punctured\n have hFcont : ContinuousAt (fun s : \u2102 => gFun (1 + s)) 0 := by\n have hg : ContinuousAt gFun 1 := gFun_continuousAt 1 (by rw [xiL_one]; norm_num)\n have hc : ContinuousAt (fun s : \u2102 => 1 + s) 0 := continuousAt_const.add continuousAt_id\n have hcomp := hg.comp hc\n have heq : (gFun \u2218 fun s : \u2102 => 1 + s) = fun s : \u2102 => gFun (1 + s) := rfl\n rw [heq] at hcomp\n exact hcomp\n have hG3 : ContDiffAt \u2102 1 (fun s : \u2102 => logDeriv Complex.Gamma\u211d (1 + s)) 0 := by\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 have hcd0 : ContDiffAt \u2102 1 (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_of_eq h1 h2 (by show (1 + (0 : \u2102)) / 2 = 1 / 2; ring)\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 1 (fun s : \u2102 => -(Real.log Real.pi : \u2102) / 2 +\n (1 / 2) * Complex.digamma ((1 + s) / 2)) 0 :=\n contDiff_const.contDiffAt.add ((contDiff_const (\ud835\udd5c := \u2102) (c := (1 / 2 : \u2102))).contDiffAt.mul hcd0)\n exact hcd.congr_of_eventuallyEq hev.symm\n have hGcont : ContinuousAt (fun s : \u2102 =>\n 1 / (1 + s) + hLiExt s + logDeriv Complex.Gamma\u211d (1 + s)) 0 := by\n have hc1 : ContinuousAt (fun s : \u2102 => 1 / (1 + s)) 0 :=\n ContinuousAt.div continuousAt_const (continuousAt_const.add continuousAt_id) (by norm_num)\n have hc2 : ContinuousAt hLiExt 0 := hLiExt_analyticAt_zero.continuousAt\n have hc3 : ContinuousAt (fun s : \u2102 => logDeriv Complex.Gamma\u211d (1 + s)) 0 :=\n hG3.continuousAt\n exact (hc1.add hc2).add hc3\n have hpt := eq_of_eventuallyEq_nhd_ne hFcont hGcont hp\n rw [eventually_nhdsWithin_iff] at hp\n filter_upwards [hp] with s hs\n by_cases h0 : s = 0\n \u00b7 subst h0\n exact hpt\n \u00b7 exact hs h0\n\n/-! ## 3. The coefficient extraction at 1 -/\n\n/-- The m-th derivative of the 1/(1+s) piece: (\u22121)^m\u00b7m!. -/\nlemma iteratedDeriv_one_div_one_add (m : \u2115) :\n iteratedDeriv m (fun s : \u2102 => 1 / (1 + s)) 0 = ((-1 : \u2102)) ^ m * (m ! : \u2102) := by\n have e : (fun s : \u2102 => 1 / (1 + s)) = fun s : \u2102 => (s + 1) ^ (-1 : \u2124) := by\n funext s\n rw [zpow_neg_one, one_div]\n congr 1\n ring\n rw [e, iteratedDeriv_zpow_neg_one m 1 (by norm_num : (0 : \u2102) + 1 \u2260 0), zero_add, one_zpow,\n mul_one]\n\n/-- **The shift coefficient extraction**: gFun^{(m)}(1) =\n(\u22121)^m\u00b7m! \u2212 m!\u00b7lcoeff m + (\u22121)^{m+1}\u00b7m!\u00b7a_{m+1}. -/\nlemma iteratedDeriv_gFun_one (hZC : ZeroCountProp) (m : \u2115) :\n iteratedDeriv m gFun 1 =\n ((-1 : \u2102)) ^ m * (m ! : \u2102) - (m ! : \u2102) * lcoeff m +\n ((-1 : \u2102)) ^ (m + 1) * (m ! : \u2102) * (lagariasA (m + 1) : \u211d) := by\n have hcomp := congr_fun (iteratedDeriv_comp_add_const m gFun (1 : \u2102)) 0\n rw [zero_add] at hcomp\n rw [\u2190 hcomp]\n have e0 : (fun z : \u2102 => gFun (z + 1)) = fun s : \u2102 => gFun (1 + s) :=\n funext fun s => by rw [add_comm]\n rw [e0, iteratedDeriv_congr_of_eventuallyEq gFun_one_add_eventuallyEq m]\n have h1 : ContDiffAt \u2102 m (fun s : \u2102 => 1 / (1 + s)) 0 :=\n (analyticAt_const.div (analyticAt_const.add analyticAt_id) (by norm_num)).contDiffAt\n have h2 : ContDiffAt \u2102 m hLiExt 0 := hLiExt_analyticAt_zero.contDiffAt\n have h3 : ContDiffAt \u2102 m (fun s : \u2102 => logDeriv Complex.Gamma\u211d (1 + s)) 0 := by\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 hs1 hs2\n exact logDeriv_Gamma\u211d_one_add hs1 hs2\n have hcd0 : ContDiffAt \u2102 m (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have ha1 : AnalyticAt \u2102 Complex.digamma ((1 : \u2102) / 2) :=\n digamma_analyticOn _ dpsiDomain_half\n have ha2 : AnalyticAt \u2102 (fun s : \u2102 => (1 + s) / 2) 0 :=\n (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)\n have ha3 := AnalyticAt.comp_of_eq ha1 ha2 (by show (1 + (0 : \u2102)) / 2 = 1 / 2; ring)\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 ha3\n exact ha3.contDiffAt\n have hcd : ContDiffAt \u2102 m (fun s : \u2102 => -(Real.log Real.pi : \u2102) / 2 +\n (1 / 2) * Complex.digamma ((1 + s) / 2)) 0 :=\n contDiff_const.contDiffAt.add ((contDiff_const (\ud835\udd5c := \u2102) (c := (1 / 2 : \u2102))).contDiffAt.mul hcd0)\n exact hcd.congr_of_eventuallyEq hev.symm\n have hsplit : (fun s : \u2102 => 1 / (1 + s) + hLiExt s + logDeriv Complex.Gamma\u211d (1 + s)) =\n (fun s : \u2102 => 1 / (1 + s)) + hLiExt + (fun s : \u2102 => logDeriv Complex.Gamma\u211d (1 + s)) :=\n rfl\n rw [hsplit, iteratedDeriv_add (h1.add h2) h3, iteratedDeriv_add h1 h2,\n iteratedDeriv_one_div_one_add, iteratedDeriv_hLiExt m, iteratedDeriv_logDeriv_Gamma\u211d m]\n ring\n\n/-! ## 4. The (4.10-a) assembly -/\n\n/-- **Lagarias (4.10), a-form (D-066 \u00a70)**: for all k \u2265 1,\nlcoeff (k\u22121) = (\u22121)^k\u00b7(lagariasA k + sigmaP k) + (\u22121)^{k\u22121}.\nThe assembly algebra of D-066 \u00a72 with the multiplied-out\nlinear_combination (the (m! : \u2102) \u2260 0 clear + the (\u22121)^{m+1}-square\nsign relation). Perimeter: ZeroCountProp only. -/\ntheorem lagarias_4_10_a (hZC : ZeroCountProp) {k : \u2115} (hk : 1 \u2264 k) :\n lcoeff (k - 1) =\n ((-1 : \u2102)) ^ k * ((lagariasA k : \u211d) + sigmaP k) + ((-1 : \u2102)) ^ (k - 1) := by\n obtain \u27e8m, rfl\u27e9 := Nat.exists_eq_succ_of_ne_zero (by omega : k \u2260 0)\n rw [Nat.add_sub_cancel]\n have hF : ((m ! : \u2115) : \u2102) \u2260 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero m)\n have hM := sigmaP_eq_neg_iteratedDeriv_gFun_div hZC (by omega : 1 \u2264 m + 1)\n rw [Nat.add_sub_cancel] at hM\n have hM2 : (m ! : \u2102) * sigmaP (m + 1) = -iteratedDeriv m gFun 0 := by\n rw [hM]\n field_simp [hF]\n have hFE := iteratedDeriv_gFun_zero m\n have hExp := iteratedDeriv_gFun_one hZC m\n have ht_sq : ((-1 : \u2102)) ^ (m + 1) * ((-1 : \u2102)) ^ (m + 1) = 1 := by\n rw [\u2190 pow_add, show (m + 1) + (m + 1) = 2 * (m + 1) by ring, pow_mul,\n show ((-1 : \u2102)) ^ 2 = 1 by norm_num, one_pow]\n have hgoal : (m ! : \u2102) * lcoeff m =\n (m ! : \u2102) * (((-1 : \u2102)) ^ (m + 1) * ((lagariasA (m + 1) : \u211d)) +\n ((-1 : \u2102)) ^ (m + 1) * sigmaP (m + 1) + ((-1 : \u2102)) ^ m) := by\n linear_combination\n (-((-1 : \u2102)) ^ (m + 1)) * hM2 + ((-1 : \u2102)) ^ (m + 1) * hFE +\n ((-1 : \u2102)) ^ (m + 1) * ((-1 : \u2102)) ^ (m + 1) * hExp +\n (-(m ! : \u2102) * lcoeff m + ((-1 : \u2102)) ^ (m + 1) * (m ! : \u2102) * (lagariasA (m + 1) : \u211d) +\n ((-1 : \u2102)) ^ m * (m ! : \u2102)) * ht_sq\n have hgoal2 : (m ! : \u2102) * lcoeff m =\n (m ! : \u2102) * (((-1 : \u2102)) ^ (m + 1) * (((lagariasA (m + 1) : \u211d)) + sigmaP (m + 1)) +\n ((-1 : \u2102)) ^ m) := by\n linear_combination hgoal\n exact mul_left_cancel\u2080 hF hgoal2\n\n/-! ## 5. The crux: Sf(n) = Res\u2081(n) -/\n\n/-- **The crux identity** (D-064 \u00a73, D-066 \u00a75): for n \u2265 1,\nResW1 n = SInfty n + 1 \u2212 liCoeff n (as \u2102), i.e. (ResW1 n).re = Sf n.\nVia ResW1_eq_sum + (4.10-a) + the two ii\u2032-2 swaps + the binomial sum\n\u03a3_{j=1}^n (\u22121)^{j\u22121}C(n,j) = 1. -/\ntheorem sf_eq_resW1 (hZC : ZeroCountProp) {n : \u2115} (hn : 1 \u2264 n) :\n (ResW1 n).re = Sf n := by\n -- the binomial sums\n have hsign : \u2200 j : \u2115, 1 \u2264 j \u2192 ((-1 : \u2102)) ^ (j - 1) = -((-1 : \u2102)) ^ j := by\n intro j hj\n have e : j - 1 + 1 = j := by omega\n calc ((-1 : \u2102)) ^ (j - 1) = -(((-1 : \u2102)) ^ (j - 1) * (-1 : \u2102)) := by ring\n _ = -((-1 : \u2102)) ^ (j - 1 + 1) := by rw [pow_succ]\n _ = -((-1 : \u2102)) ^ j := by rw [e]\n have hbinom : (\u2211 j \u2208 Finset.Icc 1 n, (-1 : \u2102) ^ j * (n.choose j : \u2102)) = -1 := by\n have h := add_pow (-1 : \u2102) 1 n\n rw [neg_add_cancel, zero_pow (by omega : n \u2260 0)] at h\n rw [Finset.sum_congr rfl (fun j _ => by rw [one_pow, mul_one] :\n \u2200 j \u2208 Finset.range (n + 1), (-1 : \u2102) ^ j * 1 ^ (n - j) * (n.choose j : \u2102) =\n (-1 : \u2102) ^ j * (n.choose j : \u2102))] at h\n rw [show Finset.range (n + 1) = insert 0 (Finset.Icc 1 n) from by\n ext j\n simp [Finset.mem_range, Finset.mem_Icc]\n omega] at h\n rw [Finset.sum_insert (by simp)] at h\n rw [pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one] at h\n linear_combination -h\n have hS3 : (\u2211 j \u2208 Finset.Icc 1 n, (-1 : \u2102) ^ (j - 1) * (n.choose j : \u2102)) = 1 := by\n have e : (\u2211 j \u2208 Finset.Icc 1 n, (-1 : \u2102) ^ (j - 1) * (n.choose j : \u2102)) =\n \u2211 j \u2208 Finset.Icc 1 n, -((-1 : \u2102) ^ j * (n.choose j : \u2102)) :=\n Finset.sum_congr rfl (fun j hj => by rw [hsign j (Finset.mem_Icc.mp hj).1, neg_mul])\n rw [e, Finset.sum_neg_distrib, hbinom, neg_neg]\n have hS : ((SInfty n : \u211d) : \u2102) =\n \u2211 j \u2208 Finset.Icc 1 n, (-1 : \u2102) ^ j * (n.choose j : \u2102) * (lagariasA j : \u211d) := by\n have h := sInfty_eq_sum n hn\n have h2 : ((SInfty n : \u211d) : \u2102) =\n ((\u2211 j \u2208 Finset.Icc 1 n, (-1 : \u211d) ^ j * (n.choose j : \u211d) * lagariasA j : \u211d) : \u2102) := by\n rw [h]\n push_cast at h2\n exact h2\n have hL : (\u2211 j \u2208 Finset.Icc 1 n, (-1 : \u2102) ^ j * (n.choose j : \u2102) * sigmaP j) =\n -liCoeff n := by\n rw [liCoeff_eq_sum_sigma, \u2190 Finset.sum_neg_distrib]\n apply Finset.sum_congr rfl\n intro j _\n ring\n -- the \u2102 identity\n have hid : ResW1 n = ((SInfty n : \u211d) : \u2102) + 1 - liCoeff n := by\n rw [ResW1_eq_sum]\n have hterms : (\u2211 j \u2208 Finset.Icc 1 n, (n.choose j : \u2102) * lcoeff (j - 1)) =\n (\u2211 j \u2208 Finset.Icc 1 n, (-1 : \u2102) ^ j * (n.choose j : \u2102) * (lagariasA j : \u211d)) +\n ((\u2211 j \u2208 Finset.Icc 1 n, (-1 : \u2102) ^ j * (n.choose j : \u2102) * sigmaP j) +\n (\u2211 j \u2208 Finset.Icc 1 n, (-1 : \u2102) ^ (j - 1) * (n.choose j : \u2102))) := by\n rw [\u2190 Finset.sum_add, \u2190 Finset.sum_add]\n apply Finset.sum_congr rfl\n intro j hj\n have hj1 : 1 \u2264 j := (Finset.mem_Icc.mp hj).1\n rw [lagarias_4_10_a hZC hj1]\n simp only [Pi.add_apply]\n ring\n rw [hterms, hS, hL, hS3]\n ring\n rw [hid, Sf]\n simp only [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.one_re]\n\nend NguyenRH1\n"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`ContDiffAt.congr_of_eventuallyEq (hf : ContDiffAt 𝕜 n f x) (h : f₁ =ᶠ[𝓝 x] f) : ContDiffAt 𝕜 n f₁ x` — so with f := digamma-form (the smooth one), f₁ := logDeriv Gammaℝ (1+s)-form, h : f₁ =ᶠ f ✓.\n\n`eventually_Gamma_ne_zero_and_pole_free` — unknown in Scratch (it's in NguyenRH1's LiArchimedean, needs the import/open). It's used inside LiArchimedean itself at line 196 ✓ exists in that namespace. My LiCrux imports LiArchimedean + opens NguyenRH1 ✓ will resolve.\n\n`add_pow (x y) (n) : (x+y)^n = ∑ m ∈ range(n+1), x^m * y^(n−m) * ↑(n.choose m)` ✓.\n\nNow rewrite the file — remove the fumbled hG3 sorry block and write the complete file properly in one go.","signature":""},{"type":"text","text":"Signatures confirmed. Rewriting LiCrux.lean completely and properly."},{"type":"tool_use","id":"Write_103","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCrux.lean","content":"/-\nLiCrux.lean — tier ii′-3c: the (4.10-a) assembly and the crux identity\nSf(n) = Res₁(n) (D-066 §2; the assembly algebra verified numerically in\nD-064 §3).\n\nThe chain (all k ≥ 1, m := k−1):\n- (M) sigmaP k = −gFun^{(m)}(0)/m! [ii′-3b capstone]\n- (FE) gFun^{(m)}(0) = (−1)^{m+1}·gFun^{(m)}(1) [xiL_one_sub]\n- (exp) gFun^{(m)}(1) = (−1)^m·m! − m!·lcoeff m\n + (−1)^{m+1}·m!·a_{m+1} [shift expansion:\n 1/(1+s) + hLiExt + ΓR′/ΓR(1+s); pieces (A)/(B) ii′-3a]\n⟹ (4.10-a): lcoeff (k−1) = (−1)^k·(lagariasA k + sigmaP k) + (−1)^{k−1}\n⟹ the crux: ResW1 n = SInfty n + 1 − liCoeff n (ℂ), i.e.\n (ResW1 n).re = Sf n, for n ≥ 1.\n\nPerimeter: ZeroCountProp only (inherited via ii′-3b's capstone).\n-/\nimport Mathlib\nimport NguyenRH1.LiMoments\nimport NguyenRH1.LiArchimedean\nimport NguyenRH1.LiZetaCoeff\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The FE relation: gFun^{(m)}(0) = (−1)^{m+1}·gFun^{(m)}(1) -/\n\n/-- The functional equation as a function identity: gFun(1−s) = −gFun(s)\neverywhere (xiL is entire; xiL(1−s) = xiL(s) + chain rule). -/\nlemma gFun_one_sub_fun : (fun s : ℂ => gFun (1 - s)) = -gFun := by\n have hderiv : ∀ s : ℂ, deriv xiL (1 - s) = -deriv xiL s := by\n intro s\n have hfun : (fun s : ℂ => xiL (1 - s)) = xiL := funext xiL_one_sub\n have h2 : deriv (fun s : ℂ => xiL (1 - s)) s = deriv xiL s := by rw [hfun]\n have h1 : DifferentiableAt ℂ xiL ((fun s : ℂ => 1 - s) s) := differentiable_xiL _\n have h2' : DifferentiableAt ℂ (fun s : ℂ => 1 - s) s :=\n (differentiableAt_const (1 : ℂ)).sub differentiableAt_id\n have hcomp : deriv (xiL ∘ fun s : ℂ => 1 - s) s =\n deriv xiL ((fun s : ℂ => 1 - s) s) * deriv (fun s : ℂ => 1 - s) s :=\n deriv_comp s h1 h2'\n have heq : (xiL ∘ fun s : ℂ => 1 - s) = fun s : ℂ => xiL (1 - s) := rfl\n rw [heq] at hcomp\n have hinner : deriv (fun s : ℂ => 1 - s) s = -1 := by\n have h0' : HasDerivAt (fun s : ℂ => 1 - s) (0 - 1) s :=\n (hasDerivAt_const s (1 : ℂ)).sub (hasDerivAt_id' s)\n rw [h0'.deriv]\n norm_num\n rw [hinner] at hcomp\n simp at hcomp\n rw [hcomp] at h2\n linear_combination -h2\n funext s\n rw [Pi.neg_apply, gFun, gFun, logDeriv_apply, logDeriv_apply, xiL_one_sub, hderiv s,\n neg_div]\n\n/-- The FE derivative relation (D-066 §2): gFun^{(m)}(0) =\n(−1)^{m+1}·gFun^{(m)}(1), via the unconditional\n`iteratedDeriv_comp_const_sub` + `iteratedDeriv_neg`. -/\nlemma iteratedDeriv_gFun_zero (m : ℕ) :\n iteratedDeriv m gFun 0 = ((-1 : ℂ)) ^ (m + 1) * iteratedDeriv m gFun 1 := by\n have h1 := congr_fun (iteratedDeriv_comp_const_sub m gFun (1 : ℂ)) 0\n rw [sub_zero, smul_eq_mul] at h1\n rw [gFun_one_sub_fun, iteratedDeriv_neg] at h1\n linear_combination -h1\n\n/-! ## 2. The shift expansion: gFun(1+s) = 1/(1+s) + hLiExt s + ΓR′/ΓR(1+s) -/\n\n/-- The punctured form of the shift expansion (pure logDeriv algebra at\n1+s, mirroring `gFun_eq_momentB`; no perimeter needed). -/\nlemma gFun_one_add_punctured :\n ∀ᶠ s in 𝓝[≠] (0 : ℂ), gFun (1 + s) =\n 1 / (1 + s) + hLiExt s + logDeriv Complex.Gammaℝ (1 + s) := by\n -- eventually facts on 𝓝 0\n have hZA : ∀ᶠ s in 𝓝 (0 : ℂ), zetaA (1 + s) ≠ 0 := by\n have h1 : Tendsto (fun s : ℂ => 1 + s) (𝓝 0) (𝓝 (1 + (0 : ℂ))) :=\n (continuousAt_const.add continuousAt_id).tendsto\n rw [add_zero] at h1\n exact h1.eventually zetaA_ne_zero_near_one\n have hΓ1 : ∀ m : ℕ, (1 : ℂ) / 2 ≠ -(m : ℂ) := by\n intro m hm\n have e := congrArg Complex.re hm\n have e2 : ((-((m : ℝ) : ℂ))).re = -(m : ℝ) := by simp\n have e3 : ((1 : ℂ) / 2).re = 1 / 2 := by simp\n rw [e3, e2] at e\n have hm0 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n linarith\n have hΓcont : ContinuousAt Complex.Gammaℝ 1 :=\n (differentiableAt_Gammaℝ_of_not_neg_nat hΓ1).continuousAt\n have hΓ : ∀ᶠ s in 𝓝 (0 : ℂ), Complex.Gammaℝ (1 + s) ≠ 0 := by\n have h1 : Tendsto (fun s : ℂ => 1 + s) (𝓝 0) (𝓝 (1 + (0 : ℂ))) :=\n (continuousAt_const.add continuousAt_id).tendsto\n rw [add_zero] at h1\n exact h1.eventually ((hΓcont.tendsto).eventually_ne (by\n rw [Complex.Gammaℝ_one]; norm_num))\n have hpole : ∀ᶠ s in 𝓝 (0 : ℂ), ∀ m : ℕ, (1 + s) / 2 ≠ -(m : ℂ) := by\n have hopen : IsOpen {s : ℂ | 0 < (((1 + s) / 2).re)} := by\n have hcont : Continuous (fun s : ℂ => (((1 + s) / 2).re)) :=\n Complex.continuous_re.comp ((continuous_const.add continuous_id).div_const 2)\n exact isOpen_Ioi.preimage hcont\n have hmem : (0 : ℂ) ∈ {s : ℂ | 0 < (((1 + s) / 2).re)} := by\n show 0 < (((1 + (0 : ℂ)) / 2).re)\n have e : (1 + (0 : ℂ)) / 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 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n linarith\n filter_upwards [self_mem_nhdsWithin, hZA.filter_mono nhdsWithin_le_nhds,\n hΓ.filter_mono nhdsWithin_le_nhds, hpole.filter_mono nhdsWithin_le_nhds,\n (eventually_ne_nhds (show (0 : ℂ) ≠ -1 by norm_num)).filter_mono nhdsWithin_le_nhds]\n with s hs0 hZAs hΓs hpols hs1\n -- point hypotheses\n have hs1' : (1 : ℂ) + s ≠ 1 := by\n intro h\n apply hs0\n linear_combination h\n have hs0' : (1 : ℂ) + s ≠ 0 := by\n intro h\n apply hs1\n linear_combination h\n have hζs : riemannZeta (1 + s) ≠ 0 := by\n intro hζ\n have e := zetaA_apply hs1'\n rw [hζ, mul_zero] at e\n exact hZAs e\n have hΓdiff : DifferentiableAt ℂ Complex.Gammaℝ (1 + s) :=\n differentiableAt_Gammaℝ_of_not_neg_nat hpols\n -- the logDeriv algebra at 1+s (the gFun_eq_momentB pattern)\n have hopen : IsOpen ({0}ᶜ ∩ {1}ᶜ : Set ℂ) :=\n isOpen_compl_singleton.inter isOpen_compl_singleton\n have hexp : xiL =ᶠ[𝓝 (1 + s)]\n (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) := by\n filter_upwards [hopen.mem_nhds ⟨hs0', hs1'⟩] with t ht\n exact xiL_eq_mul ht.1 ht.2\n have hΛeq : completedRiemannZeta =ᶠ[𝓝 (1 + s)]\n (fun t => Complex.Gammaℝ t * riemannZeta t) := by\n filter_upwards [hΓdiff.continuousAt.eventually_ne hΓs, eventually_ne_nhds hs0']\n with t htΓ ht0\n rw [riemannZeta_def_of_ne_zero ht0]\n field_simp [htΓ]\n have hlog : logDeriv xiL (1 + s) =\n logDeriv (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) (1 + s) := by\n rw [logDeriv_apply, logDeriv_apply, hexp.deriv_eq, hexp.eq_of_nhds]\n show logDeriv xiL (1 + s) = _\n rw [hlog]\n have hP : DifferentiableAt ℂ (fun t : ℂ => t * (t - 1) / 2) (1 + s) :=\n (differentiableAt_id.mul (differentiableAt_id.sub_const 1)).div_const 2\n have hΛ : DifferentiableAt ℂ completedRiemannZeta (1 + s) :=\n differentiableAt_completedZeta hs0' hs1'\n have hP0 : (1 + s) * ((1 + s) - 1) / 2 ≠ 0 :=\n div_ne_zero (mul_ne_zero hs0' (sub_ne_zero.mpr hs1')) two_ne_zero\n have hΛ0 : completedRiemannZeta (1 + s) ≠ 0 := by\n rw [Ne, RvM.completedRiemannZeta_eq_zero_iff]\n rintro h\n exact hζs h.1\n rw [logDeriv_mul (f := fun t : ℂ => t * (t - 1) / 2) (g := completedRiemannZeta) _\n hP0 hΛ0 hP hΛ]\n have hPlog : logDeriv (fun t : ℂ => t * (t - 1) / 2) (1 + s) =\n 1 / (1 + s) + 1 / s := by\n rw [logDeriv_apply]\n have hderiv : deriv (fun t : ℂ => t * (t - 1) / 2) (1 + s) = (1 + s) - 1 / 2 := by\n have h2' : HasDerivAt (fun t : ℂ => t * (t - 1) / 2)\n ((1 * ((1 + s) - 1) + (1 + s) * 1) / 2) (1 + s) :=\n ((hasDerivAt_id' (1 + s)).mul ((hasDerivAt_id' (1 + s)).sub_const 1)).div_const 2\n rw [h2'.deriv]\n ring\n rw [hderiv, show ((1 : ℂ) + s) - 1 = s by ring]\n field_simp [hs0', hs0]\n ring\n have hlogΛ : logDeriv completedRiemannZeta (1 + s) =\n logDeriv Complex.Gammaℝ (1 + s) + logDeriv riemannZeta (1 + s) := by\n have heq : logDeriv completedRiemannZeta (1 + s) =\n logDeriv (fun t => Complex.Gammaℝ t * riemannZeta t) (1 + s) := by\n rw [logDeriv_apply, logDeriv_apply, hΛeq.deriv_eq, hΛeq.eq_of_nhds]\n rw [heq, logDeriv_mul (f := Complex.Gammaℝ) (g := riemannZeta) _ hΓs hζs hΓdiff\n (differentiableAt_riemannZeta hs1')]\n rw [hPlog, hlogΛ]\n -- the hLiExt identity: hLiExt s = 1/s + ζ′/ζ(1+s)\n have hE : hLiExt s = 1 / s + logDeriv riemannZeta (1 + s) := by\n rw [hLiExt_of_ne hs0]\n have hh : hLi (1 + s) = 1 - s * (deriv zetaA (1 + s) / zetaA (1 + s)) := by\n rw [hLi]\n ring_nf\n rw [hh]\n have hX : (1 - (1 - s * (deriv zetaA (1 + s) / zetaA (1 + s)))) / s =\n deriv zetaA (1 + s) / zetaA (1 + s) := by\n field_simp [hs0]\n rw [hX]\n have hzeq : (fun w : ℂ => (w - 1) * riemannZeta w) =ᶠ[𝓝 (1 + s)] zetaA := by\n filter_upwards [eventually_ne_nhds hs1'] with z hz\n exact (zetaA_apply hz).symm\n have hderiv_zetaA : deriv zetaA (1 + s) =\n riemannZeta (1 + s) + s * deriv riemannZeta (1 + s) := by\n rw [← hzeq.deriv_eq]\n have hsplit : (fun w : ℂ => (w - 1) * riemannZeta w) =\n (fun w : ℂ => w - 1) * riemannZeta := rfl\n rw [hsplit, deriv_mul (differentiableAt_id.sub_const 1)\n (differentiableAt_riemannZeta hs1')]\n have h1 : deriv (fun w : ℂ => w - 1) (1 + s) = 1 := by\n simpa using ((hasDerivAt_id' (1 + s)).sub_const 1).deriv\n rw [h1]\n ring\n rw [hderiv_zetaA, zetaA_apply hs1', logDeriv_apply]\n field_simp [hs0, hζs]\n ring\n rw [hE]\n ring\n\n/-- The shift expansion on a full neighbourhood of 0 (both sides are\ncontinuous at 0; the point value comes from `eq_of_eventuallyEq_nhd_ne`). -/\nlemma gFun_one_add_eventuallyEq :\n (fun s : ℂ => gFun (1 + s)) =ᶠ[𝓝 (0 : ℂ)]\n fun s => 1 / (1 + s) + hLiExt s + logDeriv Complex.Gammaℝ (1 + s) := by\n have hp := gFun_one_add_punctured\n have hFcont : ContinuousAt (fun s : ℂ => gFun (1 + s)) 0 := by\n have hg : ContinuousAt gFun 1 := gFun_continuousAt 1 (by rw [xiL_one]; norm_num)\n have hc : ContinuousAt (fun s : ℂ => 1 + s) 0 := continuousAt_const.add continuousAt_id\n have hcomp := hg.comp hc\n have heq : (gFun ∘ fun s : ℂ => 1 + s) = fun s : ℂ => gFun (1 + s) := rfl\n rw [heq] at hcomp\n exact hcomp\n have hG3 : ContDiffAt ℂ 1 (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 have hcd0 : ContDiffAt ℂ 1 (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_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 have hcd : ContDiffAt ℂ 1 (fun s : ℂ => -(Real.log Real.pi : ℂ) / 2 +\n (1 / 2) * Complex.digamma ((1 + s) / 2)) 0 :=\n contDiff_const.contDiffAt.add ((contDiff_const (𝕜 := ℂ) (c := (1 / 2 : ℂ))).contDiffAt.mul hcd0)\n exact hcd.congr_of_eventuallyEq hev.symm\n have hGcont : ContinuousAt (fun s : ℂ =>\n 1 / (1 + s) + hLiExt s + logDeriv Complex.Gammaℝ (1 + s)) 0 := by\n have hc1 : ContinuousAt (fun s : ℂ => 1 / (1 + s)) 0 :=\n ContinuousAt.div continuousAt_const (continuousAt_const.add continuousAt_id) (by norm_num)\n have hc2 : ContinuousAt hLiExt 0 := hLiExt_analyticAt_zero.continuousAt\n have hc3 : ContinuousAt (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) 0 :=\n hG3.continuousAt\n exact (hc1.add hc2).add hc3\n have hpt := eq_of_eventuallyEq_nhd_ne hFcont hGcont hp\n rw [eventually_nhdsWithin_iff] at hp\n filter_upwards [hp] with s hs\n by_cases h0 : s = 0\n · subst h0\n exact hpt\n · exact hs h0\n\n/-! ## 3. The coefficient extraction at 1 -/\n\n/-- The m-th derivative of the 1/(1+s) piece: (−1)^m·m!. -/\nlemma iteratedDeriv_one_div_one_add (m : ℕ) :\n iteratedDeriv m (fun s : ℂ => 1 / (1 + s)) 0 = ((-1 : ℂ)) ^ m * (m ! : ℂ) := by\n have e : (fun s : ℂ => 1 / (1 + s)) = fun s : ℂ => (s + 1) ^ (-1 : ℤ) := by\n funext s\n rw [zpow_neg_one, one_div]\n congr 1\n ring\n rw [e, iteratedDeriv_zpow_neg_one m 1 (by norm_num : (0 : ℂ) + 1 ≠ 0), zero_add, one_zpow,\n mul_one]\n\n/-- **The shift coefficient extraction**: gFun^{(m)}(1) =\n(−1)^m·m! − m!·lcoeff m + (−1)^{m+1}·m!·a_{m+1}. -/\nlemma iteratedDeriv_gFun_one (hZC : ZeroCountProp) (m : ℕ) :\n iteratedDeriv m gFun 1 =\n ((-1 : ℂ)) ^ m * (m ! : ℂ) - (m ! : ℂ) * lcoeff m +\n ((-1 : ℂ)) ^ (m + 1) * (m ! : ℂ) * (lagariasA (m + 1) : ℝ) := by\n have hcomp := congr_fun (iteratedDeriv_comp_add_const m gFun (1 : ℂ)) 0\n rw [zero_add] at hcomp\n rw [← hcomp]\n have e0 : (fun z : ℂ => gFun (z + 1)) = fun s : ℂ => gFun (1 + s) :=\n funext fun s => by rw [add_comm]\n rw [e0, iteratedDeriv_congr_of_eventuallyEq gFun_one_add_eventuallyEq m]\n have h1 : ContDiffAt ℂ m (fun s : ℂ => 1 / (1 + s)) 0 :=\n (analyticAt_const.div (analyticAt_const.add analyticAt_id) (by norm_num)).contDiffAt\n have h2 : ContDiffAt ℂ m hLiExt 0 := hLiExt_analyticAt_zero.contDiffAt\n have h3 : 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 hs1 hs2\n exact logDeriv_Gammaℝ_one_add hs1 hs2\n have hcd0 : ContDiffAt ℂ m (fun s => Complex.digamma ((1 + s) / 2)) 0 := by\n have ha1 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) :=\n digamma_analyticOn _ dpsiDomain_half\n have ha2 : AnalyticAt ℂ (fun s : ℂ => (1 + s) / 2) 0 :=\n (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)\n have ha3 := AnalyticAt.comp_of_eq ha1 ha2 (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 ha3\n exact ha3.contDiffAt\n have hcd : ContDiffAt ℂ m (fun s : ℂ => -(Real.log Real.pi : ℂ) / 2 +\n (1 / 2) * Complex.digamma ((1 + s) / 2)) 0 :=\n contDiff_const.contDiffAt.add ((contDiff_const (𝕜 := ℂ) (c := (1 / 2 : ℂ))).contDiffAt.mul hcd0)\n exact hcd.congr_of_eventuallyEq hev.symm\n have hsplit : (fun s : ℂ => 1 / (1 + s) + hLiExt s + logDeriv Complex.Gammaℝ (1 + s)) =\n (fun s : ℂ => 1 / (1 + s)) + hLiExt + (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) :=\n rfl\n rw [hsplit, iteratedDeriv_add (h1.add h2) h3, iteratedDeriv_add h1 h2,\n iteratedDeriv_one_div_one_add, iteratedDeriv_hLiExt m, iteratedDeriv_logDeriv_Gammaℝ m]\n ring\n\n/-! ## 4. The (4.10-a) assembly -/\n\n/-- **Lagarias (4.10), a-form (D-066 §0)**: for all k ≥ 1,\nlcoeff (k−1) = (−1)^k·(lagariasA k + sigmaP k) + (−1)^{k−1}.\nThe assembly algebra of D-066 §2 with the multiplied-out\nlinear_combination (the (m! : ℂ) ≠ 0 clear + the (−1)^{m+1}-square\nsign relation). Perimeter: ZeroCountProp only. -/\ntheorem lagarias_4_10_a (hZC : ZeroCountProp) {k : ℕ} (hk : 1 ≤ k) :\n lcoeff (k - 1) =\n ((-1 : ℂ)) ^ k * ((lagariasA k : ℝ) + sigmaP k) + ((-1 : ℂ)) ^ (k - 1) := by\n obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : k ≠ 0)\n rw [Nat.add_sub_cancel]\n have hF : ((m ! : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero m)\n have hM := sigmaP_eq_neg_iteratedDeriv_gFun_div hZC (by omega : 1 ≤ m + 1)\n rw [Nat.add_sub_cancel] at hM\n have hM2 : (m ! : ℂ) * sigmaP (m + 1) = -iteratedDeriv m gFun 0 := by\n rw [hM]\n field_simp [hF]\n have hFE := iteratedDeriv_gFun_zero m\n have hExp := iteratedDeriv_gFun_one hZC m\n have ht_sq : ((-1 : ℂ)) ^ (m + 1) * ((-1 : ℂ)) ^ (m + 1) = 1 := by\n rw [← pow_add, show (m + 1) + (m + 1) = 2 * (m + 1) by ring, pow_mul,\n show ((-1 : ℂ)) ^ 2 = 1 by norm_num, one_pow]\n have hgoal : (m ! : ℂ) * lcoeff m =\n (m ! : ℂ) * (((-1 : ℂ)) ^ (m + 1) * ((lagariasA (m + 1) : ℝ)) +\n ((-1 : ℂ)) ^ (m + 1) * sigmaP (m + 1) + ((-1 : ℂ)) ^ m) := by\n linear_combination\n (-((-1 : ℂ)) ^ (m + 1)) * hM2 + ((-1 : ℂ)) ^ (m + 1) * hFE +\n ((-1 : ℂ)) ^ (m + 1) * ((-1 : ℂ)) ^ (m + 1) * hExp +\n (-(m ! : ℂ) * lcoeff m + ((-1 : ℂ)) ^ (m + 1) * (m ! : ℂ) * (lagariasA (m + 1) : ℝ) +\n ((-1 : ℂ)) ^ m * (m ! : ℂ)) * ht_sq\n have hgoal2 : (m ! : ℂ) * lcoeff m =\n (m ! : ℂ) * (((-1 : ℂ)) ^ (m + 1) * (((lagariasA (m + 1) : ℝ)) + sigmaP (m + 1)) +\n ((-1 : ℂ)) ^ m) := by\n linear_combination hgoal\n exact mul_left_cancel₀ hF hgoal2\n\n/-! ## 5. The crux: Sf(n) = Res₁(n) -/\n\n/-- **The crux identity** (D-064 §3, D-066 §5): for n ≥ 1,\nResW1 n = SInfty n + 1 − liCoeff n (as ℂ), i.e. (ResW1 n).re = Sf n.\nVia ResW1_eq_sum + (4.10-a) + the two ii′-2 swaps + the binomial sum\nΣ_{j=1}^n (−1)^{j−1}C(n,j) = 1. -/\ntheorem sf_eq_resW1 (hZC : ZeroCountProp) {n : ℕ} (hn : 1 ≤ n) :\n (ResW1 n).re = Sf n := by\n -- the binomial sums\n have hsign : ∀ j : ℕ, 1 ≤ j → ((-1 : ℂ)) ^ (j - 1) = -((-1 : ℂ)) ^ j := by\n intro j hj\n have e : j - 1 + 1 = j := by omega\n calc ((-1 : ℂ)) ^ (j - 1) = -(((-1 : ℂ)) ^ (j - 1) * (-1 : ℂ)) := by ring\n _ = -((-1 : ℂ)) ^ (j - 1 + 1) := by rw [pow_succ]\n _ = -((-1 : ℂ)) ^ j := by rw [e]\n have hbinom : (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ)) = -1 := by\n have h := add_pow (-1 : ℂ) 1 n\n rw [neg_add_cancel, zero_pow (by omega : n ≠ 0)] at h\n rw [Finset.sum_congr rfl (fun j _ => by rw [one_pow, mul_one] :\n ∀ j ∈ Finset.range (n + 1), (-1 : ℂ) ^ j * 1 ^ (n - j) * (n.choose j : ℂ) =\n (-1 : ℂ) ^ j * (n.choose j : ℂ))] at h\n rw [show Finset.range (n + 1) = insert 0 (Finset.Icc 1 n) from by\n ext j\n simp [Finset.mem_range, Finset.mem_Icc]\n omega] at h\n rw [Finset.sum_insert (by simp)] at h\n rw [pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one] at h\n linear_combination -h\n have hS3 : (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j - 1) * (n.choose j : ℂ)) = 1 := by\n have e : (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j - 1) * (n.choose j : ℂ)) =\n ∑ j ∈ Finset.Icc 1 n, -((-1 : ℂ) ^ j * (n.choose j : ℂ)) :=\n Finset.sum_congr rfl (fun j hj => by rw [hsign j (Finset.mem_Icc.mp hj).1, neg_mul])\n rw [e, Finset.sum_neg_distrib, hbinom, neg_neg]\n have hS : ((SInfty n : ℝ) : ℂ) =\n ∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ) * (lagariasA j : ℝ) := by\n have h := sInfty_eq_sum n hn\n have h2 : ((SInfty n : ℝ) : ℂ) =\n ((∑ j ∈ Finset.Icc 1 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * lagariasA j : ℝ) : ℂ) := by\n rw [h]\n push_cast at h2\n exact h2\n have hL : (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ) * sigmaP j) =\n -liCoeff n := by\n rw [liCoeff_eq_sum_sigma, ← Finset.sum_neg_distrib]\n apply Finset.sum_congr rfl\n intro j _\n ring\n -- the ℂ identity\n have hid : ResW1 n = ((SInfty n : ℝ) : ℂ) + 1 - liCoeff n := by\n rw [ResW1_eq_sum]\n have hterms : (∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1)) =\n (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ) * (lagariasA j : ℝ)) +\n ((∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ) * sigmaP j) +\n (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j - 1) * (n.choose j : ℂ))) := by\n rw [← Finset.sum_add, ← Finset.sum_add]\n apply Finset.sum_congr rfl\n intro j hj\n have hj1 : 1 ≤ j := (Finset.mem_Icc.mp hj).1\n rw [lagarias_4_10_a hZC hj1]\n simp only [Pi.add_apply]\n ring\n rw [hterms, hS, hL, hS3]\n ring\n rw [hid, Sf]\n simp only [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.one_re]\n\nend NguyenRH1\n"},"extra_content":null}]