AnalyticReciprocalLaws.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.CanonicalPartialFractions
6 import KomorebiPaperIV.AnalyticCycles
7 
8 namespace Komorebi.PaperIV
9 open Set Filter
10 open scoped Topology
11 noncomputable section
12 
13 /-- An actual analytic logarithm on a stated domain. -/
14 def IsLogarithmOn (f L : ℂ → ℂ) (s : Set ℂ) : Prop :=
15   DifferentiableOn ℂ L s ∧ ∀ z ∈ s, Complex.exp (L z) = f z
16 
17 /-- Reciprocal powers using one fixed logarithm on the whole domain. -/
18 def logarithmPower (L : ℂ → ℂ) (r : ℂ) (z : ℂ) : ℂ :=
19   Complex.exp (-r * L z)
20 
21 theorem logarithmPower_add (L : ℂ → ℂ) (r t z : ℂ) :
22     logarithmPower L r z * logarithmPower L t z = logarithmPower L (r + t) z := by
23   unfold logarithmPower
24   rw [← Complex.exp_add]
25   congr 1
26   ring
27 
28 theorem IsLogarithmOn.nonzero {f L : ℂ → ℂ} {s : Set ℂ}
29     (hL : IsLogarithmOn f L s) {z : ℂ} (hz : z ∈ s) : f z ≠ 0 := by
30   rw [← hL.2 z hz]
31   exact Complex.exp_ne_zero _
32 
33 theorem IsLogarithmOn.deriv {f L : ℂ → ℂ} {s : Set ℂ}
34     (hs : IsOpen s) (hL : IsLogarithmOn f L s) {z : ℂ} (hz : z ∈ s) :
35     deriv L z = logDeriv f z := by
36   have hd := (hL.1 z hz).differentiableAt (hs.mem_nhds hz)
37   have he : (fun w => Complex.exp (L w)) =ᶠ[𝓝 z] f :=
38     eventually_of_mem (hs.mem_nhds hz) (fun w hw => hL.2 w hw)
39   have h := he.deriv_eq
40   rw [hd.hasDerivAt.cexp.deriv, hL.2 z hz] at h
41   rw [logDeriv_apply]
42   apply (eq_div_iff (hL.nonzero hz)).mpr
43   simpa [mul_comm] using h
44 
45 theorem hasDerivAt_logarithmPower {f L : ℂ → ℂ} {s : Set ℂ}
46     (hs : IsOpen s) (hL : IsLogarithmOn f L s) (r : ℂ) {z : ℂ} (hz : z ∈ s) :
47     HasDerivAt (logarithmPower L r)
48       (r * (-logDeriv f z) * logarithmPower L r z) z := by
49   change HasDerivAt (fun w => Complex.exp (-r * L w))
50     (r * (-logDeriv f z) * Complex.exp (-r * L z)) z
51   have hd := (hL.1 z hz).differentiableAt (hs.mem_nhds hz)
52   have h := (hd.hasDerivAt.const_mul (-r)).cexp
53   rw [hL.deriv hs hz] at h
54   simpa only [logarithmPower, neg_mul, mul_neg, mul_assoc, mul_left_comm, mul_comm] using h
55 
56 theorem reciprocal_fixed_log_derivative {N : ℕ} {L : ℂ → ℂ} {s : Set ℂ}
57     (hs : IsOpen s) (hL : IsLogarithmOn (canonicalSignedDenominator N) L s)
58     (r : ℂ) {z : ℂ} (hz : z ∈ s) :
59     deriv (logarithmPower L r) z =
60       r * analyticTransferTangent N z * logarithmPower L r z :=
61   (hasDerivAt_logarithmPower hs hL r hz).deriv
62 
63 /-- Evaluation of the complete differential Bell polynomial on successive
64 derivatives of a function. Its defining recurrence is Y_(n+1)=Y_n'+gY_n. -/
65 def analyticDifferentialBell (g : ℂ → ℂ) : ℕ → ℂ → ℂ
66   | 0 => fun _ => 1
67   | n + 1 => fun z => deriv (analyticDifferentialBell g n) z + g z * analyticDifferentialBell g n z
68 
69 theorem analyticOnNhd_differentialBell {g : ℂ → ℂ} {s : Set ℂ}
70     (hg : AnalyticOnNhd ℂ g s) (n : ℕ) : AnalyticOnNhd ℂ (analyticDifferentialBell g n) s := by
71   induction n with
72   | zero => intro z _; exact analyticAt_const
73   | succ n ih => exact ih.deriv.add (hg.mul ih)
74 
75 theorem iteratedDeriv_eq_analyticDifferentialBell {f g : ℂ → ℂ} {s : Set ℂ}
76     (hs : IsOpen s) (hf : AnalyticOnNhd ℂ f s) (hg : AnalyticOnNhd ℂ g s)
77     (hfg : ∀ z ∈ s, deriv f z = g z * f z) (n : ℕ) :
78     ∀ z ∈ s, iteratedDeriv n f z = analyticDifferentialBell g n z * f z := by
79   induction n with
80   | zero => intro z _; simp [analyticDifferentialBell]
81   | succ n ih =>
82     intro z hz
83     have he : iteratedDeriv n f =ᶠ[𝓝 z]
84         (fun w => analyticDifferentialBell g n w * f w) :=
85       eventually_of_mem (hs.mem_nhds hz) (fun w hw => ih w hw)
86     rw [iteratedDeriv_succ, he.deriv_eq,
87       ((analyticOnNhd_differentialBell hg n z hz).differentiableAt.hasDerivAt.fun_mul
88         (hf z hz).differentiableAt.hasDerivAt).deriv,
89       hfg z hz]
90     simp only [analyticDifferentialBell]
91     ring
92 
93 theorem analytic_higher_riccati {N : ℕ} (hN : 0 < N) {z : ℂ}
94     (hz : canonicalSignedDenominator N z ≠ 0) :
95     analyticDifferentialBell (fun w => -analyticTransferTangent N w) N z = -1 := by
96   let f := canonicalSignedDenominator N
97   let s := {w : ℂ | f w ≠ 0}
98   have hf : Differentiable ℂ f := fun w =>
99     (analyticAt_entireSigned N 0 (canonicalPrimitiveRoot N) (canonicalSignedRoot N) w).differentiableAt
100   have hs : IsOpen s := isOpen_ne_fun hf.continuous continuous_const
101   have hg : AnalyticOnNhd ℂ (fun w => -analyticTransferTangent N w) s := by
102     intro w hw
103     change AnalyticAt ℂ (fun w => -(-logDeriv f w)) w
104     simp only [neg_neg, logDeriv_apply]
105     have hfa := hf.analyticAt w
106     have hfd := hfa.deriv
107     exact hfd.fun_div hfa (show f w ≠ 0 from hw)
108   have hfg : ∀ w ∈ s, deriv f w = (-analyticTransferTangent N w) * f w := by
109     intro w hw
110     change deriv f w = -(-logDeriv f w) * f w
111     simp only [neg_neg, logDeriv_apply]
112     exact (div_mul_cancel₀ _ hw).symm
113   have he := iteratedDeriv_eq_analyticDifferentialBell hs (fun w _ => hf.analyticAt w) hg hfg N z hz
114   have hode := entireSigned_ode (canonicalPrimitiveRoot_isPrimitive hN) (canonicalSignedRoot_pow hN) 0 z
115   change deriv^[N] f z = -f z at hode
116   rw [iteratedDeriv_eq_iterate, hode] at he
117   apply mul_right_cancel₀ hz
118   calc
119     _ = -f z := he.symm
120     _ = _ := by ring
121 
122 end
123 end Komorebi.PaperIV

Back to source controls