← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
thinking (277 chars)
I was mid-planning. All signatures confirmed, plan is complete. Now write §5/§6 into LiMoments.lean. Keep it in pieces: first append §5 lemmas (zpow, seriesTerm derivative), build-check, then M-test, build-check, then seriesFun_zero, then §6. Let me append the first chunk now.
Signatures confirmed and plan complete. Writing §5 in chunks with build checks between.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiMoments.lean",
"old_string": "/-- **(M) at k = 1**: \u03c3\u2081 = \u2212gFun(0). Via 2\u03c3\u2081 = seriesFun(1) =\ngFun(1) \u2212 B = \u22122\u00b7gFun(0). -/\nlemma sigmaP_one_eq_neg_gFun_zero (hZC : ZeroCountProp) : sigmaP 1 = -gFun 0 := by\n have h2 := two_mul_sigmaP_one\n rw [\u2190 seriesFun_one] at h2\n have hg1 := gFun_one hZC\n have hg0 := gFun_zero hZC\n have hfe := gFun_one_eq_neg\n linear_combination (h2 - hg1 + hg0 + hfe) / 2\n\nend NguyenRH1",
"new_string": "/-- **(M) at k = 1**: \u03c3\u2081 = \u2212gFun(0). Via 2\u03c3\u2081 = seriesFun(1) =\ngFun(1) \u2212 B = \u22122\u00b7gFun(0). -/\nlemma sigmaP_one_eq_neg_gFun_zero (hZC : ZeroCountProp) : sigmaP 1 = -gFun 0 := by\n have h2 := two_mul_sigmaP_one\n rw [\u2190 seriesFun_one] at h2\n have hg1 := gFun_one hZC\n have hg0 := gFun_zero hZC\n have hfe := gFun_one_eq_neg\n linear_combination (h2 - hg1 + hg0 + hfe) / 2\n\n/-! ## 5. Termwise iterated derivation of the series at 0 -/\n\n/-- The iterated derivative of s \u21a6 (s+c)\u207b\u00b9 (positive form, from\nLiDigamma's negative form via `iteratedDeriv_neg`). -/\nlemma iteratedDeriv_zpow_neg_one (k : \u2115) (c : \u2102) {s : \u2102} (hs : s + c \u2260 0) :\n iteratedDeriv k (fun s : \u2102 => (s + c) ^ (-1 : \u2124)) s =\n ((-1 : \u2102)) ^ k * (k ! : \u2102) * (s + c) ^ (-(k : \u2124) - 1) := by\n have e : (fun s : \u2102 => (s + c) ^ (-1 : \u2124)) = -fun s : \u2102 => -((s + c) ^ (-1 : \u2124)) :=\n funext fun s => neg_neg _\n rw [e, iteratedDeriv_neg k _ s, iteratedDeriv_neg_zpow_neg_one_add k c hs, neg_neg]\n\n/-- The k-th iterated derivative (k \u2265 1) of a series summand:\n(d/ds)^k [mult\u00b7(1/(s\u2212\u03c1) + 1/\u03c1)] = mult\u00b7(\u22121)^k\u00b7k!\u00b7(s\u2212\u03c1)^{\u2212k\u22121}. -/\nlemma iteratedDeriv_seriesTerm {j : \u2115} (hj : 1 \u2264 j) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1})\n {s : \u2102} (hs : s - (\u03c1 : \u2102) \u2260 0) :\n iteratedDeriv j (fun s : \u2102 => seriesTerm s \u03c1) s =\n (zeroMult \u03c1 : \u2102) * (((-1 : \u2102)) ^ j * (j ! : \u2102) * (s - (\u03c1 : \u2102)) ^ (-(j : \u2124) - 1)) := by\n have hsp : s + -(\u03c1 : \u2102) \u2260 0 := by\n rw [\u2190 sub_eq_add_neg]\n exact hs\n have e : (fun s : \u2102 => seriesTerm s \u03c1) =\n fun s : \u2102 => (zeroMult \u03c1 : \u2102) * ((s + -(\u03c1 : \u2102)) ^ (-1 : \u2124) + ((\u03c1 : \u2102))\u207b\u00b9) := by\n funext t\n rw [seriesTerm]\n simp only [one_div, zpow_neg_one, sub_eq_add_neg]\n have hcf : ContDiffAt \u2102 j (fun s : \u2102 => (s + -(\u03c1 : \u2102)) ^ (-1 : \u2124)) s := by\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s + -(\u03c1 : \u2102)) s := analyticAt_id.add analyticAt_const\n have h2 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s + -(\u03c1 : \u2102))) s := analyticAt_const.div h1 hsp\n have e2 : (fun s : \u2102 => (s + -(\u03c1 : \u2102)) ^ (-1 : \u2124)) = fun s => 1 / (s + -(\u03c1 : \u2102)) :=\n funext fun t => by rw [zpow_neg_one, one_div]\n rw [e2]\n exact h2.contDiffAt\n have hcc : ContDiffAt \u2102 j (fun _ : \u2102 => ((\u03c1 : \u2102))\u207b\u00b9) s := contDiff_const.contDiffAt\n have hinner : ContDiffAt \u2102 j (fun s : \u2102 => (s + -(\u03c1 : \u2102)) ^ (-1 : \u2124) + ((\u03c1 : \u2102))\u207b\u00b9) s :=\n hcf.add hcc\n rw [e, iteratedDeriv_const_mul _ hinner]\n congr 1\n rw [iteratedDeriv_add hcf hcc, iteratedDeriv_const, if_neg (show j \u2260 0 by omega), add_zero,\n sub_eq_add_neg]\n exact iteratedDeriv_zpow_neg_one j (-(\u03c1 : \u2102)) hsp\n\nend NguyenRH1"
}
raw content_json (database row)
[{"type":"thinking","thinking":"I was mid-planning. All signatures confirmed, plan is complete. Now write §5/§6 into LiMoments.lean. Keep it in pieces: first append §5 lemmas (zpow, seriesTerm derivative), build-check, then M-test, build-check, then seriesFun_zero, then §6. Let me append the first chunk now.","signature":""},{"type":"text","text":"Signatures confirmed and plan complete. Writing §5 in chunks with build checks between."},{"type":"tool_use","id":"Edit_14","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiMoments.lean","old_string":"/-- **(M) at k = 1**: σ₁ = −gFun(0). Via 2σ₁ = seriesFun(1) =\ngFun(1) − B = −2·gFun(0). -/\nlemma sigmaP_one_eq_neg_gFun_zero (hZC : ZeroCountProp) : sigmaP 1 = -gFun 0 := by\n have h2 := two_mul_sigmaP_one\n rw [← seriesFun_one] at h2\n have hg1 := gFun_one hZC\n have hg0 := gFun_zero hZC\n have hfe := gFun_one_eq_neg\n linear_combination (h2 - hg1 + hg0 + hfe) / 2\n\nend NguyenRH1","new_string":"/-- **(M) at k = 1**: σ₁ = −gFun(0). Via 2σ₁ = seriesFun(1) =\ngFun(1) − B = −2·gFun(0). -/\nlemma sigmaP_one_eq_neg_gFun_zero (hZC : ZeroCountProp) : sigmaP 1 = -gFun 0 := by\n have h2 := two_mul_sigmaP_one\n rw [← seriesFun_one] at h2\n have hg1 := gFun_one hZC\n have hg0 := gFun_zero hZC\n have hfe := gFun_one_eq_neg\n linear_combination (h2 - hg1 + hg0 + hfe) / 2\n\n/-! ## 5. Termwise iterated derivation of the series at 0 -/\n\n/-- The iterated derivative of s ↦ (s+c)⁻¹ (positive form, from\nLiDigamma's negative form via `iteratedDeriv_neg`). -/\nlemma iteratedDeriv_zpow_neg_one (k : ℕ) (c : ℂ) {s : ℂ} (hs : s + c ≠ 0) :\n iteratedDeriv k (fun s : ℂ => (s + c) ^ (-1 : ℤ)) s =\n ((-1 : ℂ)) ^ k * (k ! : ℂ) * (s + c) ^ (-(k : ℤ) - 1) := by\n have e : (fun s : ℂ => (s + c) ^ (-1 : ℤ)) = -fun s : ℂ => -((s + c) ^ (-1 : ℤ)) :=\n funext fun s => neg_neg _\n rw [e, iteratedDeriv_neg k _ s, iteratedDeriv_neg_zpow_neg_one_add k c hs, neg_neg]\n\n/-- The k-th iterated derivative (k ≥ 1) of a series summand:\n(d/ds)^k [mult·(1/(s−ρ) + 1/ρ)] = mult·(−1)^k·k!·(s−ρ)^{−k−1}. -/\nlemma iteratedDeriv_seriesTerm {j : ℕ} (hj : 1 ≤ j) (ρ : {ρ : ℂ // IsNontrivialZero ρ})\n {s : ℂ} (hs : s - (ρ : ℂ) ≠ 0) :\n iteratedDeriv j (fun s : ℂ => seriesTerm s ρ) s =\n (zeroMult ρ : ℂ) * (((-1 : ℂ)) ^ j * (j ! : ℂ) * (s - (ρ : ℂ)) ^ (-(j : ℤ) - 1)) := by\n have hsp : s + -(ρ : ℂ) ≠ 0 := by\n rw [← sub_eq_add_neg]\n exact hs\n have e : (fun s : ℂ => seriesTerm s ρ) =\n fun s : ℂ => (zeroMult ρ : ℂ) * ((s + -(ρ : ℂ)) ^ (-1 : ℤ) + ((ρ : ℂ))⁻¹) := by\n funext t\n rw [seriesTerm]\n simp only [one_div, zpow_neg_one, sub_eq_add_neg]\n have hcf : ContDiffAt ℂ j (fun s : ℂ => (s + -(ρ : ℂ)) ^ (-1 : ℤ)) s := by\n have h1 : AnalyticAt ℂ (fun s : ℂ => s + -(ρ : ℂ)) s := analyticAt_id.add analyticAt_const\n have h2 : AnalyticAt ℂ (fun s : ℂ => 1 / (s + -(ρ : ℂ))) s := analyticAt_const.div h1 hsp\n have e2 : (fun s : ℂ => (s + -(ρ : ℂ)) ^ (-1 : ℤ)) = fun s => 1 / (s + -(ρ : ℂ)) :=\n funext fun t => by rw [zpow_neg_one, one_div]\n rw [e2]\n exact h2.contDiffAt\n have hcc : ContDiffAt ℂ j (fun _ : ℂ => ((ρ : ℂ))⁻¹) s := contDiff_const.contDiffAt\n have hinner : ContDiffAt ℂ j (fun s : ℂ => (s + -(ρ : ℂ)) ^ (-1 : ℤ) + ((ρ : ℂ))⁻¹) s :=\n hcf.add hcc\n rw [e, iteratedDeriv_const_mul _ hinner]\n congr 1\n rw [iteratedDeriv_add hcf hcc, iteratedDeriv_const, if_neg (show j ≠ 0 by omega), add_zero,\n sub_eq_add_neg]\n exact iteratedDeriv_zpow_neg_one j (-(ρ : ℂ)) hsp\n\nend NguyenRH1"},"extra_content":null}]