CoupledUniqueness.lean

1 import CoupledEntire
2 import Mathlib.Analysis.Analytic.Order
3 
4 /-!
5 # Analytic uniqueness of the coupled equations
6 
7 The proof compares vanishing orders of differences of solution germs.
8 No parity or coefficient recurrence is assumed of the competing functions.
9 -/
10 
11 set_option autoImplicit false
12 set_option maxHeartbeats 1000000
13 
14 noncomputable section
15 
16 open Filter
17 open scoped Topology
18 
19 namespace Komorebi.SpecialFunctions.Coupled.Scales
20 
21 theorem analytic_scale_at_zero {f : ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (c : ℂ) :
22     AnalyticAt ℂ (fun z => f (c * z)) 0 := by
23   exact hf.comp_of_eq (by fun_prop) (by simp)
24 
25 /-- Scaling preserves a lower vanishing-order bound. A zero scale is handled
26 by the zero initial value, rather than by division or an inverse map. -/
27 theorem analytic_order_scale_ge {f : ℂ → ℂ} (_hf : AnalyticAt ℂ f 0)
28     (hzero : f 0 = 0) (c : ℂ) {n : ℕ} (hn : (n : ℕ∞) ≤ analyticOrderAt f 0) :
29     (n : ℕ∞) ≤ analyticOrderAt (fun z => f (c * z)) 0 := by
30   by_cases hc : c = 0
31   · have htop : analyticOrderAt (fun z => f (c * z)) 0 = ⊤ :=
32       analyticOrderAt_eq_top.mpr (.of_forall (fun z => by simp [hc, hzero]))
33     rw [htop]
34     exact le_top
35   · have ha : AnalyticAt ℂ (fun z : ℂ => c * z) 0 := by fun_prop
36     have hd : deriv (fun z : ℂ => c * z) 0 = c := by simp
37     change (n : ℕ∞) ≤ analyticOrderAt (f ∘ fun z : ℂ => c * z) 0
38     rw [analyticOrderAt_comp_of_deriv_ne_zero ha (by rwa [hd]), mul_zero]
39     exact hn
40 
41 theorem analytic_order_mul_ge_left {f g : ℂ → ℂ}
42     (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0)
43     {n : ℕ} (hn : (n : ℕ∞) ≤ analyticOrderAt f 0) :
44     (n : ℕ∞) ≤ analyticOrderAt (fun z => f z * g z) 0 := by
45   change (n : ℕ∞) ≤ analyticOrderAt (f * g) 0
46   rw [analyticOrderAt_mul hf hg]
47   exact hn.trans le_self_add
48 
49 theorem analytic_order_mul_ge_right {f g : ℂ → ℂ}
50     (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0)
51     {n : ℕ} (hn : (n : ℕ∞) ≤ analyticOrderAt g 0) :
52     (n : ℕ∞) ≤ analyticOrderAt (fun z => f z * g z) 0 := by
53   change (n : ℕ∞) ≤ analyticOrderAt (f * g) 0
54   rw [analyticOrderAt_mul hf hg]
55   exact hn.trans le_add_self
56 
57 /-- The two product-difference terms preserve the common vanishing order. -/
58 theorem analytic_row_order_ge {h k u v : ℂ → ℂ}
59     (hh : AnalyticAt ℂ h 0) (hk : AnalyticAt ℂ k 0)
60     (hu : AnalyticAt ℂ u 0) (hv : AnalyticAt ℂ v 0)
61     (hh0 : h 0 = 0) (hk0 : k 0 = 0) (x y : ℂ) {n : ℕ}
62     (hn : (n : ℕ∞) ≤ analyticOrderAt h 0)
63     (kn : (n : ℕ∞) ≤ analyticOrderAt k 0) :
64     (n : ℕ∞) ≤ analyticOrderAt
65       (fun z => h (x * z) * v (y * z) + u (x * z) * k (y * z)) 0 := by
66   have hleft := analytic_order_mul_ge_left (analytic_scale_at_zero hh x)
67     (analytic_scale_at_zero hv y) (analytic_order_scale_ge hh hh0 x hn)
68   have hright := analytic_order_mul_ge_right (analytic_scale_at_zero hu x)
69     (analytic_scale_at_zero hk y) (analytic_order_scale_ge hk hk0 y kn)
70   exact (le_min hleft hright).trans le_analyticOrderAt_add
71 
72 /-- Local equations determine the derivative of a difference in a neighborhood. -/
73 theorem derivative_difference_germ {e E f g F G : ℂ → ℂ}
74     (he : AnalyticAt ℂ e 0) (hE : AnalyticAt ℂ E 0) (x y : ℂ)
75     (heq : ∀ᶠ z in 𝓝 (0 : ℂ), deriv e z = 1 + f (x * z) * g (y * z))
76     (hEq : ∀ᶠ z in 𝓝 (0 : ℂ), deriv E z = 1 + F (x * z) * G (y * z)) :
77     deriv (fun z => e z - E z) =ᶠ[𝓝 (0 : ℂ)]
78       (fun z => (f (x * z) - F (x * z)) * g (y * z) +
79         F (x * z) * (g (y * z) - G (y * z))) := by
80   filter_upwards [heq, hEq, he.eventually_analyticAt, hE.eventually_analyticAt] with z hz hZ hez hEz
81   rw [deriv_fun_sub hez.differentiableAt hEz.differentiableAt, hz, hZ]
82   ring
83 
84 /-- The paired differential equations hold as identities of germs at zero. -/
85 def GermEquations (s : Scales) (f g : ℂ → ℂ) : Prop :=
86   ∀ᶠ z in 𝓝 (0 : ℂ),
87     deriv f z = 1 + f ((s.q : ℂ) * z) * g ((s.r : ℂ) * z) ∧
88     deriv g z = 1 + f ((s.a : ℂ) * z) * g ((s.b : ℂ) * z)
89 
90 /-- Conditional uniqueness of analytic germs, without positivity, contraction,
91 parity, or a recurrence hypothesis on the competing functions. -/
92 theorem analytic_pair_germ_unique (s : Scales) {f g F G : ℂ → ℂ}
93     (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0)
94     (hF : AnalyticAt ℂ F 0) (hG : AnalyticAt ℂ G 0)
95     (hinit : f 0 = F 0 ∧ g 0 = G 0)
96     (heq : s.GermEquations f g) (hEq : s.GermEquations F G) :
97     f =ᶠ[𝓝 (0 : ℂ)] F ∧ g =ᶠ[𝓝 (0 : ℂ)] G := by
98   have hh : AnalyticAt ℂ (fun z => f z - F z) 0 := hf.sub hF
99   have hk : AnalyticAt ℂ (fun z => g z - G z) 0 := hg.sub hG
100   have hh0 : f 0 - F 0 = 0 := sub_eq_zero.mpr hinit.1
101   have hk0 : g 0 - G 0 = 0 := sub_eq_zero.mpr hinit.2
102   have hdf := derivative_difference_germ (f := f) (g := g) (F := F) (G := G)
103     hf hF (s.q : ℂ) (s.r : ℂ)
104     (heq.mono (fun _ h => h.1)) (hEq.mono (fun _ h => h.1))
105   have hdg := derivative_difference_germ (f := f) (g := g) (F := F) (G := G)
106     hg hG (s.a : ℂ) (s.b : ℂ)
107     (heq.mono (fun _ h => h.2)) (hEq.mono (fun _ h => h.2))
108   have horders (n : ℕ) :
109       (n : ℕ∞) ≤ analyticOrderAt (fun z => f z - F z) 0 ∧
110       (n : ℕ∞) ≤ analyticOrderAt (fun z => g z - G z) 0 := by
111     induction n with
112     | zero => exact ⟨bot_le, bot_le⟩
113     | succ n ih =>
114       have hrow1 := analytic_row_order_ge hh hk hF hg hh0 hk0
115         (s.q : ℂ) (s.r : ℂ) ih.1 ih.2
116       have hrow2 := analytic_row_order_ge hh hk hF hg hh0 hk0
117         (s.a : ℂ) (s.b : ℂ) ih.1 ih.2
118       rw [← analyticOrderAt_congr hdf] at hrow1
119       rw [← analyticOrderAt_congr hdg] at hrow2
120       constructor
121       · simpa only [Nat.cast_succ, Nat.cast_add, Nat.cast_one] using
122           (analyticOrderAt_deriv_ge_iff hh hh0).mp hrow1
123       · simpa only [Nat.cast_succ, Nat.cast_add, Nat.cast_one] using
124           (analyticOrderAt_deriv_ge_iff hk hk0).mp hrow2
125   have htop1 := ENat.eq_top_iff_forall_ge.mpr (fun n => (horders n).1)
126   have htop2 := ENat.eq_top_iff_forall_ge.mpr (fun n => (horders n).2)
127   exact ⟨(analyticOrderAt_eq_top.mp htop1).mono (fun _ h => sub_eq_zero.mp h),
128     (analyticOrderAt_eq_top.mp htop2).mono (fun _ h => sub_eq_zero.mp h)⟩
129 
130 /-- A normalized entire solution uses actual derivatives at every point. -/
131 def IsEntireSolution (s : Scales) (f g : ℂ → ℂ) : Prop :=
132   f 0 = 0 ∧ g 0 = 0 ∧ ∀ z : ℂ,
133     HasDerivAt f (1 + f ((s.q : ℂ) * z) * g ((s.r : ℂ) * z)) z ∧
134     HasDerivAt g (1 + f ((s.a : ℂ) * z) * g ((s.b : ℂ) * z)) z
135 
136 theorem entire_solution_differentiable {s : Scales} {f g : ℂ → ℂ}
137     (hsol : s.IsEntireSolution f g) : Differentiable ℂ f ∧ Differentiable ℂ g :=
138   ⟨fun z => (hsol.2.2 z).1.differentiableAt, fun z => (hsol.2.2 z).2.differentiableAt⟩
139 
140 /-- Identity of germs extends to the whole plane for entire solution pairs. -/
141 theorem entire_solution_unique (s : Scales) {f g F G : ℂ → ℂ}
142     (hsol : s.IsEntireSolution f g) (hSol : s.IsEntireSolution F G) : f = F ∧ g = G := by
143   have hd := entire_solution_differentiable hsol
144   have hD := entire_solution_differentiable hSol
145   have heq : s.GermEquations f g := .of_forall (fun z =>
146     ⟨(hsol.2.2 z).1.deriv, (hsol.2.2 z).2.deriv⟩)
147   have hEq : s.GermEquations F G := .of_forall (fun z =>
148     ⟨(hSol.2.2 z).1.deriv, (hSol.2.2 z).2.deriv⟩)
149   have he := s.analytic_pair_germ_unique (hd.1.analyticAt 0) (hd.2.analyticAt 0)
150     (hD.1.analyticAt 0) (hD.2.analyticAt 0)
151     ⟨hsol.1.trans hSol.1.symm, hsol.2.1.trans hSol.2.1.symm⟩ heq hEq
152   have hfA : AnalyticOnNhd ℂ f Set.univ := fun z _ => hd.1.analyticAt z
153   have hgA : AnalyticOnNhd ℂ g Set.univ := fun z _ => hd.2.analyticAt z
154   have hFA : AnalyticOnNhd ℂ F Set.univ := fun z _ => hD.1.analyticAt z
155   have hGA : AnalyticOnNhd ℂ G Set.univ := fun z _ => hD.2.analyticAt z
156   exact ⟨hfA.eq_of_eventuallyEq hFA he.1, hgA.eq_of_eventuallyEq hGA he.2⟩
157 
158 theorem entire_solution_eq (s : Scales) (hs : s.positive)
159     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
160     {f g : ℂ → ℂ} (hsol : s.IsEntireSolution f g) : f = s.U ∧ g = s.V :=
161   s.entire_solution_unique hsol (s.coupled_entire_solution hs hstrict)
162 
163 theorem coupled_entire_exists_unique (s : Scales) (hs : s.positive)
164     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
165     ∃! pair : (ℂ → ℂ) × (ℂ → ℂ), s.IsEntireSolution pair.1 pair.2 := by
166   refine ⟨(s.U, s.V), s.coupled_entire_solution hs hstrict, ?_⟩
167   intro pair hp
168   have he := s.entire_solution_eq hs hstrict hp
169   exact Prod.ext he.1 he.2
170 
171 /-- An arbitrary normalized analytic solution germ is the canonical germ;
172 neither oddness nor any coefficient formula is assumed of it. -/
173 theorem analytic_solution_germ_eq (s : Scales) (hs : s.positive)
174     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
175     {f g : ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0)
176     (hzero : f 0 = 0 ∧ g 0 = 0) (heq : s.GermEquations f g) :
177     f =ᶠ[𝓝 (0 : ℂ)] s.U ∧ g =ᶠ[𝓝 (0 : ℂ)] s.V := by
178   have hd := s.coupled_entire hs hstrict
179   have hcanonical := s.coupled_entire_solution hs hstrict
180   exact s.analytic_pair_germ_unique hf hg (hd.1.analyticAt 0) (hd.2.analyticAt 0)
181     ⟨hzero.1.trans hcanonical.1.symm, hzero.2.trans hcanonical.2.1.symm⟩ heq
182     (.of_forall (fun z => s.coupled_entire_equations hs hstrict z))
183 
184 /-- Reverse analytic-to-series bridge in the manuscript's ordinary odd-series
185 normalization. The coefficients are the already proved unique recurrence. -/
186 theorem analytic_solution_hasSum (s : Scales) (hs : s.positive)
187     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
188     {f g : ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0)
189     (hzero : f 0 = 0 ∧ g 0 = 0) (heq : s.GermEquations f g) :
190     ∀ᶠ z in 𝓝 (0 : ℂ),
191       HasSum (fun n => ((s.coefficients n).1 : ℂ) * z ^ (2 * n + 1)) (f z) ∧
192       HasSum (fun n => ((s.coefficients n).2 : ℂ) * z ^ (2 * n + 1)) (g z) := by
193   have he := s.analytic_solution_germ_eq hs hstrict hf hg hzero heq
194   filter_upwards [he.1, he.2] with z hz hZ
195   rw [hz, hZ]
196   exact ⟨(s.coefficient_series_entire hs hstrict z).1.of_norm.hasSum,
197     (s.coefficient_series_entire hs hstrict z).2.of_norm.hasSum⟩
198 
199 theorem entire_solution_hasSum (s : Scales) (hs : s.positive)
200     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
201     {f g : ℂ → ℂ} (hsol : s.IsEntireSolution f g) (z : ℂ) :
202     HasSum (fun n => ((s.coefficients n).1 : ℂ) * z ^ (2 * n + 1)) (f z) ∧
203     HasSum (fun n => ((s.coefficients n).2 : ℂ) * z ^ (2 * n + 1)) (g z) := by
204   have he := s.entire_solution_eq hs hstrict hsol
205   rw [he.1, he.2]
206   exact ⟨(s.coefficient_series_entire hs hstrict z).1.of_norm.hasSum,
207     (s.coefficient_series_entire hs hstrict z).2.of_norm.hasSum⟩
208 
209 theorem entire_solution_odd (s : Scales) (hs : s.positive)
210     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
211     {f g : ℂ → ℂ} (hsol : s.IsEntireSolution f g) (z : ℂ) :
212     f (-z) = -f z ∧ g (-z) = -g z := by
213   have he := s.entire_solution_eq hs hstrict hsol
214   rw [he.1, he.2]
215   exact s.coupled_odd z
216 
217 /-- Appendix F.1 in the ordinary-series formulation used by the manuscript:
218 unique normalized entire pair, its canonical recurrence and positive coefficients,
219 its convergent odd expansions, and oddness of the constructed pair. -/
220 theorem coupled_F1_contract (s : Scales) (hs : s.positive)
221     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
222     (∃! pair : (ℂ → ℂ) × (ℂ → ℂ), s.IsEntireSolution pair.1 pair.2) ∧
223     s.IsCoefficientSolution s.coefficients ∧
224     (∀ n, 0 < (s.coefficients n).1 ∧ 0 < (s.coefficients n).2) ∧
225     (∀ z : ℂ,
226       HasSum (fun n => ((s.coefficients n).1 : ℂ) * z ^ (2 * n + 1)) (s.U z) ∧
227       HasSum (fun n => ((s.coefficients n).2 : ℂ) * z ^ (2 * n + 1)) (s.V z)) ∧
228     (∀ z : ℂ, s.U (-z) = -s.U z ∧ s.V (-z) = -s.V z) := by
229   refine ⟨s.coupled_entire_exists_unique hs hstrict, s.coefficients_solution,
230     s.coefficients_positive hs, ?_, s.coupled_odd⟩
231   intro z
232   exact ⟨(s.coefficient_series_entire hs hstrict z).1.of_norm.hasSum,
233     (s.coefficient_series_entire hs hstrict z).2.of_norm.hasSum⟩
234 
235 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls