CoupledUpperGrowth.lean

1 import CoupledLowerGrowth
2 
3 /-! # Explicit upper comparison for the canonical coupled functions -/
4 
5 set_option autoImplicit false
6 set_option maxHeartbeats 2500000
7 
8 noncomputable section
9 open Set
10 open scoped Topology Matrix
11 
12 namespace Komorebi.SpecialFunctions.Coupled.Scales
13 
14 theorem full_radius_upper_from_deriv {f g h : ℝ → ℝ} {p q R : ℝ}
15     (hf : Differentiable ℝ f) (hf0 : f 0 = 0)
16     (hg0 : ∀ x, 0 ≤ x → 0 ≤ g x) (hh0 : ∀ x, 0 ≤ x → 0 ≤ h x)
17     (hgm : MonotoneOn g (Ici 0)) (hhm : MonotoneOn h (Ici 0))
18     (hd : ∀ x, deriv f x = 1 + g (p * x) * h (q * x))
19     (hp : 0 ≤ p) (hq : 0 ≤ q) (hR : 0 ≤ R) :
20     f R ≤ R * (1 + g (p * R) * h (q * R)) := by
21   have hbound : ∀ x ∈ interior (Icc 0 R),
22       deriv f x ≤ 1 + g (p * R) * h (q * R) := by
23     intro x hx
24     have hxI : x ∈ Icc 0 R := interior_subset hx
25     have hgp := hgm (mul_nonneg hp hxI.1) (mul_nonneg hp hR)
26       (mul_le_mul_of_nonneg_left hxI.2 hp)
27     have hhq := hhm (mul_nonneg hq hxI.1) (mul_nonneg hq hR)
28       (mul_le_mul_of_nonneg_left hxI.2 hq)
29     rw [hd x]
30     exact add_le_add le_rfl (mul_le_mul hgp hhq
31       (hh0 _ (mul_nonneg hq hxI.1)) (hg0 _ (mul_nonneg hp hR)))
32   have hc := (convex_Icc 0 R).image_sub_le_mul_sub_of_deriv_le
33     hf.continuous.continuousOn hf.differentiableOn hbound
34     0 ⟨le_rfl, hR⟩ R ⟨hR, le_rfl⟩ hR
35   simpa only [hf0, sub_zero, mul_comm] using hc
36 
37 theorem real_axis_full_upper (s : Scales) (hs : s.positive)
38     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 0 ≤ R) :
39     s.UReal R ≤ R * (1 + s.UReal (s.q * R) * s.VReal (s.r * R)) ∧
40     s.VReal R ≤ R * (1 + s.UReal (s.a * R) * s.VReal (s.b * R)) := by
41   have hd := s.real_axis_differentiable hs hstrict
42   have hm := s.real_axis_strictMono hs hstrict
43   have hu0 : ∀ x : ℝ, 0 ≤ x → 0 ≤ s.UReal x :=
44     fun x hx => (s.real_axis_nonneg hs hstrict hx).1
45   have hv0 : ∀ x : ℝ, 0 ≤ x → 0 ≤ s.VReal x :=
46     fun x hx => (s.real_axis_nonneg hs hstrict hx).2
47   exact ⟨full_radius_upper_from_deriv hd.1 s.real_axis_zero.1 hu0 hv0
48       hm.1.monotoneOn hm.2.monotoneOn
49       (fun x => (s.real_axis_hasDerivAt hs hstrict x).1.deriv) hs.1.le hs.2.1.le hR,
50     full_radius_upper_from_deriv hd.2 s.real_axis_zero.2 hu0 hv0
51       hm.1.monotoneOn hm.2.monotoneOn
52       (fun x => (s.real_axis_hasDerivAt hs hstrict x).2.deriv) hs.2.2.1.le hs.2.2.2.le hR⟩
53 
54 theorem real_axis_at_one_le_two (s : Scales) (hs : s.positive)
55     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
56     s.UReal 1 ≤ 2 ∧ s.VReal 1 ≤ 2 := by
57   have hf := s.real_series_hasSum hs hstrict 1
58   simp only [one_pow, mul_one] at hf
59   have hg : HasSum (fun n : ℕ => (1 / 2 : ℝ) ^ n) 2 := by
60     convert hasSum_geometric_of_lt_one (by norm_num : 0 ≤ (1 / 2 : ℝ)) (by norm_num) using 1
61     norm_num
62   have hsmall := And.intro hstrict.1.le
63     (And.intro hstrict.2.1.le (And.intro hstrict.2.2.1.le hstrict.2.2.2.le))
64   exact ⟨hasSum_le (fun n => (s.coefficients_le_geometric hs hsmall n).1) hf.1 hg,
65     hasSum_le (fun n => (s.coefficients_le_geometric hs hsmall n).2) hf.2 hg⟩
66 
67 def upperRadius (s : Scales) (n : ℕ) : ℝ := (1 / s.maxScale) ^ n
68 def upperSeed (s : Scales) : ℕ → ℝ
69   | 0 => 2
70   | n + 1 => s.upperRadius (n + 1) * (1 + s.upperSeed n ^ 2)
71 def upperLogSeed (s : Scales) (n : ℕ) : ℝ :=
72   ((2 : ℝ) ^ (n + 1) - 1) * Real.log 2 +
73     ((2 : ℝ) ^ (n + 1) - (n : ℝ) - 2) * Real.log (1 / s.maxScale)
74 
75 theorem upperRadius_ge_one (s : Scales) (hs : s.positive)
76     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (n : ℕ) :
77     1 ≤ s.upperRadius n := by
78   exact one_le_pow₀ ((one_le_div (s.maxScale_positive hs)).mpr
79     (s.maxScale_lt_one hstrict).le)
80 
81 theorem upperRadius_child (s : Scales) (hs : s.positive)
82     {p : ℝ} (hp : p ≤ s.maxScale) (n : ℕ) :
83     p * s.upperRadius (n + 1) ≤ s.upperRadius n := by
84   have hQ := s.maxScale_positive hs
85   have he : s.maxScale * s.upperRadius (n + 1) = s.upperRadius n := by
86     dsimp [upperRadius]
87     rw [pow_succ]
88     field_simp
89   exact (mul_le_mul_of_nonneg_right hp (by dsimp [upperRadius]; positivity)).trans he.le
90 
91 theorem upperSeed_ge_one (s : Scales) (hs : s.positive)
92     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (n : ℕ) :
93     1 ≤ s.upperSeed n := by
94   cases n with
95   | zero => norm_num [upperSeed]
96   | succ n =>
97     have hr := s.upperRadius_ge_one hs hstrict (n + 1)
98     have hz := sq_nonneg (s.upperSeed n)
99     dsimp [upperSeed]
100     nlinarith
101 
102 theorem real_axis_upper_ladder (s : Scales) (hs : s.positive)
103     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (n : ℕ) :
104     s.UReal (s.upperRadius n) ≤ s.upperSeed n ∧
105     s.VReal (s.upperRadius n) ≤ s.upperSeed n := by
106   induction n with
107   | zero => simpa [upperRadius, upperSeed] using s.real_axis_at_one_le_two hs hstrict
108   | succ n ih =>
109     have hR := (s.upperRadius_ge_one hs hstrict (n + 1)).trans' (by norm_num : (0 : ℝ) ≤ 1)
110     have hm := s.real_axis_strictMono hs hstrict
111     have hb := s.maxScale_bounds
112     have hchild (p : ℝ) (hp : 0 ≤ p) (hpQ : p ≤ s.maxScale) :
113         s.UReal (p * s.upperRadius (n + 1)) ≤ s.upperSeed n ∧
114         s.VReal (p * s.upperRadius (n + 1)) ≤ s.upperSeed n :=
115       ⟨(hm.1.monotoneOn (mul_nonneg hp hR)
116         (show 0 ≤ s.upperRadius n from (by norm_num : (0 : ℝ) ≤ 1).trans (s.upperRadius_ge_one hs hstrict n))
117         (s.upperRadius_child hs hpQ n)).trans ih.1,
118        (hm.2.monotoneOn (mul_nonneg hp hR)
119         (show 0 ≤ s.upperRadius n from (by norm_num : (0 : ℝ) ≤ 1).trans (s.upperRadius_ge_one hs hstrict n))
120         (s.upperRadius_child hs hpQ n)).trans ih.2⟩
121     have hu := s.real_axis_full_upper hs hstrict hR
122     have hz := (s.upperSeed_ge_one hs hstrict n).trans' (by norm_num : (0 : ℝ) ≤ 1)
123     have hprod (p p' : ℝ) (hp : 0 ≤ p) (hp' : 0 ≤ p')
124         (hpQ : p ≤ s.maxScale) (hpQ' : p' ≤ s.maxScale) :
125         s.UReal (p * s.upperRadius (n + 1)) * s.VReal (p' * s.upperRadius (n + 1)) ≤
126           s.upperSeed n ^ 2 := by
127       have ha := (hchild p hp hpQ).1
128       have hb' := (hchild p' hp' hpQ').2
129       have hn := (s.real_axis_nonneg hs hstrict (mul_nonneg hp' hR)).2
130       simpa only [pow_two] using mul_le_mul ha hb' hn hz
131     constructor
132     · exact hu.1.trans (mul_le_mul_of_nonneg_left
133         (add_le_add le_rfl (hprod s.q s.r hs.1.le hs.2.1.le hb.1 hb.2.1)) hR)
134     · exact hu.2.trans (mul_le_mul_of_nonneg_left
135         (add_le_add le_rfl (hprod s.a s.b hs.2.2.1.le hs.2.2.2.le hb.2.2.1 hb.2.2.2)) hR)
136 
137 theorem upperLogSeed_recurrence (s : Scales) (n : ℕ) :
138     s.upperLogSeed (n + 1) = (n + 1 : ℝ) * Real.log (1 / s.maxScale) +
139       Real.log 2 + 2 * s.upperLogSeed n := by
140   simp only [upperLogSeed, Nat.cast_add, Nat.cast_one, pow_succ]
141   ring
142 
143 theorem upperSeed_log_le (s : Scales) (hs : s.positive)
144     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (n : ℕ) :
145     Real.log (s.upperSeed n) ≤ s.upperLogSeed n := by
146   induction n with
147   | zero => norm_num [upperSeed, upperLogSeed]
148   | succ n ih =>
149     have hz := s.upperSeed_ge_one hs hstrict n
150     have hz0 : 0 < s.upperSeed n := by linarith
151     have hr : 0 < s.upperRadius (n + 1) :=
152       lt_of_lt_of_le (by norm_num) (s.upperRadius_ge_one hs hstrict (n + 1))
153     have harg : 0 < 1 + s.upperSeed n ^ 2 := by positivity
154     have hh : 1 + s.upperSeed n ^ 2 ≤ 2 * s.upperSeed n ^ 2 := by nlinarith
155     have hl := Real.log_le_log harg hh
156     rw [Real.log_mul (by norm_num) (ne_of_gt (sq_pos_of_pos hz0)), Real.log_pow] at hl
157     norm_num only [Nat.cast_ofNat] at hl
158     rw [upperSeed, Real.log_mul (ne_of_gt hr) (ne_of_gt harg)]
159     have hrlog : Real.log (s.upperRadius (n + 1)) =
160         (n + 1 : ℝ) * Real.log (1 / s.maxScale) := by
161       simp [upperRadius, Real.log_pow]
162     rw [hrlog, s.upperLogSeed_recurrence]
163     linarith only [ih, hl]
164 
165 def scaleDelay (p : ℝ) : ℝ := Real.log (1 / p)
166 def upperDelay (s : Scales) : ℝ := scaleDelay s.minScale
167 def upperCorrection (s : Scales) : ℝ :=
168   max (scaleDelay (s.q * s.r)) (scaleDelay (s.a * s.b)) + Real.log 2
169 def upperSeedBudget (s : Scales) (n : ℕ) : ℝ :=
170   s.upperLogSeed n + 1 + s.upperDelay + s.upperCorrection
171 def upperPowerConstant (s : Scales) (n : ℕ) (ρ : ℝ) (w : Fin 2 → ℝ) : ℝ :=
172   Real.exp (-ρ) * s.upperSeedBudget n / min (w 0) (w 1)
173 def UpperPowerAt (s : Scales) (n : ℕ) (ρ : ℝ) (w : Fin 2 → ℝ) (t : ℝ) : Prop :=
174   Real.log (s.UReal (Real.exp t)) + t + s.upperCorrection ≤
175     s.upperPowerConstant n ρ w * w 0 * Real.exp (ρ * t) ∧
176   Real.log (s.VReal (Real.exp t)) + t + s.upperCorrection ≤
177     s.upperPowerConstant n ρ w * w 1 * Real.exp (ρ * t)
178 
179 theorem scaleDelay_positive {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
180     0 < scaleDelay p := by
181   exact Real.log_pos ((one_lt_div hp).mpr hp1)
182 
183 theorem scaleDelay_bounds (s : Scales) (hs : s.positive)
184     {p : ℝ} (hmp : s.minScale ≤ p) (hpQ : p ≤ s.maxScale) :
185     scaleDelay s.maxScale ≤ scaleDelay p ∧ scaleDelay p ≤ s.upperDelay := by
186   have hm := s.minScale_positive hs
187   have hp := hm.trans_le hmp
188   have hQ := s.maxScale_positive hs
189   constructor
190   · exact Real.log_le_log (by positivity) (one_div_le_one_div_of_le hp hpQ)
191   · exact Real.log_le_log (by positivity) (one_div_le_one_div_of_le hm hmp)
192 
193 theorem upperCorrection_positive (s : Scales) (hs : s.positive)
194     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
195     0 < s.upperCorrection := by
196   have hh := mul_lt_mul_of_pos_right hstrict.1 hs.2.1
197   have hqr : s.q * s.r < 1 := by nlinarith only [hh, hstrict.2.1]
198   have hd := scaleDelay_positive (mul_pos hs.1 hs.2.1) hqr
199   have hm := le_max_left (scaleDelay (s.q * s.r)) (scaleDelay (s.a * s.b))
200   dsimp [upperCorrection]
201   linarith [Real.log_pos (by norm_num : (1 : ℝ) < 2)]
202 
203 theorem upperCorrection_rows (s : Scales) (hs : s.positive) :
204     scaleDelay s.q + scaleDelay s.r + Real.log 2 ≤ s.upperCorrection ∧
205     scaleDelay s.a + scaleDelay s.b + Real.log 2 ≤ s.upperCorrection := by
206   have he (p p' : ℝ) (hp : 0 < p) (hp' : 0 < p') :
207       scaleDelay (p * p') = scaleDelay p + scaleDelay p' := by
208     simp only [scaleDelay, one_div, mul_inv_rev, Real.log_mul
209       (inv_ne_zero (ne_of_gt hp')) (inv_ne_zero (ne_of_gt hp))]
210     ring
211   rw [upperCorrection, he s.q s.r hs.1 hs.2.1, he s.a s.b hs.2.2.1 hs.2.2.2]
212   exact ⟨add_le_add (le_max_left _ _) le_rfl, add_le_add (le_max_right _ _) le_rfl⟩
213 
214 theorem exp_one_lt_three : Real.exp 1 < 3 := by
215   have hh := Real.exp_bound_div_one_sub_of_interval
216     (by norm_num : (0 : ℝ) ≤ 1 / 6) (by norm_num : (1 / 6 : ℝ) < 1)
217   norm_num at hh
218   have hp := pow_le_pow_left₀ (Real.exp_pos (1 / 6)).le hh 6
219   have he : Real.exp 1 = Real.exp (1 / 6) ^ 6 := by
220     convert Real.exp_nat_mul (1 / 6) 6 using 1
221     norm_num
222   rw [← he] at hp
223   norm_num at hp ⊢
224   linarith only [hp]
225 
226 theorem exists_upper_seed_index (s : Scales) (hs : s.positive)
227     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
228     ∃ n : ℕ, 3 / s.minScale ≤ s.upperRadius n := by
229   obtain ⟨n, hn⟩ := pow_unbounded_of_one_lt (3 / s.minScale)
230     ((one_lt_div (s.maxScale_positive hs)).mpr (s.maxScale_lt_one hstrict))
231   exact ⟨n, hn.le⟩
232 
233 theorem upper_seed_exp_radius (s : Scales) (hs : s.positive)
234     {n : ℕ} (hn : 3 / s.minScale ≤ s.upperRadius n) {t : ℝ}
235     (ht : t ≤ 1 + s.upperDelay) : Real.exp t ≤ s.upperRadius n := by
236   have hm := s.minScale_positive hs
237   have he : Real.exp (1 + s.upperDelay) = Real.exp 1 / s.minScale := by
238     rw [Real.exp_add]
239     dsimp [upperDelay, scaleDelay]
240     rw [Real.exp_log (by positivity)]
241     ring
242   calc
243     Real.exp t ≤ Real.exp (1 + s.upperDelay) := Real.exp_le_exp.mpr ht
244     _ = Real.exp 1 / s.minScale := he
245     _ ≤ 3 / s.minScale := (div_le_div_of_nonneg_right exp_one_lt_three.le hm.le)
246     _ ≤ s.upperRadius n := hn
247 
248 theorem real_axis_upper_log_seed (s : Scales) (hs : s.positive)
249     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
250     {n : ℕ} (hn : 3 / s.minScale ≤ s.upperRadius n) {t : ℝ}
251     (ht : t ≤ 1 + s.upperDelay) :
252     Real.log (s.UReal (Real.exp t)) ≤ s.upperLogSeed n ∧
253     Real.log (s.VReal (Real.exp t)) ≤ s.upperLogSeed n := by
254   have hR := s.upper_seed_exp_radius hs hn ht
255   have hm := s.real_axis_strictMono hs hstrict
256   have hl := s.real_axis_upper_ladder hs hstrict n
257   have hpos := s.real_axis_lower_linear hs hstrict (Real.exp_pos t).le
258   have hRn : 0 ≤ s.upperRadius n :=
259     (by norm_num : (0 : ℝ) ≤ 1).trans (s.upperRadius_ge_one hs hstrict n)
260   constructor
261   · exact (Real.log_le_log (lt_of_lt_of_le (Real.exp_pos t) hpos.1)
262       ((hm.1.monotoneOn (Real.exp_pos t).le hRn hR).trans hl.1)).trans
263       (s.upperSeed_log_le hs hstrict n)
264   · exact (Real.log_le_log (lt_of_lt_of_le (Real.exp_pos t) hpos.2)
265       ((hm.2.monotoneOn (Real.exp_pos t).le hRn hR).trans hl.2)).trans
266       (s.upperSeed_log_le hs hstrict n)
267 
268 theorem log_upper_from_full {f u v R : ℝ} (hf : 0 < f) (hR : 0 < R)
269     (hu : 1 ≤ u) (hv : 1 ≤ v) (hfull : f ≤ R * (1 + u * v)) :
270     Real.log f ≤ Real.log R + Real.log 2 + Real.log u + Real.log v := by
271   have hu0 : 0 < u := by linarith
272   have hv0 : 0 < v := by linarith
273   have hprod : 1 ≤ u * v := one_le_mul_of_one_le_of_one_le hu hv
274   have hf' : f ≤ R * (2 * (u * v)) := by nlinarith only [hfull, hprod, hR]
275   have hh := Real.log_le_log hf hf'
276   rw [Real.log_mul (ne_of_gt hR) (by positivity),
277     Real.log_mul (by norm_num) (by positivity),
278     Real.log_mul (ne_of_gt hu0) (ne_of_gt hv0)] at hh
279   linarith only [hh]
280 
281 theorem real_axis_log_full_upper (s : Scales) (hs : s.positive)
282     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
283     {R : ℝ} (hR : 0 < R) (hmR : 1 ≤ s.minScale * R) :
284     Real.log (s.UReal R) ≤ Real.log R + Real.log 2 +
285       Real.log (s.UReal (s.q * R)) + Real.log (s.VReal (s.r * R)) ∧
286     Real.log (s.VReal R) ≤ Real.log R + Real.log 2 +
287       Real.log (s.UReal (s.a * R)) + Real.log (s.VReal (s.b * R)) := by
288   have hb := s.minScale_bounds
289   have hl := s.real_axis_lower_linear hs hstrict hR.le
290   have hp (p : ℝ) (hmp : s.minScale ≤ p) :
291       1 ≤ s.UReal (p * R) ∧ 1 ≤ s.VReal (p * R) := by
292     have hpR : 1 ≤ p * R := hmR.trans (mul_le_mul_of_nonneg_right hmp hR.le)
293     have hx := s.real_axis_lower_linear hs hstrict (by linarith : 0 ≤ p * R)
294     exact ⟨hpR.trans hx.1, hpR.trans hx.2⟩
295   have hu := s.real_axis_full_upper hs hstrict hR.le
296   exact ⟨log_upper_from_full (hR.trans_le hl.1) hR (hp s.q hb.1).1 (hp s.r hb.2.1).2 hu.1,
297     log_upper_from_full (hR.trans_le hl.2) hR (hp s.a hb.2.2.1).1 (hp s.b hb.2.2.2).2 hu.2⟩
298 
299 theorem upperSeedBudget_positive (s : Scales) (hs : s.positive)
300     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (n : ℕ) :
301     0 < s.upperSeedBudget n := by
302   have hW := (Real.log_nonneg (s.upperSeed_ge_one hs hstrict n)).trans
303     (s.upperSeed_log_le hs hstrict n)
304   have hΔ := scaleDelay_positive (s.minScale_positive hs)
305     (s.minScale_bounds.1.trans_lt hstrict.1)
306   change 0 < s.upperDelay at hΔ
307   have hD := s.upperCorrection_positive hs hstrict
308   dsimp [upperSeedBudget]
309   linarith only [hW, hΔ, hD]
310 
311 theorem upperPowerConstant_positive (s : Scales) (hs : s.positive)
312     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
313     (n : ℕ) (ρ : ℝ) {w : Fin 2 → ℝ} (hw : ∀ i, 0 < w i) :
314     0 < s.upperPowerConstant n ρ w :=
315   div_pos (mul_pos (Real.exp_pos _) (s.upperSeedBudget_positive hs hstrict n))
316     (lt_min (hw 0) (hw 1))
317 
318 theorem upper_power_seed (s : Scales) (hs : s.positive)
319     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
320     {n : ℕ} (hn : 3 / s.minScale ≤ s.upperRadius n)
321     {ρ : ℝ} (hρ : 0 < ρ) {w : Fin 2 → ℝ} (hw : ∀ i, 0 < w i)
322     {t : ℝ} (ht : 1 ≤ t) (htB : t ≤ 1 + s.upperDelay) :
323     s.UpperPowerAt n ρ w t := by
324   have hS := s.upperSeedBudget_positive hs hstrict n
325   have hm : 0 < min (w 0) (w 1) := lt_min (hw 0) (hw 1)
326   have hl := s.real_axis_upper_log_seed hs hstrict hn htB
327   have hmin (i : Fin 2) : min (w 0) (w 1) ≤ w i := by
328     fin_cases i
329     · exact min_le_left _ _
330     · exact min_le_right _ _
331   have hweight (i : Fin 2) : s.upperSeedBudget n ≤
332       s.upperSeedBudget n / min (w 0) (w 1) * w i := by
333     calc
334       _ = s.upperSeedBudget n / min (w 0) (w 1) * min (w 0) (w 1) :=
335         (div_mul_cancel₀ _ (ne_of_gt hm)).symm
336       _ ≤ _ := mul_le_mul_of_nonneg_left (hmin i) (div_nonneg hS.le hm.le)
337   have he : 1 ≤ Real.exp (-ρ) * Real.exp (ρ * t) := by
338     rw [← Real.exp_add]
339     exact Real.one_le_exp_iff.mpr (by nlinarith only [hρ, ht])
340   have hbound (i : Fin 2) : s.upperSeedBudget n ≤
341       s.upperPowerConstant n ρ w * w i * Real.exp (ρ * t) := by
342     calc
343       _ ≤ s.upperSeedBudget n / min (w 0) (w 1) * w i := hweight i
344       _ ≤ (s.upperSeedBudget n / min (w 0) (w 1) * w i) *
345           (Real.exp (-ρ) * Real.exp (ρ * t)) :=
346         le_mul_of_one_le_right (le_trans hS.le (hweight i)) he
347       _ = _ := by dsimp [upperPowerConstant]; ring
348   constructor
349   · exact (show Real.log (s.UReal (Real.exp t)) + t + s.upperCorrection ≤
350         s.upperSeedBudget n from by dsimp [upperSeedBudget]; linarith only [hl.1, htB]).trans (hbound 0)
351   · exact (show Real.log (s.VReal (Real.exp t)) + t + s.upperCorrection ≤
352         s.upperSeedBudget n from by dsimp [upperSeedBudget]; linarith only [hl.2, htB]).trans (hbound 1)
353 
354 theorem exp_sub_scaleDelay {p : ℝ} (hp : 0 < p) (t : ℝ) :
355     Real.exp (t - scaleDelay p) = p * Real.exp t := by
356   rw [Real.exp_sub]
357   dsimp [scaleDelay]
358   rw [Real.exp_log (by positivity : 0 < 1 / p)]
359   field_simp
360 
361 theorem real_axis_log_delayed_upper (s : Scales) (hs : s.positive)
362     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
363     {t : ℝ} (ht : 1 + s.upperDelay ≤ t) :
364     Real.log (s.UReal (Real.exp t)) + t + s.upperCorrection ≤
365       (Real.log (s.UReal (Real.exp (t - scaleDelay s.q))) + (t - scaleDelay s.q) + s.upperCorrection) +
366       (Real.log (s.VReal (Real.exp (t - scaleDelay s.r))) + (t - scaleDelay s.r) + s.upperCorrection) ∧
367     Real.log (s.VReal (Real.exp t)) + t + s.upperCorrection ≤
368       (Real.log (s.UReal (Real.exp (t - scaleDelay s.a))) + (t - scaleDelay s.a) + s.upperCorrection) +
369       (Real.log (s.VReal (Real.exp (t - scaleDelay s.b))) + (t - scaleDelay s.b) + s.upperCorrection) := by
370   have hm := s.minScale_positive hs
371   have hchild : 1 ≤ s.minScale * Real.exp t := by
372     rw [← exp_sub_scaleDelay hm t]
373     exact Real.one_le_exp_iff.mpr (by change 0 ≤ t - s.upperDelay; linarith only [ht])
374   have hh := s.real_axis_log_full_upper hs hstrict (Real.exp_pos t) hchild
375   rw [Real.log_exp, ← exp_sub_scaleDelay hs.1 t, ← exp_sub_scaleDelay hs.2.1 t,
376     ← exp_sub_scaleDelay hs.2.2.1 t, ← exp_sub_scaleDelay hs.2.2.2 t] at hh
377   have hD := s.upperCorrection_rows hs
378   constructor
379   · linarith only [hh.1, hD.1]
380   · linarith only [hh.2, hD.2]
381 
382 theorem exp_weight_shift {p ρ t : ℝ} (hp : 0 < p) :
383     Real.exp (ρ * (t - scaleDelay p)) = p ^ ρ * Real.exp (ρ * t) := by
384   rw [Real.rpow_def_of_pos hp, ← Real.exp_add]
385   congr 1
386   simp only [scaleDelay, one_div, Real.log_inv]
387   ring
388 
389 theorem real_log_delay_induction {P : ℝ → Prop} {B d : ℝ} (hd : 0 < d)
390     (hseed : ∀ t, 1 ≤ t → t ≤ B → P t)
391     (hstep : ∀ t, 1 ≤ t → B < t → (∀ u, 1 ≤ u → u ≤ t - d → P u) → P t) :
392     ∀ t, 1 ≤ t → P t := by
393   have h := real_radius_descent_induction (P := fun R => P (R - 1))
394     (B := B + 1) (d := d) hd
395     (fun R hR hRB => hseed (R - 1) (by linarith only [hR]) (by linarith only [hRB]))
396     (fun R hR hBR hIH => hstep (R - 1) (by linarith only [hR])
397       (by linarith only [hBR]) (fun u hu hud => by
398         have hh := hIH (u + 1) (by linarith only [hu]) (by linarith only [hud])
399         simpa only [add_sub_cancel_right] using hh))
400   intro t ht
401   have hh := h (t + 1) (by linarith only [ht])
402   simpa only [add_sub_cancel_right] using hh
403 
404 theorem upper_power_step (s : Scales) (hs : s.positive)
405     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
406     (n : ℕ) (ρ : ℝ) (w : Fin 2 → ℝ)
407     (he : s.characteristicMatrix ρ *ᵥ w = w) {t : ℝ}
408     (ht : 1 + s.upperDelay < t)
409     (hIH : ∀ u, 1 ≤ u → u ≤ t - scaleDelay s.maxScale → s.UpperPowerAt n ρ w u) :
410     s.UpperPowerAt n ρ w t := by
411   have hb := s.minScale_bounds
412   have hQ := s.maxScale_bounds
413   have hchild (p : ℝ) (hmp : s.minScale ≤ p) (hpQ : p ≤ s.maxScale) :
414       s.UpperPowerAt n ρ w (t - scaleDelay p) := by
415     have hh := s.scaleDelay_bounds hs hmp hpQ
416     exact hIH _ (by linarith only [ht, hh.2]) (by linarith only [hh.1])
417   have hq := hchild s.q hb.1 hQ.1
418   have hr := hchild s.r hb.2.1 hQ.2.1
419   have ha := hchild s.a hb.2.2.1 hQ.2.2.1
420   have hB := hchild s.b hb.2.2.2 hQ.2.2.2
421   have hh := s.real_axis_log_delayed_upper hs hstrict ht.le
422   have hu := hh.1.trans (add_le_add hq.1 hr.2)
423   have hv := hh.2.trans (add_le_add ha.1 hB.2)
424   rw [exp_weight_shift hs.1, exp_weight_shift hs.2.1] at hu
425   rw [exp_weight_shift hs.2.2.1, exp_weight_shift hs.2.2.2] at hv
426   have he0 := congrFun he 0
427   have he1 := congrFun he 1
428   norm_num [characteristicMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two] at he0 he1
429   have h0 := congrArg (fun x : ℝ => s.upperPowerConstant n ρ w * x * Real.exp (ρ * t)) he0
430   have h1 := congrArg (fun x : ℝ => s.upperPowerConstant n ρ w * x * Real.exp (ρ * t)) he1
431   constructor
432   · nlinarith only [hu, h0]
433   · nlinarith only [hv, h1]
434 
435 theorem coupled_upper_log_power (s : Scales) (hs : s.positive)
436     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
437     {n : ℕ} (hn : 3 / s.minScale ≤ s.upperRadius n)
438     {ρ : ℝ} (hρ : 0 < ρ) {w : Fin 2 → ℝ} (hw : ∀ i, 0 < w i)
439     (he : s.characteristicMatrix ρ *ᵥ w = w) :
440     ∀ t, 1 ≤ t → s.UpperPowerAt n ρ w t := by
441   exact real_log_delay_induction (B := 1 + s.upperDelay)
442     (d := scaleDelay s.maxScale) (scaleDelay_positive (s.maxScale_positive hs) (s.maxScale_lt_one hstrict))
443     (fun t ht htB => s.upper_power_seed hs hstrict hn hρ hw ht htB)
444     (fun t _ ht hIH => s.upper_power_step hs hstrict n ρ w he ht hIH)
445 
446 theorem canonical_upper_log_power (s : Scales) (hs : s.positive)
447     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
448     {n : ℕ} (hn : 3 / s.minScale ≤ s.upperRadius n)
449     {R : ℝ} (hR : Real.exp 1 ≤ R) :
450     Real.log (s.UReal R) ≤ s.upperPowerConstant n (s.characteristicExponent hs hstrict)
451       (s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict)) *
452       s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) 0 *
453       R ^ (s.characteristicExponent hs hstrict) - Real.log R - s.upperCorrection ∧
454     Real.log (s.VReal R) ≤ s.upperPowerConstant n (s.characteristicExponent hs hstrict)
455       (s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict)) *
456       s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) 1 *
457       R ^ (s.characteristicExponent hs hstrict) - Real.log R - s.upperCorrection := by
458   have hR0 := (Real.exp_pos 1).trans_le hR
459   have ht : 1 ≤ Real.log R := (Real.le_log_iff_exp_le hR0).mpr hR
460   have hρ := s.characteristicExponent_spec hs hstrict
461   have hh := s.coupled_upper_log_power hs hstrict hn hρ.1
462     (s.normalizedCharacteristicVector_positive hs hstrict.1 hρ.1)
463     (s.normalized_characteristic_eigenvector hs hρ.2) (Real.log R) ht
464   dsimp [UpperPowerAt] at hh
465   rw [Real.exp_log hR0] at hh
466   have he : Real.exp (s.characteristicExponent hs hstrict * Real.log R) =
467       R ^ (s.characteristicExponent hs hstrict) := by
468     rw [Real.rpow_def_of_pos hR0, mul_comm]
469   rw [he] at hh
470   constructor
471   · linarith only [hh.1]
472   · linarith only [hh.2]
473 
474 def upperSeedIndex (s : Scales) (hs : s.positive)
475     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) : ℕ :=
476   Nat.find (s.exists_upper_seed_index hs hstrict)
477 
478 theorem upperSeedIndex_spec (s : Scales) (hs : s.positive)
479     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
480     3 / s.minScale ≤ s.upperRadius (s.upperSeedIndex hs hstrict) :=
481   Nat.find_spec (s.exists_upper_seed_index hs hstrict)
482 
483 def canonicalUpperCoefficient (s : Scales) (hs : s.positive)
484     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) : ℝ :=
485   s.upperPowerConstant (s.upperSeedIndex hs hstrict) (s.characteristicExponent hs hstrict)
486     (s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict)) *
487     s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) i
488 
489 theorem canonicalUpperCoefficient_positive (s : Scales) (hs : s.positive)
490     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) :
491     0 < s.canonicalUpperCoefficient hs hstrict i := by
492   have hρ := s.characteristicExponent_spec hs hstrict
493   have hw := s.normalizedCharacteristicVector_positive hs hstrict.1 hρ.1
494   exact mul_pos (s.upperPowerConstant_positive hs hstrict _ _ hw) (hw i)
495 
496 theorem canonical_upper_growth_ratio (s : Scales) (hs : s.positive)
497     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
498     {R : ℝ} (hR : Real.exp 1 ≤ R) :
499     Real.log (s.UReal R) / R ^ (s.characteristicExponent hs hstrict) ≤
500       s.canonicalUpperCoefficient hs hstrict 0 ∧
501     Real.log (s.VReal R) / R ^ (s.characteristicExponent hs hstrict) ≤
502       s.canonicalUpperCoefficient hs hstrict 1 := by
503   have hR0 := (Real.exp_pos 1).trans_le hR
504   have hp := Real.rpow_pos_of_pos hR0 (s.characteristicExponent hs hstrict)
505   have hh := s.canonical_upper_log_power hs hstrict (s.upperSeedIndex_spec hs hstrict) hR
506   have hlog : 1 ≤ Real.log R := (Real.le_log_iff_exp_le hR0).mpr hR
507   have hD := s.upperCorrection_positive hs hstrict
508   constructor
509   · apply (div_le_iff₀ hp).mpr
510     change Real.log (s.UReal R) ≤
511       (s.upperPowerConstant (s.upperSeedIndex hs hstrict) (s.characteristicExponent hs hstrict)
512         (s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict)) *
513         s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) 0) *
514         R ^ (s.characteristicExponent hs hstrict)
515     linarith only [hh.1, hlog, hD]
516   · apply (div_le_iff₀ hp).mpr
517     change Real.log (s.VReal R) ≤
518       (s.upperPowerConstant (s.upperSeedIndex hs hstrict) (s.characteristicExponent hs hstrict)
519         (s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict)) *
520         s.normalizedCharacteristicVector (s.characteristicExponent hs hstrict) 1) *
521         R ^ (s.characteristicExponent hs hstrict)
522     linarith only [hh.2, hlog, hD]
523 
524 theorem canonical_two_sided_growth_ratio (s : Scales) (hs : s.positive)
525     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
526     {R : ℝ} (hR : Real.exp 1 ≤ R) :
527     (s.canonicalLowerCoefficient hs hstrict 0 ≤
528       Real.log (s.UReal R) / R ^ (s.characteristicExponent hs hstrict) ∧
529       Real.log (s.UReal R) / R ^ (s.characteristicExponent hs hstrict) ≤
530         s.canonicalUpperCoefficient hs hstrict 0) ∧
531     (s.canonicalLowerCoefficient hs hstrict 1 ≤
532       Real.log (s.VReal R) / R ^ (s.characteristicExponent hs hstrict) ∧
533       Real.log (s.VReal R) / R ^ (s.characteristicExponent hs hstrict) ≤
534         s.canonicalUpperCoefficient hs hstrict 1) := by
535   have h2 : (2 : ℝ) ≤ Real.exp 1 := by simpa only [one_add_one_eq_two] using Real.add_one_le_exp (1 : ℝ)
536   have hl := s.canonical_lower_growth_ratio hs hstrict (h2.trans hR)
537   have hu := s.canonical_upper_growth_ratio hs hstrict hR
538   exact ⟨⟨hl.1, hu.1⟩, ⟨hl.2, hu.2⟩⟩
539 
540 theorem canonical_upper_norm_power (s : Scales) (hs : s.positive)
541     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
542     {R : ℝ} (hR : Real.exp 1 ≤ R) :
543     Real.log ‖s.U (R : ℂ)‖ ≤ s.canonicalUpperCoefficient hs hstrict 0 *
544       R ^ (s.characteristicExponent hs hstrict) - Real.log R - s.upperCorrection ∧
545     Real.log ‖s.V (R : ℂ)‖ ≤ s.canonicalUpperCoefficient hs hstrict 1 *
546       R ^ (s.characteristicExponent hs hstrict) - Real.log R - s.upperCorrection := by
547   have hR0 := (Real.exp_pos 1).trans_le hR
548   have he := s.real_axis_norm hs hstrict hR0.le
549   rw [he.1, he.2]
550   exact s.canonical_upper_log_power hs hstrict (s.upperSeedIndex_spec hs hstrict) hR
551 
552 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls