AnalyticCycles.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ODESolutions
6 import KomorebiPaperIV.CompanionCompletion
7 
8 /-! # Exact pointwise derivative cycles from formal Taylor coefficients -/
9 
10 namespace Komorebi.PaperIV
11 noncomputable section
12 open scoped PowerSeries
13 
14 /-- Entire functions are determined by all their derivatives at the origin. -/
15 theorem entire_eq_of_all_derivatives {f g : ℂ → ℂ}
16     (hf : ∀ z, AnalyticAt ℂ f z) (hg : ∀ z, AnalyticAt ℂ g z)
17     (hjets : ∀ k, deriv^[k] f 0 = deriv^[k] g 0) : f = g := by
18   have hd : ∀ z, AnalyticAt ℂ (f - g) z := fun z => (hf z).sub (hg z)
19   have hzero : f - g = 0 := by
20     apply (AnalyticOnNhd.analyticOrderAt_eq_top_iff_eq_zero 0 hd).mp
21     rw [ENat.eq_top_iff_forall_ge]
22     intro n
23     apply (natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (hd 0)).mpr
24     intro k _
25     rw [iteratedDeriv_sub (hf 0).contDiffAt (hg 0).contDiffAt,
26       iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate, hjets k, sub_self]
27   exact sub_eq_zero.mp hzero
28 
29 /-- A formal differential identity transfers to entire analytic realizations
30 with the corresponding Taylor coefficients. -/
31 theorem entire_derivative_of_formal {f g : ℂ → ℂ} {F G : ℂ⟦X⟧} (c : ℂ)
32     (hf : ∀ z, AnalyticAt ℂ f z) (hg : ∀ z, AnalyticAt ℂ g z)
33     (hfjets : ∀ k, deriv^[k] f 0 = (k.factorial : ℂ) * PowerSeries.coeff k F)
34     (hgjets : ∀ k, deriv^[k] g 0 = (k.factorial : ℂ) * PowerSeries.coeff k G)
35     (hformal : PowerSeries.derivative ℂ F = PowerSeries.C c * G) :
36     deriv f = fun z => c * g z := by
37   apply entire_eq_of_all_derivatives (fun z => (hf z).deriv)
38     (fun z => analyticAt_const.mul (hg z))
39   intro k
40   change deriv^[k] (deriv f) 0 = deriv^[k] (fun z => c * g z) 0
41   rw [← Function.iterate_succ_apply, hfjets,
42     ← iteratedDeriv_eq_iterate, iteratedDeriv_const_mul_field, iteratedDeriv_eq_iterate,
43     hgjets]
44   have hc := congrArg (PowerSeries.coeff k) hformal
45   rw [PowerSeries.coeff_derivative, PowerSeries.coeff_C_mul] at hc
46   rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
47   linear_combination (k.factorial : ℂ) * hc
48 
49 theorem entireTransfer_derivative_of_pos {N j : ℕ} (hN : 0 < N)
50     (hj : 0 < j) (hjN : j < N) {omega : ℂ} (homega : IsPrimitiveRoot omega N)
51     (lambda : ℂ) :
52     deriv (entireTransfer N j omega lambda) =
53       fun z => lambda * entireTransfer N (j - 1) omega lambda z := by
54   apply entire_derivative_of_formal lambda
55     (analyticAt_entireTransfer N j omega lambda)
56     (analyticAt_entireTransfer N (j - 1) omega lambda)
57     (entireTransfer_derivative_at_zero hN hjN homega lambda)
58     (entireTransfer_derivative_at_zero hN (by omega) homega lambda)
59   exact derivative_transferSection_of_pos hN hj hjN lambda
60 
61 theorem entireTransfer_derivative_zero {N : ℕ} (hN : 0 < N)
62     {omega : ℂ} (homega : IsPrimitiveRoot omega N) (lambda : ℂ) :
63     deriv (entireTransfer N 0 omega lambda) =
64       fun z => lambda * entireTransfer N (N - 1) omega lambda z := by
65   apply entire_derivative_of_formal lambda
66     (analyticAt_entireTransfer N 0 omega lambda)
67     (analyticAt_entireTransfer N (N - 1) omega lambda)
68     (entireTransfer_derivative_at_zero hN hN homega lambda)
69     (entireTransfer_derivative_at_zero hN (by omega) homega lambda)
70   exact derivative_transferSection_zero hN lambda
71 
72 theorem entireSigned_derivative_of_pos {N j : ℕ} (hN : 0 < N)
73     (hj : 0 < j) (hjN : j < N) {omega rho : ℂ}
74     (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1) :
75     deriv (entireSigned N j omega rho) = entireSigned N (j - 1) omega rho := by
76   have h := entire_derivative_of_formal 1
77     (analyticAt_entireSigned N j omega rho)
78     (analyticAt_entireSigned N (j - 1) omega rho)
79     (entireSigned_derivative_at_zero hN hjN homega hrho)
80     (entireSigned_derivative_at_zero hN (by omega) homega hrho)
81     (by simpa using derivative_signedSection_of_pos (R := ℂ) hN hj hjN)
82   simpa using h
83 
84 theorem entireSigned_derivative_zero {N : ℕ} (hN : 0 < N)
85     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1) :
86     deriv (entireSigned N 0 omega rho) = fun z => -entireSigned N (N - 1) omega rho z := by
87   have h := entire_derivative_of_formal (-1)
88     (analyticAt_entireSigned N 0 omega rho)
89     (analyticAt_entireSigned N (N - 1) omega rho)
90     (entireSigned_derivative_at_zero hN hN homega hrho)
91     (entireSigned_derivative_at_zero hN (by omega) homega hrho)
92     (by simpa using derivative_signedSection_zero (R := ℂ) hN)
93   simpa using h
94 
95 end
96 end Komorebi.PaperIV

Back to source controls