CoupledCharacteristic.lean

1 import CoupledRescaling
2 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
3 import Mathlib.Topology.Order.IntermediateValue
4 import Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
5 import Mathlib.Analysis.Normed.Algebra.Spectrum
6 import Mathlib.Analysis.Complex.Polynomial.Basic
7 
8 /-! # The positive characteristic exponent of the coupled scales
9 
10 All powers in the determinant balance are real powers. This file separates
11 the matrix/exponent prerequisites from the later analytic growth theorem.
12 -/
13 
14 set_option autoImplicit false
15 set_option maxHeartbeats 1500000
16 
17 noncomputable section
18 
19 open Filter Set
20 open scoped Topology Matrix ENNReal NNReal
21 
22 namespace Komorebi.SpecialFunctions.Coupled.Scales
23 
24 def characteristicBalance (s : Scales) (t : ℝ) : ℝ :=
25   (1 - s.q ^ t) * (1 - s.b ^ t) - (s.a * s.r) ^ t
26 
27 theorem characteristicBalance_zero (s : Scales) : s.characteristicBalance 0 = -1 := by
28   simp [characteristicBalance]
29 
30 theorem rpow_contraction_bounds {x t : ℝ} (hx : 0 < x) (hx1 : x < 1) (ht : 0 < t) :
31     0 < x ^ t ∧ x ^ t < 1 := by
32   exact ⟨Real.rpow_pos_of_pos hx t, by
33     simpa using Real.rpow_lt_rpow_of_exponent_gt hx hx1 ht⟩
34 
35 theorem characteristicBalance_continuous (s : Scales) (hs : s.positive) :
36     Continuous s.characteristicBalance := by
37   exact ((continuous_const.sub (Real.continuous_const_rpow (ne_of_gt hs.1))).mul
38     (continuous_const.sub (Real.continuous_const_rpow (ne_of_gt hs.2.2.2)))).sub
39       (Real.continuous_const_rpow (ne_of_gt (mul_pos hs.2.2.1 hs.2.1)))
40 
41 theorem characteristicBalance_strictMono (s : Scales) (hs : s.positive)
42     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
43     StrictMonoOn s.characteristicBalance (Ici 0) := by
44   intro x hx y _ hxy
45   have hq := Real.rpow_lt_rpow_of_exponent_gt hs.1 hstrict.1 hxy
46   have hb := Real.rpow_lt_rpow_of_exponent_gt hs.2.2.2 hstrict.2.2.2 hxy
47   have hq0 : 0 ≤ 1 - s.q ^ x := by
48     have h := Real.rpow_le_rpow_of_exponent_ge hs.1 hstrict.1.le hx
49     simpa using sub_nonneg.mpr h
50   have hb0 : 0 ≤ 1 - s.b ^ x := by
51     have h := Real.rpow_le_rpow_of_exponent_ge hs.2.2.2 hstrict.2.2.2.le hx
52     simpa using sub_nonneg.mpr h
53   have hprod : (1 - s.q ^ x) * (1 - s.b ^ x) ≤
54       (1 - s.q ^ y) * (1 - s.b ^ y) :=
55     mul_le_mul (by linarith only [hq]) (by linarith only [hb]) hb0 (by linarith only [hq0, hq])
56   have har0 : 0 < s.a * s.r := mul_pos hs.2.2.1 hs.2.1
57   have har1 : s.a * s.r < 1 :=
58     lt_trans (mul_lt_mul_of_pos_right hstrict.2.2.1 hs.2.1) (by simpa using hstrict.2.1)
59   have har := Real.rpow_lt_rpow_of_exponent_gt har0 har1 hxy
60   dsimp [characteristicBalance]
61   linarith only [hprod, har]
62 
63 theorem characteristicBalance_tendsto (s : Scales) (hs : s.positive)
64     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
65     Tendsto s.characteristicBalance atTop (𝓝 1) := by
66   have hq := tendsto_rpow_atTop_of_base_lt_one s.q (by linarith [hs.1]) hstrict.1
67   have hb := tendsto_rpow_atTop_of_base_lt_one s.b (by linarith [hs.2.2.2]) hstrict.2.2.2
68   have har0 : 0 < s.a * s.r := mul_pos hs.2.2.1 hs.2.1
69   have har1 : s.a * s.r < 1 :=
70     lt_trans (mul_lt_mul_of_pos_right hstrict.2.2.1 hs.2.1) (by simpa using hstrict.2.1)
71   have har := tendsto_rpow_atTop_of_base_lt_one (s.a * s.r) (by linarith) har1
72   have h1 : Tendsto (fun _ : ℝ => (1 : ℝ)) atTop (𝓝 1) := tendsto_const_nhds
73   convert ((h1.sub hq).mul (h1.sub hb)).sub har using 1 <;> norm_num
74   funext t
75   rfl
76 
77 theorem characteristic_exponent_exists_unique (s : Scales) (hs : s.positive)
78     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
79     ∃! t : ℝ, 0 < t ∧ (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t := by
80   have hev : ∀ᶠ t in atTop, 0 < s.characteristicBalance t :=
81     (s.characteristicBalance_tendsto hs hstrict).eventually (Ioi_mem_nhds (by norm_num))
82   obtain ⟨T, hT0, hT⟩ := (hev.and (eventually_gt_atTop (0 : ℝ))).exists
83   have hC := s.characteristicBalance_continuous hs
84   obtain ⟨t, ht, hroot⟩ := intermediate_value_Icc hT.le hC.continuousOn
85     (show (0 : ℝ) ∈ Icc (s.characteristicBalance 0) (s.characteristicBalance T) by
86       exact ⟨by rw [characteristicBalance_zero]; norm_num, hT0.le⟩)
87   have htpos : 0 < t := by
88     have htne : t ≠ 0 := by
89       intro he
90       rw [he, characteristicBalance_zero] at hroot
91       norm_num at hroot
92     exact lt_of_le_of_ne ht.1 htne.symm
93   have heq : (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t := sub_eq_zero.mp hroot
94   refine ⟨t, ⟨htpos, heq⟩, ?_⟩
95   intro u hu
96   apply (s.characteristicBalance_strictMono hs hstrict).injOn hu.1.le htpos.le
97   exact (sub_eq_zero.mpr hu.2).trans hroot.symm
98 
99 def characteristicExponent (s : Scales) (hs : s.positive)
100     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) : ℝ :=
101   Classical.choose (s.characteristic_exponent_exists_unique hs hstrict)
102 
103 theorem characteristicExponent_spec (s : Scales) (hs : s.positive)
104     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
105     0 < s.characteristicExponent hs hstrict ∧
106       (1 - s.q ^ (s.characteristicExponent hs hstrict)) *
107         (1 - s.b ^ (s.characteristicExponent hs hstrict)) =
108           (s.a * s.r) ^ (s.characteristicExponent hs hstrict) :=
109   (Classical.choose_spec (s.characteristic_exponent_exists_unique hs hstrict)).1
110 
111 def characteristicMatrix (s : Scales) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
112   !![s.q ^ t, s.r ^ t; s.a ^ t, s.b ^ t]
113 
114 def characteristicMatrixC (s : Scales) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℂ :=
115   (s.characteristicMatrix t).map (algebraMap ℝ ℂ)
116 
117 def characteristicVector (s : Scales) (t : ℝ) : Fin 2 → ℝ := ![s.r ^ t, 1 - s.q ^ t]
118 
119 def characteristicLeftVector (s : Scales) (t : ℝ) : Fin 2 → ℝ := ![s.a ^ t, 1 - s.q ^ t]
120 
121 def characteristicNormalizer (s : Scales) (t : ℝ) : ℝ :=
122   max (s.characteristicVector t 0) (s.characteristicVector t 1)
123 
124 def normalizedCharacteristicVector (s : Scales) (t : ℝ) : Fin 2 → ℝ :=
125   (s.characteristicNormalizer t)⁻¹ • s.characteristicVector t
126 
127 theorem characteristicVector_positive (s : Scales) (hs : s.positive)
128     (hq : s.q < 1) {t : ℝ} (ht : 0 < t) (i : Fin 2) :
129     0 < s.characteristicVector t i := by
130   fin_cases i
131   · exact Real.rpow_pos_of_pos hs.2.1 t
132   · exact sub_pos.mpr (rpow_contraction_bounds hs.1 hq ht).2
133 
134 theorem characteristicLeftVector_positive (s : Scales) (hs : s.positive)
135     (hq : s.q < 1) {t : ℝ} (ht : 0 < t) (i : Fin 2) :
136     0 < s.characteristicLeftVector t i := by
137   fin_cases i
138   · exact Real.rpow_pos_of_pos hs.2.2.1 t
139   · exact sub_pos.mpr (rpow_contraction_bounds hs.1 hq ht).2
140 
141 theorem characteristic_right_eigenvector (s : Scales) (hs : s.positive) {t : ℝ}
142     (he : (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t) :
143     s.characteristicMatrix t *ᵥ s.characteristicVector t = s.characteristicVector t := by
144   rw [Real.mul_rpow hs.2.2.1.le hs.2.1.le] at he
145   funext i
146   fin_cases i <;>
147     simp [characteristicMatrix, characteristicVector, Matrix.mulVec, dotProduct, Fin.sum_univ_two] <;>
148     nlinarith only [he]
149 
150 theorem characteristic_left_eigenvector (s : Scales) (hs : s.positive) {t : ℝ}
151     (he : (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t) :
152     (s.characteristicMatrix t)ᵀ *ᵥ s.characteristicLeftVector t = s.characteristicLeftVector t := by
153   rw [Real.mul_rpow hs.2.2.1.le hs.2.1.le] at he
154   funext i
155   fin_cases i <;>
156     simp [characteristicMatrix, characteristicLeftVector, Matrix.mulVec, dotProduct, Fin.sum_univ_two] <;>
157     nlinarith only [he]
158 
159 theorem characteristicNormalizer_positive (s : Scales) (hs : s.positive)
160     (hq : s.q < 1) {t : ℝ} (ht : 0 < t) : 0 < s.characteristicNormalizer t :=
161   lt_of_lt_of_le (s.characteristicVector_positive hs hq ht 0) (le_max_left _ _)
162 
163 theorem normalizedCharacteristicVector_positive (s : Scales) (hs : s.positive)
164     (hq : s.q < 1) {t : ℝ} (ht : 0 < t) (i : Fin 2) :
165     0 < s.normalizedCharacteristicVector t i :=
166   mul_pos (inv_pos.mpr (s.characteristicNormalizer_positive hs hq ht))
167     (s.characteristicVector_positive hs hq ht i)
168 
169 theorem normalizedCharacteristicVector_max (s : Scales) (hs : s.positive)
170     (hq : s.q < 1) {t : ℝ} (ht : 0 < t) :
171     max (s.normalizedCharacteristicVector t 0) (s.normalizedCharacteristicVector t 1) = 1 := by
172   have hd := s.characteristicNormalizer_positive hs hq ht
173   change max ((s.characteristicNormalizer t)⁻¹ * _) ((s.characteristicNormalizer t)⁻¹ * _) = 1
174   rw [← mul_max_of_nonneg _ _ (inv_pos.mpr hd).le]
175   exact inv_mul_cancel₀ (ne_of_gt hd)
176 
177 theorem normalized_characteristic_eigenvector (s : Scales) (hs : s.positive) {t : ℝ}
178     (he : (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t) :
179     s.characteristicMatrix t *ᵥ s.normalizedCharacteristicVector t =
180       s.normalizedCharacteristicVector t := by
181   rw [normalizedCharacteristicVector, Matrix.mulVec_smul, s.characteristic_right_eigenvector hs he]
182 
183 theorem characteristic_second_eigenvalue_bound (s : Scales) (hs : s.positive)
184     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {t : ℝ} (ht : 0 < t) :
185     |s.q ^ t + s.b ^ t - 1| < 1 := by
186   have hq := rpow_contraction_bounds hs.1 hstrict.1 ht
187   have hb := rpow_contraction_bounds hs.2.2.2 hstrict.2.2.2 ht
188   rw [abs_lt]
189   constructor <;> linarith
190 
191 theorem characteristic_spectrum (s : Scales) (hs : s.positive) {t : ℝ}
192     (he : (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t) :
193     spectrum ℂ (s.characteristicMatrixC t) =
194       {1, ((s.q ^ t + s.b ^ t - 1 : ℝ) : ℂ)} := by
195   rw [Real.mul_rpow hs.2.2.1.le hs.2.1.le] at he
196   have hc : (1 - ((s.q ^ t : ℝ) : ℂ)) * (1 - ((s.b ^ t : ℝ) : ℂ)) =
197       ((s.a ^ t : ℝ) : ℂ) * ((s.r ^ t : ℝ) : ℂ) := by exact_mod_cast he
198   ext z
199   rw [Matrix.mem_spectrum_iff_isRoot_charpoly, Polynomial.IsRoot, Matrix.eval_charpoly]
200   have hd : (Matrix.scalar (Fin 2) z - s.characteristicMatrixC t).det =
201       (z - 1) * (z - ((s.q ^ t + s.b ^ t - 1 : ℝ) : ℂ)) := by
202     norm_num [Matrix.det_fin_two, characteristicMatrixC, characteristicMatrix, Matrix.scalar]
203     linear_combination hc
204   rw [hd, mul_eq_zero]
205   simp only [sub_eq_zero, Set.mem_insert_iff, Set.mem_singleton_iff]
206 
207 theorem characteristic_spectralRadius (s : Scales) (hs : s.positive)
208     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {t : ℝ} (ht : 0 < t)
209     (he : (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t) :
210     spectralRadius ℂ (s.characteristicMatrixC t) = 1 := by
211   have hbound := s.characteristic_second_eigenvalue_bound hs hstrict ht
212   have hn : (‖((s.q ^ t + s.b ^ t - 1 : ℝ) : ℂ)‖₊ : ℝ≥0∞) ≤ 1 := by
213     exact_mod_cast (le_of_lt (show ‖((s.q ^ t + s.b ^ t - 1 : ℝ) : ℂ)‖ < 1 by
214       simpa only [Complex.norm_real, Real.norm_eq_abs] using hbound))
215   rw [spectralRadius_eq_of_unital]
216   apply le_antisymm
217   · refine iSup₂_le fun z hz => ?_
218     rw [s.characteristic_spectrum hs he, Set.mem_insert_iff, Set.mem_singleton_iff] at hz
219     rcases hz with rfl | rfl
220     · simp
221     · exact hn
222   · have hm : (1 : ℂ) ∈ spectrum ℂ (s.characteristicMatrixC t) := by
223       rw [s.characteristic_spectrum hs he]
224       simp
225     exact le_iSup₂_of_le (1 : ℂ) hm (by simp)
226 
227 theorem characteristic_mem_spectrum_iff (s : Scales) (t : ℝ) (z : ℂ) :
228     z ∈ spectrum ℂ (s.characteristicMatrixC t) ↔
229       (z - ((s.q ^ t : ℝ) : ℂ)) * (z - ((s.b ^ t : ℝ) : ℂ)) -
230         ((s.r ^ t : ℝ) : ℂ) * ((s.a ^ t : ℝ) : ℂ) = 0 := by
231   rw [Matrix.mem_spectrum_iff_isRoot_charpoly, Polynomial.IsRoot, Matrix.eval_charpoly]
232   norm_num [Matrix.det_fin_two, characteristicMatrixC, characteristicMatrix, Matrix.scalar]
233 
234 theorem characteristic_spectrum_real (s : Scales) (hs : s.positive) (t : ℝ)
235     {z : ℂ} (hz : z ∈ spectrum ℂ (s.characteristicMatrixC t)) : z.im = 0 := by
236   have he := (s.characteristic_mem_spectrum_iff t z).mp hz
237   have hre := congrArg Complex.re he
238   have him := congrArg Complex.im he
239   norm_num [Complex.mul_re, Complex.mul_im] at hre him
240   by_contra hne
241   have hp : z.im * (2 * z.re - s.q ^ t - s.b ^ t) = 0 := by
242     nlinarith only [him]
243   have hx : z.re = (s.q ^ t + s.b ^ t) / 2 := by
244     have h := (mul_eq_zero.mp hp).resolve_left hne
245     linarith only [h]
246   rw [hx] at hre
247   have hprod : 0 < s.r ^ t * s.a ^ t :=
248     mul_pos (Real.rpow_pos_of_pos hs.2.1 t) (Real.rpow_pos_of_pos hs.2.2.1 t)
249   nlinarith [sq_nonneg (s.q ^ t - s.b ^ t), sq_nonneg z.im]
250 
251 theorem characteristic_spectrum_norm_attained (s : Scales) (t : ℝ) :
252     ∃ z ∈ spectrum ℂ (s.characteristicMatrixC t),
253       (‖z‖₊ : ℝ≥0∞) = spectralRadius ℂ (s.characteristicMatrixC t) := by
254   have hf : (spectrum ℂ (s.characteristicMatrixC t)).Finite := by
255     apply (Polynomial.finite_setOfPred_isRoot (s.characteristicMatrixC t).charpoly_monic.ne_zero).subset
256     intro z hz
257     exact Matrix.mem_spectrum_iff_isRoot_charpoly.mp hz
258   have hn := spectrum.nonempty_of_isAlgClosed_of_finiteDimensional ℂ (s.characteristicMatrixC t)
259   obtain ⟨z, hz, hmax⟩ := hf.isCompact.exists_isMaxOn hn continuous_nnnorm.continuousOn
260   refine ⟨z, hz, ?_⟩
261   rw [spectralRadius_eq_of_unital]
262   apply le_antisymm
263   · exact le_iSup₂_of_le z hz le_rfl
264   · refine iSup₂_le fun w hw => ?_
265     exact_mod_cast hmax hw
266 
267 theorem characteristic_spectralRadius_iff (s : Scales) (hs : s.positive)
268     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {t : ℝ} (ht : 0 < t) :
269     spectralRadius ℂ (s.characteristicMatrixC t) = 1 ↔
270       (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t := by
271   constructor
272   · intro hrad
273     obtain ⟨z, hz, hn⟩ := s.characteristic_spectrum_norm_attained t
274     have hnNN : ‖z‖₊ = 1 := by exact_mod_cast hn.trans hrad
275     have hn1 : ‖z‖ = 1 := by
276       simpa only [NNReal.coe_one, coe_nnnorm] using congrArg (fun r : ℝ≥0 => (r : ℝ)) hnNN
277     have him := s.characteristic_spectrum_real hs t hz
278     have hzreal : z = (z.re : ℂ) := Complex.ext (by simp) (by simpa using him)
279     have habs : |z.re| = |(1 : ℝ)| := by
280       rw [hzreal, Complex.norm_real, Real.norm_eq_abs] at hn1
281       simpa only [abs_one] using hn1
282     have he := (s.characteristic_mem_spectrum_iff t z).mp hz
283     rcases abs_eq_abs.mp habs with hre | hre
284     · have hz1 : z = 1 := by rw [hzreal, hre]; norm_num
285       rw [hz1] at he
286       have hr : (1 - s.q ^ t) * (1 - s.b ^ t) = s.r ^ t * s.a ^ t := by
287         exact_mod_cast (sub_eq_zero.mp he)
288       rw [Real.mul_rpow hs.2.2.1.le hs.2.1.le]
289       nlinarith only [hr]
290     · have hz1 : z = -1 := by rw [hzreal, hre]; norm_num
291       rw [hz1] at he
292       have hr : (-1 - s.q ^ t) * (-1 - s.b ^ t) - s.r ^ t * s.a ^ t = 0 := by
293         exact_mod_cast he
294       have hq := rpow_contraction_bounds hs.1 hstrict.1 ht
295       have hb := rpow_contraction_bounds hs.2.2.2 hstrict.2.2.2 ht
296       have ha := rpow_contraction_bounds hs.2.2.1 hstrict.2.2.1 ht
297       have hR := rpow_contraction_bounds hs.2.1 hstrict.2.1 ht
298       have hprod : s.r ^ t * s.a ^ t < 1 :=
299         lt_trans (mul_lt_mul_of_pos_right hR.2 ha.1) (by simpa using ha.2)
300       nlinarith [mul_pos hq.1 hb.1]
301   · exact s.characteristic_spectralRadius hs hstrict ht
302 
303 theorem characteristic_spectral_exponent_exists_unique (s : Scales) (hs : s.positive)
304     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
305     ∃! t : ℝ, 0 < t ∧ spectralRadius ℂ (s.characteristicMatrixC t) = 1 := by
306   obtain ⟨t, ht, hu⟩ := s.characteristic_exponent_exists_unique hs hstrict
307   refine ⟨t, ⟨ht.1, (s.characteristic_spectralRadius_iff hs hstrict ht.1).mpr ht.2⟩, ?_⟩
308   intro u hU
309   exact hu u ⟨hU.1, (s.characteristic_spectralRadius_iff hs hstrict hU.1).mp hU.2⟩
310 
311 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls