Special Functions · Lean source
CoupledTypeProportions.lean
Selected results recorded Coverage and evidence
Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
CoupledTypeProportions.lean477 lines
Original source path
lean/CoupledTypeProportions.leanSkip declarations and read code
1 import CoupledGrowthTypes
2
3 /-! # Perron proportions of the two real type vectors
4
5 The limiting comparisons below retain real-filter boundedness explicitly.
6 They do not presume convergence of either ordinary type profile.
7 -/
8
9 set_option autoImplicit false
10 set_option maxHeartbeats 2000000
11
12 noncomputable section
13 open Filter Set
14 open scoped Topology Matrix
15
16 namespace Komorebi.SpecialFunctions.Coupled.Scales
17
18 theorem affine_scale_tendsto {p : ℝ} (hp : 0 < p) (c : ℝ) :
19 Tendsto (fun R : ℝ => p * (R - c)) atTop atTop := by
20 apply tendsto_atTop.2
21 intro B
22 filter_upwards [eventually_ge_atTop (B / p + c)] with R hR
23 have hh := mul_le_mul_of_nonneg_left hR hp.le
24 have hd : p * (B / p) = B := mul_div_cancel₀ B (ne_of_gt hp)
25 nlinarith only [hh, hd]
26
27 theorem affine_power_ratio_tendsto {p : ℝ} (hp : 0 < p) (c ρ : ℝ) :
28 Tendsto (fun R : ℝ => (p * (R - c)) ^ ρ / R ^ ρ) atTop (𝓝 (p ^ ρ)) := by
29 have hh : Tendsto (fun R : ℝ => p * (1 - c / R)) atTop (𝓝 p) := by
30 convert (tendsto_const_nhds (x := p)).mul
31 ((tendsto_const_nhds (x := (1 : ℝ))).sub (tendsto_id.const_div_atTop c)) using 1 <;>
32 simp
33 apply (hh.rpow_const (Or.inl (ne_of_gt hp))).congr'
34 filter_upwards [eventually_gt_atTop (max c 0)] with R hR
35 have hR0 : 0 < R := lt_of_le_of_lt (le_max_right _ _) hR
36 have hRc : 0 < R - c := sub_pos.mpr (lt_of_le_of_lt (le_max_left _ _) hR)
37 rw [← Real.div_rpow (mul_pos hp hRc).le hR0.le]
38 congr 1
39 field_simp
40
41 theorem lower_comparison_of_tendsto {f g : ℝ → ℝ} {a : ℝ}
42 (hb : atTop.IsBoundedUnder (· ≤ ·) f)
43 (hg : Tendsto g atTop (𝓝 a)) (hgf : g ≤ᶠ[atTop] f) :
44 a ≤ Filter.liminf f atTop := by
45 have hh := liminf_le_liminf hgf hg.isBoundedUnder_ge hb.isCoboundedUnder_ge
46 rwa [hg.liminf_eq] at hh
47
48 theorem upper_comparison_of_tendsto {f g : ℝ → ℝ} {a : ℝ}
49 (hb : atTop.IsBoundedUnder (· ≥ ·) f)
50 (hg : Tendsto g atTop (𝓝 a)) (hfg : f ≤ᶠ[atTop] g) :
51 Filter.limsup f atTop ≤ a := by
52 have hh := limsup_le_limsup hfg hb.isCoboundedUnder_le hg.isBoundedUnder_le
53 rwa [hg.limsup_eq] at hh
54
55 theorem canonical_type_envelopes (s : Scales) (hs : s.positive)
56 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
57 {ε : ℝ} (hε : 0 < ε) :
58 (∀ᶠ R in atTop, s.lowerType hs hstrict i - ε ≤ s.growthRatio hs hstrict i R) ∧
59 (∀ᶠ R in atTop, s.growthRatio hs hstrict i R ≤ s.upperType hs hstrict i + ε) := by
60 have hb := s.canonical_growth_ratio_bounded hs hstrict i
61 exact ⟨(eventually_lt_of_lt_liminf (by dsimp [lowerType]; linarith) hb.2).mono
62 (fun _ h => h.le),
63 (eventually_lt_of_limsup_lt (by dsimp [upperType]; linarith) hb.1).mono
64 (fun _ h => h.le)⟩
65
66 def scaledLogProfile (s : Scales) (ρ : ℝ) (i : Fin 2) (p c R : ℝ) : ℝ :=
67 Real.log (s.realComponent i (p * (R - c))) / R ^ ρ
68
69 theorem scaled_log_factorization (s : Scales) (hs : s.positive)
70 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
71 {p c R : ℝ} (hp : 0 < p) (hR : c < R) :
72 s.scaledLogProfile (s.characteristicExponent hs hstrict) i p c R =
73 s.growthRatio hs hstrict i (p * (R - c)) *
74 ((p * (R - c)) ^ (s.characteristicExponent hs hstrict) /
75 R ^ (s.characteristicExponent hs hstrict)) := by
76 have hn := ne_of_gt (Real.rpow_pos_of_pos (mul_pos hp (sub_pos.mpr hR))
77 (s.characteristicExponent hs hstrict))
78 dsimp [scaledLogProfile, growthRatio]
79 field_simp
80
81 theorem scaled_type_envelopes (s : Scales) (hs : s.positive)
82 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
83 {p ε : ℝ} (hp : 0 < p) (c : ℝ) (hε : 0 < ε) :
84 (∀ᶠ R in atTop, (s.lowerType hs hstrict i - ε) *
85 ((p * (R - c)) ^ (s.characteristicExponent hs hstrict) /
86 R ^ (s.characteristicExponent hs hstrict)) ≤
87 s.scaledLogProfile (s.characteristicExponent hs hstrict) i p c R) ∧
88 (∀ᶠ R in atTop, s.scaledLogProfile (s.characteristicExponent hs hstrict) i p c R ≤
89 (s.upperType hs hstrict i + ε) *
90 ((p * (R - c)) ^ (s.characteristicExponent hs hstrict) /
91 R ^ (s.characteristicExponent hs hstrict))) := by
92 have ht := affine_scale_tendsto hp c
93 have hh := s.canonical_type_envelopes hs hstrict i hε
94 have hlo := ht.eventually hh.1
95 have hhi := ht.eventually hh.2
96 have hboth : ∀ᶠ R : ℝ in atTop,
97 (s.lowerType hs hstrict i - ε) *
98 ((p * (R - c)) ^ (s.characteristicExponent hs hstrict) /
99 R ^ (s.characteristicExponent hs hstrict)) ≤
100 s.scaledLogProfile (s.characteristicExponent hs hstrict) i p c R ∧
101 s.scaledLogProfile (s.characteristicExponent hs hstrict) i p c R ≤
102 (s.upperType hs hstrict i + ε) *
103 ((p * (R - c)) ^ (s.characteristicExponent hs hstrict) /
104 R ^ (s.characteristicExponent hs hstrict)) := by
105 filter_upwards [hlo, hhi, eventually_gt_atTop (max c 0)] with R hl hu hR
106 have hR0 := lt_of_le_of_lt (le_max_right c 0) hR
107 have hRc := lt_of_le_of_lt (le_max_left c 0) hR
108 have hf : 0 ≤ (p * (R - c)) ^ (s.characteristicExponent hs hstrict) /
109 R ^ (s.characteristicExponent hs hstrict) :=
110 (div_pos (Real.rpow_pos_of_pos (mul_pos hp (sub_pos.mpr hRc)) _)
111 (Real.rpow_pos_of_pos hR0 _)).le
112 rw [s.scaled_log_factorization hs hstrict i hp hRc]
113 exact ⟨mul_le_mul_of_nonneg_right hl hf, mul_le_mul_of_nonneg_right hu hf⟩
114 exact ⟨hboth.mono (fun _ h => h.1), hboth.mono (fun _ h => h.2)⟩
115
116 theorem log_power_correction_tendsto {ρ : ℝ} (hρ : 0 < ρ) (c : ℝ) :
117 Tendsto (fun R : ℝ => (Real.log R + c) / R ^ ρ) atTop (𝓝 0) := by
118 have h1 := (isLittleO_log_rpow_atTop hρ).tendsto_div_nhds_zero
119 have h2 := (tendsto_rpow_atTop hρ).const_div_atTop c
120 simpa only [add_div, add_zero] using h1.add h2
121
122 theorem lower_type_row (s : Scales) (hs : s.positive)
123 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
124 {p u : ℝ} (hp : 0 < p) (hu : 0 < u)
125 (hrow : ∀ᶠ R in atTop,
126 s.scaledLogProfile (s.characteristicExponent hs hstrict) 0 p 1 R +
127 s.scaledLogProfile (s.characteristicExponent hs hstrict) 1 u 1 R ≤
128 s.growthRatio hs hstrict i R) :
129 s.lowerType hs hstrict 0 * p ^ (s.characteristicExponent hs hstrict) +
130 s.lowerType hs hstrict 1 * u ^ (s.characteristicExponent hs hstrict) ≤
131 s.lowerType hs hstrict i := by
132 have hε (ε : ℝ) (hε : 0 < ε) :
133 (s.lowerType hs hstrict 0 - ε) * p ^ (s.characteristicExponent hs hstrict) +
134 (s.lowerType hs hstrict 1 - ε) * u ^ (s.characteristicExponent hs hstrict) ≤
135 s.lowerType hs hstrict i := by
136 have hlim := ((affine_power_ratio_tendsto hp 1 (s.characteristicExponent hs hstrict)).const_mul
137 (s.lowerType hs hstrict 0 - ε)).add
138 ((affine_power_ratio_tendsto hu 1 (s.characteristicExponent hs hstrict)).const_mul
139 (s.lowerType hs hstrict 1 - ε))
140 apply lower_comparison_of_tendsto (s.canonical_growth_ratio_bounded hs hstrict i).1 hlim
141 filter_upwards [(s.scaled_type_envelopes hs hstrict 0 hp 1 hε).1,
142 (s.scaled_type_envelopes hs hstrict 1 hu 1 hε).1, hrow] with R h0 h1 hR
143 exact (add_le_add h0 h1).trans hR
144 have ht : Tendsto (fun ε : ℝ =>
145 (s.lowerType hs hstrict 0 - ε) * p ^ (s.characteristicExponent hs hstrict) +
146 (s.lowerType hs hstrict 1 - ε) * u ^ (s.characteristicExponent hs hstrict))
147 (𝓝[>] 0) (𝓝 (s.lowerType hs hstrict 0 * p ^ (s.characteristicExponent hs hstrict) +
148 s.lowerType hs hstrict 1 * u ^ (s.characteristicExponent hs hstrict))) := by
149 have hc : Continuous (fun ε : ℝ =>
150 (s.lowerType hs hstrict 0 - ε) * p ^ (s.characteristicExponent hs hstrict) +
151 (s.lowerType hs hstrict 1 - ε) * u ^ (s.characteristicExponent hs hstrict)) := by fun_prop
152 simpa only [sub_zero] using (hc.tendsto 0).mono_left nhdsWithin_le_nhds
153 apply le_of_tendsto ht
154 filter_upwards [self_mem_nhdsWithin] with ε hpos
155 exact hε ε hpos
156
157 theorem upper_type_row (s : Scales) (hs : s.positive)
158 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
159 {p u : ℝ} (hp : 0 < p) (hu : 0 < u)
160 (hrow : ∀ᶠ R in atTop, s.growthRatio hs hstrict i R ≤
161 (Real.log R + Real.log 2) / R ^ (s.characteristicExponent hs hstrict) +
162 s.scaledLogProfile (s.characteristicExponent hs hstrict) 0 p 0 R +
163 s.scaledLogProfile (s.characteristicExponent hs hstrict) 1 u 0 R) :
164 s.upperType hs hstrict i ≤
165 s.upperType hs hstrict 0 * p ^ (s.characteristicExponent hs hstrict) +
166 s.upperType hs hstrict 1 * u ^ (s.characteristicExponent hs hstrict) := by
167 have hρ := (s.characteristicExponent_spec hs hstrict).1
168 have hε (ε : ℝ) (hε : 0 < ε) : s.upperType hs hstrict i ≤
169 (s.upperType hs hstrict 0 + ε) * p ^ (s.characteristicExponent hs hstrict) +
170 (s.upperType hs hstrict 1 + ε) * u ^ (s.characteristicExponent hs hstrict) := by
171 have hlim := ((log_power_correction_tendsto hρ (Real.log 2)).add
172 ((affine_power_ratio_tendsto hp 0 (s.characteristicExponent hs hstrict)).const_mul
173 (s.upperType hs hstrict 0 + ε))).add
174 ((affine_power_ratio_tendsto hu 0 (s.characteristicExponent hs hstrict)).const_mul
175 (s.upperType hs hstrict 1 + ε))
176 simp only [zero_add] at hlim
177 apply upper_comparison_of_tendsto (s.canonical_growth_ratio_bounded hs hstrict i).2 hlim
178 filter_upwards [(s.scaled_type_envelopes hs hstrict 0 hp 0 hε).2,
179 (s.scaled_type_envelopes hs hstrict 1 hu 0 hε).2, hrow] with R h0 h1 hR
180 exact hR.trans (add_le_add (add_le_add le_rfl h0) h1)
181 have ht : Tendsto (fun ε : ℝ =>
182 (s.upperType hs hstrict 0 + ε) * p ^ (s.characteristicExponent hs hstrict) +
183 (s.upperType hs hstrict 1 + ε) * u ^ (s.characteristicExponent hs hstrict))
184 (𝓝[>] 0) (𝓝 (s.upperType hs hstrict 0 * p ^ (s.characteristicExponent hs hstrict) +
185 s.upperType hs hstrict 1 * u ^ (s.characteristicExponent hs hstrict))) := by
186 have hc : Continuous (fun ε : ℝ =>
187 (s.upperType hs hstrict 0 + ε) * p ^ (s.characteristicExponent hs hstrict) +
188 (s.upperType hs hstrict 1 + ε) * u ^ (s.characteristicExponent hs hstrict)) := by fun_prop
189 simpa only [add_zero] using (hc.tendsto 0).mono_left nhdsWithin_le_nhds
190 apply ge_of_tendsto ht
191 filter_upwards [self_mem_nhdsWithin] with ε hpos
192 exact hε ε hpos
193
194 theorem canonical_lower_type_superinvariant (s : Scales) (hs : s.positive)
195 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
196 s.characteristicMatrix (s.characteristicExponent hs hstrict) *ᵥ
197 s.lowerType hs hstrict ≤ s.lowerType hs hstrict := by
198 have hrow : ∀ i : Fin 2, ∀ᶠ R in atTop,
199 s.scaledLogProfile (s.characteristicExponent hs hstrict) 0 (![s.q, s.a] i) 1 R +
200 s.scaledLogProfile (s.characteristicExponent hs hstrict) 1 (![s.r, s.b] i) 1 R ≤
201 s.growthRatio hs hstrict i R := by
202 intro i
203 filter_upwards [eventually_gt_atTop (1 : ℝ)] with R hR
204 have hh := s.real_axis_log_unit_lower hs hstrict hR
205 have hden := (Real.rpow_pos_of_pos (by linarith only [hR] : 0 < R)
206 (s.characteristicExponent hs hstrict)).le
207 fin_cases i
208 · simpa [scaledLogProfile, growthRatio, realComponent, ← add_div] using
209 div_le_div_of_nonneg_right hh.1 hden
210 · simpa [scaledLogProfile, growthRatio, realComponent, ← add_div] using
211 div_le_div_of_nonneg_right hh.2 hden
212 intro i
213 fin_cases i
214 · have hh := s.lower_type_row hs hstrict 0 hs.1 hs.2.1 (hrow 0)
215 simpa [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two, mul_comm] using hh
216 · have hh := s.lower_type_row hs hstrict 1 hs.2.2.1 hs.2.2.2 (hrow 1)
217 simpa [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two, mul_comm] using hh
218
219 theorem canonical_upper_type_subinvariant (s : Scales) (hs : s.positive)
220 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
221 s.upperType hs hstrict ≤
222 s.characteristicMatrix (s.characteristicExponent hs hstrict) *ᵥ s.upperType hs hstrict := by
223 have hm := s.minScale_positive hs
224 have hrow : ∀ i : Fin 2, ∀ᶠ R in atTop, s.growthRatio hs hstrict i R ≤
225 (Real.log R + Real.log 2) / R ^ (s.characteristicExponent hs hstrict) +
226 s.scaledLogProfile (s.characteristicExponent hs hstrict) 0 (![s.q, s.a] i) 0 R +
227 s.scaledLogProfile (s.characteristicExponent hs hstrict) 1 (![s.r, s.b] i) 0 R := by
228 intro i
229 filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_ge_atTop (1 / s.minScale)]
230 with R hR hRm
231 have hmr : 1 ≤ s.minScale * R := by
232 have hh := mul_le_mul_of_nonneg_left hRm hm.le
233 rwa [mul_one_div_cancel (ne_of_gt hm)] at hh
234 have hh := s.real_axis_log_full_upper hs hstrict hR hmr
235 have hden := (Real.rpow_pos_of_pos hR (s.characteristicExponent hs hstrict)).le
236 fin_cases i
237 · simpa [scaledLogProfile, growthRatio, realComponent, ← add_div] using
238 div_le_div_of_nonneg_right hh.1 hden
239 · simpa [scaledLogProfile, growthRatio, realComponent, ← add_div] using
240 div_le_div_of_nonneg_right hh.2 hden
241 intro i
242 fin_cases i
243 · have hh := s.upper_type_row hs hstrict 0 hs.1 hs.2.1 (hrow 0)
244 simpa [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two, mul_comm] using hh
245 · have hh := s.upper_type_row hs hstrict 1 hs.2.2.1 hs.2.2.2 (hrow 1)
246 simpa [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two, mul_comm] using hh
247
248 theorem positive_dot_rigidity {l x y : Fin 2 → ℝ}
249 (hl : ∀ i, 0 < l i) (hxy : x ≤ y) (hd : dotProduct l x = dotProduct l y) : x = y := by
250 have he : l 0 * (y 0 - x 0) + l 1 * (y 1 - x 1) = 0 := by
251 simp only [dotProduct, Fin.sum_univ_two] at hd
252 nlinarith only [hd]
253 have h0 := mul_nonneg (hl 0).le (sub_nonneg.mpr (hxy 0))
254 have h1 := mul_nonneg (hl 1).le (sub_nonneg.mpr (hxy 1))
255 have hz0 : l 0 * (y 0 - x 0) = 0 := by linarith only [he, h0, h1]
256 have hz1 : l 1 * (y 1 - x 1) = 0 := by linarith only [he, h0, h1]
257 have hx0 := (mul_eq_zero.mp hz0).resolve_left (ne_of_gt (hl 0))
258 have hx1 := (mul_eq_zero.mp hz1).resolve_left (ne_of_gt (hl 1))
259 funext i
260 fin_cases i
261 · exact (sub_eq_zero.mp hx0).symm
262 · exact (sub_eq_zero.mp hx1).symm
263
264 theorem left_eigenvector_preserves_dot {P : Matrix (Fin 2) (Fin 2) ℝ}
265 {l : Fin 2 → ℝ} (hleft : Pᵀ *ᵥ l = l) (x : Fin 2 → ℝ) :
266 dotProduct l (P *ᵥ x) = dotProduct l x := by
267 calc
268 _ = dotProduct x (Pᵀ *ᵥ l) := (Matrix.dotProduct_transpose_mulVec P x l).symm
269 _ = dotProduct x l := by rw [hleft]
270 _ = dotProduct l x := dotProduct_comm _ _
271
272 theorem canonical_type_fixed_vectors (s : Scales) (hs : s.positive)
273 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
274 s.characteristicMatrix (s.characteristicExponent hs hstrict) *ᵥ s.lowerType hs hstrict =
275 s.lowerType hs hstrict ∧
276 s.characteristicMatrix (s.characteristicExponent hs hstrict) *ᵥ s.upperType hs hstrict =
277 s.upperType hs hstrict := by
278 have hρ := s.characteristicExponent_spec hs hstrict
279 have hleft := s.characteristic_left_eigenvector hs hρ.2
280 have hl := s.characteristicLeftVector_positive hs hstrict.1 hρ.1
281 constructor
282 · exact positive_dot_rigidity hl (s.canonical_lower_type_superinvariant hs hstrict)
283 (left_eigenvector_preserves_dot hleft _)
284 · exact (positive_dot_rigidity hl (s.canonical_upper_type_subinvariant hs hstrict)
285 (left_eigenvector_preserves_dot hleft _).symm).symm
286
287 theorem characteristic_fixed_proportion (s : Scales) (hs : s.positive)
288 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {x : Fin 2 → ℝ}
289 (hx : s.characteristicMatrix (s.characteristicExponent hs hstrict) *ᵥ x = x) :
290 x = (x 1 / s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) 1) •
291 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) := by
292 let ρ := s.characteristicExponent hs hstrict
293 let w := s.normalizedCharacteristicVector ρ
294 have hρ := s.characteristicExponent_spec hs hstrict
295 have hq : 0 < 1 - s.q ^ ρ :=
296 sub_pos.mpr (rpow_contraction_bounds hs.1 hstrict.1 hρ.1).2
297 have hw1 : w 1 ≠ 0 := ne_of_gt (s.normalizedCharacteristicVector_positive hs hstrict.1 hρ.1 1)
298 have hx0 := congrFun hx 0
299 simp only [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two] at hx0
300 have hww : (1 - s.q ^ ρ) * w 0 = s.r ^ ρ * w 1 := by
301 have hh : s.q ^ ρ * w 0 + s.r ^ ρ * w 1 = w 0 := by
302 simpa [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two, ρ, w] using
303 congrFun (s.normalized_characteristic_eigenvector hs hρ.2) 0
304 nlinarith only [hh]
305 funext i
306 fin_cases i
307 · change x 0 = x 1 / w 1 * w 0
308 apply (mul_left_cancel₀ (ne_of_gt hq))
309 calc
310 (1 - s.q ^ ρ) * x 0 = s.r ^ ρ * x 1 := by
311 change s.q ^ ρ * x 0 + s.r ^ ρ * x 1 = x 0 at hx0
312 nlinarith only [hx0]
313 _ = (x 1 / w 1) * (s.r ^ ρ * w 1) := by field_simp
314 _ = (x 1 / w 1) * ((1 - s.q ^ ρ) * w 0) := by rw [hww]
315 _ = (1 - s.q ^ ρ) * (x 1 / w 1 * w 0) := by ring
316 · change x 1 = x 1 / w 1 * w 1
317 exact (div_mul_cancel₀ _ hw1).symm
318
319 def lowerTypeScalar (s : Scales) (hs : s.positive)
320 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) : ℝ :=
321 s.lowerType hs hstrict 1 /
322 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) 1
323
324 def upperTypeScalar (s : Scales) (hs : s.positive)
325 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) : ℝ :=
326 s.upperType hs hstrict 1 /
327 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) 1
328
329 theorem canonical_type_proportions (s : Scales) (hs : s.positive)
330 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
331 0 < s.lowerTypeScalar hs hstrict ∧
332 s.lowerTypeScalar hs hstrict ≤ s.upperTypeScalar hs hstrict ∧
333 s.lowerType hs hstrict = s.lowerTypeScalar hs hstrict •
334 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) ∧
335 s.upperType hs hstrict = s.upperTypeScalar hs hstrict •
336 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) := by
337 have hρ := (s.characteristicExponent_spec hs hstrict).1
338 have hw := s.normalizedCharacteristicVector_positive hs hstrict.1 hρ 1
339 have hf := s.canonical_type_fixed_vectors hs hstrict
340 exact ⟨div_pos (s.canonical_types_positive hs hstrict 1).1 hw,
341 div_le_div_of_nonneg_right (s.canonical_type_bounds hs hstrict 1).2.1 hw.le,
342 s.characteristic_fixed_proportion hs hstrict hf.1,
343 s.characteristic_fixed_proportion hs hstrict hf.2⟩
344
345 theorem canonical_positive_type_proportions (s : Scales) (hs : s.positive)
346 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
347 ∃ τlo τhi : ℝ, 0 < τlo ∧ τlo ≤ τhi ∧
348 s.lowerType hs hstrict = τlo •
349 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) ∧
350 s.upperType hs hstrict = τhi •
351 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) :=
352 ⟨s.lowerTypeScalar hs hstrict, s.upperTypeScalar hs hstrict,
353 s.canonical_type_proportions hs hstrict⟩
354
355 theorem characteristic_fixed_ratios (s : Scales) (hs : s.positive)
356 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {x : Fin 2 → ℝ}
357 (hx : s.characteristicMatrix (s.characteristicExponent hs hstrict) *ᵥ x = x)
358 (hx1 : 0 < x 1) :
359 x 0 / x 1 = s.r ^ (s.characteristicExponent hs hstrict) /
360 (1 - s.q ^ (s.characteristicExponent hs hstrict)) ∧
361 x 0 / x 1 = (1 - s.b ^ (s.characteristicExponent hs hstrict)) /
362 s.a ^ (s.characteristicExponent hs hstrict) := by
363 have hρ := (s.characteristicExponent_spec hs hstrict).1
364 have hq := (rpow_contraction_bounds hs.1 hstrict.1 hρ).2
365 have ha := Real.rpow_pos_of_pos hs.2.2.1 (s.characteristicExponent hs hstrict)
366 have h0 : s.q ^ (s.characteristicExponent hs hstrict) * x 0 +
367 s.r ^ (s.characteristicExponent hs hstrict) * x 1 = x 0 := by
368 simpa [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two] using congrFun hx 0
369 have h1 : s.a ^ (s.characteristicExponent hs hstrict) * x 0 +
370 s.b ^ (s.characteristicExponent hs hstrict) * x 1 = x 1 := by
371 simpa [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two] using congrFun hx 1
372 constructor
373 · apply (div_eq_div_iff (ne_of_gt hx1) (ne_of_gt (sub_pos.mpr hq))).2
374 nlinarith only [h0]
375 · apply (div_eq_div_iff (ne_of_gt hx1) (ne_of_gt ha)).2
376 nlinarith only [h1]
377
378 theorem canonical_type_ratios (s : Scales) (hs : s.positive)
379 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
380 s.lowerType hs hstrict 0 / s.lowerType hs hstrict 1 =
381 s.upperType hs hstrict 0 / s.upperType hs hstrict 1 ∧
382 s.lowerType hs hstrict 0 / s.lowerType hs hstrict 1 =
383 s.r ^ (s.characteristicExponent hs hstrict) /
384 (1 - s.q ^ (s.characteristicExponent hs hstrict)) ∧
385 s.lowerType hs hstrict 0 / s.lowerType hs hstrict 1 =
386 (1 - s.b ^ (s.characteristicExponent hs hstrict)) /
387 s.a ^ (s.characteristicExponent hs hstrict) := by
388 have hf := s.canonical_type_fixed_vectors hs hstrict
389 have hpos := s.canonical_types_positive hs hstrict 1
390 have hl := s.characteristic_fixed_ratios hs hstrict hf.1 hpos.1
391 have hu := s.characteristic_fixed_ratios hs hstrict hf.2 hpos.2
392 exact ⟨hl.1.trans hu.1.symm, hl⟩
393
394 theorem ordinary_type_limit_iff (s : Scales) (hs : s.positive)
395 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
396 (∃ τ : ℝ, Tendsto (s.growthRatio hs hstrict i) atTop (𝓝 τ)) ↔
397 s.lowerType hs hstrict i = s.upperType hs hstrict i := by
398 constructor
399 · rintro ⟨τ, hτ⟩
400 exact hτ.liminf_eq.trans hτ.limsup_eq.symm
401 · intro he
402 have hb := s.canonical_growth_ratio_bounded hs hstrict i
403 exact ⟨s.lowerType hs hstrict i, tendsto_of_liminf_eq_limsup rfl he.symm hb.1 hb.2⟩
404
405 theorem type_equality_iff_scalar_equality (s : Scales) (hs : s.positive)
406 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
407 s.lowerType hs hstrict i = s.upperType hs hstrict i ↔
408 s.lowerTypeScalar hs hstrict = s.upperTypeScalar hs hstrict := by
409 have hh := s.canonical_type_proportions hs hstrict
410 have hl := congrFun hh.2.2.1 i
411 have hu := congrFun hh.2.2.2 i
412 have hw := s.normalizedCharacteristicVector_positive hs hstrict.1
413 (s.characteristicExponent_spec hs hstrict).1 i
414 change s.lowerType hs hstrict i = s.lowerTypeScalar hs hstrict *
415 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) i at hl
416 change s.upperType hs hstrict i = s.upperTypeScalar hs hstrict *
417 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) i at hu
418 rw [hl, hu]
419 exact mul_left_inj' (ne_of_gt hw)
420
421 theorem canonical_type_limit_equivalence (s : Scales) (hs : s.positive)
422 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i j : Fin 2) :
423 (∃ τ : ℝ, Tendsto (s.growthRatio hs hstrict i) atTop (𝓝 τ)) ↔
424 (∃ τ : ℝ, Tendsto (s.growthRatio hs hstrict j) atTop (𝓝 τ)) := by
425 rw [s.ordinary_type_limit_iff hs hstrict i, s.ordinary_type_limit_iff hs hstrict j,
426 s.type_equality_iff_scalar_equality hs hstrict i,
427 s.type_equality_iff_scalar_equality hs hstrict j]
428
429 theorem canonical_type_limit_vector (s : Scales) (hs : s.positive)
430 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
431 (hi : ∃ τ : ℝ, Tendsto (s.growthRatio hs hstrict i) atTop (𝓝 τ)) :
432 ∃ τ : ℝ, 0 < τ ∧ Tendsto (fun R : ℝ => fun j : Fin 2 => s.growthRatio hs hstrict j R)
433 atTop (𝓝 (τ • s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict))) := by
434 have hh := s.canonical_type_proportions hs hstrict
435 have he := (s.type_equality_iff_scalar_equality hs hstrict i).mp
436 ((s.ordinary_type_limit_iff hs hstrict i).mp hi)
437 refine ⟨s.lowerTypeScalar hs hstrict, hh.1, tendsto_pi_nhds.2 ?_⟩
438 intro j
439 have hb := s.canonical_growth_ratio_bounded hs hstrict j
440 have hj := (s.type_equality_iff_scalar_equality hs hstrict j).mpr he
441 have ht := tendsto_of_liminf_eq_limsup rfl hj.symm hb.1 hb.2
442 exact (congrFun hh.2.2.1 j) ▸ ht
443
444 theorem canonical_maximum_type_proportions (s : Scales) (hs : s.positive)
445 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
446 ∃ τlo τhi : ℝ, 0 < τlo ∧ τlo ≤ τhi ∧
447 (fun i : Fin 2 => Filter.liminf (fun R : ℝ => Real.log (s.maximumModulus i R) /
448 R ^ (s.characteristicExponent hs hstrict)) atTop) = τlo •
449 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) ∧
450 (fun i : Fin 2 => Filter.limsup (fun R : ℝ => Real.log (s.maximumModulus i R) /
451 R ^ (s.characteristicExponent hs hstrict)) atTop) = τhi •
452 s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) := by
453 have hlo : (fun i : Fin 2 => Filter.liminf (fun R : ℝ => Real.log (s.maximumModulus i R) /
454 R ^ (s.characteristicExponent hs hstrict)) atTop) = s.lowerType hs hstrict :=
455 funext (fun i => (s.maximum_type_identification hs hstrict i).1)
456 have hhi : (fun i : Fin 2 => Filter.limsup (fun R : ℝ => Real.log (s.maximumModulus i R) /
457 R ^ (s.characteristicExponent hs hstrict)) atTop) = s.upperType hs hstrict :=
458 funext (fun i => (s.maximum_type_identification hs hstrict i).2)
459 rw [hlo, hhi]
460 exact s.canonical_positive_type_proportions hs hstrict
461
462 theorem canonical_maximum_type_limit_equivalence (s : Scales) (hs : s.positive)
463 (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i j : Fin 2) :
464 (∃ τ : ℝ, Tendsto (fun R : ℝ => Real.log (s.maximumModulus i R) /
465 R ^ (s.characteristicExponent hs hstrict)) atTop (𝓝 τ)) ↔
466 (∃ τ : ℝ, Tendsto (fun R : ℝ => Real.log (s.maximumModulus j R) /
467 R ^ (s.characteristicExponent hs hstrict)) atTop (𝓝 τ)) := by
468 have hconv (k : Fin 2) :
469 (∃ τ : ℝ, Tendsto (fun R : ℝ => Real.log (s.maximumModulus k R) /
470 R ^ (s.characteristicExponent hs hstrict)) atTop (𝓝 τ)) ↔
471 (∃ τ : ℝ, Tendsto (s.growthRatio hs hstrict k) atTop (𝓝 τ)) := by
472 exact exists_congr (fun τ =>
473 Filter.tendsto_congr' (s.maximum_growth_ratio_eventually_eq hs hstrict k))
474 rw [hconv, hconv]
475 exact s.canonical_type_limit_equivalence hs hstrict i j
476
477 end Komorebi.SpecialFunctions.Coupled.Scales
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: c6b3d8dfb786730a7b0ed456992dd87af160016841bfd7195596017b42a16194