CoupledEvaluation.lean

1 import CoupledOperator
2 
3 /-! # Arbitrary-radius disk and Taylor evaluation certificates -/
4 
5 set_option autoImplicit false
6 set_option maxHeartbeats 2500000
7 
8 noncomputable section
9 open Filter Set
10 open scoped Topology Matrix
11 
12 namespace Komorebi.SpecialFunctions.Coupled.Scales
13 
14 theorem component_real_hasSum (s : Scales) (hs : s.positive)
15     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) (R : ℝ) :
16     HasSum (fun n => s.componentCoefficient i n * R ^ (2*n+1)) (s.realComponent i R) := by
17   have h := s.real_series_hasSum hs hc R
18   fin_cases i
19   · exact h.1
20   · exact h.2
21 
22 theorem component_norm_summable (s : Scales) (hs : s.positive)
23     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) (z : ℂ) :
24     Summable (fun n => ‖(s.componentCoefficient i n : ℂ) * z ^ (2*n+1)‖) := by
25   have h := s.coefficient_series_entire hs hc z
26   fin_cases i
27   · exact h.1
28   · exact h.2
29 
30 theorem component_real_nonneg (s : Scales) (hs : s.positive)
31     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) {R : ℝ}
32     (hR : 0 ≤ R) : 0 ≤ s.realComponent i R := by
33   have h := s.real_axis_nonneg hs hc hR
34   fin_cases i
35   · exact h.1
36   · exact h.2
37 
38 theorem component_real_mono (s : Scales) (hs : s.positive)
39     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
40     {R S : ℝ} (hR : 0 ≤ R) (hRS : R ≤ S) : s.realComponent i R ≤ s.realComponent i S := by
41   have h := s.real_axis_strictMono hs hc
42   fin_cases i
43   · exact h.1.monotoneOn hR (hR.trans hRS) hRS
44   · exact h.2.monotoneOn hR (hR.trans hRS) hRS
45 
46 theorem component_at_real (s : Scales) (hs : s.positive)
47     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) (x : ℝ) :
48     s.complexComponent i (x : ℂ) = (s.realComponent i x : ℂ) := by
49   have h := s.real_axis_identification hs hc x
50   fin_cases i
51   · exact h.1
52   · exact h.2
53 
54 def realPairMax (s : Scales) (R : ℝ) : ℝ := max (s.UReal R) (s.VReal R)
55 
56 theorem component_le_pairMax (s : Scales) (i : Fin 2) (R : ℝ) :
57     s.realComponent i R ≤ s.realPairMax R := by
58   fin_cases i
59   · exact le_max_left _ _
60   · exact le_max_right _ _
61 
62 theorem realPairMax_nonneg (s : Scales) (hs : s.positive)
63     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 0 ≤ R) :
64     0 ≤ s.realPairMax R :=
65   (s.real_axis_nonneg hs hc hR).1.trans (le_max_left _ _)
66 
67 theorem realPairMax_recurrence (s : Scales) (hs : s.positive)
68     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 0 ≤ R) :
69     s.realPairMax R ≤ R * (1 + s.realPairMax (s.maxScale * R) ^ 2) := by
70   have harg {p : ℝ} (hp : 0 ≤ p) (hpQ : p ≤ s.maxScale) (i : Fin 2) :
71       s.realComponent i (p * R) ≤ s.realPairMax (s.maxScale * R) :=
72     (s.component_real_mono hs hc i (mul_nonneg hp hR)
73       (mul_le_mul_of_nonneg_right hpQ hR)).trans (s.component_le_pairMax i _)
74   have hq := harg hs.1.le s.maxScale_bounds.1 0
75   have hr := harg hs.2.1.le s.maxScale_bounds.2.1 1
76   have ha := harg hs.2.2.1.le s.maxScale_bounds.2.2.1 0
77   have hb := harg hs.2.2.2.le s.maxScale_bounds.2.2.2 1
78   have hM := s.realPairMax_nonneg hs hc (mul_nonneg (s.maxScale_positive hs).le hR)
79   have hvr := (s.real_axis_nonneg hs hc (mul_nonneg hs.2.1.le hR)).2
80   have hvb := (s.real_axis_nonneg hs hc (mul_nonneg hs.2.2.2.le hR)).2
81   have hU : s.UReal (s.q * R) * s.VReal (s.r * R) ≤ s.realPairMax (s.maxScale * R)^2 := by
82     simpa only [realComponent, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
83       pow_two] using mul_le_mul hq hr hvr hM
84   have hV : s.UReal (s.a * R) * s.VReal (s.b * R) ≤ s.realPairMax (s.maxScale * R)^2 := by
85     simpa only [realComponent, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
86       pow_two] using mul_le_mul ha hb hvb hM
87   have hf := s.real_axis_full_upper hs hc hR
88   exact max_le (hf.1.trans (mul_le_mul_of_nonneg_left (add_le_add le_rfl hU) hR))
89     (hf.2.trans (mul_le_mul_of_nonneg_left (add_le_add le_rfl hV) hR))
90 
91 theorem component_coefficient_le_one (s : Scales) (hs : s.positive)
92     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) (n : ℕ) :
93     s.componentCoefficient i n ≤ 1 := by
94   apply (s.component_coefficient_majorant hs hc i n).2.trans
95   exact pow_le_one₀ (by norm_num) (by norm_num)
96 
97 theorem component_small_disk_bound (s : Scales) (hs : s.positive)
98     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
99     {R : ℝ} (hR : 0 ≤ R) (hR1 : R < 1) : s.realComponent i R ≤ R / (1 - R^2) := by
100   have hg : HasSum (fun n : ℕ => R * (R^2)^n) (R / (1-R^2)) := by
101     simpa only [div_eq_mul_inv] using
102       (hasSum_geometric_of_lt_one (sq_nonneg R) (by nlinarith only [hR, hR1])).mul_left R
103   apply hasSum_le _ (s.component_real_hasSum hs hc i R) hg
104   intro n
105   calc
106     _ ≤ 1 * R^(2*n+1) := mul_le_mul_of_nonneg_right
107       (s.component_coefficient_le_one hs hc i n) (pow_nonneg hR _)
108     _ = R * (R^2)^n := by ring
109 
110 theorem pair_small_disk_bound (s : Scales) (hs : s.positive)
111     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
112     {R : ℝ} (hR : 0 ≤ R) (hR1 : R < 1) : s.realPairMax R ≤ R / (1-R^2) :=
113   max_le (s.component_small_disk_bound hs hc 0 hR hR1)
114     (s.component_small_disk_bound hs hc 1 hR hR1)
115 
116 def diskMajorant (Q : ℝ) : ℕ → ℝ → ℝ
117   | 0, R => R / (1-R^2)
118   | n+1, R => if R < 1 then R / (1-R^2) else R * (1 + diskMajorant Q n (Q*R)^2)
119 
120 theorem diskMajorant_of_small (Q : ℝ) (n : ℕ) {R : ℝ} (hR : R < 1) :
121     diskMajorant Q n R = R / (1-R^2) := by cases n <;> simp [diskMajorant, hR]
122 
123 theorem pair_le_diskMajorant (s : Scales) (hs : s.positive)
124     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (n : ℕ)
125     {R : ℝ} (hR : 0 ≤ R) (ht : s.maxScale^n * R < 1) :
126     s.realPairMax R ≤ diskMajorant s.maxScale n R := by
127   induction n generalizing R with
128   | zero => exact s.pair_small_disk_bound hs hc hR (by simpa using ht)
129   | succ n ih =>
130     by_cases hsmall : R < 1
131     · rw [diskMajorant_of_small _ _ hsmall]
132       exact s.pair_small_disk_bound hs hc hR hsmall
133     · simp only [diskMajorant, ite_eq_right hsmall]
134       have hQR := mul_nonneg (s.maxScale_positive hs).le hR
135       have ht' : s.maxScale^n * (s.maxScale*R) < 1 := by
136         convert ht using 1
137         ring
138       have hh := ih hQR ht'
139       have hp := s.realPairMax_nonneg hs hc hQR
140       exact (s.realPairMax_recurrence hs hc hR).trans
141         (mul_le_mul_of_nonneg_left
142           (add_le_add le_rfl (pow_le_pow_left₀ hp hh 2)) hR)
143 
144 theorem exists_diskMajorant_fuel (s : Scales) (hs : s.positive)
145     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (R : ℝ) :
146     ∃ n : ℕ, s.maxScale^n * R < 1 := by
147   have ht : Tendsto (fun n : ℕ => s.maxScale^n * R) atTop (𝓝 0) := by
148     simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one (s.maxScale_positive hs).le
149       (s.maxScale_lt_one hc)).mul_const R
150   exact (ht.eventually_lt_const (by norm_num : (0 : ℝ) < 1)).exists
151 
152 theorem component_disk_majorant (s : Scales) (hs : s.positive)
153     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
154     {R : ℝ} (hR : 0 ≤ R) (n : ℕ) (ht : s.maxScale^n * R < 1)
155     {z : ℂ} (hz : ‖z‖ ≤ R) : ‖s.complexComponent i z‖ ≤ diskMajorant s.maxScale n R := by
156   have h := s.complex_norm_le_real_axis hs hc hz
157   have hh : ‖s.complexComponent i z‖ ≤ s.realComponent i R := by
158     fin_cases i
159     · exact h.1
160     · exact h.2
161   exact hh.trans ((s.component_le_pairMax i R).trans (s.pair_le_diskMajorant hs hc n hR ht))
162 
163 theorem disk_majorant_exists (s : Scales) (hs : s.positive)
164     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 0 ≤ R) :
165     ∃ n : ℕ, s.maxScale^n * R < 1 ∧ ∀ i : Fin 2, ∀ z : ℂ, ‖z‖ ≤ R →
166       ‖s.complexComponent i z‖ ≤ diskMajorant s.maxScale n R := by
167   obtain ⟨n, hn⟩ := s.exists_diskMajorant_fuel hs hc R
168   exact ⟨n, hn, fun i _ hz => s.component_disk_majorant hs hc i hR n hn hz⟩
169 
170 theorem outer_power_comparison {R S : ℝ} (hR : 0 ≤ R) (hRS : R < S)
171     {k m : ℕ} (hkm : k ≤ m) : R^m ≤ (R/S)^k * S^m := by
172   have hS : 0 < S := hR.trans_lt hRS
173   have hb0 := div_nonneg hR hS.le
174   have hb1 : R/S ≤ 1 := (div_le_one hS).mpr hRS.le
175   have hp := pow_le_pow_of_le_one hb0 hb1 hkm
176   calc
177     _ = ((R/S)*S)^m := by rw [div_mul_cancel₀ _ (ne_of_gt hS)]
178     _ = (R/S)^m * S^m := mul_pow _ _ _
179     _ ≤ _ := mul_le_mul_of_nonneg_right hp (pow_nonneg hS.le _)
180 
181 theorem positive_odd_outer_remainder {c : ℕ → ℝ} (hc : ∀ n, 0 ≤ c n)
182     {z : ℂ} {R S F : ℝ} (hR : 0 ≤ R) (hRS : R < S) (hz : ‖z‖ ≤ R)
183     (hZ : Summable (fun n => (c n : ℂ) * z^(2*n+1)))
184     (hS : HasSum (fun n => c n * S^(2*n+1)) F) (N : ℕ) :
185     ‖oddSum c z - ∑ n ∈ Finset.range (N+1), (c n : ℂ)*z^(2*n+1)‖ ≤
186       F * (R/S)^(2*N+3) := by
187   rw [oddSum_truncation_eq_tail hZ (N+1)]
188   have hS0 : 0 ≤ S := (hR.trans hRS.le)
189   have hfac : 0 ≤ (R/S)^(2*N+3) := pow_nonneg (div_nonneg hR hS0) _
190   have hTS : Summable (fun n => c (n+(N+1)) * S^(2*(n+(N+1))+1)) :=
191     (summable_nat_add_iff (N+1)).mpr hS.summable
192   have hTZ : Summable (fun n => (c (n+(N+1)) : ℂ) * z^(2*(n+(N+1))+1)) :=
193     (summable_nat_add_iff (N+1)).mpr hZ
194   have hterm (n : ℕ) : ‖(c (n+(N+1)) : ℂ) * z^(2*(n+(N+1))+1)‖ ≤
195       (R/S)^(2*N+3) * (c (n+(N+1)) * S^(2*(n+(N+1))+1)) := by
196     rw [norm_mul, Complex.norm_of_nonneg (hc _), norm_pow]
197     calc
198       _ ≤ c (n+(N+1)) * R^(2*(n+(N+1))+1) :=
199         mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (norm_nonneg z) hz _) (hc _)
200       _ ≤ c (n+(N+1)) * ((R/S)^(2*N+3) * S^(2*(n+(N+1))+1)) :=
201         mul_le_mul_of_nonneg_left (outer_power_comparison hR hRS (by omega)) (hc _)
202       _ = _ := by ring
203   have hn := hTZ.hasSum.norm_le_of_bounded (hTS.hasSum.mul_left ((R/S)^(2*N+3))) hterm
204   have hsplit := hS.summable.sum_add_tsum_nat_add (N+1)
205   have hprefix : 0 ≤ ∑ n ∈ Finset.range (N+1), c n * S^(2*n+1) :=
206     Finset.sum_nonneg (fun n _ => mul_nonneg (hc n) (pow_nonneg hS0 _))
207   have ht : (∑' n, c (n+(N+1)) * S^(2*(n+(N+1))+1)) ≤ F := by
208     rw [hS.tsum_eq] at hsplit
209     linarith only [hsplit, hprefix]
210   exact hn.trans (by simpa only [mul_comm] using mul_le_mul_of_nonneg_left ht hfac)
211 
212 def oddPolynomial (s : Scales) (i : Fin 2) (N : ℕ) (z : ℂ) : ℂ :=
213   ∑ n ∈ Finset.range (N+1), (s.componentCoefficient i n : ℂ)*z^(2*n+1)
214 
215 def realOddPolynomial (s : Scales) (i : Fin 2) (N : ℕ) (x : ℝ) : ℝ :=
216   ∑ n ∈ Finset.range (N+1), s.componentCoefficient i n * x^(2*n+1)
217 
218 theorem oddPolynomial_at_real (s : Scales) (i : Fin 2) (N : ℕ) (x : ℝ) :
219     s.oddPolynomial i N (x : ℂ) = (s.realOddPolynomial i N x : ℂ) := by
220   simp only [oddPolynomial, realOddPolynomial, Complex.ofReal_sum, Complex.ofReal_mul,
221     Complex.ofReal_pow]
222 
223 theorem canonical_outer_remainder (s : Scales) (hs : s.positive)
224     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
225     {R S B : ℝ} (hR : 0 ≤ R) (hRS : R < S) (hB : s.realComponent i S ≤ B)
226     (N : ℕ) {z : ℂ} (hz : ‖z‖ ≤ R) :
227     ‖s.complexComponent i z - s.oddPolynomial i N z‖ ≤ B * (R/S)^(2*N+3) := by
228   rw [s.component_oddSum i z]
229   have h := positive_odd_outer_remainder
230     (fun n => (s.component_coefficient_majorant hs hc i n).1) hR hRS hz
231     (s.component_norm_summable hs hc i z).of_norm (s.component_real_hasSum hs hc i S) N
232   exact h.trans (mul_le_mul_of_nonneg_right hB (pow_nonneg (div_nonneg hR (hR.trans hRS.le)) _))
233 
234 theorem canonical_ladder_remainder (s : Scales) (hs : s.positive)
235     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
236     {R S : ℝ} (hR : 0 ≤ R) (hRS : R < S) (fuel : ℕ)
237     (ht : s.maxScale^fuel * S < 1) (N : ℕ) {z : ℂ} (hz : ‖z‖ ≤ R) :
238     ‖s.complexComponent i z - s.oddPolynomial i N z‖ ≤
239       diskMajorant s.maxScale fuel S * (R/S)^(2*N+3) :=
240   s.canonical_outer_remainder hs hc i hR hRS
241     ((s.component_le_pairMax i S).trans (s.pair_le_diskMajorant hs hc fuel (hR.trans hRS.le) ht)) N hz
242 
243 theorem real_polynomial_le_component (s : Scales) (hs : s.positive)
244     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
245     {x : ℝ} (hx : 0 ≤ x) (N : ℕ) : s.realOddPolynomial i N x ≤ s.realComponent i x := by
246   exact sum_le_hasSum (Finset.range (N+1))
247     (fun n _ => mul_nonneg (s.component_coefficient_majorant hs hc i n).1 (pow_nonneg hx _))
248     (s.component_real_hasSum hs hc i x)
249 
250 theorem real_evaluation_enclosure (s : Scales) (hs : s.positive)
251     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
252     {x S B : ℝ} (hx : 0 ≤ x) (hxS : x < S) (hB : s.realComponent i S ≤ B) (N : ℕ) :
253     s.realOddPolynomial i N x ≤ s.realComponent i x ∧
254       s.realComponent i x ≤ s.realOddPolynomial i N x + B*(x/S)^(2*N+3) := by
255   refine ⟨s.real_polynomial_le_component hs hc i hx N, ?_⟩
256   have he := s.canonical_outer_remainder hs hc i hx hxS hB N
257     (z := (x : ℂ)) (by rw [Complex.norm_of_nonneg hx])
258   rw [s.component_at_real hs hc i x, s.oddPolynomial_at_real i N x,
259     ← Complex.ofReal_sub] at he
260   have hh : s.realComponent i x - s.realOddPolynomial i N x ≤ B*(x/S)^(2*N+3) :=
261     (le_abs_self _).trans (by simpa only [Complex.norm_real, Real.norm_eq_abs] using he)
262   linarith only [hh]
263 
264 theorem real_ladder_enclosure (s : Scales) (hs : s.positive)
265     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
266     {x S : ℝ} (hx : 0 ≤ x) (hxS : x < S) (fuel : ℕ)
267     (ht : s.maxScale^fuel * S < 1) (N : ℕ) :
268     s.realOddPolynomial i N x ≤ s.realComponent i x ∧
269       s.realComponent i x ≤ s.realOddPolynomial i N x +
270         diskMajorant s.maxScale fuel S * (x/S)^(2*N+3) :=
271   s.real_evaluation_enclosure hs hc i hx hxS
272     ((s.component_le_pairMax i S).trans (s.pair_le_diskMajorant hs hc fuel (hx.trans hxS.le) ht)) N
273 
274 def rationalDiskMajorant (Q : ℚ) : ℕ → ℚ → ℚ
275   | 0, R => R / (1-R^2)
276   | n+1, R => if R < 1 then R / (1-R^2) else R * (1 + rationalDiskMajorant Q n (Q*R)^2)
277 
278 theorem rationalDiskMajorant_cast (Q : ℚ) (fuel : ℕ) (R : ℚ) :
279     (rationalDiskMajorant Q fuel R : ℝ) = diskMajorant (Q : ℝ) fuel (R : ℝ) := by
280   induction fuel generalizing R with
281   | zero => simp only [rationalDiskMajorant, diskMajorant, Rat.cast_div, Rat.cast_sub,
282       Rat.cast_one, Rat.cast_pow]
283   | succ n ih =>
284     by_cases hR : R < 1
285     · have hRR : (R : ℝ) < 1 := by exact_mod_cast hR
286       simp only [rationalDiskMajorant, diskMajorant, ite_eq_left hR, ite_eq_left hRR,
287         Rat.cast_div, Rat.cast_sub, Rat.cast_one, Rat.cast_pow]
288     · have hRR : ¬(R : ℝ) < 1 := by exact_mod_cast hR
289       simp only [rationalDiskMajorant, diskMajorant, ite_eq_right hR, ite_eq_right hRR,
290         Rat.cast_mul, Rat.cast_add, Rat.cast_one, Rat.cast_pow, ih]
291 
292 theorem rational_disk_majorant_sound (s : Scales) (hs : s.positive)
293     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (Q R : ℚ)
294     (hQ : (Q : ℝ) = s.maxScale) (hR : 0 ≤ R) (fuel : ℕ) (ht : Q^fuel * R < 1)
295     (i : Fin 2) {z : ℂ} (hz : ‖z‖ ≤ (R : ℝ)) :
296     ‖s.complexComponent i z‖ ≤ (rationalDiskMajorant Q fuel R : ℝ) := by
297   rw [rationalDiskMajorant_cast, hQ]
298   exact s.component_disk_majorant hs hc i (by exact_mod_cast hR) fuel
299     (by rw [← hQ]; exact_mod_cast ht) hz
300 
301 theorem rational_outer_remainder (s : Scales) (hs : s.positive)
302     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (Q R S : ℚ)
303     (hQ : (Q : ℝ) = s.maxScale) (hR : 0 ≤ R) (hRS : R < S)
304     (fuel : ℕ) (ht : Q^fuel * S < 1) (N : ℕ) (i : Fin 2)
305     {z : ℂ} (hz : ‖z‖ ≤ (R : ℝ)) :
306     ‖s.complexComponent i z - s.oddPolynomial i N z‖ ≤
307       ((rationalDiskMajorant Q fuel S * (R/S)^(2*N+3) : ℚ) : ℝ) := by
308   have h := s.canonical_ladder_remainder hs hc i
309     (by exact_mod_cast hR : (0 : ℝ) ≤ R) (by exact_mod_cast hRS : (R : ℝ) < S)
310     fuel (by rw [← hQ]; exact_mod_cast ht) N hz
311   simpa only [Rat.cast_mul, Rat.cast_pow, Rat.cast_div, rationalDiskMajorant_cast, hQ] using h
312 
313 theorem rational_real_enclosure (s : Scales) (hs : s.positive)
314     (hc : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (Q x S : ℚ)
315     (hQ : (Q : ℝ) = s.maxScale) (hx : 0 ≤ x) (hxS : x < S)
316     (fuel : ℕ) (ht : Q^fuel * S < 1) (N : ℕ) (i : Fin 2) :
317     s.realOddPolynomial i N (x : ℝ) ≤ s.realComponent i (x : ℝ) ∧
318       s.realComponent i (x : ℝ) ≤ s.realOddPolynomial i N (x : ℝ) +
319         ((rationalDiskMajorant Q fuel S * (x/S)^(2*N+3) : ℚ) : ℝ) := by
320   have h := s.real_ladder_enclosure hs hc i
321     (by exact_mod_cast hx : (0 : ℝ) ≤ x) (by exact_mod_cast hxS : (x : ℝ) < S)
322     fuel (by rw [← hQ]; exact_mod_cast ht) N
323   simpa only [Rat.cast_mul, Rat.cast_pow, Rat.cast_div, rationalDiskMajorant_cast, hQ] using h
324 
325 structure RationalScales where
326   q : ℚ
327   r : ℚ
328   a : ℚ
329   b : ℚ
330 
331 def RationalScales.toReal (p : RationalScales) : Scales := ⟨p.q, p.r, p.a, p.b⟩
332 
333 def RationalScales.coefficients (p : RationalScales) : ℕ → ℚ × ℚ
334   | 0 => (1, 1)
335   | n+1 =>
336     ((∑ i : Fin (n+1), p.q^(2*i.val+1) * p.r^(2*(n-i.val)+1) *
337       (p.coefficients i.val).1 * (p.coefficients (n-i.val)).2) / (2*(n : ℚ)+3),
338      (∑ i : Fin (n+1), p.a^(2*i.val+1) * p.b^(2*(n-i.val)+1) *
339       (p.coefficients i.val).1 * (p.coefficients (n-i.val)).2) / (2*(n : ℚ)+3))
340 termination_by n => n
341 decreasing_by all_goals omega
342 
343 theorem rational_coefficients_cast (p : RationalScales) (n : ℕ) :
344     (((p.coefficients n).1 : ℝ), ((p.coefficients n).2 : ℝ)) = p.toReal.coefficients n := by
345   have hsol : p.toReal.IsCoefficientSolution
346       (fun k => (((p.coefficients k).1 : ℝ), ((p.coefficients k).2 : ℝ))) := by
347     constructor
348     · change (((p.coefficients 0).1 : ℝ), ((p.coefficients 0).2 : ℝ)) = (1,1)
349       have hz : p.coefficients 0 = (1,1) := by rw [RationalScales.coefficients.eq_def]
350       rw [hz]
351       norm_num
352     · intro k
353       change (((p.coefficients (k+1)).1 : ℝ), ((p.coefficients (k+1)).2 : ℝ)) = _
354       have hk : p.coefficients (k+1) =
355           ((∑ i : Fin (k+1), p.q^(2*i.val+1) * p.r^(2*(k-i.val)+1) *
356             (p.coefficients i.val).1 * (p.coefficients (k-i.val)).2) / (2*(k : ℚ)+3),
357            (∑ i : Fin (k+1), p.a^(2*i.val+1) * p.b^(2*(k-i.val)+1) *
358             (p.coefficients i.val).1 * (p.coefficients (k-i.val)).2) / (2*(k : ℚ)+3)) := by
359         rw [RationalScales.coefficients.eq_def]
360       rw [hk]
361       simp only [nextCoefficient, RationalScales.toReal, Rat.cast_div, Rat.cast_sum,
362         Rat.cast_mul, Rat.cast_pow, Rat.cast_add, Rat.cast_ofNat, Rat.cast_natCast]
363   exact congrFun (coefficient_solution_unique hsol p.toReal.coefficients_solution) n
364 
365 def RationalScales.componentCoefficient (p : RationalScales) (i : Fin 2) (n : ℕ) : ℚ :=
366   ![(p.coefficients n).1, (p.coefficients n).2] i
367 
368 theorem rational_component_coefficient_cast (p : RationalScales) (i : Fin 2) (n : ℕ) :
369     (p.componentCoefficient i n : ℝ) = p.toReal.componentCoefficient i n := by
370   have h := rational_coefficients_cast p n
371   fin_cases i
372   · exact congrArg Prod.fst h
373   · exact congrArg Prod.snd h
374 
375 def RationalScales.polynomial (p : RationalScales) (i : Fin 2) (N : ℕ) (x : ℚ) : ℚ :=
376   ∑ n ∈ Finset.range (N+1), p.componentCoefficient i n * x^(2*n+1)
377 
378 theorem rational_polynomial_cast (p : RationalScales) (i : Fin 2) (N : ℕ) (x : ℚ) :
379     (p.polynomial i N x : ℝ) = p.toReal.realOddPolynomial i N (x : ℝ) := by
380   simp only [RationalScales.polynomial, realOddPolynomial, Rat.cast_sum, Rat.cast_mul,
381     Rat.cast_pow, rational_component_coefficient_cast]
382 
383 def RationalScales.maxScale (p : RationalScales) : ℚ := max (max p.q p.r) (max p.a p.b)
384 
385 theorem rational_maxScale_cast (p : RationalScales) :
386     (p.maxScale : ℝ) = p.toReal.maxScale := by
387   simp only [RationalScales.maxScale, maxScale, RationalScales.toReal, Rat.cast_max]
388 
389 theorem rational_fuel_exists (p : RationalScales) (hs : p.toReal.positive)
390     (hc : p.toReal.q < 1 ∧ p.toReal.r < 1 ∧ p.toReal.a < 1 ∧ p.toReal.b < 1) (S : ℚ) :
391     ∃ fuel : ℕ, p.maxScale^fuel * S < 1 := by
392   obtain ⟨fuel, hf⟩ := p.toReal.exists_diskMajorant_fuel hs hc (S : ℝ)
393   refine ⟨fuel, ?_⟩
394   rw [← rational_maxScale_cast p] at hf
395   exact_mod_cast hf
396 
397 theorem rational_endpoint_enclosure (p : RationalScales) (hs : p.toReal.positive)
398     (hc : p.toReal.q < 1 ∧ p.toReal.r < 1 ∧ p.toReal.a < 1 ∧ p.toReal.b < 1)
399     (x S : ℚ) (hx : 0 ≤ x) (hxS : x < S) (fuel : ℕ) (ht : p.maxScale^fuel*S < 1)
400     (N : ℕ) (i : Fin 2) :
401     (p.polynomial i N x : ℝ) ≤ p.toReal.realComponent i (x : ℝ) ∧
402       p.toReal.realComponent i (x : ℝ) ≤
403         ((p.polynomial i N x + rationalDiskMajorant p.maxScale fuel S *
404           (x/S)^(2*N+3) : ℚ) : ℝ) := by
405   have h := p.toReal.rational_real_enclosure hs hc p.maxScale x S
406     (rational_maxScale_cast p) hx hxS fuel ht N i
407   simpa only [Rat.cast_add, rational_polynomial_cast] using h
408 
409 theorem unequal_last_thirty_tail_rational :
410     rationalDiskMajorant (7/10) 2 2 * (1/2 : ℚ)^63 < 16/100000000000000 := by
411   norm_num [rationalDiskMajorant]
412 
413 theorem unequal_last_thirty_error (i : Fin 2) (z : ℂ) (hz : ‖z‖ ≤ 1) :
414     ‖unequalScales.complexComponent i z - unequalScales.oddPolynomial i 30 z‖ <
415       (16/100000000000000 : ℝ) := by
416   have he := unequalScales.rational_outer_remainder unequalScales_positive unequalScales_strict
417     (7/10) 1 2 (by norm_num [maxScale, unequalScales]) (by norm_num) (by norm_num)
418     2 (by norm_num) 30 i (by simpa using hz)
419   have hb : ((rationalDiskMajorant (7/10) 2 2 * (1/2 : ℚ)^63 : ℚ) : ℝ) <
420       (16/100000000000000 : ℝ) := by
421     have h := (Rat.cast_lt (K := ℝ)).mpr unequal_last_thirty_tail_rational
422     norm_num only [Rat.cast_div, Rat.cast_ofNat] at h ⊢
423     exact h
424   exact he.trans_lt (by simpa using hb)
425 
426 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls