CoupledRescaling.lean

1 import CoupledGermInverse
2 
3 /-! # Component rescaling for the canonical coupled functions
4 
5 Complex rescalings are allowed in the obstruction direction. The converse
6 uses the positive real square root and a normalized scalar entire solution.
7 -/
8 
9 set_option autoImplicit false
10 set_option maxHeartbeats 1500000
11 
12 noncomputable section
13 
14 open Filter
15 open scoped Topology
16 
17 namespace Komorebi.SpecialFunctions.Coupled.Scales
18 
19 def denseOddComplex (c : ℕ → ℂ) (k : ℕ) : ℂ :=
20   if k % 2 = 1 then c (k / 2) else 0
21 
22 theorem denseOddComplex_odd (c : ℕ → ℂ) (n : ℕ) :
23     denseOddComplex c (2 * n + 1) = c n := by
24   have hm : (2 * n + 1) % 2 = 1 := by omega
25   have hd : (2 * n + 1) / 2 = n := by omega
26   simp [denseOddComplex, hm, hd]
27 
28 theorem complex_odd_series_hasFPowerSeriesAt {c : ℕ → ℂ} {f : ℂ → ℂ}
29     (h : ∀ᶠ z in 𝓝 (0 : ℂ), HasSum (fun n => c n * z ^ (2 * n + 1)) (f z)) :
30     HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars ℂ (denseOddComplex c)) 0 := by
31   apply hasFPowerSeriesAt_iff.mpr
32   filter_upwards [h] with z hz
33   have hi : Function.Injective (fun n : ℕ => 2 * n + 1) := by
34     intro a b hab
35     change 2 * a + 1 = 2 * b + 1 at hab
36     omega
37   have hsum : HasSum (fun k => denseOddComplex c k * z ^ k) (f z) := by
38     apply (hi.hasSum_iff (f := fun k => denseOddComplex c k * z ^ k) ?_).mp
39     · simpa only [Function.comp_def, denseOddComplex_odd] using hz
40     · intro k hk
41       have hm : k % 2 ≠ 1 := by
42         intro hm
43         apply hk
44         refine ⟨k / 2, ?_⟩
45         change 2 * (k / 2) + 1 = k
46         omega
47       simp [denseOddComplex, hm]
48   simpa only [FormalMultilinearSeries.coeff_ofScalars, zero_add, smul_eq_mul,
49     mul_comm] using hsum
50 
51 theorem complex_odd_coefficients_eq {c d : ℕ → ℂ} {f g : ℂ → ℂ}
52     (hc : ∀ᶠ z in 𝓝 (0 : ℂ), HasSum (fun n => c n * z ^ (2 * n + 1)) (f z))
53     (hd : ∀ᶠ z in 𝓝 (0 : ℂ), HasSum (fun n => d n * z ^ (2 * n + 1)) (g z))
54     (he : f =ᶠ[𝓝 0] g) : c = d := by
55   have hp := (complex_odd_series_hasFPowerSeriesAt hc).eq_formalMultilinearSeries_of_eventually
56     (complex_odd_series_hasFPowerSeriesAt hd) he
57   funext n
58   simpa only [FormalMultilinearSeries.coeff_ofScalars, denseOddComplex_odd] using
59     congrArg (fun p : FormalMultilinearSeries ℂ ℂ ℂ => p.coeff (2 * n + 1)) hp
60 
61 theorem rescaling_coefficient_identity (s : Scales) (hs : s.positive)
62     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
63     {A B : ℂ} (he : ∀ z, s.V z = A * s.U (B * z)) (n : ℕ) :
64     ((s.coefficients n).2 : ℂ) = A * ((s.coefficients n).1 : ℂ) * B ^ (2 * n + 1) := by
65   have hc : ∀ᶠ z in 𝓝 (0 : ℂ),
66       HasSum (fun n => ((s.coefficients n).2 : ℂ) * z ^ (2 * n + 1)) (s.V z) :=
67     Eventually.of_forall fun z => (s.coefficient_series_entire hs hstrict z).2.of_norm.hasSum
68   have hd : ∀ᶠ z in 𝓝 (0 : ℂ),
69       HasSum (fun n => (A * ((s.coefficients n).1 : ℂ) * B ^ (2 * n + 1)) *
70         z ^ (2 * n + 1)) (A * s.U (B * z)) := by
71     apply Eventually.of_forall
72     intro z
73     simpa only [U, oddSum, mul_pow, mul_assoc, mul_left_comm, mul_comm] using
74       ((s.coefficient_series_entire hs hstrict (B * z)).1.of_norm.hasSum).mul_left A
75   exact congrFun (complex_odd_coefficients_eq hc hd (Eventually.of_forall he)) n
76 
77 theorem rescaling_forces_defect_zero (s : Scales) (hs : s.positive)
78     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
79     {A B : ℂ} (he : ∀ z, s.V z = A * s.U (B * z)) : s.defect = 0 := by
80   have h0 := s.rescaling_coefficient_identity hs hstrict he 0
81   have h1 := s.rescaling_coefficient_identity hs hstrict he 1
82   have h2 := s.rescaling_coefficient_identity hs hstrict he 2
83   simp only [coefficients_zero, Complex.ofReal_one, mul_one] at h0
84   have hab : A * B = 1 := by simpa using h0.symm
85   simp only [coefficients_one, u1, v1,
86     Complex.ofReal_div, Complex.ofReal_ofNat] at h1
87   have hkp : (s.k : ℂ) = (s.p : ℂ) * B ^ 2 := by
88     linear_combination 3 * h1 + (s.p : ℂ) * B ^ 2 * hab
89   simp only [coefficients_two] at h2
90   have hvu : (s.v2 : ℂ) = (s.u2 : ℂ) * B ^ 4 := by
91     linear_combination h2 + (s.u2 : ℂ) * B ^ 4 * hab
92   apply Complex.ofReal_inj.mp
93   change (s.defect : ℂ) = (0 : ℂ)
94   simp only [defect, Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_pow]
95   rw [hkp, hvu]
96   ring
97 
98 def scalarScales (x y : ℝ) : Scales := ⟨x, y, x, y⟩
99 
100 def scalarT (x y : ℝ) : ℂ → ℂ := (scalarScales x y).U
101 
102 theorem scalar_components_equal (x y : ℝ) :
103     (scalarScales x y).U = (scalarScales x y).V := by
104   have hc : ∀ n, ((scalarScales x y).coefficients n).1 =
105       ((scalarScales x y).coefficients n).2 := by
106     intro n
107     cases n with
108     | zero => rw [coefficients_zero]
109     | succ n => rw [(scalarScales x y).coefficients_solution.2]; rfl
110   change oddSum _ = oddSum _
111   congr 1
112   funext n
113   exact hc n
114 
115 theorem scalarT_solution {x y : ℝ} (hx : 0 < x) (hy : 0 < y)
116     (hx1 : x < 1) (hy1 : y < 1) :
117     scalarT x y 0 = 0 ∧ ∀ z : ℂ,
118       HasDerivAt (scalarT x y) (1 + scalarT x y ((x : ℂ) * z) *
119         scalarT x y ((y : ℂ) * z)) z := by
120   have hs : (scalarScales x y).positive := ⟨hx, hy, hx, hy⟩
121   have hsol := (scalarScales x y).coupled_entire_solution hs ⟨hx1, hy1, hx1, hy1⟩
122   refine ⟨hsol.1, ?_⟩
123   intro z
124   have h := (hsol.2.2 z).1
125   rw [← scalar_components_equal x y] at h
126   simpa only [scalarT, scalarScales] using h
127 
128 def reductionScale (s : Scales) : ℝ := Real.sqrt (s.k / s.p)
129 
130 theorem reductionScale_positive_sq (s : Scales) (hs : s.positive) :
131     0 < s.reductionScale ∧ s.reductionScale ^ 2 = s.k / s.p := by
132   have hp : 0 < s.p := mul_pos hs.1 hs.2.1
133   have hk : 0 < s.k := mul_pos hs.2.2.1 hs.2.2.2
134   exact ⟨Real.sqrt_pos.2 (div_pos hk hp), Real.sq_sqrt (div_pos hk hp).le⟩
135 
136 theorem reductionScale_surface (s : Scales) (hs : s.positive)
137     (hred : s.q = s.b ∨ s.q * s.b = s.a * s.r) :
138     (s.a = s.reductionScale * s.q ∧ s.b = s.reductionScale * s.r) ∨
139     (s.b = s.q ∧ s.a = s.reductionScale ^ 2 * s.r) := by
140   have hS := s.reductionScale_positive_sq hs
141   have hp : s.p ≠ 0 := ne_of_gt (mul_pos hs.1 hs.2.1)
142   have hSq : s.reductionScale ^ 2 * s.p = s.k := (eq_div_iff hp).mp hS.2
143   rcases hred with hqb | har
144   · right
145     refine ⟨hqb.symm, ?_⟩
146     apply mul_right_cancel₀ (ne_of_gt hs.1)
147     calc
148       s.a * s.q = s.a * s.b := by rw [hqb]
149       _ = s.reductionScale ^ 2 * s.p := hSq.symm
150       _ = (s.reductionScale ^ 2 * s.r) * s.q := by dsimp [p]; ring
151   · have hm : s.q * (s.reductionScale * s.r) ^ 2 = s.q * s.b ^ 2 := by
152       dsimp [p, k] at hSq
153       linear_combination s.r * hSq - s.b * har
154     have he : s.reductionScale * s.r = s.b :=
155       (sq_eq_sq₀ (mul_pos hS.1 hs.2.1).le hs.2.2.2.le).mp
156         (mul_left_cancel₀ (ne_of_gt hs.1) hm)
157     left
158     refine ⟨?_, he.symm⟩
159     apply mul_right_cancel₀ (ne_of_gt hs.2.1)
160     calc
161       s.a * s.r = s.q * s.b := har.symm
162       _ = (s.reductionScale * s.q) * s.r := by rw [← he]; ring
163 
164 theorem effective_scalar_scales (s : Scales) (hs : s.positive)
165     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
166     (hred : s.q = s.b ∨ s.q * s.b = s.a * s.r) :
167     0 < s.reductionScale * s.r ∧ s.reductionScale * s.r < 1 := by
168   have hS := s.reductionScale_positive_sq hs
169   refine ⟨mul_pos hS.1 hs.2.1, ?_⟩
170   rcases s.reductionScale_surface hs hred with h | h
171   · rw [← h.2]
172     exact hstrict.2.2.2
173   · have har : s.a * s.r < 1 :=
174       lt_trans (mul_lt_mul_of_pos_right hstrict.2.2.1 hs.2.1) (by simpa using hstrict.2.1)
175     have he : (s.reductionScale * s.r) ^ 2 = s.a * s.r := by rw [h.2]; ring
176     nlinarith [sq_nonneg (s.reductionScale * s.r - 1)]
177 
178 /-- A scalar solution generates a coupled solution when the two arguments
179 match in the displayed order or after interchanging the scalar factors. -/
180 theorem scalar_rescaled_solution (s : Scales) {T : ℂ → ℂ} {c e : ℂ}
181     (hc : c ≠ 0) (hzero : T 0 = 0)
182     (hT : ∀ z, HasDerivAt T (1 + T ((s.q : ℂ) * z) * T (e * z)) z)
183     (he : e = c ^ 2 * (s.r : ℂ))
184     (hmatch : ((s.a : ℂ) = c ^ 2 * (s.q : ℂ) ∧ (s.b : ℂ) = e) ∨
185       ((s.b : ℂ) = (s.q : ℂ) ∧ (s.a : ℂ) = c ^ 2 * e)) :
186     s.IsEntireSolution (fun z => c * T (c⁻¹ * z)) (fun z => c⁻¹ * T (c * z)) := by
187   refine ⟨by simp [hzero], by simp [hzero], ?_⟩
188   intro z
189   have hF := ((hT (c⁻¹ * z)).comp z ((hasDerivAt_id z).const_mul c⁻¹)).const_mul c
190   have hG := ((hT (c * z)).comp z ((hasDerivAt_id z).const_mul c)).const_mul c⁻¹
191   have harg : e * (c⁻¹ * z) = c * ((s.r : ℂ) * z) := by
192     rw [he]
193     field_simp [hc]
194   constructor
195   · apply hF.congr_deriv
196     rw [harg]
197     field_simp [hc]
198   · rcases hmatch with h | h
199     · have ha : c⁻¹ * ((s.a : ℂ) * z) = (s.q : ℂ) * (c * z) := by
200         rw [h.1]
201         field_simp [hc]
202       have hb : c * ((s.b : ℂ) * z) = e * (c * z) := by rw [h.2]; ring
203       apply hG.congr_deriv
204       dsimp only
205       rw [ha, hb]
206       field_simp [hc]
207     · have ha : c⁻¹ * ((s.a : ℂ) * z) = e * (c * z) := by
208         rw [h.2]
209         field_simp [hc]
210       have hb : c * ((s.b : ℂ) * z) = (s.q : ℂ) * (c * z) := by rw [h.1]; ring
211       apply hG.congr_deriv
212       dsimp only
213       rw [ha, hb]
214       field_simp [hc]
215 
216 def reductionRoot (s : Scales) : ℝ := Real.sqrt s.reductionScale
217 
218 theorem reductionRoot_positive_sq (s : Scales) (hs : s.positive) :
219     0 < s.reductionRoot ∧ s.reductionRoot ^ 2 = s.reductionScale :=
220   ⟨Real.sqrt_pos.2 (s.reductionScale_positive_sq hs).1,
221     Real.sq_sqrt (s.reductionScale_positive_sq hs).1.le⟩
222 
223 theorem coupled_scalar_representation (s : Scales) (hs : s.positive)
224     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
225     (hred : s.q = s.b ∨ s.q * s.b = s.a * s.r) (z : ℂ) :
226     s.U z = (s.reductionRoot : ℂ) * scalarT s.q (s.reductionScale * s.r)
227       ((s.reductionRoot : ℂ)⁻¹ * z) ∧
228     s.V z = (s.reductionRoot : ℂ)⁻¹ * scalarT s.q (s.reductionScale * s.r)
229       ((s.reductionRoot : ℂ) * z) := by
230   have heff := s.effective_scalar_scales hs hstrict hred
231   have hT := scalarT_solution hs.1 heff.1 hstrict.1 heff.2
232   have hroot := s.reductionRoot_positive_sq hs
233   have hc : (s.reductionRoot : ℂ) ≠ 0 := by exact_mod_cast ne_of_gt hroot.1
234   have hcsq : (s.reductionRoot : ℂ) ^ 2 = (s.reductionScale : ℂ) := by
235     exact_mod_cast hroot.2
236   have he : ((s.reductionScale * s.r : ℝ) : ℂ) =
237       (s.reductionRoot : ℂ) ^ 2 * (s.r : ℂ) := by rw [hcsq]; push_cast; rfl
238   have hm : ((s.a : ℂ) = (s.reductionRoot : ℂ) ^ 2 * (s.q : ℂ) ∧
239       (s.b : ℂ) = ((s.reductionScale * s.r : ℝ) : ℂ)) ∨
240       ((s.b : ℂ) = (s.q : ℂ) ∧ (s.a : ℂ) =
241         (s.reductionRoot : ℂ) ^ 2 * ((s.reductionScale * s.r : ℝ) : ℂ)) := by
242     rcases s.reductionScale_surface hs hred with h | h
243     · left
244       constructor
245       · rw [hcsq]
246         exact_mod_cast h.1
247       · exact_mod_cast h.2
248     · right
249       refine ⟨by exact_mod_cast h.1, ?_⟩
250       calc
251         (s.a : ℂ) = ((s.reductionScale ^ 2 * s.r : ℝ) : ℂ) :=
252           congrArg (fun x : ℝ => (x : ℂ)) h.2
253         _ = (s.reductionRoot : ℂ) ^ 2 * ((s.reductionScale * s.r : ℝ) : ℂ) := by
254           push_cast
255           rw [hcsq]
256           ring
257   have hsol := s.scalar_rescaled_solution hc hT.1 hT.2 he hm
258   have heq := s.entire_solution_eq hs hstrict hsol
259   exact ⟨congrFun heq.1.symm z, congrFun heq.2.symm z⟩
260 
261 theorem canonical_component_rescaling (s : Scales) (hs : s.positive)
262     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
263     (hred : s.q = s.b ∨ s.q * s.b = s.a * s.r) (z : ℂ) :
264     s.V z = (s.reductionScale : ℂ)⁻¹ * s.U ((s.reductionScale : ℂ) * z) := by
265   have hroot := s.reductionRoot_positive_sq hs
266   have hc : (s.reductionRoot : ℂ) ≠ 0 := by exact_mod_cast ne_of_gt hroot.1
267   have hcsq : (s.reductionRoot : ℂ) ^ 2 = (s.reductionScale : ℂ) := by
268     exact_mod_cast hroot.2
269   have harg : (s.reductionRoot : ℂ)⁻¹ * ((s.reductionScale : ℂ) * z) =
270       (s.reductionRoot : ℂ) * z := by
271     rw [← hcsq]
272     field_simp [hc]
273   rw [(s.coupled_scalar_representation hs hstrict hred z).2,
274     (s.coupled_scalar_representation hs hstrict hred ((s.reductionScale : ℂ) * z)).1,
275     harg, ← hcsq]
276   field_simp [hc]
277 
278 theorem component_rescaling_iff_defect (s : Scales) (hs : s.positive)
279     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
280     (∃ A B : ℂ, A ≠ 0 ∧ B ≠ 0 ∧ ∀ z, s.V z = A * s.U (B * z)) ↔
281       s.defect = 0 := by
282   constructor
283   · rintro ⟨A, B, _, _, he⟩
284     exact s.rescaling_forces_defect_zero hs hstrict he
285   · intro hD
286     have hS : (s.reductionScale : ℂ) ≠ 0 := by
287       exact_mod_cast ne_of_gt (s.reductionScale_positive_sq hs).1
288     exact ⟨(s.reductionScale : ℂ)⁻¹, (s.reductionScale : ℂ), inv_ne_zero hS, hS,
289       s.canonical_component_rescaling hs hstrict ((s.defect_eq_zero_iff hs).mp hD)⟩
290 
291 theorem component_rescaling_iff_surfaces (s : Scales) (hs : s.positive)
292     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
293     (∃ A B : ℂ, A ≠ 0 ∧ B ≠ 0 ∧ ∀ z, s.V z = A * s.U (B * z)) ↔
294       s.q = s.b ∨ s.q * s.b = s.a * s.r := by
295   rw [s.component_rescaling_iff_defect hs hstrict, s.defect_eq_zero_iff hs]
296 
297 theorem scalarT_unique {x y : ℝ} (hx : 0 < x) (hy : 0 < y)
298     (hx1 : x < 1) (hy1 : y < 1) {f : ℂ → ℂ} (hzero : f 0 = 0)
299     (hf : ∀ z, HasDerivAt f (1 + f ((x : ℂ) * z) * f ((y : ℂ) * z)) z) :
300     f = scalarT x y := by
301   have hsol : (scalarScales x y).IsEntireSolution f f :=
302     ⟨hzero, hzero, fun z => ⟨hf z, hf z⟩⟩
303   exact ((scalarScales x y).entire_solution_eq ⟨hx, hy, hx, hy⟩
304     ⟨hx1, hy1, hx1, hy1⟩ hsol).1
305 
306 theorem scalarT_symm {x y : ℝ} (hx : 0 < x) (hy : 0 < y)
307     (hx1 : x < 1) (hy1 : y < 1) : scalarT x y = scalarT y x := by
308   have hsol := scalarT_solution hx hy hx1 hy1
309   apply scalarT_unique hy hx hy1 hx1 hsol.1
310   intro z
311   simpa only [mul_comm] using hsol.2 z
312 
313 /-- The earlier finite-jet collision is in fact a collision of the labeled
314 entire pairs, so the defect guard cannot be dropped from the germ inverse. -/
315 theorem boundary_entire_collision : boundaryLeft.U = boundaryRight.U ∧
316     boundaryLeft.V = boundaryRight.V ∧ boundaryLeft ≠ boundaryRight := by
317   have hU : boundaryLeft.U = boundaryRight.U := by
318     change scalarT (1 / 4) (1 / 2) = scalarT (1 / 2) (1 / 4)
319     exact scalarT_symm (by norm_num) (by norm_num) (by norm_num) (by norm_num)
320   have hl : boundaryLeft.U = boundaryLeft.V := scalar_components_equal (1 / 4) (1 / 2)
321   have hr : boundaryRight.U = boundaryRight.V := scalar_components_equal (1 / 2) (1 / 4)
322   exact ⟨hU, hl.symm.trans (hU.trans hr), boundary_collision.2.2.2.2⟩
323 
324 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls