CoupledLowerGrowth.lean

1 import CoupledPositiveReal
2 
3 /-! # Explicit lower logarithmic growth comparison
4 
5 The argument uses closed finite caps and a positive real descent. It does
6 not require convexity of the power function or an exponent at least one.
7 -/
8 
9 set_option autoImplicit false
10 set_option maxHeartbeats 2000000
11 
12 noncomputable section
13 
14 open Set
15 open scoped Topology Matrix
16 
17 namespace Komorebi.SpecialFunctions.Coupled.Scales
18 
19 def lowerShift (s : Scales) : ℝ := s.maxScale / (1 - s.maxScale)
20 def lowerDescent (s : Scales) : ℝ := (1 - s.maxScale) * s.lowerThreshold + s.maxScale
21 def lowerPowerConstant (s : Scales) (ρ : ℝ) : ℝ :=
22   Real.log 2 / (s.lowerThreshold + s.lowerShift) ^ ρ
23 
24 def LowerPowerAt (s : Scales) (ρ : ℝ) (w : Fin 2 → ℝ) (R : ℝ) : Prop :=
25   s.lowerPowerConstant ρ * w 0 * (R + s.lowerShift) ^ ρ ≤ Real.log (s.UReal R) ∧
26   s.lowerPowerConstant ρ * w 1 * (R + s.lowerShift) ^ ρ ≤ Real.log (s.VReal R)
27 
28 theorem maxScale_positive (s : Scales) (hs : s.positive) : 0 < s.maxScale :=
29   lt_of_lt_of_le hs.1 s.maxScale_bounds.1
30 
31 theorem lowerShift_positive (s : Scales) (hs : s.positive)
32     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) : 0 < s.lowerShift :=
33   div_pos (s.maxScale_positive hs) (sub_pos.mpr (s.maxScale_lt_one hstrict))
34 
35 theorem lowerDescent_positive (s : Scales) (hs : s.positive)
36     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) : 0 < s.lowerDescent := by
37   have hQ := s.maxScale_positive hs
38   have hden := sub_pos.mpr (s.maxScale_lt_one hstrict)
39   have hB : 0 < s.lowerThreshold := lt_trans (by norm_num) (s.lowerThreshold_gt_one hs)
40   exact add_pos (mul_pos hden hB) hQ
41 
42 theorem lowerPowerConstant_positive (s : Scales) (hs : s.positive)
43     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (ρ : ℝ) :
44     0 < s.lowerPowerConstant ρ := by
45   have hB : 0 < s.lowerThreshold := lt_trans (by norm_num) (s.lowerThreshold_gt_one hs)
46   exact div_pos (Real.log_pos (by norm_num))
47     (Real.rpow_pos_of_pos (add_pos hB (s.lowerShift_positive hs hstrict)) ρ)
48 
49 theorem shifted_child_radius (s : Scales) (hs : s.positive)
50     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
51     {p : ℝ} (hp : p ≤ s.maxScale) (R : ℝ) :
52     p * (R + s.lowerShift) ≤ p * (R - 1) + s.lowerShift := by
53   have hc := s.lowerShift_positive hs hstrict
54   have hden := sub_pos.mpr (s.maxScale_lt_one hstrict)
55   have he : (1 - s.maxScale) * s.lowerShift = s.maxScale := by
56     dsimp [lowerShift]
57     field_simp [ne_of_gt hden]
58   have hm : 0 ≤ (s.maxScale - p) * (1 + s.lowerShift) :=
59     mul_nonneg (sub_nonneg.mpr hp) (by linarith)
60   nlinarith only [he, hm]
61 
62 theorem child_radius_descent (s : Scales) (hs : s.positive)
63     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
64     {p R : ℝ} (hp : p ≤ s.maxScale) (hR : s.lowerThreshold ≤ R) :
65     p * (R - 1) ≤ R - s.lowerDescent := by
66   have hR0 : 0 ≤ R - 1 := by linarith [s.lowerThreshold_gt_one hs]
67   have hm := mul_le_mul_of_nonneg_right hp hR0
68   have hn := mul_nonneg (sub_pos.mpr (s.maxScale_lt_one hstrict)).le (sub_nonneg.mpr hR)
69   dsimp [lowerDescent]
70   nlinarith only [hm, hn]
71 
72 theorem real_radius_descent_induction {P : ℝ → Prop} {B d : ℝ} (hd : 0 < d)
73     (hseed : ∀ R, 2 ≤ R → R ≤ B → P R)
74     (hstep : ∀ R, 2 ≤ R → B < R → (∀ y, 2 ≤ y → y ≤ R - d → P y) → P R) :
75     ∀ R, 2 ≤ R → P R := by
76   have hcap : ∀ n : ℕ, ∀ R : ℝ, 2 ≤ R → R ≤ B + (n : ℝ) * d → P R := by
77     intro n
78     induction n with
79     | zero =>
80       intro R hR hcap
81       exact hseed R hR (by simpa only [Nat.cast_zero, zero_mul, add_zero] using hcap)
82     | succ n ih =>
83       intro R hR hcap
84       by_cases hRB : R ≤ B
85       · exact hseed R hR hRB
86       · apply hstep R hR (lt_of_not_ge hRB)
87         intro y hy hyd
88         apply ih y hy
89         simp only [Nat.cast_succ] at hcap
90         nlinarith only [hyd, hcap]
91   intro R hR
92   obtain ⟨n, hn⟩ := exists_nat_gt ((R - B) / d)
93   have hnR : R ≤ B + (n : ℝ) * d := by
94     have h := (div_lt_iff₀ hd).mp hn
95     linarith only [h]
96   exact hcap n R hR hnR
97 
98 theorem lower_power_seed (s : Scales) (hs : s.positive)
99     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
100     {ρ : ℝ} (hρ : 0 < ρ) {w : Fin 2 → ℝ} (hw : ∀ i, w i ≤ 1)
101     {R : ℝ} (hR : 2 ≤ R) (hRB : R ≤ s.lowerThreshold) : s.LowerPowerAt ρ w R := by
102   have hc := s.lowerPowerConstant_positive hs hstrict ρ
103   have hC := s.lowerShift_positive hs hstrict
104   have hR0 : 0 < R := by linarith
105   have hB : 0 < s.lowerThreshold + s.lowerShift := by linarith [s.lowerThreshold_gt_one hs]
106   have hpR := Real.rpow_pos_of_pos (by linarith : 0 < R + s.lowerShift) ρ
107   have hpB := Real.rpow_pos_of_pos hB ρ
108   have hRB' : R + s.lowerShift ≤ s.lowerThreshold + s.lowerShift := by linarith only [hRB]
109   have hp := Real.rpow_le_rpow (by linarith : 0 ≤ R + s.lowerShift)
110     hRB' hρ.le
111   have he : s.lowerPowerConstant ρ * (s.lowerThreshold + s.lowerShift) ^ ρ = Real.log 2 := by
112     exact div_mul_cancel₀ _ (ne_of_gt hpB)
113   have ht (i : Fin 2) : s.lowerPowerConstant ρ * w i * (R + s.lowerShift) ^ ρ ≤ Real.log 2 := by
114     calc
115       _ ≤ s.lowerPowerConstant ρ * 1 * (R + s.lowerShift) ^ ρ :=
116         mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left (hw i) hc.le) hpR.le
117       _ = s.lowerPowerConstant ρ * (R + s.lowerShift) ^ ρ := by ring
118       _ ≤ s.lowerPowerConstant ρ * (s.lowerThreshold + s.lowerShift) ^ ρ :=
119         mul_le_mul_of_nonneg_left hp hc.le
120       _ = Real.log 2 := he
121   have hl := s.real_axis_lower_linear hs hstrict hR0.le
122   have hlog := Real.log_le_log (by norm_num : (0 : ℝ) < 2) hR
123   exact ⟨(ht 0).trans (hlog.trans (Real.log_le_log hR0 hl.1)),
124     (ht 1).trans (hlog.trans (Real.log_le_log hR0 hl.2))⟩
125 
126 theorem lower_power_step (s : Scales) (hs : s.positive)
127     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
128     {ρ : ℝ} (hρ : 0 < ρ) {w : Fin 2 → ℝ} (hw : ∀ i, 0 ≤ w i)
129     (he : s.characteristicMatrix ρ *ᵥ w = w) {R : ℝ} (hR : 2 ≤ R)
130     (hBR : s.lowerThreshold < R)
131     (hIH : ∀ y, 2 ≤ y → y ≤ R - s.lowerDescent → s.LowerPowerAt ρ w y) :
132     s.LowerPowerAt ρ w R := by
133   have hc := s.lowerPowerConstant_positive hs hstrict ρ
134   have hC := s.lowerShift_positive hs hstrict
135   have hRp : 0 ≤ R + s.lowerShift := by linarith
136   have hb := s.maxScale_bounds
137   have hk := s.lower_child_radii hs hBR.le
138   have hq := hIH (s.q * (R - 1)) hk.1 (s.child_radius_descent hs hstrict hb.1 hBR.le)
139   have hr := hIH (s.r * (R - 1)) hk.2.1 (s.child_radius_descent hs hstrict hb.2.1 hBR.le)
140   have ha := hIH (s.a * (R - 1)) hk.2.2.1 (s.child_radius_descent hs hstrict hb.2.2.1 hBR.le)
141   have hB := hIH (s.b * (R - 1)) hk.2.2.2 (s.child_radius_descent hs hstrict hb.2.2.2 hBR.le)
142   have hscale (p : ℝ) (hp0 : 0 ≤ p) (hpQ : p ≤ s.maxScale) (i : Fin 2) :
143       s.lowerPowerConstant ρ * w i * (p ^ ρ * (R + s.lowerShift) ^ ρ) ≤
144         s.lowerPowerConstant ρ * w i * (p * (R - 1) + s.lowerShift) ^ ρ := by
145     have hp := Real.rpow_le_rpow (mul_nonneg hp0 hRp)
146       (s.shifted_child_radius hs hstrict hpQ R) hρ.le
147     rw [Real.mul_rpow hp0 hRp] at hp
148     exact mul_le_mul_of_nonneg_left hp (mul_nonneg hc.le (hw i))
149   have hlog := s.real_axis_log_unit_lower hs hstrict
150     (lt_trans (s.lowerThreshold_gt_one hs) hBR)
151   have hu := (add_le_add ((hscale s.q hs.1.le hb.1 0).trans hq.1)
152     ((hscale s.r hs.2.1.le hb.2.1 1).trans hr.2)).trans hlog.1
153   have hv := (add_le_add ((hscale s.a hs.2.2.1.le hb.2.2.1 0).trans ha.1)
154     ((hscale s.b hs.2.2.2.le hb.2.2.2 1).trans hB.2)).trans hlog.2
155   have he0 := congrFun he 0
156   have he1 := congrFun he 1
157   norm_num [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two] at he0 he1
158   have h0 := congrArg (fun x : ℝ => s.lowerPowerConstant ρ * x * (R + s.lowerShift) ^ ρ) he0
159   have h1 := congrArg (fun x : ℝ => s.lowerPowerConstant ρ * x * (R + s.lowerShift) ^ ρ) he1
160   constructor
161   · nlinarith only [hu, h0]
162   · nlinarith only [hv, h1]
163 
164 theorem coupled_lower_log_power (s : Scales) (hs : s.positive)
165     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
166     {ρ : ℝ} (hρ : 0 < ρ) {w : Fin 2 → ℝ} (hw0 : ∀ i, 0 ≤ w i)
167     (hw1 : ∀ i, w i ≤ 1) (he : s.characteristicMatrix ρ *ᵥ w = w) :
168     ∀ R, 2 ≤ R → s.LowerPowerAt ρ w R := by
169   exact real_radius_descent_induction (P := fun R => s.LowerPowerAt ρ w R)
170     (B := s.lowerThreshold) (d := s.lowerDescent) (s.lowerDescent_positive hs hstrict)
171     (fun R hR hRB => s.lower_power_seed hs hstrict hρ hw1 hR hRB)
172     (fun R hR hBR hIH => s.lower_power_step hs hstrict hρ hw0 he hR hBR hIH)
173 
174 theorem normalizedCharacteristicVector_le_one (s : Scales) (hs : s.positive)
175     (hq : s.q < 1) {ρ : ℝ} (hρ : 0 < ρ) (i : Fin 2) :
176     s.normalizedCharacteristicVector ρ i ≤ 1 := by
177   have hm := s.normalizedCharacteristicVector_max hs hq hρ
178   fin_cases i
179   · exact (le_max_left _ _).trans hm.le
180   · exact (le_max_right _ _).trans hm.le
181 
182 theorem canonical_lower_log_power (s : Scales) (hs : s.positive)
183     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 2 ≤ R) :
184     s.LowerPowerAt (s.characteristicExponent hs hstrict)
185       (s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict)) R := by
186   have hρ := s.characteristicExponent_spec hs hstrict
187   exact s.coupled_lower_log_power hs hstrict hρ.1
188     (fun i => (s.normalizedCharacteristicVector_positive hs hstrict.1 hρ.1 i).le)
189     (s.normalizedCharacteristicVector_le_one hs hstrict.1 hρ.1)
190     (s.normalized_characteristic_eigenvector hs hρ.2) R hR
191 
192 theorem lower_log_power_ratio (s : Scales) (hs : s.positive)
193     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
194     {ρ : ℝ} (hρ : 0 < ρ) {w : Fin 2 → ℝ} (hw : ∀ i, 0 ≤ w i)
195     {R : ℝ} (hR : 2 ≤ R) (hL : s.LowerPowerAt ρ w R) :
196     s.lowerPowerConstant ρ * w 0 ≤ Real.log (s.UReal R) / R ^ ρ ∧
197     s.lowerPowerConstant ρ * w 1 ≤ Real.log (s.VReal R) / R ^ ρ := by
198   have hc := s.lowerPowerConstant_positive hs hstrict ρ
199   have hC := s.lowerShift_positive hs hstrict
200   have hR0 : 0 < R := by linarith
201   have hpR := Real.rpow_pos_of_pos hR0 ρ
202   have hp := Real.rpow_le_rpow hR0.le (by linarith : R ≤ R + s.lowerShift) hρ.le
203   constructor
204   · apply (le_div_iff₀ hpR).mpr
205     exact (mul_le_mul_of_nonneg_left hp (mul_nonneg hc.le (hw 0))).trans hL.1
206   · apply (le_div_iff₀ hpR).mpr
207     exact (mul_le_mul_of_nonneg_left hp (mul_nonneg hc.le (hw 1))).trans hL.2
208 
209 def canonicalLowerCoefficient (s : Scales) (hs : s.positive)
210     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) : ℝ :=
211   s.lowerPowerConstant (s.characteristicExponent hs hstrict) *
212     s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) i
213 
214 theorem canonicalLowerCoefficient_positive (s : Scales) (hs : s.positive)
215     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
216     0 < s.canonicalLowerCoefficient hs hstrict i :=
217   mul_pos (s.lowerPowerConstant_positive hs hstrict _)
218     (s.normalizedCharacteristicVector_positive hs hstrict.1
219       (s.characteristicExponent_spec hs hstrict).1 i)
220 
221 theorem canonical_lower_growth_ratio (s : Scales) (hs : s.positive)
222     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 2 ≤ R) :
223     s.canonicalLowerCoefficient hs hstrict 0 ≤
224       Real.log (s.UReal R) / R ^ (s.characteristicExponent hs hstrict) ∧
225     s.canonicalLowerCoefficient hs hstrict 1 ≤
226       Real.log (s.VReal R) / R ^ (s.characteristicExponent hs hstrict) := by
227   have hρ := s.characteristicExponent_spec hs hstrict
228   exact s.lower_log_power_ratio hs hstrict hρ.1
229     (fun i => (s.normalizedCharacteristicVector_positive hs hstrict.1 hρ.1 i).le)
230     hR (s.canonical_lower_log_power hs hstrict hR)
231 
232 theorem canonical_lower_norm_power (s : Scales) (hs : s.positive)
233     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 2 ≤ R) :
234     s.canonicalLowerCoefficient hs hstrict 0 *
235       (R + s.lowerShift) ^ (s.characteristicExponent hs hstrict) ≤ Real.log ‖s.U (R : ℂ)‖ ∧
236     s.canonicalLowerCoefficient hs hstrict 1 *
237       (R + s.lowerShift) ^ (s.characteristicExponent hs hstrict) ≤ Real.log ‖s.V (R : ℂ)‖ := by
238   have he := s.real_axis_norm hs hstrict (by linarith : 0 ≤ R)
239   rw [he.1, he.2]
240   exact s.canonical_lower_log_power hs hstrict hR
241 
242 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls