[{"type":"thinking","thinking":"Now Section 8: the derivative-family SummableLocallyUniformlyOn + the tsum application + DinfC's iterated values at 1/2 + the transfer to digamma. Let me write it.\n\n```lean\n/-! ## 8. The polygamma values at 1/2 -/\n\n/-- The k-th derivative family (k ≥ 1) is summable locally uniformly on the domain. -/\nlemma dpsiTermC_deriv_summableLocallyUniformlyOn (k : ℕ) (hk : 1 ≤ k) :\n    SummableLocallyUniformlyOn\n      (fun m => (iteratedDerivWithin k (fun s : ℂ => dpsiTermC s m) dpsiDomain)) dpsiDomain := by\n  apply SummableLocallyUniformlyOn_of_locally_bounded dpsiDomain_isOpen\n  intro K hK hKc\n  refine ⟨fun m => (k ! : ℝ) / ((m : ℝ) + 1) ^ (k + 1),\n    summable_div_add_one_pow _ (k + 1) (by omega), fun m s hs => ?_⟩\n  have hsd : s ∈ dpsiDomain := hK hs\n  rw [iteratedDerivWithin_dpsiTermC k hk m hsd]\n  -- norm: ‖−(−1)^k·k!·(s+↑m+1)^{−(k+1)}‖ = k!·‖s+↑m+1‖^{−(k+1)}\n  rw [norm_mul, norm_mul]\n  have hnorm1 : ‖-((-1 : ℂ)) ^ k‖ = 1 := by\n    rw [norm_neg, norm_pow, norm_neg, norm_one, one_pow]  -- hmm — ‖(−1)^k‖ = 1: norm_pow + ‖−1‖ = 1 (norm_neg norm_one)\n  rw [hnorm1, RCLike.norm_natCast, norm_zpow]  -- hmm RCLike.norm_natCast : ‖(n:ℂ)‖ = ↑n ✓ used before\n  -- now: 1 * k! * ‖s+↑m+1‖^(−(k+1):ℤ) ≤ k!/(m+1)^{k+1}\n  ...\n```\nHmm — the norm of the zpow: `norm_zpow : ‖x ^ (n : ℤ)‖ = ‖x‖ ^ n` ✓ (Complex.norm_zpow? — the general `norm_zpow` in normed division rings ✓). Then ‖s+↑m+1‖^{−(k+1):ℤ} = (‖s+↑m+1‖^{k+1})⁻¹ ≤ ((m+1)^{k+1})⁻¹ — since ‖s+↑m+1‖ ≥ m+1: the zpow monotonicity: for 0 < a ≤ b: a^{−(k+1):ℤ} ≥ b^{−(k+1):ℤ} — `zpow_le_zpow_iff`? — negative exponent flips: 1/‖·‖^{k+1} ≤ 1/(m+1)^{k+1} ⟸ ‖·‖^{k+1} ≥ (m+1)^{k+1} ⟸ ‖·‖ ≥ m+1 (pow_le_pow_right₀ hmm pow_le_pow_left₀ (0 ≤ m+1) (m+1 ≤ ‖·‖) (k+1)) — then one_div_le_one_div_of_le... — the chain:\n  ‖s+↑m+1‖ ≥ m+1 (re-part: (s+↑m+1).re = s.re + m + 1 ≥ m+1 since s.re > 0 ✓ and ‖·‖ ≥ re via re_le_norm... wait need nonneg re for abs_re_le_norm: re > 0 ✓).\n  Then ‖s+↑m+1‖^(k+1) ≥ (m+1)^(k+1) — pow_le_pow_left₀ (0 ≤ m+1) hle (k+1)? — `pow_le_pow_left₀ (ha : 0 ≤ a) (h : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n` ✓ (used in LiSkeleton: pow_le_pow_left₀ (by positivity) hbase n ✓).\n  Then zpow: ‖s+↑m+1‖^(−(k+1):ℤ) = (‖s+↑m+1‖^(k+1))⁻¹ (zpow_neg_natCast? or zpow_natCast + zpow_neg: (−(k+1):ℤ) = −((k+1:ℕ):ℤ) — zpow_neg : x^(−n) = (x^n)⁻¹ ✓) — and (‖s+..‖^(k+1))⁻¹ ≤ ((m+1)^(k+1))⁻¹ via inv_le_inv_of_le₀? — `inv_le_inv_of_le₀ (ha : 0 < a) (h : a ≤ b) : b⁻¹ ≤ a⁻¹`? — hmm name: `inv_le_inv_of_le₀`? or `one_div_le_one_div_of_le` (verified earlier ✓): 1/(m+1)^{k+1}... — let me convert to one_div forms: b⁻¹ = 1/b via one_div... — Let me use: `inv_le_inv_of_le₀ (ha : 0 < a) (hab : a ≤ b) : b⁻¹ ≤ a⁻¹` — hmm — I recall `inv_le_inv_of_le₀`? — or `inv_le_inv_of_nonneg`? — there are several renames — safer: use one_div forms: x⁻¹ = 1/x (one_div) then one_div_le_one_div_of_le (hpos) (hle) ✓ verified name.\n  Then k!·(‖s+..‖^{k+1})⁻¹ ≤ k!·((m+1)^{k+1})⁻¹ via mul_le_mul_of_nonneg_left (0 ≤ k!) ✓ and the target form k!/(m+1)^{k+1} = k!·((m+1)^{k+1})⁻¹ via div_eq_mul_inv ✓.\n\nLet me structure the norm computation:\n```lean\n  rw [iteratedDerivWithin_dpsiTermC k hk m hsd]\n  have hre : 0 < s.re := dpsiDomain_re_pos hsd\n  have hnormS : (m : ℝ) + 1 ≤ ‖s + ↑m + 1‖ := by\n    have h6 : (s + ↑m + 1).re = s.re + m + 1 := by\n      have h3 : (↑m : ℂ).re = (m : ℝ) := by simp\n      simp [Complex.add_re, Complex.one_re, h3]\n    have h5 : s.re + m + 1 ≤ ‖s + ↑m + 1‖ := by\n      rw [← h6]\n      exact Complex.re_le_norm _\n    linarith [h5, hre]\n  rw [norm_mul, norm_mul]\n  have hsign : ‖-((-1 : ℂ)) ^ k‖ = 1 := by\n    have h7 : ‖((-1 : ℂ))‖ = 1 := by rw [norm_neg, norm_one]\n    rw [norm_neg, norm_pow, h7, one_pow]\n  rw [hsign, one_mul, RCLike.norm_natCast, norm_zpow]\n  -- goal: k! * ‖s+↑m+1‖^(−(k:ℤ)−1) ≤ k!/(m+1)^{k+1}\n  rw [show (-(k : ℤ) - 1 : ℤ) = -((k + 1 : ℕ) : ℤ) by push_cast; ring]\n  rw [zpow_neg_natCast?]  -- hmm — x ^ (−(n:ℤ)) = (x^n)⁻¹ — `zpow_neg_natCast`? or zpow_neg ∘ zpow_natCast\n  ...\n```\nHmm — zpow_neg_natCast — let me use zpow_neg + zpow_natCast: x^(−(n:ℤ)) = (x^(n:ℤ))⁻¹ [zpow_neg] = (x^n)⁻¹ [zpow_natCast : x^((n:ℕ):ℤ) = x^n ✓]. So:\n```lean\n  rw [show (-(k : ℤ) - 1 : ℤ) = -(((k + 1 : ℕ) : ℤ)) by push_cast; ring, zpow_neg, zpow_natCast]\n  -- goal: k! * (‖s+↑m+1‖^(k+1))⁻¹ ≤ k! / (m+1)^{k+1}\n  rw [div_eq_mul_inv]\n  apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n  rw [one_div?]... — the LHS has (‖s+..‖^(k+1))⁻¹ and the rewritten target k!·((m+1)^{k+1})⁻¹ (via div_eq_mul_inv : k!/(m+1)^{k+1} = k!·((m+1)^{k+1})⁻¹) — so need (‖s+..‖^(k+1))⁻¹ ≤ ((m+1)^(k+1))⁻¹ — via inv_le_inv_of_le₀ (pow_pos ...) (pow_le_pow_left₀ (by positivity) hnormS (k+1)) — name check needed for inv_le_inv_of_le₀.\n```\nLet me check inv_le_inv names quickly... — `inv_le_inv_of_le₀ (ha : 0 < a) (h : a ≤ b) : b⁻¹ ≤ a⁻¹` — I'm fairly confident this exists (GroupWithZero order file). Then:\n\nThen the tsum application:\n```lean\nlemma iteratedDerivWithin_tsum_dpsiTermC (k : ℕ) (hk : 1 ≤ k) :\n    iteratedDerivWithin k (fun s : ℂ => ∑' m : ℕ, dpsiTermC s m) dpsiDomain ((1 : ℂ) / 2) =\n      ∑' m : ℕ, -((-1 : ℂ)) ^ k * (k ! : ℂ) * ((1 / 2 : ℂ) + ↑m + 1) ^ (-(k : ℤ) - 1) := by\n  rw [iteratedDerivWithin_tsum k dpsiDomain_isOpen dpsiDomain_half\n    (fun s hs => dpsiTermC_summable hs)\n    (fun j hj1 hjm => ?_)  -- the SummableLocallyUniformlyOn for each 1 ≤ j ≤ k\n    ?_]\n  · apply tsum_congr\n    intro m\n    exact iteratedDerivWithin_dpsiTermC k hk m dpsiDomain_half\n  · -- the derivative-family uniform summability for 1 ≤ j ≤ k\n    exact dpsiTermC_deriv_summableLocallyUniformlyOn j hj1  -- wait — needs j ≤ k — my lemma doesn't need j ≤ k — the uniform summability holds for any j ≥ 1 ✓ (independent of k) ✓ so just the hk... hmm my lemma takes (k) (hk : 1 ≤ k) — call with j hj1 ✓ (no upper bound needed) ✓\n  · -- hf2: differentiability of the iteratedDerivWithin's\n    intro n j r hjm hr\n    rw [iteratedDerivWithin_dpsiTermC j (by omega) n hr]  -- hmm j could be 0! hf2's k ranges over k ≤ m INCLUDING 0 — for j = 0 the iteratedDerivWithin 0 = the term itself — my lemma needs 1 ≤ j. Handle j = 0 separately.\n    ...\n```\nThe hf2's k ranges over all k ≤ m including 0. For j = 0: iteratedDerivWithin 0 (dpsiTermC · n) dpsiDomain r = dpsiTermC r n — differentiable ✓ (the term is differentiable on the domain). For j ≥ 1: the closed form is differentiable ✓. So:\n```lean\n  · intro n j r hjm hr\n    rcases Nat.eq_zero_or_pos j with hj0 | hj0\n    · subst hj0\n      rw [iteratedDerivWithin_zero]  -- = the term\n      -- dpsiTermC r n differentiable at r ∈ domain\n      have hsm : r + n + 1 ≠ 0 := dpsiTermC_pole_free hr n\n      have h1 : DifferentiableAt ℂ (fun s : ℂ => 1 / ((n : ℂ) + 1)) r := differentiableAt_const _\n      have h2 : DifferentiableAt ℂ (fun s : ℂ => 1 / (s + ↑n + 1)) r := by\n        have h3 : DifferentiableAt ℂ (fun s : ℂ => s + ↑n + 1) r :=\n          (differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _)\n        exact (differentiableAt_const (1 : ℂ)).div h3 hsm\n      -- the term as a function\n      have heq : (fun s : ℂ => dpsiTermC s n) = fun s => 1/((n:ℂ)+1) − 1/(s+↑n+1) := by funext s; rw [dpsiTermC]\n      rw [heq]\n      exact h1.sub h2\n    · rw [iteratedDerivWithin_dpsiTermC j (by omega) n hr]\n      -- the closed form is differentiable at r\n      apply DifferentiableAt.mul\n      · exact differentiableAt_const _\n      · -- derivable: (r+↑n+1)^(−(j:ℤ)−1) — zpow differentiable off pole\n        have hsm : r + n + 1 ≠ 0 := dpsiTermC_pole_free hr n\n        have h4 : DifferentiableAt ℂ (fun s : ℂ => s + ↑n + 1) r :=\n          (differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _)\n        exact h4.zpow (Or.inl hsm)?  -- DifferentiableAt.zpow? — hmm — `DifferentiableAt.zpow (hf : DifferentiableAt f x) (h : f x ≠ 0)?: DifferentiableAt (fun x => f x ^ (n:ℤ)) x`? — there's `DifferentiableAt.zpow`? — maybe `DifferentiableAt.zpow (hf) (hx)?`... — or via hasDerivAt_zpow.differentiableAt + comp ✓ pattern from LiPrincipal's Gprim_differentiableAt ✓\n```\nLiPrincipal's Gprim_differentiableAt used: `(((hasDerivAt_zpow (-((i : ℤ) - 1)) (w - 1) (Or.inl hw1)).differentiableAt).comp w (((hasDerivAt_id w).sub_const 1).differentiableAt))` — the pattern ✓ reuse.\n\nHmm — the const_mul target: the closed form is −(−1)^j·↑j!·(s+↑n+1)^(−(j:ℤ)−1) — as a function: fun s => (−(−1)^j·↑j!) * (s+↑n+1)^(−(j:ℤ)−1) — hmm — the closed form from the lemma is written `-(−1)^j * ↑j! * (s + ↑n + 1) ^ (−(j:ℤ) − 1)` — left-nested (a·b)·X — DifferentiableAt: ((differentiableAt_const _).mul (the zpow one)) ✓.\n\nAlso note — the iteratedDerivWithin_dpsiTermC at j with hj : 1 ≤ j — and hf2's j with j ≤ k but possibly... — the hf2's hypothesis: ∀ n k r, k ≤ m → r ∈ s → DifferentiableAt ... — k here is the loop variable (j in my writing) with j ≤ m — could be 0 ✓ handled.\n\nThen the final value at 1/2 — the DinfC combination and the transfer to digamma + the series evaluation + reindexing. Let me now write Section 8 wholesale. Given the length, let me write it and iterate.","signature":""},{"type":"text","text":"Now the derivative-family uniform summability and the tsum application."},{"type":"tool_use","id":"Edit_421","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean","old_string":"  rw [h4]\n  rw [zero_add]\n\nend NguyenRH1","new_string":"  rw [h4]\n  rw [zero_add]\n\n/-- The k-th derivative family (k ≥ 1) is summable locally uniformly on the domain. -/\nlemma dpsiTermC_deriv_summableLocallyUniformlyOn (k : ℕ) (hk : 1 ≤ k) :\n    SummableLocallyUniformlyOn\n      (fun m => (iteratedDerivWithin k (fun s : ℂ => dpsiTermC s m) dpsiDomain)) dpsiDomain := by\n  apply SummableLocallyUniformlyOn_of_locally_bounded dpsiDomain_isOpen\n  intro K hK hKc\n  refine ⟨fun m => (k ! : ℝ) / ((m : ℝ) + 1) ^ (k + 1),\n    summable_div_add_one_pow _ (k + 1) (by omega), fun m s hs => ?_⟩\n  have hsd : s ∈ dpsiDomain := hK hs\n  rw [iteratedDerivWithin_dpsiTermC k hk m hsd]\n  have hre : 0 < s.re := dpsiDomain_re_pos hsd\n  have hnormS : (m : ℝ) + 1 ≤ ‖s + ↑m + 1‖ := by\n    have h6 : (s + ↑m + 1).re = s.re + m + 1 := by\n      have h3 : (↑m : ℂ).re = (m : ℝ) := by simp\n      simp [Complex.add_re, Complex.one_re, h3]\n    have h5 : s.re + m + 1 ≤ ‖s + ↑m + 1‖ := by\n      rw [← h6]\n      exact Complex.re_le_norm _\n    linarith [h5, hre]\n  rw [norm_mul, norm_mul]\n  have hsign : ‖-((-1 : ℂ)) ^ k‖ = 1 := by\n    have h7 : ‖((-1 : ℂ))‖ = 1 := by rw [norm_neg, norm_one]\n    rw [norm_neg, norm_pow, h7, one_pow]\n  rw [hsign, one_mul, RCLike.norm_natCast, norm_zpow]\n  rw [show (-(k : ℤ) - 1 : ℤ) = -(((k + 1 : ℕ) : ℤ)) by push_cast; ring, zpow_neg, zpow_natCast]\n  rw [div_eq_mul_inv]\n  apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n  rw [show (((m : ℝ) + 1) ^ (k + 1))⁻¹ = 1 / (((m : ℝ) + 1) ^ (k + 1)) from by rw [one_div]]\n  rw [show (‖s + ↑m + 1‖ ^ (k + 1))⁻¹ = 1 / (‖s + ↑m + 1‖ ^ (k + 1)) from by rw [one_div]]\n  apply one_div_le_one_div_of_le (by positivity)\n  exact pow_le_pow_left₀ (by positivity : (0 : ℝ) ≤ (m : ℝ) + 1) hnormS (k + 1)\n\n/-- The iterated derivative of the series function at 1/2 (termwise). -/\nlemma iteratedDerivWithin_tsum_dpsiTermC (k : ℕ) (hk : 1 ≤ k) :\n    iteratedDerivWithin k (fun s : ℂ => ∑' m : ℕ, dpsiTermC s m) dpsiDomain ((1 : ℂ) / 2) =\n      ∑' m : ℕ, -((-1 : ℂ)) ^ k * (k ! : ℂ) * ((1 / 2 : ℂ) + ↑m + 1) ^ (-(k : ℤ) - 1) := by\n  rw [iteratedDerivWithin_tsum k dpsiDomain_isOpen dpsiDomain_half\n    (fun s hs => dpsiTermC_summable hs)\n    (fun j hj1 _ => dpsiTermC_deriv_summableLocallyUniformlyOn j hj1)\n    ?_]\n  · apply tsum_congr\n    intro m\n    exact iteratedDerivWithin_dpsiTermC k hk m dpsiDomain_half\n  · intro n j r hjm hr\n    rcases Nat.eq_zero_or_pos j with hj0 | hj0\n    · subst hj0\n      rw [iteratedDerivWithin_zero]\n      have hsm : r + n + 1 ≠ 0 := dpsiTermC_pole_free hr n\n      have heq : (fun s : ℂ => dpsiTermC s n) = fun s => 1 / ((n : ℂ) + 1) - 1 / (s + ↑n + 1) := by\n        funext s; rw [dpsiTermC]\n      rw [heq]\n      apply DifferentiableAt.sub (differentiableAt_const _)\n      have h3 : DifferentiableAt ℂ (fun s : ℂ => s + ↑n + 1) r :=\n        (differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _)\n      exact (differentiableAt_const (1 : ℂ)).div h3 hsm\n    · rw [iteratedDerivWithin_dpsiTermC j (by omega) n hr]\n      have hsm : r + n + 1 ≠ 0 := dpsiTermC_pole_free hr n\n      apply DifferentiableAt.mul (differentiableAt_const _)\n      have h4 : DifferentiableAt ℂ (fun s : ℂ => s + ↑n + 1) r :=\n        (differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _)\n      exact (((hasDerivAt_zpow (-(j : ℤ) - 1) (r + ↑n + 1) (Or.inl hsm)).differentiableAt).comp r\n        h4.hasDerivAt)\n\nend NguyenRH1"},"extra_content":null}]