CoupledOperator.lean

1 import CoupledScalarReduction
2 import Mathlib.Order.Filter.Germ.Basic
3 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
4 
5 /-! # Autonomous linear projections of the coupled functional field -/
6 
7 set_option autoImplicit false
8 set_option maxHeartbeats 2000000
9 
10 noncomputable section
11 open Filter Set
12 open scoped Topology Matrix
13 
14 namespace Komorebi.SpecialFunctions.Coupled.Scales
15 
16 structure EntireInput where
17   u : ℂ → ℂ
18   v : ℂ → ℂ
19   hu : Differentiable ℂ u
20   hv : Differentiable ℂ v
21   u_zero : u 0 = 0
22   v_zero : v 0 = 0
23 
24 structure LocalInput where
25   u : ℂ → ℂ
26   v : ℂ → ℂ
27   hu : AnalyticAt ℂ u 0
28   hv : AnalyticAt ℂ v 0
29   u_zero : u 0 = 0
30   v_zero : v 0 = 0
31 
32 def EntireInput.toLocal (X : EntireInput) : LocalInput :=
33   ⟨X.u, X.v, X.hu.analyticAt 0, X.hv.analyticAt 0, X.u_zero, X.v_zero⟩
34 
35 def rowProjection (c : Fin 2 → ℂ) (u v : ℂ → ℂ) (z : ℂ) : ℂ :=
36   c 0 * u z + c 1 * v z
37 
38 def rowField (s : Scales) (c : Fin 2 → ℂ) (u v : ℂ → ℂ) (z : ℂ) : ℂ :=
39   c 0 * (1 + u ((s.q : ℂ) * z) * v ((s.r : ℂ) * z)) +
40     c 1 * (1 + u ((s.a : ℂ) * z) * v ((s.b : ℂ) * z))
41 
42 def entireProjection (c : Fin 2 → ℂ) (X : EntireInput) : ℂ → ℂ :=
43   rowProjection c X.u X.v
44 
45 def entireField (s : Scales) (c : Fin 2 → ℂ) (X : EntireInput) : ℂ → ℂ :=
46   s.rowField c X.u X.v
47 
48 def Autonomous (s : Scales) (c : Fin 2 → ℂ) : Prop :=
49   Function.FactorsThrough (s.entireField c) (entireProjection c)
50 
51 theorem autonomous_iff_scalar_functional (s : Scales) (c : Fin 2 → ℂ) :
52     s.Autonomous c ↔ ∃ H : (ℂ → ℂ) → (ℂ → ℂ),
53       ∀ X : EntireInput, s.entireField c X = H (entireProjection c X) := by
54   rw [Autonomous, Function.factorsThrough_iff]
55   constructor
56   · rintro ⟨H, hH⟩
57     exact ⟨H, fun X => congrFun hH X⟩
58   · rintro ⟨H, hH⟩
59     exact ⟨H, funext hH⟩
60 
61 def scaledInput (f : ℂ → ℂ) (hf : Differentiable ℂ f) (hzero : f 0 = 0)
62     (x y : ℂ) : EntireInput :=
63   ⟨fun z => x * f z, fun z => y * f z, hf.const_mul x, hf.const_mul y,
64     by simp [hzero], by simp [hzero]⟩
65 
66 def nodePolynomial (s : Scales) (z : ℂ) : ℂ :=
67   1 - (1 - z / (s.q : ℂ)) * (1 - z / (s.r : ℂ)) *
68     (1 - z / (s.a : ℂ)) * (1 - z / (s.b : ℂ))
69 
70 theorem nodePolynomial_differentiable (s : Scales) :
71     Differentiable ℂ s.nodePolynomial := by unfold nodePolynomial; fun_prop
72 
73 theorem nodePolynomial_zero (s : Scales) : s.nodePolynomial 0 = 0 := by
74   simp [nodePolynomial]
75 
76 theorem nodePolynomial_values (s : Scales) (hs : s.positive) :
77     s.nodePolynomial s.q = 1 ∧ s.nodePolynomial s.r = 1 ∧
78       s.nodePolynomial s.a = 1 ∧ s.nodePolynomial s.b = 1 := by
79   have hq : (s.q : ℂ) ≠ 0 := by exact_mod_cast ne_of_gt hs.1
80   have hr : (s.r : ℂ) ≠ 0 := by exact_mod_cast ne_of_gt hs.2.1
81   have ha : (s.a : ℂ) ≠ 0 := by exact_mod_cast ne_of_gt hs.2.2.1
82   have hb : (s.b : ℂ) ≠ 0 := by exact_mod_cast ne_of_gt hs.2.2.2
83   simp [nodePolynomial, hq, hr, ha, hb]
84 
85 theorem autonomous_scalar_fibers (s : Scales) (c : Fin 2 → ℂ) (h : s.Autonomous c)
86     {f : ℂ → ℂ} (hf : Differentiable ℂ f) (hz : f 0 = 0)
87     (hn : f s.q = 1 ∧ f s.r = 1 ∧ f s.a = 1 ∧ f s.b = 1)
88     {x y x' y' : ℂ} (he : c 0 * x + c 1 * y = c 0 * x' + c 1 * y') :
89     (c 0 + c 1) * x * y = (c 0 + c 1) * x' * y' := by
90   have hp : entireProjection c (scaledInput f hf hz x y) =
91       entireProjection c (scaledInput f hf hz x' y') := by
92     funext z
93     dsimp [entireProjection, rowProjection, scaledInput]
94     linear_combination f z * he
95   have hh := congrFun (h hp) 1
96   simp only [entireField, rowField, scaledInput, mul_one, hn.1, hn.2.1,
97     hn.2.2.1, hn.2.2.2] at hh
98   linear_combination hh
99 
100 theorem autonomous_row_sum_zero (s : Scales) (hs : s.positive) (c : Fin 2 → ℂ)
101     (h : s.Autonomous c) : c 0 + c 1 = 0 := by
102   have hh : ∀ {x y x' y' : ℂ}, c 0 * x + c 1 * y = c 0 * x' + c 1 * y' →
103       (c 0 + c 1) * x * y = (c 0 + c 1) * x' * y' :=
104     s.autonomous_scalar_fibers c h s.nodePolynomial_differentiable
105       s.nodePolynomial_zero (s.nodePolynomial_values hs)
106   have h0 := hh (x := 0) (y := 0) (x' := c 1) (y' := -c 0) (by ring)
107   have h1 := hh (x := 1) (y := 0) (x' := 1 + c 1) (y' := -c 0) (by ring)
108   have h2 := hh (x := 0) (y := 1) (x' := c 1) (y' := 1 - c 0) (by ring)
109   have hmul0 : (c 0 + c 1) * c 0 = 0 := by linear_combination h1 - h0
110   have hmul1 : (c 0 + c 1) * c 1 = 0 := by linear_combination h0 - h2
111   by_contra hsum
112   have hc0 := (mul_eq_zero.mp hmul0).resolve_left hsum
113   have hc1 := (mul_eq_zero.mp hmul1).resolve_left hsum
114   exact hsum (by simp [hc0, hc1])
115 
116 theorem nonzero_row_first_ne_zero {c : Fin 2 → ℂ} (hc : c ≠ 0)
117     (hsum : c 0 + c 1 = 0) : c 0 ≠ 0 := by
118   intro hz
119   apply hc
120   have hz1 : c 1 = 0 := by simpa [hz] using hsum
121   funext i
122   fin_cases i
123   · exact hz
124   · exact hz1
125 
126 theorem autonomous_scale_products (s : Scales) (hs : s.positive) (c : Fin 2 → ℂ)
127     (hc : c ≠ 0) (h : s.Autonomous c) :
128     s.q * s.r = s.a * s.b ∧ s.q ^ 2 * s.r = s.a ^ 2 * s.b := by
129   have hsum := s.autonomous_row_sum_zero hs c h
130   have hc0 := nonzero_row_first_ne_zero hc hsum
131   have hc1 : c 1 = -c 0 := by linear_combination hsum
132   let X : EntireInput := ⟨fun z => z, fun z => z, by fun_prop, by fun_prop,
133     by simp, by simp⟩
134   let Z : EntireInput := ⟨fun _ => 0, fun _ => 0, by fun_prop, by fun_prop,
135     by simp, by simp⟩
136   have hp : entireProjection c X = entireProjection c Z := by
137     funext z; dsimp [entireProjection, rowProjection, X, Z]; rw [hc1]; ring
138   have hF := congrFun (h hp) 1
139   dsimp [entireField, rowField, X, Z] at hF
140   rw [hc1] at hF
141   have he : c 0 * ((s.q : ℂ) * s.r - (s.a : ℂ) * s.b) = 0 := by
142     linear_combination hF
143   have hpC : (s.q : ℂ) * s.r = (s.a : ℂ) * s.b :=
144     sub_eq_zero.mp ((mul_eq_zero.mp he).resolve_left hc0)
145   have hpR : s.q * s.r = s.a * s.b := by exact_mod_cast hpC
146   let Y : EntireInput := ⟨fun z => z ^ 2 + z, fun z => z, by fun_prop, by fun_prop,
147     by simp, by simp⟩
148   let W : EntireInput := ⟨fun z => z ^ 2, fun _ => 0, by fun_prop, by fun_prop,
149     by simp, by simp⟩
150   have hp2 : entireProjection c Y = entireProjection c W := by
151     funext z; dsimp [entireProjection, rowProjection, Y, W]; rw [hc1]; ring
152   have hF2 := congrFun (h hp2) 1
153   dsimp [entireField, rowField, Y, W] at hF2
154   rw [hc1] at hF2
155   have he2 : c 0 * ((s.q : ℂ) ^ 2 * s.r - (s.a : ℂ) ^ 2 * s.b) = 0 := by
156     linear_combination hF2 - c 0 * hpC
157   have hp2C := sub_eq_zero.mp ((mul_eq_zero.mp he2).resolve_left hc0)
158   exact ⟨hpR, by exact_mod_cast hp2C⟩
159 
160 theorem autonomous_ordered_rows (s : Scales) (hs : s.positive) (c : Fin 2 → ℂ)
161     (hc : c ≠ 0) (h : s.Autonomous c) : s.q = s.a ∧ s.r = s.b := by
162   have hp := s.autonomous_scale_products hs c hc h
163   have hm := congrArg (fun t : ℝ => s.a * t) hp.1
164   have he : (s.q - s.a) * (s.q * s.r) = 0 := by nlinarith only [hp.2, hm]
165   have hq := sub_eq_zero.mp ((mul_eq_zero.mp he).resolve_right
166     (ne_of_gt (mul_pos hs.1 hs.2.1)))
167   exact ⟨hq, mul_left_cancel₀ (ne_of_gt hs.1) (by simpa only [← hq] using hp.1)⟩
168 
169 theorem ordered_rows_field_zero (s : Scales) (c : Fin 2 → ℂ)
170     (hq : s.q = s.a) (hr : s.r = s.b) (hc : c 0 + c 1 = 0)
171     (u v : ℂ → ℂ) : s.rowField c u v = 0 := by
172   funext z
173   dsimp [rowField]
174   rw [hq, hr]
175   calc
176     _ = (c 0 + c 1) * (1 + u ((s.a : ℂ) * z) * v ((s.b : ℂ) * z)) := by ring
177     _ = 0 := by rw [hc, zero_mul]
178 
179 theorem ordered_rows_autonomous (s : Scales) (c : Fin 2 → ℂ)
180     (hq : s.q = s.a) (hr : s.r = s.b) (hc : c 0 + c 1 = 0) : s.Autonomous c := by
181   intro X Y _
182   exact (s.ordered_rows_field_zero c hq hr hc X.u X.v).trans
183     (s.ordered_rows_field_zero c hq hr hc Y.u Y.v).symm
184 
185 theorem zero_row_autonomous (s : Scales) : s.Autonomous 0 := by
186   intro X Y _
187   ext z
188   simp [entireField, rowField]
189 
190 theorem autonomous_iff_zero_or_ordered (s : Scales) (hs : s.positive) (c : Fin 2 → ℂ) :
191     s.Autonomous c ↔ c = 0 ∨ (s.q = s.a ∧ s.r = s.b ∧ c 0 + c 1 = 0) := by
192   constructor
193   · intro h
194     by_cases hc : c = 0
195     · exact Or.inl hc
196     · exact Or.inr ⟨(s.autonomous_ordered_rows hs c hc h).1,
197         (s.autonomous_ordered_rows hs c hc h).2, s.autonomous_row_sum_zero hs c h⟩
198   · rintro (rfl | ⟨hq, hr, hc⟩)
199     · exact s.zero_row_autonomous
200     · exact s.ordered_rows_autonomous c hq hr hc
201 
202 theorem autonomous_nonzero_classification (s : Scales) (hs : s.positive)
203     (c : Fin 2 → ℂ) (hc : c ≠ 0) :
204     s.Autonomous c ↔ s.q = s.a ∧ s.r = s.b ∧ ∃ γ : ℂ, γ ≠ 0 ∧ c = ![γ, -γ] := by
205   constructor
206   · intro h
207     have hsum := s.autonomous_row_sum_zero hs c h
208     have hr := s.autonomous_ordered_rows hs c hc h
209     refine ⟨hr.1, hr.2, c 0, nonzero_row_first_ne_zero hc hsum, ?_⟩
210     funext i
211     fin_cases i
212     · rfl
213     · change c 1 = -c 0
214       linear_combination hsum
215   · rintro ⟨hq, hr, γ, _, rfl⟩
216     exact s.ordered_rows_autonomous ![γ, -γ] hq hr (by simp)
217 
218 theorem autonomous_projected_field_zero (s : Scales) (hs : s.positive)
219     (c : Fin 2 → ℂ) (h : s.Autonomous c) (u v : ℂ → ℂ) : s.rowField c u v = 0 := by
220   rcases (s.autonomous_iff_zero_or_ordered hs c).mp h with rfl | ⟨hq, hr, hc⟩
221   · ext z; simp [rowField]
222   · exact s.ordered_rows_field_zero c hq hr hc u v
223 
224 theorem no_nonzero_autonomous_if_rows_differ (s : Scales) (hs : s.positive)
225     (hne : ¬(s.q = s.a ∧ s.r = s.b)) (c : Fin 2 → ℂ) (hc : c ≠ 0) :
226     ¬s.Autonomous c := fun h => hne (s.autonomous_ordered_rows hs c hc h)
227 
228 theorem autonomous_matrix_det_zero (s : Scales) (hs : s.positive)
229     (P : Matrix (Fin 2) (Fin 2) ℂ) (h : ∀ i, s.Autonomous (P i)) : P.det = 0 := by
230   have h0 := s.autonomous_row_sum_zero hs (P 0) (h 0)
231   have h1 := s.autonomous_row_sum_zero hs (P 1) (h 1)
232   rw [Matrix.det_fin_two]
233   linear_combination P 0 0 * h1 - P 1 0 * h0
234 
235 theorem no_invertible_constant_decoupling (s : Scales) (hs : s.positive)
236     (P : Matrix (Fin 2) (Fin 2) ℂ) (hP : IsUnit P) : ¬∀ i, s.Autonomous (P i) := by
237   intro h
238   exact ((Matrix.isUnit_iff_isUnit_det P).mp hP).ne_zero (s.autonomous_matrix_det_zero hs P h)
239 
240 abbrev ScalarGerm := Germ (𝓝 (0 : ℂ)) ℂ
241 
242 def localProjection (c : Fin 2 → ℂ) (X : LocalInput) : ScalarGerm :=
243   (rowProjection c X.u X.v : ℂ → ℂ)
244 
245 def localField (s : Scales) (c : Fin 2 → ℂ) (X : LocalInput) : ScalarGerm :=
246   (s.rowField c X.u X.v : ℂ → ℂ)
247 
248 def GermAutonomous (s : Scales) (c : Fin 2 → ℂ) : Prop :=
249   Function.FactorsThrough (s.localField c) (localProjection c)
250 
251 theorem local_projection_analytic (c : Fin 2 → ℂ) (X : LocalInput) :
252     AnalyticAt ℂ (rowProjection c X.u X.v) 0 := by
253   exact (analyticAt_const.mul X.hu).add (analyticAt_const.mul X.hv)
254 
255 theorem local_field_analytic (s : Scales) (c : Fin 2 → ℂ) (X : LocalInput) :
256     AnalyticAt ℂ (s.rowField c X.u X.v) 0 := by
257   have hq := analytic_scale_at_zero X.hu (s.q : ℂ)
258   have hr := analytic_scale_at_zero X.hv (s.r : ℂ)
259   have ha := analytic_scale_at_zero X.hu (s.a : ℂ)
260   have hb := analytic_scale_at_zero X.hv (s.b : ℂ)
261   exact (analyticAt_const.mul (analyticAt_const.add (hq.mul hr))).add
262     (analyticAt_const.mul (analyticAt_const.add (ha.mul hb)))
263 
264 theorem local_field_respects_component_germs (s : Scales) (c : Fin 2 → ℂ)
265     (X Y : LocalInput) (hu : X.u =ᶠ[𝓝 (0 : ℂ)] Y.u)
266     (hv : X.v =ᶠ[𝓝 (0 : ℂ)] Y.v) : s.localField c X = s.localField c Y := by
267   apply Germ.coe_eq.mpr
268   have ht (p : ℂ) : Tendsto (fun z : ℂ => p * z) (𝓝 0) (𝓝 0) := by
269     have hp : Continuous (fun z : ℂ => p * z) := by fun_prop
270     simpa only [mul_zero] using hp.tendsto (0 : ℂ)
271   have hq := hu.comp_tendsto (ht (s.q : ℂ))
272   have hr := hv.comp_tendsto (ht (s.r : ℂ))
273   have ha := hu.comp_tendsto (ht (s.a : ℂ))
274   have hb := hv.comp_tendsto (ht (s.b : ℂ))
275   filter_upwards [hq, hr, ha, hb] with z hq hr ha hb
276   simp only [Function.comp_apply] at hq hr ha hb
277   simp only [rowField, hq, hr, ha, hb]
278 
279 theorem germ_autonomous_iff_scalar_functional (s : Scales) (c : Fin 2 → ℂ) :
280     s.GermAutonomous c ↔ ∃ H : ScalarGerm → ScalarGerm,
281       ∀ X : LocalInput, s.localField c X = H (localProjection c X) := by
282   rw [GermAutonomous, Function.factorsThrough_iff]
283   constructor
284   · rintro ⟨H, hH⟩
285     exact ⟨H, fun X => congrFun hH X⟩
286   · rintro ⟨H, hH⟩
287     exact ⟨H, funext hH⟩
288 
289 theorem entire_field_differentiable (s : Scales) (c : Fin 2 → ℂ) (X : EntireInput) :
290     Differentiable ℂ (s.entireField c X) := by
291   change Differentiable ℂ (fun z =>
292     c 0 * (1 + X.u ((s.q : ℂ) * z) * X.v ((s.r : ℂ) * z)) +
293     c 1 * (1 + X.u ((s.a : ℂ) * z) * X.v ((s.b : ℂ) * z)))
294   have hu := X.hu
295   have hv := X.hv
296   fun_prop
297 
298 theorem germ_autonomous_implies_entire (s : Scales) (c : Fin 2 → ℂ)
299     (h : s.GermAutonomous c) : s.Autonomous c := by
300   intro X Y hp
301   have hpG : localProjection c X.toLocal = localProjection c Y.toLocal := by
302     exact congrArg (fun f : ℂ → ℂ => (f : ScalarGerm)) hp
303   have hG := h hpG
304   have he : s.entireField c X =ᶠ[𝓝 (0 : ℂ)] s.entireField c Y := Germ.coe_eq.mp hG
305   have hX : AnalyticOnNhd ℂ (s.entireField c X) univ :=
306     fun z _ => (s.entire_field_differentiable c X).analyticAt z
307   have hY : AnalyticOnNhd ℂ (s.entireField c Y) univ :=
308     fun z _ => (s.entire_field_differentiable c Y).analyticAt z
309   exact hX.eq_of_eventuallyEq hY he
310 
311 theorem germ_autonomous_iff_entire (s : Scales) (hs : s.positive) (c : Fin 2 → ℂ) :
312     s.GermAutonomous c ↔ s.Autonomous c := by
313   refine ⟨s.germ_autonomous_implies_entire c, ?_⟩
314   intro h X Y _
315   have hX := s.autonomous_projected_field_zero hs c h X.u X.v
316   have hY := s.autonomous_projected_field_zero hs c h Y.u Y.v
317   exact congrArg (fun f : ℂ → ℂ => (f : ScalarGerm)) (hX.trans hY.symm)
318 
319 theorem germ_autonomous_nonzero_classification (s : Scales) (hs : s.positive)
320     (c : Fin 2 → ℂ) (hc : c ≠ 0) :
321     s.GermAutonomous c ↔ s.q = s.a ∧ s.r = s.b ∧ ∃ γ : ℂ, γ ≠ 0 ∧ c = ![γ, -γ] := by
322   rw [s.germ_autonomous_iff_entire hs c, s.autonomous_nonzero_classification hs c hc]
323 
324 theorem no_invertible_constant_germ_decoupling (s : Scales) (hs : s.positive)
325     (P : Matrix (Fin 2) (Fin 2) ℂ) (hP : IsUnit P) : ¬∀ i, s.GermAutonomous (P i) := by
326   intro h
327   exact s.no_invertible_constant_decoupling hs P hP
328     (fun i => s.germ_autonomous_implies_entire (P i) (h i))
329 
330 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls