CoupledGrowthTypes.lean

1 import CoupledUpperGrowth
2 import Mathlib.Topology.Order.LiminfLimsup
3 
4 /-! # Real types and the radial exponent for the canonical coupled pair -/
5 
6 set_option autoImplicit false
7 set_option maxHeartbeats 2000000
8 
9 noncomputable section
10 open Filter Set
11 open scoped Topology Matrix
12 
13 namespace Komorebi.SpecialFunctions.Coupled.Scales
14 
15 def realComponent (s : Scales) (i : Fin 2) (R : ℝ) : ℝ := ![s.UReal R, s.VReal R] i
16 def growthRatio (s : Scales) (hs : s.positive)
17     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) (R : ℝ) : ℝ :=
18   Real.log (s.realComponent i R) / R ^ (s.characteristicExponent hs hstrict)
19 def lowerType (s : Scales) (hs : s.positive)
20     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) : ℝ :=
21   Filter.liminf (s.growthRatio hs hstrict i) atTop
22 def upperType (s : Scales) (hs : s.positive)
23     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) : ℝ :=
24   Filter.limsup (s.growthRatio hs hstrict i) atTop
25 def radialExponent (s : Scales) (i : Fin 2) (R : ℝ) : ℝ :=
26   Real.log (Real.log (s.realComponent i R)) / Real.log R
27 def radialOrder (s : Scales) (i : Fin 2) : ℝ := Filter.limsup (s.radialExponent i) atTop
28 
29 theorem realComponent_positive (s : Scales) (hs : s.positive)
30     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
31     {R : ℝ} (hR : 0 < R) : 0 < s.realComponent i R := by
32   have hh := s.real_axis_lower_linear hs hstrict hR.le
33   fin_cases i
34   · exact hR.trans_le hh.1
35   · exact hR.trans_le hh.2
36 
37 theorem canonical_growth_ratio_bounds (s : Scales) (hs : s.positive)
38     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
39     {R : ℝ} (hR : Real.exp 1 ≤ R) :
40     s.canonicalLowerCoefficient hs hstrict i ≤ s.growthRatio hs hstrict i R ∧
41     s.growthRatio hs hstrict i R ≤ s.canonicalUpperCoefficient hs hstrict i := by
42   have hh := s.canonical_two_sided_growth_ratio hs hstrict hR
43   fin_cases i
44   · exact hh.1
45   · exact hh.2
46 
47 theorem canonical_growth_ratio_eventually (s : Scales) (hs : s.positive)
48     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
49     ∀ᶠ R in atTop, s.canonicalLowerCoefficient hs hstrict i ≤ s.growthRatio hs hstrict i R ∧
50       s.growthRatio hs hstrict i R ≤ s.canonicalUpperCoefficient hs hstrict i := by
51   filter_upwards [eventually_ge_atTop (Real.exp 1)] with R hR
52   exact s.canonical_growth_ratio_bounds hs hstrict i hR
53 
54 theorem canonical_growth_ratio_bounded (s : Scales) (hs : s.positive)
55     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
56     atTop.IsBoundedUnder (· ≤ ·) (s.growthRatio hs hstrict i) ∧
57     atTop.IsBoundedUnder (· ≥ ·) (s.growthRatio hs hstrict i) := by
58   have hh := s.canonical_growth_ratio_eventually hs hstrict i
59   exact ⟨⟨s.canonicalUpperCoefficient hs hstrict i, hh.mono (fun _ h => h.2)⟩,
60     ⟨s.canonicalLowerCoefficient hs hstrict i, hh.mono (fun _ h => h.1)⟩⟩
61 
62 theorem real_type_sandwich {f : ℝ → ℝ} {lo hi : ℝ}
63     (hh : ∀ᶠ R in atTop, lo ≤ f R ∧ f R ≤ hi) :
64     lo ≤ Filter.liminf f atTop ∧ Filter.liminf f atTop ≤ Filter.limsup f atTop ∧
65       Filter.limsup f atTop ≤ hi := by
66   have hlo := hh.mono (fun _ h => h.1)
67   have hhi := hh.mono (fun _ h => h.2)
68   have hbA : atTop.IsBoundedUnder (· ≤ ·) f := ⟨hi, hhi⟩
69   have hbB : atTop.IsBoundedUnder (· ≥ ·) f := ⟨lo, hlo⟩
70   exact ⟨le_liminf_of_le hbA.isCoboundedUnder_ge hlo,
71     liminf_le_limsup hbA hbB, limsup_le_of_le hbB.isCoboundedUnder_le hhi⟩
72 
73 theorem canonical_type_bounds (s : Scales) (hs : s.positive)
74     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
75     s.canonicalLowerCoefficient hs hstrict i ≤ s.lowerType hs hstrict i ∧
76     s.lowerType hs hstrict i ≤ s.upperType hs hstrict i ∧
77     s.upperType hs hstrict i ≤ s.canonicalUpperCoefficient hs hstrict i :=
78   real_type_sandwich (s.canonical_growth_ratio_eventually hs hstrict i)
79 
80 theorem canonical_types_positive (s : Scales) (hs : s.positive)
81     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
82     0 < s.lowerType hs hstrict i ∧ 0 < s.upperType hs hstrict i := by
83   have hh := s.canonical_type_bounds hs hstrict i
84   have hl := (s.canonicalLowerCoefficient_positive hs hstrict i).trans_le hh.1
85   exact ⟨hl, hl.trans_le hh.2.1⟩
86 
87 theorem loglog_ratio_sandwich {f : ℝ → ℝ} {ρ lo hi R : ℝ}
88     (hlo : 0 < lo) (hhi : 0 < hi) (hR : 1 < R)
89     (hh : lo ≤ Real.log (f R) / R ^ ρ ∧ Real.log (f R) / R ^ ρ ≤ hi) :
90     ρ + Real.log lo / Real.log R ≤ Real.log (Real.log (f R)) / Real.log R ∧
91       Real.log (Real.log (f R)) / Real.log R ≤ ρ + Real.log hi / Real.log R := by
92   have hR0 : 0 < R := by linarith only [hR]
93   have hp := Real.rpow_pos_of_pos hR0 ρ
94   have hlogR := Real.log_pos hR
95   have hL := (le_div_iff₀ hp).mp hh.1
96   have hU := (div_le_iff₀ hp).mp hh.2
97   have hlogF := (mul_pos hlo hp).trans_le hL
98   have hLL := Real.log_le_log (mul_pos hlo hp) hL
99   have hUU := Real.log_le_log hlogF hU
100   rw [Real.log_mul (ne_of_gt hlo) (ne_of_gt hp), Real.log_rpow hR0] at hLL
101   rw [Real.log_mul (ne_of_gt hhi) (ne_of_gt hp), Real.log_rpow hR0] at hUU
102   constructor
103   · simpa only [add_div, mul_div_cancel_right₀ _ (ne_of_gt hlogR), add_comm] using
104       div_le_div_of_nonneg_right hLL hlogR.le
105   · simpa only [add_div, mul_div_cancel_right₀ _ (ne_of_gt hlogR), add_comm] using
106       div_le_div_of_nonneg_right hUU hlogR.le
107 
108 theorem tendsto_loglog_of_ratio_bounds {f : ℝ → ℝ} {ρ lo hi : ℝ}
109     (hlo : 0 < lo) (hhi : 0 < hi)
110     (hh : ∀ᶠ R in atTop, lo ≤ Real.log (f R) / R ^ ρ ∧
111       Real.log (f R) / R ^ ρ ≤ hi) :
112     Tendsto (fun R => Real.log (Real.log (f R)) / Real.log R) atTop (𝓝 ρ) := by
113   have hc (c : ℝ) : Tendsto (fun R : ℝ => ρ + Real.log c / Real.log R) atTop (𝓝 ρ) := by
114     simpa only [add_zero] using
115       (tendsto_const_nhds (x := ρ)).add (Real.tendsto_log_atTop.const_div_atTop (Real.log c))
116   have hb : ∀ᶠ R in atTop,
117       ρ + Real.log lo / Real.log R ≤ Real.log (Real.log (f R)) / Real.log R ∧
118       Real.log (Real.log (f R)) / Real.log R ≤ ρ + Real.log hi / Real.log R := by
119     filter_upwards [hh, eventually_gt_atTop (1 : ℝ)] with R hR hR1
120     exact loglog_ratio_sandwich hlo hhi hR1 hR
121   exact tendsto_of_tendsto_of_tendsto_of_le_of_le' (hc lo) (hc hi)
122     (hb.mono (fun _ h => h.1)) (hb.mono (fun _ h => h.2))
123 
124 theorem canonical_radial_exponent_limit (s : Scales) (hs : s.positive)
125     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
126     Tendsto (s.radialExponent i) atTop (𝓝 (s.characteristicExponent hs hstrict)) :=
127   tendsto_loglog_of_ratio_bounds (s.canonicalLowerCoefficient_positive hs hstrict i)
128     (s.canonicalUpperCoefficient_positive hs hstrict i)
129     (s.canonical_growth_ratio_eventually hs hstrict i)
130 
131 theorem canonical_radial_order (s : Scales) (hs : s.positive)
132     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
133     s.radialOrder i = s.characteristicExponent hs hstrict :=
134   (s.canonical_radial_exponent_limit hs hstrict i).limsup_eq
135 
136 def complexComponent (s : Scales) (i : Fin 2) (z : ℂ) : ℂ := ![s.U z, s.V z] i
137 
138 theorem component_spherical_maximum (s : Scales) (hs : s.positive)
139     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
140     {R : ℝ} (hR : 0 ≤ R) :
141     IsGreatest ((fun z => ‖s.complexComponent i z‖) '' Metric.sphere (0 : ℂ) R)
142       (s.realComponent i R) := by
143   have hh := s.maximum_modulus_real_axis hs hstrict hR
144   fin_cases i
145   · exact hh.1
146   · exact hh.2
147 
148 theorem component_real_norm (s : Scales) (hs : s.positive)
149     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
150     {R : ℝ} (hR : 0 ≤ R) : ‖s.complexComponent i (R : ℂ)‖ = s.realComponent i R := by
151   have hh := s.real_axis_norm hs hstrict hR
152   fin_cases i
153   · exact hh.1
154   · exact hh.2
155 
156 theorem norm_growth_ratio_eventually_eq (s : Scales) (hs : s.positive)
157     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
158     (fun R : ℝ => Real.log ‖s.complexComponent i (R : ℂ)‖ /
159       R ^ (s.characteristicExponent hs hstrict)) =ᶠ[atTop] s.growthRatio hs hstrict i := by
160   filter_upwards [eventually_ge_atTop (0 : ℝ)] with R hR
161   rw [s.component_real_norm hs hstrict i hR]
162   rfl
163 
164 theorem norm_type_identification (s : Scales) (hs : s.positive)
165     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
166     Filter.liminf (fun R : ℝ => Real.log ‖s.complexComponent i (R : ℂ)‖ /
167       R ^ (s.characteristicExponent hs hstrict)) atTop = s.lowerType hs hstrict i ∧
168     Filter.limsup (fun R : ℝ => Real.log ‖s.complexComponent i (R : ℂ)‖ /
169       R ^ (s.characteristicExponent hs hstrict)) atTop = s.upperType hs hstrict i := by
170   have hh := s.norm_growth_ratio_eventually_eq hs hstrict i
171   exact ⟨Filter.liminf_congr hh, Filter.limsup_congr hh⟩
172 
173 theorem canonical_norm_radial_limit (s : Scales) (hs : s.positive)
174     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
175     Tendsto (fun R : ℝ => Real.log (Real.log ‖s.complexComponent i (R : ℂ)‖) / Real.log R)
176       atTop (𝓝 (s.characteristicExponent hs hstrict)) := by
177   apply (s.canonical_radial_exponent_limit hs hstrict i).congr'
178   filter_upwards [eventually_ge_atTop (0 : ℝ)] with R hR
179   rw [s.component_real_norm hs hstrict i hR]
180   rfl
181 
182 def maximumModulus (s : Scales) (i : Fin 2) (R : ℝ) : ℝ :=
183   sSup ((fun z => ‖s.complexComponent i z‖) '' Metric.sphere (0 : ℂ) R)
184 
185 theorem maximumModulus_eq (s : Scales) (hs : s.positive)
186     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
187     {R : ℝ} (hR : 0 ≤ R) : s.maximumModulus i R = s.realComponent i R := by
188   have hh := s.component_spherical_maximum hs hstrict i hR
189   exact hh.isLUB.csSup_eq ⟨_, hh.1⟩
190 
191 theorem maximum_growth_ratio_eventually_eq (s : Scales) (hs : s.positive)
192     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
193     (fun R : ℝ => Real.log (s.maximumModulus i R) /
194       R ^ (s.characteristicExponent hs hstrict)) =ᶠ[atTop] s.growthRatio hs hstrict i := by
195   filter_upwards [eventually_ge_atTop (0 : ℝ)] with R hR
196   rw [s.maximumModulus_eq hs hstrict i hR]
197   rfl
198 
199 theorem maximum_type_identification (s : Scales) (hs : s.positive)
200     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
201     Filter.liminf (fun R : ℝ => Real.log (s.maximumModulus i R) /
202       R ^ (s.characteristicExponent hs hstrict)) atTop = s.lowerType hs hstrict i ∧
203     Filter.limsup (fun R : ℝ => Real.log (s.maximumModulus i R) /
204       R ^ (s.characteristicExponent hs hstrict)) atTop = s.upperType hs hstrict i := by
205   have hh := s.maximum_growth_ratio_eventually_eq hs hstrict i
206   exact ⟨Filter.liminf_congr hh, Filter.limsup_congr hh⟩
207 
208 theorem canonical_maximum_type_bounds (s : Scales) (hs : s.positive)
209     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
210     s.canonicalLowerCoefficient hs hstrict i ≤
211       Filter.liminf (fun R : ℝ => Real.log (s.maximumModulus i R) /
212         R ^ (s.characteristicExponent hs hstrict)) atTop ∧
213     Filter.liminf (fun R : ℝ => Real.log (s.maximumModulus i R) /
214       R ^ (s.characteristicExponent hs hstrict)) atTop ≤
215       Filter.limsup (fun R : ℝ => Real.log (s.maximumModulus i R) /
216         R ^ (s.characteristicExponent hs hstrict)) atTop ∧
217     Filter.limsup (fun R : ℝ => Real.log (s.maximumModulus i R) /
218       R ^ (s.characteristicExponent hs hstrict)) atTop ≤ s.canonicalUpperCoefficient hs hstrict i := by
219   have hh := s.maximum_type_identification hs hstrict i
220   rw [hh.1, hh.2]
221   exact s.canonical_type_bounds hs hstrict i
222 
223 theorem canonical_maximum_radial_limit (s : Scales) (hs : s.positive)
224     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
225     Tendsto (fun R : ℝ => Real.log (Real.log (s.maximumModulus i R)) / Real.log R)
226       atTop (𝓝 (s.characteristicExponent hs hstrict)) := by
227   apply (s.canonical_radial_exponent_limit hs hstrict i).congr'
228   filter_upwards [eventually_ge_atTop (0 : ℝ)] with R hR
229   rw [s.maximumModulus_eq hs hstrict i hR]
230   rfl
231 
232 theorem canonical_maximum_order (s : Scales) (hs : s.positive)
233     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
234     Filter.limsup (fun R : ℝ => Real.log (Real.log (s.maximumModulus i R)) / Real.log R)
235       atTop = s.characteristicExponent hs hstrict :=
236   (s.canonical_maximum_radial_limit hs hstrict i).limsup_eq
237 
238 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls