← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
thinking (109 chars)
M-test green. Now §5 chunk 3: `iteratedDeriv_seriesFun_zero`. Also clean up the probe file. Append the lemma.
M-test green. Appending §5 chunk 3 (`iteratedDeriv_seriesFun_zero`).
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiMoments.lean",
"old_string": " _ = (\u2191j ! * 2 ^ (j + 1) * (1 / \u03b4) ^ (j - 1)) * ((\u2191(zeroMult \u03c1)) / \u2016(\u03c1 : \u2102)\u2016 ^ 2) := by ring\n\nend NguyenRH1",
"new_string": " _ = (\u2191j ! * 2 ^ (j + 1) * (1 / \u03b4) ^ (j - 1)) * ((\u2191(zeroMult \u03c1)) / \u2016(\u03c1 : \u2102)\u2016 ^ 2) := by ring\n\n/-- The j-th iterated derivative (j \u2265 1) of seriesFun at 0, termwise:\n(d/ds)^j seriesFun (0) = \u03a3_\u03c1 mult\u00b7(\u22121)^j\u00b7j!\u00b7(0\u2212\u03c1)^{\u2212j\u22121}\n(the LiDigamma \u00a78 `iteratedDerivWithin_tsum` pattern on ball(0, \u03b4/2)). -/\nlemma iteratedDeriv_seriesFun_zero {j : \u2115} (hj : 1 \u2264 j) :\n iteratedDeriv j seriesFun 0 =\n \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n (zeroMult \u03c1 : \u2102) * (((-1 : \u2102)) ^ j * (j ! : \u2102) * (0 - (\u03c1 : \u2102)) ^ (-(j : \u2124) - 1)) := by\n obtain \u27e8\u03b4, h\u03b4, h\u03b4le\u27e9 := exists_norm_lower_bound\n have h0mem : (0 : \u2102) \u2208 Metric.ball (0 : \u2102) (\u03b4 / 2) := by\n rw [Metric.mem_ball, dist_zero_right, norm_zero]\n positivity\n have pole_free : \u2200 t : \u2102, t \u2208 Metric.ball (0 : \u2102) (\u03b4 / 2) \u2192\n \u2200 \u03c3 : {\u03c3 : \u2102 // IsNontrivialZero \u03c3}, t - (\u03c3 : \u2102) \u2260 0 := by\n intro t ht \u03c3\n rw [Metric.mem_ball, dist_zero_right] at ht\n have h\u03c3 := h\u03b4le \u03c3\n have h1 : \u2016(\u03c3 : \u2102)\u2016 - \u2016t\u2016 \u2264 \u2016t - (\u03c3 : \u2102)\u2016 := by\n have h2 := norm_sub_norm_le (\u03c3 : \u2102) t\n rw [norm_sub_rev]\n exact h2\n have hpos : (0 : \u211d) < \u2016t - (\u03c3 : \u2102)\u2016 := lt_of_lt_of_le (by linarith) h1\n exact norm_pos_iff.mp hpos\n rw [seriesFun, \u2190 (iteratedDerivWithin_of_isOpen Metric.isOpen_ball) h0mem,\n iteratedDerivWithin_tsum j Metric.isOpen_ball h0mem\n (fun t _ => seriesSummable t)\n (fun k hk1 _ => seriesTerm_deriv_summableLocallyUniformlyOn hk1 h\u03b4 h\u03b4le)\n ?_]\n \u00b7 apply tsum_congr\n intro \u03c1\n rw [(iteratedDerivWithin_of_isOpen Metric.isOpen_ball) h0mem]\n exact iteratedDeriv_seriesTerm hj \u03c1 (pole_free 0 h0mem \u03c1)\n \u00b7 intro \u03c3 k r _ hr\n rcases Nat.eq_zero_or_pos k with hk0 | hk0\n \u00b7 subst hk0\n rw [iteratedDerivWithin_zero]\n have hr\u03c3 := pole_free r hr \u03c3\n have h1 : AnalyticAt \u2102 (fun z : \u2102 => z - (\u03c3 : \u2102)) r := analyticAt_id.sub analyticAt_const\n have h2 : AnalyticAt \u2102 (fun z : \u2102 => 1 / (z - (\u03c3 : \u2102))) r := analyticAt_const.div h1 hr\u03c3\n have h3 : AnalyticAt \u2102 (fun z : \u2102 =>\n (zeroMult \u03c3 : \u2102) * (1 / (z - (\u03c3 : \u2102)) + 1 / (\u03c3 : \u2102))) r :=\n analyticAt_const.mul (h2.add analyticAt_const)\n show DifferentiableAt \u2102 (fun z : \u2102 =>\n (zeroMult \u03c3 : \u2102) * (1 / (z - (\u03c3 : \u2102)) + 1 / (\u03c3 : \u2102))) r\n exact h3.differentiableAt\n \u00b7 have h5 : (fun t => iteratedDerivWithin k (fun z : \u2102 => seriesTerm z \u03c3)\n (Metric.ball 0 (\u03b4 / 2)) t) =\u1da0[\ud835\udcdd r]\n fun t => (zeroMult \u03c3 : \u2102) * (((-1 : \u2102)) ^ k * (k ! : \u2102) *\n (t - (\u03c3 : \u2102)) ^ (-(k : \u2124) - 1)) := by\n filter_upwards [Metric.isOpen_ball.mem_nhds hr] with t ht\n rw [(iteratedDerivWithin_of_isOpen Metric.isOpen_ball) ht]\n exact iteratedDeriv_seriesTerm (by omega) \u03c3 (pole_free t ht \u03c3)\n apply h5.differentiableAt_iff.mpr\n have hr\u03c3 := pole_free r hr \u03c3\n have h4 : DifferentiableAt \u2102 (fun t : \u2102 => t - (\u03c3 : \u2102)) r :=\n differentiableAt_id.sub (differentiableAt_const _)\n have h6 : DifferentiableAt \u2102 (fun t : \u2102 => (t - (\u03c3 : \u2102)) ^ (-(k : \u2124) - 1)) r := by\n have h7 := ((hasDerivAt_zpow (-(k : \u2124) - 1) (r - (\u03c3 : \u2102))\n (Or.inl hr\u03c3)).differentiableAt).comp r h4\n have heq : ((fun x : \u2102 => x ^ (-(k : \u2124) - 1)) \u2218 fun t : \u2102 => t - (\u03c3 : \u2102)) =\n fun t : \u2102 => (t - (\u03c3 : \u2102)) ^ (-(k : \u2124) - 1) := rfl\n rw [heq] at h7\n exact h7\n exact (differentiableAt_const _).mul ((differentiableAt_const _).mul h6)\n\nend NguyenRH1"
}
raw content_json (database row)
[{"type":"thinking","thinking":"M-test green. Now §5 chunk 3: `iteratedDeriv_seriesFun_zero`. Also clean up the probe file. Append the lemma.","signature":""},{"type":"text","text":"M-test green. Appending §5 chunk 3 (`iteratedDeriv_seriesFun_zero`)."},{"type":"tool_use","id":"Edit_56","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiMoments.lean","old_string":" _ = (↑j ! * 2 ^ (j + 1) * (1 / δ) ^ (j - 1)) * ((↑(zeroMult ρ)) / ‖(ρ : ℂ)‖ ^ 2) := by ring\n\nend NguyenRH1","new_string":" _ = (↑j ! * 2 ^ (j + 1) * (1 / δ) ^ (j - 1)) * ((↑(zeroMult ρ)) / ‖(ρ : ℂ)‖ ^ 2) := by ring\n\n/-- The j-th iterated derivative (j ≥ 1) of seriesFun at 0, termwise:\n(d/ds)^j seriesFun (0) = Σ_ρ mult·(−1)^j·j!·(0−ρ)^{−j−1}\n(the LiDigamma §8 `iteratedDerivWithin_tsum` pattern on ball(0, δ/2)). -/\nlemma iteratedDeriv_seriesFun_zero {j : ℕ} (hj : 1 ≤ j) :\n iteratedDeriv j seriesFun 0 =\n ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n (zeroMult ρ : ℂ) * (((-1 : ℂ)) ^ j * (j ! : ℂ) * (0 - (ρ : ℂ)) ^ (-(j : ℤ) - 1)) := by\n obtain ⟨δ, hδ, hδle⟩ := exists_norm_lower_bound\n have h0mem : (0 : ℂ) ∈ Metric.ball (0 : ℂ) (δ / 2) := by\n rw [Metric.mem_ball, dist_zero_right, norm_zero]\n positivity\n have pole_free : ∀ t : ℂ, t ∈ Metric.ball (0 : ℂ) (δ / 2) →\n ∀ σ : {σ : ℂ // IsNontrivialZero σ}, t - (σ : ℂ) ≠ 0 := by\n intro t ht σ\n rw [Metric.mem_ball, dist_zero_right] at ht\n have hσ := hδle σ\n have h1 : ‖(σ : ℂ)‖ - ‖t‖ ≤ ‖t - (σ : ℂ)‖ := by\n have h2 := norm_sub_norm_le (σ : ℂ) t\n rw [norm_sub_rev]\n exact h2\n have hpos : (0 : ℝ) < ‖t - (σ : ℂ)‖ := lt_of_lt_of_le (by linarith) h1\n exact norm_pos_iff.mp hpos\n rw [seriesFun, ← (iteratedDerivWithin_of_isOpen Metric.isOpen_ball) h0mem,\n iteratedDerivWithin_tsum j Metric.isOpen_ball h0mem\n (fun t _ => seriesSummable t)\n (fun k hk1 _ => seriesTerm_deriv_summableLocallyUniformlyOn hk1 hδ hδle)\n ?_]\n · apply tsum_congr\n intro ρ\n rw [(iteratedDerivWithin_of_isOpen Metric.isOpen_ball) h0mem]\n exact iteratedDeriv_seriesTerm hj ρ (pole_free 0 h0mem ρ)\n · intro σ k r _ hr\n rcases Nat.eq_zero_or_pos k with hk0 | hk0\n · subst hk0\n rw [iteratedDerivWithin_zero]\n have hrσ := pole_free r hr σ\n have h1 : AnalyticAt ℂ (fun z : ℂ => z - (σ : ℂ)) r := analyticAt_id.sub analyticAt_const\n have h2 : AnalyticAt ℂ (fun z : ℂ => 1 / (z - (σ : ℂ))) r := analyticAt_const.div h1 hrσ\n have h3 : AnalyticAt ℂ (fun z : ℂ =>\n (zeroMult σ : ℂ) * (1 / (z - (σ : ℂ)) + 1 / (σ : ℂ))) r :=\n analyticAt_const.mul (h2.add analyticAt_const)\n show DifferentiableAt ℂ (fun z : ℂ =>\n (zeroMult σ : ℂ) * (1 / (z - (σ : ℂ)) + 1 / (σ : ℂ))) r\n exact h3.differentiableAt\n · have h5 : (fun t => iteratedDerivWithin k (fun z : ℂ => seriesTerm z σ)\n (Metric.ball 0 (δ / 2)) t) =ᶠ[𝓝 r]\n fun t => (zeroMult σ : ℂ) * (((-1 : ℂ)) ^ k * (k ! : ℂ) *\n (t - (σ : ℂ)) ^ (-(k : ℤ) - 1)) := by\n filter_upwards [Metric.isOpen_ball.mem_nhds hr] with t ht\n rw [(iteratedDerivWithin_of_isOpen Metric.isOpen_ball) ht]\n exact iteratedDeriv_seriesTerm (by omega) σ (pole_free t ht σ)\n apply h5.differentiableAt_iff.mpr\n have hrσ := pole_free r hr σ\n have h4 : DifferentiableAt ℂ (fun t : ℂ => t - (σ : ℂ)) r :=\n differentiableAt_id.sub (differentiableAt_const _)\n have h6 : DifferentiableAt ℂ (fun t : ℂ => (t - (σ : ℂ)) ^ (-(k : ℤ) - 1)) r := by\n have h7 := ((hasDerivAt_zpow (-(k : ℤ) - 1) (r - (σ : ℂ))\n (Or.inl hrσ)).differentiableAt).comp r h4\n have heq : ((fun x : ℂ => x ^ (-(k : ℤ) - 1)) ∘ fun t : ℂ => t - (σ : ℂ)) =\n fun t : ℂ => (t - (σ : ℂ)) ^ (-(k : ℤ) - 1) := rfl\n rw [heq] at h7\n exact h7\n exact (differentiableAt_const _).mul ((differentiableAt_const _).mul h6)\n\nend NguyenRH1"},"extra_content":null}]