ZeroMomentDerivatives.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.CanonicalPartialFractions
6 import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 theorem locally_uniform_sum_deriv {ι : Type*} {F : ι → ℂ → ℂ} {G : ℂ → ℂ} {U : Set ℂ}
14     (h : HasSumLocallyUniformlyOn F G U) (hU : IsOpen U)
15     (hF : ∀ i, DifferentiableOn ℂ (F i) U) :
16     HasSumLocallyUniformlyOn (fun i => deriv (F i)) (deriv G) U := by
17   have hh := h.deriv (Eventually.of_forall (fun S => DifferentiableOn.fun_sum (fun i _ => hF i))) hU
18   apply hh.congr
19   intro S z hz
20   exact (deriv_fun_sum (fun i _ => (hF i).differentiableAt (hU.mem_nhds hz)))
21 
22 def zeroResolventJet (f : ℂ → ℂ) (n : ℕ) (i : ZeroMultiplicityIndex f) (w : ℂ) : ℂ :=
23   (n.factorial : ℂ) / (indexedZero i - w) ^ (n + 1)
24 
25 theorem zeroResolventJet_hasDerivAt {f : ℂ → ℂ} (n : ℕ) (i : ZeroMultiplicityIndex f)
26     {w : ℂ} (hw : w ≠ indexedZero i) :
27     HasDerivAt (zeroResolventJet f n i) (zeroResolventJet f (n + 1) i w) w := by
28   have hd := (hasDerivAt_const w (indexedZero i)).sub (hasDerivAt_id w)
29   have hn : indexedZero i - w ≠ 0 := sub_ne_zero.mpr hw.symm
30   have h := (hasDerivAt_const w (n.factorial : ℂ)).div (hd.pow (n + 1)) (pow_ne_zero _ hn)
31   convert! h using 1
32   dsimp only [zeroResolventJet, Pi.pow_apply, Pi.sub_apply, id_eq]
33   simp only [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.add_sub_cancel]
34   field_simp
35   ring
36 
37 theorem zeroResolventJet_locally_uniform {f : ℂ → ℂ} (hf : Differentiable ℂ f)
38     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (n : ℕ) :
39     HasSumLocallyUniformlyOn (zeroResolventJet f n)
40       (iteratedDeriv n (fun w => ∑' i, zeroPartialFraction f i w)) {w | f w ≠ 0} := by
41   have hU : IsOpen {w : ℂ | f w ≠ 0} := isOpen_ne_fun hf.continuous continuous_const
42   have hn : ∀ i : ZeroMultiplicityIndex f, ∀ w ∈ {w | f w ≠ 0}, w ≠ indexedZero i := by
43     intro i w hw he
44     apply hw
45     rw [he]
46     exact i.1.property
47   induction n with
48   | zero =>
49       have he : zeroResolventJet f 0 = zeroPartialFraction f := by
50         funext i w
51         simp [zeroResolventJet, zeroPartialFraction]
52       rw [he, iteratedDeriv_zero]
53       exact (zeroPartialFraction_locally_uniform hs hf0).mono (subset_univ _)
54   | succ n ih =>
55       have hd := locally_uniform_sum_deriv ih hU (fun i w hw =>
56         (zeroResolventJet_hasDerivAt n i (hn i w hw)).differentiableAt.differentiableWithinAt)
57       rw [← iteratedDeriv_succ] at hd
58       apply hd.congr
59       intro S w hw
60       apply Finset.sum_congr rfl
61       intro i _
62       exact (zeroResolventJet_hasDerivAt n i (hn i w hw)).deriv
63 
64 /-- The zero power sum uses the complete actual zero multiset. -/
65 def zeroPowerSum (f : ℂ → ℂ) (m : ℕ) : ℂ :=
66   ∑' i : ZeroMultiplicityIndex f, 1 / indexedZero i ^ m
67 
68 theorem zeroPowerSum_hasSum_from_resolvent {f : ℂ → ℂ} (hf : Differentiable ℂ f)
69     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (n : ℕ) :
70     HasSum (fun i : ZeroMultiplicityIndex f => (n.factorial : ℂ) / indexedZero i ^ (n + 1))
71       (iteratedDeriv n (fun w => ∑' i, zeroPartialFraction f i w) 0) := by
72   simpa only [zeroResolventJet, sub_zero] using
73     (zeroResolventJet_locally_uniform hf hs hf0 n).hasSum hf0
74 
75 theorem zeroPowerSum_resolvent_derivative {f : ℂ → ℂ} (hf : Differentiable ℂ f)
76     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (n : ℕ) :
77     iteratedDeriv n (fun w => ∑' i, zeroPartialFraction f i w) 0 =
78       (n.factorial : ℂ) * zeroPowerSum f (n + 1) := by
79   rw [← (zeroPowerSum_hasSum_from_resolvent hf hs hf0 n).tsum_eq, zeroPowerSum, ← tsum_mul_left]
80   apply tsum_congr
81   intro i
82   rw [mul_one_div]
83 
84 end
85 end Komorebi.PaperIV

Back to source controls