CoupledScalarReduction.lean

1 import CoupledTypeProportions
2 import Mathlib.Analysis.Complex.Trigonometric
3 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
4 
5 /-! # Exact scalar reduction and explicit symmetric coupled functions -/
6 
7 set_option autoImplicit false
8 set_option maxHeartbeats 2000000
9 
10 noncomputable section
11 open Filter Set
12 open scoped Topology Matrix
13 
14 namespace Komorebi.SpecialFunctions.Coupled.Scales
15 
16 def sameUnorderedRows (s : Scales) : Prop :=
17   (s.q = s.a ∧ s.r = s.b) ∨ (s.q = s.b ∧ s.r = s.a)
18 
19 theorem positive_pair_from_product_and_square_sum {q r a b : ℝ}
20     (hq : 0 < q) (hr : 0 < r) (ha : 0 < a) (hb : 0 < b)
21     (hp : q * r = a * b) (hsq : q ^ 2 + r ^ 2 = a ^ 2 + b ^ 2) :
22     (q = a ∧ r = b) ∨ (q = b ∧ r = a) := by
23   have hf : (q + r - (a + b)) * (q + r + (a + b)) = 0 := by
24     nlinarith only [hp, hsq]
25   have hsum : q + r = a + b := sub_eq_zero.mp
26     ((mul_eq_zero.mp hf).resolve_right (ne_of_gt (by linarith only [hq, hr, ha, hb])))
27   have hmul := congrArg (fun t : ℝ => q * t) hsum
28   have hfactor : (q - a) * (q - b) = 0 := by nlinarith only [hp, hmul]
29   rcases mul_eq_zero.mp hfactor with h | h
30   · left
31     have hqa := sub_eq_zero.mp h
32     exact ⟨hqa, by linarith only [hsum, hqa]⟩
33   · right
34     have hqb := sub_eq_zero.mp h
35     exact ⟨hqb, by linarith only [hsum, hqb]⟩
36 
37 theorem equal_components_coefficients (s : Scales) (hs : s.positive)
38     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
39     (he : s.U = s.V) (n : ℕ) : (s.coefficients n).1 = (s.coefficients n).2 := by
40   have h := s.rescaling_coefficient_identity hs hstrict
41     (A := (1 : ℂ)) (B := (1 : ℂ)) (by intro z; simpa using congrFun he.symm z) n
42   have hh : ((s.coefficients n).2 : ℂ) = ((s.coefficients n).1 : ℂ) := by simpa using h
43   exact (Complex.ofReal_inj.mp hh).symm
44 
45 theorem equal_components_product (s : Scales) (hs : s.positive)
46     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (he : s.U = s.V) :
47     s.p = s.k := by
48   have h := s.equal_components_coefficients hs hstrict he 1
49   simp only [coefficients_one, u1, v1] at h
50   linarith only [h]
51 
52 theorem equal_components_square_sum (s : Scales) (hs : s.positive)
53     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (he : s.U = s.V) :
54     s.q ^ 2 + s.r ^ 2 = s.a ^ 2 + s.b ^ 2 := by
55   have hp : 0 < s.p := mul_pos hs.1 hs.2.1
56   have hpk := s.equal_components_product hs hstrict he
57   have h := s.equal_components_coefficients hs hstrict he 2
58   simp only [coefficients_two, u2, v2, ← hpk] at h
59   have hh : s.p * (s.p * (s.q ^ 2 + s.r ^ 2)) =
60       s.p * (s.p * (s.a ^ 2 + s.b ^ 2)) := by nlinarith only [h]
61   exact mul_left_cancel₀ (ne_of_gt hp) (mul_left_cancel₀ (ne_of_gt hp) hh)
62 
63 theorem equal_components_unordered_rows (s : Scales) (hs : s.positive)
64     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (he : s.U = s.V) :
65     s.sameUnorderedRows :=
66   positive_pair_from_product_and_square_sum hs.1 hs.2.1 hs.2.2.1 hs.2.2.2
67     (s.equal_components_product hs hstrict he) (s.equal_components_square_sum hs hstrict he)
68 
69 theorem scalar_pair_solution (s : Scales) (hs : s.positive)
70     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (hrows : s.sameUnorderedRows) :
71     s.IsEntireSolution (scalarT s.q s.r) (scalarT s.q s.r) := by
72   have hT := scalarT_solution hs.1 hs.2.1 hstrict.1 hstrict.2.1
73   refine ⟨hT.1, hT.1, fun z => ⟨hT.2 z, ?_⟩⟩
74   rcases hrows with h | h
75   · simpa only [← h.1, ← h.2] using hT.2 z
76   · simpa only [← h.1, ← h.2, mul_comm] using hT.2 z
77 
78 theorem unordered_rows_scalar_representation (s : Scales) (hs : s.positive)
79     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (hrows : s.sameUnorderedRows) :
80     s.U = scalarT s.q s.r ∧ s.V = scalarT s.q s.r := by
81   have he := s.entire_solution_eq hs hstrict (s.scalar_pair_solution hs hstrict hrows)
82   exact ⟨he.1.symm, he.2.symm⟩
83 
84 theorem components_equal_iff_unordered_rows (s : Scales) (hs : s.positive)
85     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
86     s.U = s.V ↔ s.sameUnorderedRows := by
87   refine ⟨s.equal_components_unordered_rows hs hstrict, ?_⟩
88   intro hrows
89   have he := s.unordered_rows_scalar_representation hs hstrict hrows
90   exact he.1.trans he.2.symm
91 
92 theorem components_equal_iff_scale_pair_set (s : Scales) (hs : s.positive)
93     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
94     s.U = s.V ↔ ({s.q, s.r} : Set ℝ) = {s.a, s.b} := by
95   rw [s.components_equal_iff_unordered_rows hs hstrict, Set.pair_eq_pair_iff]
96   rfl
97 
98 theorem characteristicExponent_eq_of_balance (s : Scales) (hs : s.positive)
99     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {t : ℝ} (ht : 0 < t)
100     (he : (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t) :
101     s.characteristicExponent hs hstrict = t :=
102   ((Classical.choose_spec (s.characteristic_exponent_exists_unique hs hstrict)).2 t ⟨ht, he⟩).symm
103 
104 theorem scalar_characteristic_balance_iff (s : Scales) (hs : s.positive)
105     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (hrows : s.sameUnorderedRows)
106     {t : ℝ} (ht : 0 < t) :
107     (1 - s.q ^ t) * (1 - s.b ^ t) = (s.a * s.r) ^ t ↔ s.q ^ t + s.r ^ t = 1 := by
108   rw [Real.mul_rpow hs.2.2.1.le hs.2.1.le]
109   rcases hrows with h | h
110   · rw [← h.1, ← h.2]
111     constructor <;> intro he <;> nlinarith only [he]
112   · rw [← h.1, ← h.2]
113     have hq := (rpow_contraction_bounds hs.1 hstrict.1 ht).2
114     have hr := Real.rpow_pos_of_pos hs.2.1 t
115     constructor
116     · intro he
117       have hh : (1 - s.q ^ t - s.r ^ t) * (1 - s.q ^ t + s.r ^ t) = 0 := by
118         nlinarith only [he]
119       have hz := (mul_eq_zero.mp hh).resolve_right (ne_of_gt (by linarith only [hq, hr]))
120       linarith only [hz]
121     · intro he
122       have hh : 1 - s.q ^ t = s.r ^ t := by linarith only [he]
123       rw [hh]
124 
125 theorem scalar_characteristic_order (s : Scales) (hs : s.positive)
126     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (hrows : s.sameUnorderedRows) :
127     s.q ^ (s.characteristicExponent hs hstrict) +
128       s.r ^ (s.characteristicExponent hs hstrict) = 1 :=
129   (s.scalar_characteristic_balance_iff hs hstrict hrows
130     (s.characteristicExponent_spec hs hstrict).1).mp
131       (s.characteristicExponent_spec hs hstrict).2
132 
133 theorem characteristic_order_invariant (s v : Scales) (hs : s.positive) (hv : v.positive)
134     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1)
135     (vstrict : v.q < 1 ∧ v.r < 1 ∧ v.a < 1 ∧ v.b < 1)
136     (hq : s.q = v.q) (hb : s.b = v.b) (hcross : s.a * s.r = v.a * v.r) :
137     s.characteristicExponent hs hstrict = v.characteristicExponent hv vstrict := by
138   have he := v.characteristicExponent_spec hv vstrict
139   apply s.characteristicExponent_eq_of_balance hs hstrict he.1
140   rw [hq, hb, hcross]
141   exact he.2
142 
143 theorem complex_sinh_hasDerivAt (z : ℂ) : HasDerivAt Complex.sinh (Complex.cosh z) z := by
144   simp only [Complex.cosh, div_eq_mul_inv]
145   convert!
146     ((Complex.hasDerivAt_exp z).sub (hasDerivAt_id z).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
147   rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]
148 
149 theorem sinh_half_derivative_identity {c : ℂ} (hc : c ^ 2 = 2) (z : ℂ) :
150     Complex.cosh (c⁻¹ * z) =
151       1 + (c * Complex.sinh (c⁻¹ * ((1 / 2 : ℂ) * z))) *
152         (c * Complex.sinh (c⁻¹ * ((1 / 2 : ℂ) * z))) := by
153   let x := c⁻¹ * ((1 / 2 : ℂ) * z)
154   have hx : 2 * x = c⁻¹ * z := by dsimp [x]; ring
155   change Complex.cosh (c⁻¹ * z) = 1 + (c * Complex.sinh x) * (c * Complex.sinh x)
156   calc
157     _ = Complex.cosh x ^ 2 + Complex.sinh x ^ 2 := by rw [← hx, Complex.cosh_two_mul]
158     _ = 1 + 2 * Complex.sinh x ^ 2 := by
159       linear_combination Complex.cosh_sq_sub_sinh_sq x
160     _ = 1 + (c * Complex.sinh x) * (c * Complex.sinh x) := by
161       linear_combination -(Complex.sinh x ^ 2) * hc
162 
163 theorem scaled_sinh_half_equation {c : ℂ} (hc : c ^ 2 = 2) (z : ℂ) :
164     HasDerivAt (fun z : ℂ => c * Complex.sinh (c⁻¹ * z))
165       (1 + (c * Complex.sinh (c⁻¹ * ((1 / 2 : ℂ) * z))) *
166         (c * Complex.sinh (c⁻¹ * ((1 / 2 : ℂ) * z)))) z := by
167   have hc0 : c ≠ 0 := by intro hz; simp [hz] at hc
168   have hd := ((complex_sinh_hasDerivAt (c⁻¹ * z)).comp z
169     ((hasDerivAt_id z).const_mul c⁻¹)).const_mul c
170   convert! hd using 1
171   rw [← sinh_half_derivative_identity hc z]
172   field_simp [hc0]
173 
174 def halfScales : Scales := ⟨1 / 2, 1 / 2, 1 / 2, 1 / 2⟩
175 
176 theorem halfScales_positive : halfScales.positive := by norm_num [positive, halfScales]
177 
178 theorem halfScales_strict :
179     halfScales.q < 1 ∧ halfScales.r < 1 ∧ halfScales.a < 1 ∧ halfScales.b < 1 := by
180   norm_num [halfScales]
181 
182 theorem scaled_sinh_half_solution {c : ℂ} (hc : c ^ 2 = 2) :
183     halfScales.IsEntireSolution (fun z : ℂ => c * Complex.sinh (c⁻¹ * z))
184       (fun z : ℂ => c * Complex.sinh (c⁻¹ * z)) := by
185   refine ⟨by simp, by simp, fun z => ?_⟩
186   have hh := scaled_sinh_half_equation hc z
187   exact ⟨by simpa [halfScales] using hh, by simpa [halfScales] using hh⟩
188 
189 theorem sqrt_two_complex_square : ((Real.sqrt 2 : ℝ) : ℂ) ^ 2 = 2 := by
190   exact_mod_cast Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)
191 
192 theorem canonical_half_sinh (z : ℂ) :
193     halfScales.U z = (Real.sqrt 2 : ℂ) * Complex.sinh (z / (Real.sqrt 2 : ℂ)) ∧
194     halfScales.V z = (Real.sqrt 2 : ℂ) * Complex.sinh (z / (Real.sqrt 2 : ℂ)) := by
195   have he := halfScales.entire_solution_eq halfScales_positive halfScales_strict
196     (scaled_sinh_half_solution sqrt_two_complex_square)
197   exact ⟨by simpa only [div_eq_inv_mul] using congrFun he.1.symm z,
198     by simpa only [div_eq_inv_mul] using congrFun he.2.symm z⟩
199 
200 theorem half_characteristic_order :
201     halfScales.characteristicExponent halfScales_positive halfScales_strict = 1 := by
202   apply halfScales.characteristicExponent_eq_of_balance halfScales_positive halfScales_strict
203     (by norm_num : (0 : ℝ) < 1)
204   norm_num [halfScales]
205 
206 theorem half_radial_order (i : Fin 2) : halfScales.radialOrder i = 1 := by
207   rw [halfScales.canonical_radial_order halfScales_positive halfScales_strict, half_characteristic_order]
208 
209 def unequalScales : Scales := ⟨1 / 5, 2 / 5, 3 / 5, 7 / 10⟩
210 
211 theorem unequalScales_positive : unequalScales.positive := by norm_num [positive, unequalScales]
212 
213 theorem unequalScales_strict :
214     unequalScales.q < 1 ∧ unequalScales.r < 1 ∧ unequalScales.a < 1 ∧ unequalScales.b < 1 := by
215   norm_num [unequalScales]
216 
217 theorem unequal_characteristic_order :
218     unequalScales.characteristicExponent unequalScales_positive unequalScales_strict = 1 := by
219   apply unequalScales.characteristicExponent_eq_of_balance unequalScales_positive unequalScales_strict
220     (by norm_num : (0 : ℝ) < 1)
221   norm_num [unequalScales]
222 
223 theorem unequal_radial_order (i : Fin 2) : unequalScales.radialOrder i = 1 := by
224   rw [unequalScales.canonical_radial_order unequalScales_positive unequalScales_strict,
225     unequal_characteristic_order]
226 
227 theorem unequal_normalized_vector :
228     unequalScales.normalizedCharacteristicVector
229       (unequalScales.characteristicExponent unequalScales_positive unequalScales_strict) = ![1 / 2, 1] := by
230   rw [unequal_characteristic_order]
231   funext i
232   fin_cases i <;> norm_num [normalizedCharacteristicVector, characteristicNormalizer,
233     characteristicVector, unequalScales]
234 
235 theorem unequal_type_proportions :
236     unequalScales.lowerType unequalScales_positive unequalScales_strict 1 =
237       2 * unequalScales.lowerType unequalScales_positive unequalScales_strict 0 ∧
238     unequalScales.upperType unequalScales_positive unequalScales_strict 1 =
239       2 * unequalScales.upperType unequalScales_positive unequalScales_strict 0 := by
240   have hh := unequalScales.canonical_type_proportions unequalScales_positive unequalScales_strict
241   rw [unequal_normalized_vector] at hh
242   have hl0 := congrFun hh.2.2.1 0
243   have hl1 := congrFun hh.2.2.1 1
244   have hu0 := congrFun hh.2.2.2 0
245   have hu1 := congrFun hh.2.2.2 1
246   simp only [Pi.smul_apply, smul_eq_mul, Matrix.cons_val_zero, Matrix.cons_val_one,
247     Matrix.cons_val_fin_one, mul_one] at hl0 hl1 hu0 hu1
248   constructor <;> linarith only [hl0, hl1, hu0, hu1]
249 
250 theorem unequal_components_different : unequalScales.U ≠ unequalScales.V := by
251   intro he
252   have hh := (unequalScales.components_equal_iff_unordered_rows
253     unequalScales_positive unequalScales_strict).mp he
254   norm_num [sameUnorderedRows, unequalScales] at hh
255 
256 theorem unequal_coefficients_through_seven :
257     unequalScales.coefficients 0 = (1, 1) ∧
258     unequalScales.coefficients 1 = (2 / 75, 7 / 50) ∧
259     unequalScales.coefficients 2 = (88 / 234375, 8211 / 1250000) ∧
260     unequalScales.coefficients 3 = (18814 / 8544921875, 85664601 / 625000000000) := by
261   norm_num [coefficients_zero, coefficients_one, coefficients_two, coefficients_three,
262     u1, v1, u2, v2, u3, v3, p, k, unequalScales]
263 
264 theorem unequal_row_sums :
265     unequalScales.q + unequalScales.r = 3 / 5 ∧
266     unequalScales.a + unequalScales.b = 13 / 10 ∧
267     (unequalScales.q + unequalScales.r + unequalScales.a + unequalScales.b) / 2 = 19 / 20 := by
268   norm_num [unequalScales]
269 
270 theorem unequal_lower_constants :
271     unequalScales.minScale = 1 / 5 ∧ unequalScales.maxScale = 7 / 10 ∧
272     unequalScales.lowerThreshold = 11 ∧ unequalScales.lowerShift = 7 / 3 ∧
273     unequalScales.lowerPowerConstant 1 = 3 * Real.log 2 / 40 := by
274   norm_num [minScale, maxScale, lowerThreshold, lowerShift, lowerPowerConstant, unequalScales]
275   ring
276 
277 theorem unequal_explicit_lower_growth {R : ℝ} (hR : 2 ≤ R) :
278     3 * Real.log 2 / 80 * (R + 7 / 3) ≤ Real.log (unequalScales.UReal R) ∧
279     3 * Real.log 2 / 40 * (R + 7 / 3) ≤ Real.log (unequalScales.VReal R) := by
280   have hh := unequalScales.canonical_lower_log_power unequalScales_positive unequalScales_strict hR
281   change unequalScales.lowerPowerConstant _ * _ * _ ≤ _ ∧
282     unequalScales.lowerPowerConstant _ * _ * _ ≤ _ at hh
283   rw [unequal_normalized_vector, unequal_characteristic_order] at hh
284   rw [unequal_lower_constants.2.2.2.1, unequal_lower_constants.2.2.2.2] at hh
285   norm_num at hh
286   ring_nf at hh ⊢
287   exact hh
288 
289 def surfaceCrossScale (q r b t : ℝ) : ℝ :=
290   ((1 - q ^ t) * (1 - b ^ t)) ^ (1 / t) / r
291 
292 theorem surface_cross_scale_contract {q r b t : ℝ}
293     (hq : 0 < q) (hr : 0 < r) (hb : 0 < b) (hq1 : q < 1) (hb1 : b < 1)
294     (ht : 0 < t) (hbudget : (1 - q ^ t) * (1 - b ^ t) < r ^ t) :
295     0 < surfaceCrossScale q r b t ∧ surfaceCrossScale q r b t < 1 ∧
296       (surfaceCrossScale q r b t * r) ^ t = (1 - q ^ t) * (1 - b ^ t) := by
297   let d := (1 - q ^ t) * (1 - b ^ t)
298   have hd : 0 < d := mul_pos (sub_pos.mpr (rpow_contraction_bounds hq hq1 ht).2)
299     (sub_pos.mpr (rpow_contraction_bounds hb hb1 ht).2)
300   have hroot : 0 < d ^ (1 / t) := Real.rpow_pos_of_pos hd _
301   have hlt := Real.rpow_lt_rpow hd.le hbudget (one_div_pos.mpr ht)
302   rw [one_div, Real.rpow_rpow_inv hr.le (ne_of_gt ht)] at hlt
303   have hcancel : (d ^ (1 / t)) ^ t = d := by
304     rw [one_div, Real.rpow_inv_rpow hd.le (ne_of_gt ht)]
305   refine ⟨div_pos hroot hr, ?_, ?_⟩
306   · change d ^ (1 / t) / r < 1
307     exact (div_lt_one hr).mpr (by simpa only [one_div] using hlt)
308   · change (d ^ (1 / t) / r * r) ^ t = d
309     rw [div_mul_cancel₀ _ (ne_of_gt hr)]
310     exact hcancel
311 
312 def orderSurfaceScales (q r b t : ℝ) : Scales := ⟨q, r, surfaceCrossScale q r b t, b⟩
313 
314 theorem order_surface_realization {q r b t : ℝ}
315     (hq : 0 < q) (hr : 0 < r) (hb : 0 < b)
316     (hq1 : q < 1) (hr1 : r < 1) (hb1 : b < 1) (ht : 0 < t)
317     (hbudget : (1 - q ^ t) * (1 - b ^ t) < r ^ t) :
318     ∃ hs : (orderSurfaceScales q r b t).positive,
319       ∃ hc : (orderSurfaceScales q r b t).q < 1 ∧ (orderSurfaceScales q r b t).r < 1 ∧
320         (orderSurfaceScales q r b t).a < 1 ∧ (orderSurfaceScales q r b t).b < 1,
321       (orderSurfaceScales q r b t).characteristicExponent hs hc = t ∧
322         ∀ i : Fin 2, (orderSurfaceScales q r b t).radialOrder i = t := by
323   have ha := surface_cross_scale_contract hq hr hb hq1 hb1 ht hbudget
324   have hs : (orderSurfaceScales q r b t).positive := ⟨hq, hr, ha.1, hb⟩
325   have hc : (orderSurfaceScales q r b t).q < 1 ∧ (orderSurfaceScales q r b t).r < 1 ∧
326       (orderSurfaceScales q r b t).a < 1 ∧ (orderSurfaceScales q r b t).b < 1 :=
327     ⟨hq1, hr1, ha.2.1, hb1⟩
328   have he : (orderSurfaceScales q r b t).characteristicExponent hs hc = t :=
329     (orderSurfaceScales q r b t).characteristicExponent_eq_of_balance hs hc ht ha.2.2.symm
330   refine ⟨hs, hc, he, fun i => ?_⟩
331   rw [(orderSurfaceScales q r b t).canonical_radial_order hs hc, he]
332 
333 def componentCoefficient (s : Scales) (i : Fin 2) (n : ℕ) : ℝ :=
334   ![(s.coefficients n).1, (s.coefficients n).2] i
335 
336 theorem component_oddSum (s : Scales) (i : Fin 2) (z : ℂ) :
337     s.complexComponent i z = oddSum (s.componentCoefficient i) z := by
338   fin_cases i <;> rfl
339 
340 theorem component_coefficient_majorant (s : Scales) (hs : s.positive)
341     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2) (n : ℕ) :
342     0 ≤ s.componentCoefficient i n ∧ s.componentCoefficient i n ≤ (1 / 2 : ℝ) ^ n := by
343   have hp := s.coefficients_positive hs n
344   have hb := s.coefficients_le_geometric hs
345     ⟨hstrict.1.le, hstrict.2.1.le, hstrict.2.2.1.le, hstrict.2.2.2.le⟩ n
346   fin_cases i
347   · exact ⟨hp.1.le, hb.1⟩
348   · exact ⟨hp.2.le, hb.2⟩
349 
350 theorem oddSum_truncation_eq_tail {c : ℕ → ℝ} {z : ℂ}
351     (hc : Summable (fun n => (c n : ℂ) * z ^ (2 * n + 1))) (N : ℕ) :
352     oddSum c z - ∑ n ∈ Finset.range N, (c n : ℂ) * z ^ (2 * n + 1) =
353       ∑' n, (c (n + N) : ℂ) * z ^ (2 * (n + N) + 1) := by
354   have hh := hc.sum_add_tsum_nat_add N
355   dsimp [oddSum]
356   rw [← hh]
357   ring
358 
359 theorem canonical_complex_truncation_bound (s : Scales) (hs : s.positive)
360     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
361     (z : ℂ) (hz : ‖z‖ ^ 2 < 2) (N : ℕ) :
362     ‖s.complexComponent i z -
363       ∑ n ∈ Finset.range N, (s.componentCoefficient i n : ℂ) * z ^ (2 * n + 1)‖ ≤
364         ‖z‖ * (‖z‖ ^ 2 / 2) ^ N / (1 - ‖z‖ ^ 2 / 2) := by
365   have hc := s.component_coefficient_majorant hs hstrict i
366   have hsum := odd_series_summable hc z hz
367   rw [s.component_oddSum i z, oddSum_truncation_eq_tail hsum N]
368   exact odd_series_tail_bound hc z hz N
369 
370 theorem canonical_four_term_remainder (s : Scales) (hs : s.positive)
371     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (i : Fin 2)
372     (z : ℂ) (hz : ‖z‖ ≤ 1) :
373     ‖s.complexComponent i z -
374       ∑ n ∈ Finset.range 4, (s.componentCoefficient i n : ℂ) * z ^ (2 * n + 1)‖ ≤
375         ‖z‖ ^ 9 / 8 := by
376   have hn := norm_nonneg z
377   have hsq : ‖z‖ ^ 2 ≤ 1 := by nlinarith only [hn, hz]
378   have hh := s.canonical_complex_truncation_bound hs hstrict i z (by linarith only [hsq]) 4
379   apply hh.trans
380   have hd : 0 < 1 - ‖z‖ ^ 2 / 2 := by linarith only [hsq]
381   apply (div_le_iff₀ hd).mpr
382   have hbound : 0 ≤ ‖z‖ ^ 9 * (1 - ‖z‖ ^ 2) :=
383     mul_nonneg (pow_nonneg hn _) (sub_nonneg.mpr hsq)
384   nlinarith only [hbound]
385 
386 theorem unequal_degree_seven_polynomials (z : ℂ) :
387     (∑ n ∈ Finset.range 4, (unequalScales.componentCoefficient 0 n : ℂ) * z ^ (2 * n + 1)) =
388       z + (2 / 75 : ℂ) * z ^ 3 + (88 / 234375 : ℂ) * z ^ 5 +
389         (18814 / 8544921875 : ℂ) * z ^ 7 ∧
390     (∑ n ∈ Finset.range 4, (unequalScales.componentCoefficient 1 n : ℂ) * z ^ (2 * n + 1)) =
391       z + (7 / 50 : ℂ) * z ^ 3 + (8211 / 1250000 : ℂ) * z ^ 5 +
392         (85664601 / 625000000000 : ℂ) * z ^ 7 := by
393   constructor <;>
394     norm_num [Finset.sum_range_succ, componentCoefficient, coefficients_zero, coefficients_one,
395       coefficients_two, coefficients_three, u1, v1, u2, v2, u3, v3, p, k, unequalScales]
396 
397 theorem unequal_degree_seven_error (z : ℂ) (hz : ‖z‖ ≤ 1) :
398     ‖unequalScales.U z - (z + (2 / 75 : ℂ) * z ^ 3 + (88 / 234375 : ℂ) * z ^ 5 +
399       (18814 / 8544921875 : ℂ) * z ^ 7)‖ ≤ ‖z‖ ^ 9 / 8 ∧
400     ‖unequalScales.V z - (z + (7 / 50 : ℂ) * z ^ 3 + (8211 / 1250000 : ℂ) * z ^ 5 +
401       (85664601 / 625000000000 : ℂ) * z ^ 7)‖ ≤ ‖z‖ ^ 9 / 8 := by
402   have h0 := unequalScales.canonical_four_term_remainder unequalScales_positive unequalScales_strict 0 z hz
403   have h1 := unequalScales.canonical_four_term_remainder unequalScales_positive unequalScales_strict 1 z hz
404   rw [(unequal_degree_seven_polynomials z).1] at h0
405   rw [(unequal_degree_seven_polynomials z).2] at h1
406   exact ⟨h0, h1⟩
407 
408 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls