← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
Now the Tendsto/EventuallyEq fixes and the residue-lemma coercion fix.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean",
"old_string": " have hev : \u2200\u1da0 s in \ud835\udcdd[\u2260] (1 : \u2102), Rfun n s = 0 := by\n filter_upwards [Rfun_eq_sub_div_near_one n, mem_nhdsWithin_of_mem_nhds h0] with s hs hg0\n have hg0' : Ffun n s - TaylP n s = 0 := hg0\n rw [hs, hg0']\n exact zero_div _\n exact tendsto_const_nhds.congr' hev.symm",
"new_string": " have hev : (Rfun n) =\u1da0[\ud835\udcdd[\u2260] (1 : \u2102)] (fun _ => (0 : \u2102)) := by\n filter_upwards [Rfun_eq_sub_div_near_one n, mem_nhdsWithin_of_mem_nhds h0] with s hs hg0\n have hg0' : Ffun n s - TaylP n s = 0 := hg0\n rw [hs, hg0']\n exact zero_div _\n exact tendsto_const_nhds.congr' hev.symm"
}
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean",
"old_string": " have hev : \u2200\u1da0 s in \ud835\udcdd[\u2260] (1 : \u2102),\n Rfun n s = (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s := by\n filter_upwards [Rfun_eq_sub_div_near_one n,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds, self_mem_nhdsWithin] with s hs hgf hs1",
"new_string": " have hev : (Rfun n) =\u1da0[\ud835\udcdd[\u2260] (1 : \u2102)]\n (fun s => (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s) := by\n filter_upwards [Rfun_eq_sub_div_near_one n,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds, self_mem_nhdsWithin] with s hs hgf hs1"
}
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean",
"old_string": " rw [e, mul_assoc, mul_div_cancel_left\u2080 (pow_ne_zero (n + 1) hs1n)]",
"new_string": " rw [e, mul_assoc, mul_div_cancel_left\u2080 _ (pow_ne_zero (n + 1) hs1n)]"
}
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean",
"old_string": " filter_upwards [self_mem_nhdsWithin,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hs\u03c1 hfhs hhs hhas\n have hs\u03c1' : s - \u03c1 \u2260 0 := sub_ne_zero.mpr hs\u03c1\n have hld : logDeriv riemannZeta s =\n (analyticOrderNatAt riemannZeta \u03c1 : \u2102) / (s - \u03c1) + logDeriv h s := by\n have e1 : logDeriv riemannZeta s =\n logDeriv (fun z => (z - \u03c1) ^ analyticOrderNatAt riemannZeta \u03c1 * h z) s := by\n simp only [logDeriv_apply, hfhs.deriv_eq, hfhs.self_of_nhds, smul_eq_mul]",
"new_string": " filter_upwards [self_mem_nhdsWithin,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hs\u03c1 hfhs hhs hhas\n have hfhs' : riemannZeta =\u1da0[\ud835\udcdd s]\n (fun z => (z - \u03c1) ^ analyticOrderNatAt riemannZeta \u03c1 \u2022 h z) := hfhs\n have hs\u03c1' : s - \u03c1 \u2260 0 := sub_ne_zero.mpr hs\u03c1\n have hld : logDeriv riemannZeta s =\n (analyticOrderNatAt riemannZeta \u03c1 : \u2102) / (s - \u03c1) + logDeriv h s := by\n have e1 : logDeriv riemannZeta s =\n logDeriv (fun z => (z - \u03c1) ^ analyticOrderNatAt riemannZeta \u03c1 * h z) s := by\n simp only [logDeriv_apply, hfhs'.deriv_eq, hfhs'.self_of_nhds, smul_eq_mul]"
}
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean",
"old_string": " rcases hp with rfl | hp\n \u00b7 simpa [hAdef] using Rfun_bounded_near_one n\n \u00b7 have hp1 : p \u2260 1 := hSz_ne_one p hp",
"new_string": " rcases hp with rfl | hp\n \u00b7 have hA1 : A 1 = 0 := by simp [hAdef]\n have h2 : ((Rfun n) - fun s => A 1 / (s - 1)) = Rfun n := by\n rw [hA1]; simp\n rw [h2]\n exact Rfun_bounded_near_one n\n \u00b7 have hp1 : p \u2260 1 := hSz_ne_one p hp"
}
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean",
"old_string": " have hsc : s \u2209 (\u2191(insert (1 : \u2102) Sz) : Set \u2102) := hs.2\n have hs1 : s \u2260 1 := fun h => hsc (Finset.mem_coe.mpr (h \u25b8 Finset.mem_insert_self 1 Sz))",
"new_string": " have hsc : s \u2209 (\u2191(insert (1 : \u2102) Sz) : Set \u2102) := hs.2\n have hs1 : s \u2260 1 := fun h =>\n hsc (Finset.mem_coe.mpr (h.symm \u25b8 Finset.mem_insert_self 1 Sz))"
}
raw content_json (database row)
[{"type":"text","text":"Now the Tendsto/EventuallyEq fixes and the residue-lemma coercion fix."},{"type":"tool_use","id":"Edit_41","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean","old_string":" have hev : ∀ᶠ s in 𝓝[≠] (1 : ℂ), Rfun n s = 0 := by\n filter_upwards [Rfun_eq_sub_div_near_one n, mem_nhdsWithin_of_mem_nhds h0] with s hs hg0\n have hg0' : Ffun n s - TaylP n s = 0 := hg0\n rw [hs, hg0']\n exact zero_div _\n exact tendsto_const_nhds.congr' hev.symm","new_string":" have hev : (Rfun n) =ᶠ[𝓝[≠] (1 : ℂ)] (fun _ => (0 : ℂ)) := by\n filter_upwards [Rfun_eq_sub_div_near_one n, mem_nhdsWithin_of_mem_nhds h0] with s hs hg0\n have hg0' : Ffun n s - TaylP n s = 0 := hg0\n rw [hs, hg0']\n exact zero_div _\n exact tendsto_const_nhds.congr' hev.symm"},"extra_content":null},{"type":"tool_use","id":"Edit_42","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean","old_string":" have hev : ∀ᶠ s in 𝓝[≠] (1 : ℂ),\n Rfun n s = (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s := by\n filter_upwards [Rfun_eq_sub_div_near_one n,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds, self_mem_nhdsWithin] with s hs hgf hs1","new_string":" have hev : (Rfun n) =ᶠ[𝓝[≠] (1 : ℂ)]\n (fun s => (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s) := by\n filter_upwards [Rfun_eq_sub_div_near_one n,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds, self_mem_nhdsWithin] with s hs hgf hs1"},"extra_content":null},{"type":"tool_use","id":"Edit_43","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean","old_string":" rw [e, mul_assoc, mul_div_cancel_left₀ (pow_ne_zero (n + 1) hs1n)]","new_string":" rw [e, mul_assoc, mul_div_cancel_left₀ _ (pow_ne_zero (n + 1) hs1n)]"},"extra_content":null},{"type":"tool_use","id":"Edit_44","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean","old_string":" filter_upwards [self_mem_nhdsWithin,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hsρ hfhs hhs hhas\n have hsρ' : s - ρ ≠ 0 := sub_ne_zero.mpr hsρ\n have hld : logDeriv riemannZeta s =\n (analyticOrderNatAt riemannZeta ρ : ℂ) / (s - ρ) + logDeriv h s := by\n have e1 : logDeriv riemannZeta s =\n logDeriv (fun z => (z - ρ) ^ analyticOrderNatAt riemannZeta ρ * h z) s := by\n simp only [logDeriv_apply, hfhs.deriv_eq, hfhs.self_of_nhds, smul_eq_mul]","new_string":" filter_upwards [self_mem_nhdsWithin,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hsρ hfhs hhs hhas\n have hfhs' : riemannZeta =ᶠ[𝓝 s]\n (fun z => (z - ρ) ^ analyticOrderNatAt riemannZeta ρ • h z) := hfhs\n have hsρ' : s - ρ ≠ 0 := sub_ne_zero.mpr hsρ\n have hld : logDeriv riemannZeta s =\n (analyticOrderNatAt riemannZeta ρ : ℂ) / (s - ρ) + logDeriv h s := by\n have e1 : logDeriv riemannZeta s =\n logDeriv (fun z => (z - ρ) ^ analyticOrderNatAt riemannZeta ρ * h z) s := by\n simp only [logDeriv_apply, hfhs'.deriv_eq, hfhs'.self_of_nhds, smul_eq_mul]"},"extra_content":null},{"type":"tool_use","id":"Edit_45","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean","old_string":" rcases hp with rfl | hp\n · simpa [hAdef] using Rfun_bounded_near_one n\n · have hp1 : p ≠ 1 := hSz_ne_one p hp","new_string":" rcases hp with rfl | hp\n · have hA1 : A 1 = 0 := by simp [hAdef]\n have h2 : ((Rfun n) - fun s => A 1 / (s - 1)) = Rfun n := by\n rw [hA1]; simp\n rw [h2]\n exact Rfun_bounded_near_one n\n · have hp1 : p ≠ 1 := hSz_ne_one p hp"},"extra_content":null},{"type":"tool_use","id":"Edit_46","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean","old_string":" have hsc : s ∉ (↑(insert (1 : ℂ) Sz) : Set ℂ) := hs.2\n have hs1 : s ≠ 1 := fun h => hsc (Finset.mem_coe.mpr (h ▸ Finset.mem_insert_self 1 Sz))","new_string":" have hsc : s ∉ (↑(insert (1 : ℂ) Sz) : Set ℂ) := hs.2\n have hs1 : s ≠ 1 := fun h =>\n hsc (Finset.mem_coe.mpr (h.symm ▸ Finset.mem_insert_self 1 Sz))"},"extra_content":null}]