CoupledGermInverse.lean

1 import CoupledUniqueness
2 import Mathlib.Analysis.Analytic.OfScalars
3 
4 /-! # Recovering labeled scale parameters from canonical analytic germs
5 
6 The coefficients use the ordinary odd series, not exponential generating series.
7 The comparison with Mathlib's formal multilinear series inserts zero even terms.
8 -/
9 
10 set_option autoImplicit false
11 set_option maxHeartbeats 1000000
12 
13 noncomputable section
14 
15 open Filter
16 open scoped Topology
17 
18 namespace Komorebi.SpecialFunctions.Coupled.Scales
19 
20 def denseOdd (c : ℕ → ℝ) (k : ℕ) : ℂ :=
21   if k % 2 = 1 then (c (k / 2) : ℂ) else 0
22 
23 theorem denseOdd_odd (c : ℕ → ℝ) (n : ℕ) :
24     denseOdd c (2 * n + 1) = (c n : ℂ) := by
25   have hm : (2 * n + 1) % 2 = 1 := by omega
26   have hd : (2 * n + 1) / 2 = n := by omega
27   simp [denseOdd, hm, hd]
28 
29 theorem denseOdd_even (c : ℕ → ℝ) (n : ℕ) :
30     denseOdd c (2 * n) = 0 := by
31   have hm : (2 * n) % 2 = 0 := by omega
32   simp [denseOdd, hm]
33 
34 theorem odd_hasSum_dense {c : ℕ → ℝ} {z w : ℂ}
35     (h : HasSum (fun n => (c n : ℂ) * z ^ (2 * n + 1)) w) :
36     HasSum (fun k => denseOdd c k * z ^ k) w := by
37   have hi : Function.Injective (fun n : ℕ => 2 * n + 1) := by
38     intro a b hab
39     change 2 * a + 1 = 2 * b + 1 at hab
40     omega
41   apply (hi.hasSum_iff (f := fun k => denseOdd c k * z ^ k) ?_).mp
42   · simpa only [Function.comp_def, denseOdd_odd] using h
43   · intro k hk
44     have hm : k % 2 ≠ 1 := by
45       intro hm
46       apply hk
47       refine ⟨k / 2, ?_⟩
48       change 2 * (k / 2) + 1 = k
49       omega
50     simp [denseOdd, hm]
51 
52 theorem odd_series_hasFPowerSeriesAt {c : ℕ → ℝ} {f : ℂ → ℂ}
53     (h : ∀ᶠ z in 𝓝 (0 : ℂ),
54       HasSum (fun n => (c n : ℂ) * z ^ (2 * n + 1)) (f z)) :
55     HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars ℂ (denseOdd c)) 0 := by
56   apply hasFPowerSeriesAt_iff.mpr
57   filter_upwards [h] with z hz
58   simpa only [FormalMultilinearSeries.coeff_ofScalars, zero_add, smul_eq_mul,
59     mul_comm] using odd_hasSum_dense hz
60 
61 theorem odd_coefficients_eq_of_germ_eq {c d : ℕ → ℝ} {f g : ℂ → ℂ}
62     (hc : ∀ᶠ z in 𝓝 (0 : ℂ),
63       HasSum (fun n => (c n : ℂ) * z ^ (2 * n + 1)) (f z))
64     (hd : ∀ᶠ z in 𝓝 (0 : ℂ),
65       HasSum (fun n => (d n : ℂ) * z ^ (2 * n + 1)) (g z))
66     (hfg : f =ᶠ[𝓝 0] g) : c = d := by
67   have hp := (odd_series_hasFPowerSeriesAt hc).eq_formalMultilinearSeries_of_eventually
68     (odd_series_hasFPowerSeriesAt hd) hfg
69   funext n
70   have hn := congrArg (fun p : FormalMultilinearSeries ℂ ℂ ℂ => p.coeff (2 * n + 1)) hp
71   simpa only [FormalMultilinearSeries.coeff_ofScalars, denseOdd_odd,
72     Complex.ofReal_inj] using hn
73 
74 theorem odd_series_Taylor_coefficients {c : ℕ → ℝ} {f : ℂ → ℂ}
75     {p : FormalMultilinearSeries ℂ ℂ ℂ} (hp : HasFPowerSeriesAt f p 0)
76     (hc : ∀ᶠ z in 𝓝 (0 : ℂ),
77       HasSum (fun n => (c n : ℂ) * z ^ (2 * n + 1)) (f z)) (k : ℕ) :
78     p.coeff k = denseOdd c k := by
79   have he := hp.eq_formalMultilinearSeries (odd_series_hasFPowerSeriesAt hc)
80   simpa only [FormalMultilinearSeries.coeff_ofScalars] using
81     congrArg (fun q : FormalMultilinearSeries ℂ ℂ ℂ => q.coeff k) he
82 
83 theorem coupled_hasFPowerSeriesAt (s : Scales) (hs : s.positive)
84     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
85     HasFPowerSeriesAt s.U
86       (FormalMultilinearSeries.ofScalars ℂ (denseOdd (fun n => (s.coefficients n).1))) 0 ∧
87     HasFPowerSeriesAt s.V
88       (FormalMultilinearSeries.ofScalars ℂ (denseOdd (fun n => (s.coefficients n).2))) 0 := by
89   exact ⟨odd_series_hasFPowerSeriesAt (Eventually.of_forall fun z =>
90       (s.coefficient_series_entire hs hstrict z).1.of_norm.hasSum),
91     odd_series_hasFPowerSeriesAt (Eventually.of_forall fun z =>
92       (s.coefficient_series_entire hs hstrict z).2.of_norm.hasSum)⟩
93 
94 theorem coefficients_eq_of_analytic_germs {s t : Scales}
95     (hs : s.positive) (ht : t.positive)
96     (hstricts : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
97     (hstrictt : t.q < 1 ∧ t.r < 1 ∧ t.a < 1 ∧ t.b < 1)
98     (hU : s.U =ᶠ[𝓝 0] t.U) (hV : s.V =ᶠ[𝓝 0] t.V) :
99     s.coefficients = t.coefficients := by
100   have h1 := odd_coefficients_eq_of_germ_eq
101     (Eventually.of_forall fun z => (s.coefficient_series_entire hs hstricts z).1.of_norm.hasSum)
102     (Eventually.of_forall fun z => (t.coefficient_series_entire ht hstrictt z).1.of_norm.hasSum) hU
103   have h2 := odd_coefficients_eq_of_germ_eq
104     (Eventually.of_forall fun z => (s.coefficient_series_entire hs hstricts z).2.of_norm.hasSum)
105     (Eventually.of_forall fun z => (t.coefficient_series_entire ht hstrictt z).2.of_norm.hasSum) hV
106   funext n
107   exact Prod.ext (congrFun h1 n) (congrFun h2 n)
108 
109 theorem sameJet_of_analytic_germs {s t : Scales}
110     (hs : s.positive) (ht : t.positive)
111     (hstricts : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
112     (hstrictt : t.q < 1 ∧ t.r < 1 ∧ t.a < 1 ∧ t.b < 1)
113     (hU : s.U =ᶠ[𝓝 0] t.U) (hV : s.V =ᶠ[𝓝 0] t.V) : s.sameJet t := by
114   apply sameJet_of_coefficients_eq
115   intro n _ _
116   exact congrFun (coefficients_eq_of_analytic_germs hs ht hstricts hstrictt hU hV) n
117 
118 /-- The guarded analytic-germ parameter-recovery implication of Theorem G.2. -/
119 theorem parameters_of_analytic_germs {s t : Scales}
120     (hs : s.positive) (ht : t.positive)
121     (hstricts : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
122     (hstrictt : t.q < 1 ∧ t.r < 1 ∧ t.a < 1 ∧ t.b < 1)
123     (hD : s.defect ≠ 0)
124     (hU : s.U =ᶠ[𝓝 0] t.U) (hV : s.V =ᶠ[𝓝 0] t.V) : s = t :=
125   parameters_of_formal_pair_eq hs ht hD
126     (coefficients_eq_of_analytic_germs hs ht hstricts hstrictt hU hV)
127 
128 theorem parameters_of_entire_pair_eq {s t : Scales}
129     (hs : s.positive) (ht : t.positive)
130     (hstricts : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
131     (hstrictt : t.q < 1 ∧ t.r < 1 ∧ t.a < 1 ∧ t.b < 1)
132     (hD : s.defect ≠ 0) (hU : s.U = t.U) (hV : s.V = t.V) : s = t :=
133   parameters_of_analytic_germs hs ht hstricts hstrictt hD
134     (Eventually.of_forall fun z => congrFun hU z)
135     (Eventually.of_forall fun z => congrFun hV z)
136 
137 theorem analytic_solution_Taylor_coefficients (s : Scales) (hs : s.positive)
138     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
139     {f g : ℂ → ℂ} {p q : FormalMultilinearSeries ℂ ℂ ℂ}
140     (hp : HasFPowerSeriesAt f p 0) (hq : HasFPowerSeriesAt g q 0)
141     (hzero : f 0 = 0 ∧ g 0 = 0) (heq : s.GermEquations f g) (k : ℕ) :
142     p.coeff k = denseOdd (fun n => (s.coefficients n).1) k ∧
143     q.coeff k = denseOdd (fun n => (s.coefficients n).2) k := by
144   have hc := s.analytic_solution_hasSum hs hstrict hp.analyticAt hq.analyticAt hzero heq
145   exact ⟨odd_series_Taylor_coefficients hp (hc.mono fun _ hz => hz.1) k,
146     odd_series_Taylor_coefficients hq (hc.mono fun _ hz => hz.2) k⟩
147 
148 theorem parameters_of_shared_solution_germ {s t : Scales}
149     (hs : s.positive) (ht : t.positive)
150     (hstricts : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
151     (hstrictt : t.q < 1 ∧ t.r < 1 ∧ t.a < 1 ∧ t.b < 1)
152     (hD : s.defect ≠ 0) {f g : ℂ → ℂ}
153     (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0)
154     (hzero : f 0 = 0 ∧ g 0 = 0)
155     (heqs : s.GermEquations f g) (heqt : t.GermEquations f g) : s = t := by
156   have hsc := s.analytic_solution_germ_eq hs hstricts hf hg hzero heqs
157   have htc := t.analytic_solution_germ_eq ht hstrictt hf hg hzero heqt
158   exact parameters_of_analytic_germs hs ht hstricts hstrictt hD
159     (hsc.1.symm.trans htc.1) (hsc.2.symm.trans htc.2)
160 
161 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls