ODESolutions.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.EntireBridge
6 import Mathlib.Analysis.Analytic.Order
7 
8 /-! # Uniqueness and exact finite basis for the entire ODE solution space -/
9 
10 namespace Komorebi.PaperIV
11 noncomputable section
12 
13 /-- Zero initial derivatives force every Taylor coefficient to vanish. -/
14 theorem ode_all_derivatives_zero {N : ℕ} (hN : 0 < N) (c : ℂ) (f : ℂ → ℂ)
15     (hode : deriv^[N] f = fun z => c * f z)
16     (hinit : ∀ k < N, deriv^[k] f 0 = 0) :
17     ∀ k : ℕ, deriv^[k] f 0 = 0 := by
18   intro k
19   induction k using Nat.strong_induction_on with
20   | h k ih =>
21     by_cases hk : k < N
22     · exact hinit k hk
23     · have he : k = (k - N) + N := by omega
24       rw [he, Function.iterate_add_apply, hode,
25         ← iteratedDeriv_eq_iterate, iteratedDeriv_const_mul_field,
26         iteratedDeriv_eq_iterate, ih (k - N) (by omega), mul_zero]
27 
28 /-- Entire homogeneous ODE uniqueness derived from analytic order and the
29 identity theorem, without an ODE uniqueness certificate. -/
30 theorem entire_ode_zero_of_initial_zero {N : ℕ} (hN : 0 < N) (c : ℂ)
31     {f : ℂ → ℂ} (hf : ∀ z, AnalyticAt ℂ f z)
32     (hode : deriv^[N] f = fun z => c * f z)
33     (hinit : ∀ k < N, deriv^[k] f 0 = 0) : f = 0 := by
34   apply (AnalyticOnNhd.analyticOrderAt_eq_top_iff_eq_zero 0 hf).mp
35   rw [ENat.eq_top_iff_forall_ge]
36   intro n
37   apply (natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (hf 0)).mpr
38   intro k _
39   rw [iteratedDeriv_eq_iterate]
40   exact ode_all_derivatives_zero hN c f hode hinit k
41 
42 /-- Two entire solutions with the same first N derivatives are identical. -/
43 theorem entire_ode_unique {N : ℕ} (hN : 0 < N) (c : ℂ)
44     {f g : ℂ → ℂ} (hf : ∀ z, AnalyticAt ℂ f z) (hg : ∀ z, AnalyticAt ℂ g z)
45     (hfode : deriv^[N] f = fun z => c * f z)
46     (hgode : deriv^[N] g = fun z => c * g z)
47     (hinit : ∀ k < N, deriv^[k] f 0 = deriv^[k] g 0) : f = g := by
48   have hd (k : ℕ) (z : ℂ) :
49       deriv^[k] (f - g) z = deriv^[k] f z - deriv^[k] g z := by
50     simp only [← iteratedDeriv_eq_iterate]
51     exact iteratedDeriv_sub (hf z).contDiffAt (hg z).contDiffAt
52   have hzero := entire_ode_zero_of_initial_zero hN c (fun z => (hf z).sub (hg z))
53     (by funext z; rw [hd, hfode, hgode]; simp only [Pi.sub_apply]; ring)
54     (by intro k hk; rw [hd, hinit k hk, sub_self])
55   funext z
56   have hz := congrFun hzero z
57   exact sub_eq_zero.mp hz
58 
59 /-- A linear combination of the transfer basis, with ordinary complex coefficients. -/
60 def transferCombination (N : ℕ) (omega lambda : ℂ) (b : Fin N → ℂ) (z : ℂ) : ℂ :=
61   ∑ j : Fin N, b j * entireTransfer N j.val omega lambda z
62 
63 theorem analyticAt_transferCombination (N : ℕ) (omega lambda : ℂ)
64     (b : Fin N → ℂ) (z : ℂ) : AnalyticAt ℂ (transferCombination N omega lambda b) z := by
65   unfold transferCombination
66   have h := Finset.analyticAt_sum (N := Finset.univ) (f := fun j : Fin N => fun z =>
67     b j * entireTransfer N j.val omega lambda z)
68     (fun j _ => analyticAt_const.mul (analyticAt_entireTransfer N j.val omega lambda z))
69   simpa only [Finset.sum_fn] using h
70 
71 theorem transferCombination_derivative (N k : ℕ) (omega lambda : ℂ)
72     (b : Fin N → ℂ) (z : ℂ) :
73     deriv^[k] (transferCombination N omega lambda b) z =
74       ∑ j : Fin N, b j * deriv^[k] (entireTransfer N j.val omega lambda) z := by
75   rw [← iteratedDeriv_eq_iterate]
76   unfold transferCombination
77   simp only [← iteratedDeriv_eq_iterate]
78   rw [iteratedDeriv_fun_sum (fun j _ =>
79     (analyticAt_const.mul (analyticAt_entireTransfer N j.val omega lambda z)).contDiffAt)]
80   simp only [iteratedDeriv_const_mul_field]
81 
82 theorem transferCombination_ode {N : ℕ} {omega : ℂ}
83     (homega : IsPrimitiveRoot omega N) (lambda : ℂ) (b : Fin N → ℂ) :
84     deriv^[N] (transferCombination N omega lambda b) =
85       fun z => lambda ^ N * transferCombination N omega lambda b z := by
86   funext z
87   rw [transferCombination_derivative]
88   simp only [entireTransfer_ode homega, transferCombination, Finset.mul_sum]
89   apply Finset.sum_congr rfl
90   intro j _
91   ring
92 
93 theorem transferCombination_initial {N : ℕ} (hN : 0 < N)
94     {omega : ℂ} (homega : IsPrimitiveRoot omega N) (lambda : ℂ)
95     (b : Fin N → ℂ) (k : Fin N) :
96     deriv^[k.val] (transferCombination N omega lambda b) 0 = b k * lambda ^ k.val := by
97   rw [transferCombination_derivative]
98   have ht (j : Fin N) := entireTransfer_initial_data hN j.isLt k.isLt homega lambda
99   simp_rw [ht]
100   rw [Finset.sum_eq_single k]
101   · simp
102   · intro j _ hj
103     have hne : k.val ≠ j.val := by intro h; exact hj (Fin.ext h.symm)
104     simp [hne]
105   · simp
106 
107 /-- The exact solution formula for every entire solution of y^(N)=lambda^N y. -/
108 theorem entireTransfer_solution_expansion {N : ℕ} (hN : 0 < N)
109     {omega lambda : ℂ} (homega : IsPrimitiveRoot omega N) (hlambda : lambda ≠ 0)
110     {f : ℂ → ℂ} (hf : ∀ z, AnalyticAt ℂ f z)
111     (hode : deriv^[N] f = fun z => lambda ^ N * f z) :
112     f = transferCombination N omega lambda
113       (fun j => deriv^[j.val] f 0 / lambda ^ j.val) := by
114   apply entire_ode_unique hN (lambda ^ N) hf
115     (analyticAt_transferCombination N omega lambda _) hode
116     (transferCombination_ode homega lambda _)
117   intro k hk
118   have h := transferCombination_initial hN homega lambda
119     (fun j => deriv^[j.val] f 0 / lambda ^ j.val) (⟨k, hk⟩ : Fin N)
120   rw [h]
121   simp [pow_ne_zero k hlambda]
122 
123 /-- The coefficients in the solution expansion are unique, proving independence. -/
124 theorem transferCombination_injective {N : ℕ} (hN : 0 < N)
125     {omega lambda : ℂ} (homega : IsPrimitiveRoot omega N) (hlambda : lambda ≠ 0) :
126     Function.Injective (transferCombination N omega lambda) := by
127   intro b d h
128   funext k
129   have he := congrArg (fun f : ℂ → ℂ => deriv^[k.val] f 0) h
130   rw [transferCombination_initial hN homega, transferCombination_initial hN homega] at he
131   exact mul_right_cancel₀ (pow_ne_zero k.val hlambda) he
132 
133 /-- A linear combination in the signed basis. -/
134 def signedCombination (N : ℕ) (omega rho : ℂ) (b : Fin N → ℂ) (z : ℂ) : ℂ :=
135   ∑ j : Fin N, b j * entireSigned N j.val omega rho z
136 
137 theorem signedCombination_eq_transfer (N : ℕ) (omega rho : ℂ) (b : Fin N → ℂ) :
138     signedCombination N omega rho b =
139       transferCombination N omega rho (fun j => b j / rho ^ j.val) := by
140   funext z
141   unfold signedCombination transferCombination entireSigned
142   apply Finset.sum_congr rfl
143   intro j _
144   simp only [div_eq_mul_inv]
145   ring
146 
147 /-- The signed sections span every entire solution of y^(N) = -y. -/
148 theorem entireSigned_solution_expansion {N : ℕ} (hN : 0 < N)
149     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
150     {f : ℂ → ℂ} (hf : ∀ z, AnalyticAt ℂ f z)
151     (hode : deriv^[N] f = fun z => -f z) :
152     f = signedCombination N omega rho (fun j => deriv^[j.val] f 0) := by
153   have hr : rho ≠ 0 := by
154     intro h
155     simp [h, hN.ne'] at hrho
156   rw [signedCombination_eq_transfer]
157   apply entireTransfer_solution_expansion hN homega hr hf
158   simpa only [hrho, neg_one_mul] using hode
159 
160 /-- Signed solution coefficients are unique; the signed sections are independent. -/
161 theorem signedCombination_injective {N : ℕ} (hN : 0 < N)
162     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1) :
163     Function.Injective (signedCombination N omega rho) := by
164   have hr : rho ≠ 0 := by
165     intro h
166     simp [h, hN.ne'] at hrho
167   intro b d h
168   rw [signedCombination_eq_transfer, signedCombination_eq_transfer] at h
169   have he := transferCombination_injective hN homega hr h
170   funext j
171   exact (div_left_inj' (pow_ne_zero j.val hr)).mp (congrFun he j)
172 
173 end
174 end Komorebi.PaperIV

Back to source controls