Mathlib.Analysis.Jackson­Approximation

@[fun_prop] theorem continuous_jraw (K : ℕ) : Continuous (jraw K) := by by_cases hK : K = 0 · subst K convert (continuous_const : Continuous (fun _ : ℝ => (0 : ℝ))) using 1 funext t simp [jraw] · have hKpos : 0 < K := Nat.pos_of_ne_zero hK rw [show jraw K = fun t => ((Polynomial.Chebyshev.U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2))) ^ 4 by funext t exact jraw_eq_chebyshev K hKpos t] fun_prop

theorem jraw_even (K : ℕ) : Even (jraw K) := by intro t by_cases ht : sin (t / 2) = 0 · have hnt : sin (-t / 2) = 0 := by rw [show -t / 2 = -(t / 2) by ring, Real.sin_neg, ht, neg_zero] rw [jraw_eq_of_sin_eq_zero K hnt, jraw_eq_of_sin_eq_zero K ht] · have hnt : sin (-t / 2) ≠ 0 := by rw [show -t / 2 = -(t / 2) by ring, Real.sin_neg, neg_ne_zero] exact ht rw [jraw_eq_of_sin_ne_zero K hnt, jraw_eq_of_sin_ne_zero K ht] rw [show (K : ℝ) * -t / 2 = -((K : ℝ) * t / 2) by ring, show -t / 2 = -(t / 2) by ring, Real.sin_neg] have hs : sin (-(t / 2)) = -sin (t / 2) := Real.sin_neg _ rw [hs] congr 1 field_simp

theorem jrawMass_eq (K : ℕ) (hK : 0 < K) : jrawMass K = (2 * pi / 3) * (K : ℝ) * (2 * (K : ℝ) ^ 2 + 1) := by have hcast : ((K - 1 : ℕ) : ℝ) = (K : ℝ) - 1 := by rw [Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr (Nat.ne_of_gt hK))] norm_num have hfun : jraw K = fun t => ((K : ℝ) + ∑ j ∈ range (K - 1), (2 * (((K - 1 : ℕ) : ℝ) - (j : ℝ))) * cos (((j + 1 : ℕ) : ℝ) * t)) ^ 2 := by funext t rw [jraw_eq_chebyshev K hK t] rw [show (Polynomial.Chebyshev.U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 4 = ((Polynomial.Chebyshev.U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 2) ^ 2 by ring] congr 1 rw [cheb_U_sq_eval (K - 1) t] have hsucc : K - 1 + 1 = K := by omega rw [hcast] rw [Finset.mul_sum] have hlead : (K : ℝ) - 1 + 1 = (K : ℝ) := by ring rw [hlead] apply congrArg ((K : ℝ) + ·) apply Finset.sum_congr rfl intro j hj ring rw [jrawMass, hfun, integral_sq_cos_sum] have hsum := sum_range_sub_sq (K - 1) have hcoeff : (∑ j ∈ range (K - 1), (2 * (((K - 1 : ℕ) : ℝ) - (j : ℝ))) ^ 2) = 4 * (((K - 1 : ℕ) : ℝ) * ((K - 1 : ℕ) + 1) * (2 * (K - 1 : ℕ) + 1) / 6) := by calc (∑ j ∈ range (K - 1), (2 * (((K - 1 : ℕ) : ℝ) - (j : ℝ))) ^ 2) = 4 * ∑ j ∈ range (K - 1), (((K - 1 : ℕ) : ℝ) - (j : ℝ)) ^ 2 := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring _ = _ := by rw [hsum] rw [hcoeff, hcast] push_cast ring

theorem jrawMass_lower (K : ℕ) (hK : 0 < K) : (4 * pi / 3) * (K : ℝ) ^ 3 ≤ jrawMass K := by rw [jrawMass_eq K hK] have hpi : 0 < pi := Real.pi_pos have hKR : (1 : ℝ) ≤ K := by exact_mod_cast hK nlinarith [sq_nonneg ((K : ℝ) - 1)]

theorem jrawMass_upper (K : ℕ) (hK : 0 < K) : jrawMass K ≤ 2 * pi * (K : ℝ) ^ 3 := by rw [jrawMass_eq K hK] have hpi : 0 < pi := Real.pi_pos have hKR : (1 : ℝ) ≤ K := by exact_mod_cast hK have hsquare : 2 * (K : ℝ) ^ 2 + 1 ≤ 3 * (K : ℝ) ^ 2 := by nlinarith calc (2 * pi / 3) * (K : ℝ) * (2 * (K : ℝ) ^ 2 + 1) ≤ (2 * pi / 3) * (K : ℝ) * (3 * (K : ℝ) ^ 2) := by exact mul_le_mul_of_nonneg_left hsquare (by positivity) _ = 2 * pi * (K : ℝ) ^ 3 := by ring

theorem jrawMass_pos (K : ℕ) (hK : 0 < K) : 0 < jrawMass K := by have hl := jrawMass_lower K hK have hpi : 0 < pi := Real.pi_pos have hKR : (0 : ℝ) < K := by exact_mod_cast hK exact lt_of_lt_of_le (by positivity) hl

theorem jackson_integral_eq_one (K : ℕ) (hK : 0 < K) : (∫ t in Icc (-pi) pi, jackson K t) = 1 := by rw [show jackson K = fun t => jraw K t / jrawMass K by rfl, MeasureTheory.integral_div, ← jrawMass] exact div_self (jrawMass_pos K hK).ne'

theorem jackson_first_moment (K : ℕ) (hK : 0 < K) : (∫ t in Icc (-pi) pi, |t| * jackson K t) ≤ 32 / (K : ℝ) := by have hKR : (0 : ℝ) < K := by exact_mod_cast hK have hpoint (t : ℝ) : |t| ≤ (K : ℝ) / 4 * t ^ 2 + 1 / (K : ℝ) := by have hs := sq_nonneg ((K : ℝ) * |t| - 2) have ht2 : |t| ^ 2 = t ^ 2 := sq_abs t field_simp nlinarith have hiLeft : IntegrableOn (fun t => |t| * jackson K t) (Icc (-pi) pi) := (show Continuous (fun t => |t| * jackson K t) by fun_prop).continuousOn |>.integrableOn_compact isCompact_Icc have hiRight : IntegrableOn (fun t => ((K : ℝ) / 4 * t ^ 2 + 1 / (K : ℝ)) * jackson K t) (Icc (-pi) pi) := (show Continuous (fun t => ((K : ℝ) / 4 * t ^ 2 + 1 / (K : ℝ)) * jackson K t) by fun_prop).continuousOn |>.integrableOn_compact isCompact_Icc calc (∫ t in Icc (-pi) pi, |t| * jackson K t) ≤ ∫ t in Icc (-pi) pi, ((K : ℝ) / 4 * t ^ 2 + 1 / (K : ℝ)) * jackson K t := by exact MeasureTheory.setIntegral_mono_on hiLeft hiRight measurableSet_Icc (fun t ht => mul_le_mul_of_nonneg_right (hpoint t) (jackson_nonneg K hK t)) _ = (K : ℝ) / 4 * (∫ t in Icc (-pi) pi, t ^ 2 * jackson K t) + (1 / (K : ℝ)) * (∫ t in Icc (-pi) pi, jackson K t) := by have hi₁ : IntegrableOn (fun t => (K : ℝ) / 4 * (t ^ 2 * jackson K t)) (Icc (-pi) pi) := (show Continuous (fun t => (K : ℝ) / 4 * (t ^ 2 * jackson K t)) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc have hi₂ : IntegrableOn (fun t => (1 / (K : ℝ)) * jackson K t) (Icc (-pi) pi) := (show Continuous (fun t => (1 / (K : ℝ)) * jackson K t) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc rw [show (fun t => ((K : ℝ) / 4 * t ^ 2 + 1 / (K : ℝ)) * jackson K t) = fun t => (K : ℝ) / 4 * (t ^ 2 * jackson K t) + (1 / (K : ℝ)) * jackson K t by funext t; ring] rw [MeasureTheory.integral_add hi₁ hi₂, MeasureTheory.integral_const_mul, MeasureTheory.integral_const_mul] _ ≤ (K : ℝ) / 4 * (24 / (K : ℝ) ^ 2) + (1 / (K : ℝ)) * 1 := by gcongr · exact jackson_second_moment_aux K hK · exact (jackson_integral_eq_one K hK).le _ ≤ 32 / (K : ℝ) := by field_simp nlinarith

theorem jraw_isTrigPolyLE (K : ℕ) (hK : 0 < K) : IsTrigPolyLE (2 * (K - 1)) (jraw K) := by let U : Polynomial ℝ := Polynomial.Chebyshev.U ℝ ((K - 1 : ℕ) : ℤ) let p : Polynomial ℝ := U ^ 4 have hpneg : ∀ x : ℝ, p.eval (-x) = p.eval x := by intro x simp only [p, Polynomial.eval_pow, U] rw [Polynomial.Chebyshev.U_eval_neg] rw [mul_pow] have hsign : (((((K - 1 : ℕ) : ℤ)).negOnePow : ℤ) : ℝ) ^ 4 = 1 := by have habs : |(((((K - 1 : ℕ) : ℤ)).negOnePow : ℤ) : ℝ)| = 1 := by norm_cast exact Int.abs_negOnePow _ calc (((((K - 1 : ℕ) : ℤ)).negOnePow : ℤ) : ℝ) ^ 4 = |(((((K - 1 : ℕ) : ℤ)).negOnePow : ℤ) : ℝ) ^ 4| := by rw [abs_of_nonneg (by positivity)] _ = |(((((K - 1 : ℕ) : ℤ)).negOnePow : ℤ) : ℝ)| ^ 4 := by exact abs_pow _ _ _ = 1 := by rw [habs]; norm_num rw [hsign, one_mul] obtain ⟨q, hqdeg, hpq⟩ := exists_comp_sq_of_eval_neg_eq p hpneg let A : Polynomial ℝ := Polynomial.C (1 / 2 : ℝ) * (Polynomial.X + 1) let R : Polynomial ℝ := q.comp A have hAdeg : A.natDegree ≤ 1 := by dsimp [A] compute_degree have hpdeg : p.natDegree = 4 * (K - 1) := by dsimp [p, U] rw [Polynomial.natDegree_pow, Polynomial.Chebyshev.natDegree_U_natCast] have hRdeg : R.natDegree ≤ 2 * (K - 1) := by calc R.natDegree ≤ q.natDegree * A.natDegree := Polynomial.natDegree_comp_le _ ≤ q.natDegree * 1 := Nat.mul_le_mul_left _ hAdeg _ = q.natDegree := Nat.mul_one _ _ ≤ p.natDegree / 2 := hqdeg _ = 2 * (K - 1) := by rw [hpdeg]; omega apply (cosComp_isTrigPolyLE R (2 * (K - 1)) hRdeg).congr intro t rw [jraw_eq_chebyshev K hK t] have hhalf : cos (t / 2) ^ 2 = (cos t + 1) / 2 := by have hcos := Real.cos_two_mul (t / 2) rw [show 2 * (t / 2) = t by ring] at hcos nlinarith calc (Polynomial.Chebyshev.U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 4 = p.eval (cos (t / 2)) := by simp [p, U] _ = q.eval (cos (t / 2) ^ 2) := by rw [hpq, Polynomial.eval_comp, Polynomial.eval_pow, Polynomial.eval_X] _ = q.eval ((cos t + 1) / 2) := by rw [hhalf] _ = R.eval (cos t) := by simp [R, A, Polynomial.eval_comp] congr 1 ring

theorem jackson_isTrigPolyLE (K : ℕ) (hK : 0 < K) : IsTrigPolyLE (2 * (K - 1)) (jackson K) := by apply (const_mul (jrawMass K)⁻¹ (jraw_isTrigPolyLE K hK)).congr intro t simp [jackson, div_eq_mul_inv, mul_comm]

theorem integrableOn_tensorJackson (K d : ℕ) : IntegrableOn (tensorJackson K d) (periodBox d) := by change Integrable (fun u : Fin d → ℝ ↦ ∏ i, jackson K (u i)) (volume.restrict (periodBox d)) rw [show periodBox d = Set.univ.pi (fun _ ↦ Icc (-pi) pi) by ext u simp only [periodBox, Set.mem_ofPred_eq, Set.mem_pi, Set.mem_univ, true_implies, Set.mem_Icc], volume_pi, Measure.restrict_pi_pi] exact Integrable.fintype_prod fun _ ↦ integrableOn_jackson K

theorem integral_periodBox_prod {d : ℕ} (g : Fin d → ℝ → ℝ) (hg : ∀ i, IntegrableOn (g i) (Icc (-pi) pi)) : (∫ u in periodBox d, ∏ i, g i (u i)) = ∏ i, ∫ t in Icc (-pi) pi, g i t := by rw [show periodBox d = Set.univ.pi (fun _ ↦ Icc (-pi) pi) by ext u simp only [periodBox, Set.mem_ofPred_eq, Set.mem_pi, Set.mem_univ, true_implies, Set.mem_Icc], volume_pi, Measure.restrict_pi_pi] exact MeasureTheory.integral_fintype_prod_eq_prod g

theorem tensorJackson_first_moment_eq {d K : ℕ} (hK : 0 < K) (i : Fin d) : (∫ u in periodBox d, |u i| * tensorJackson K d u) = ∫ t in Icc (-pi) pi, |t| * jackson K t := by classical let g : Fin d → ℝ → ℝ := fun j t ↦ (if j = i then |t| else 1) * jackson K t have hi : IntegrableOn (fun t : ℝ ↦ |t| * jackson K t) (Icc (-pi) pi) := ((continuous_abs.comp continuous_id).mul (continuous_jackson K)).continuousOn.integrableOn_compact isCompact_Icc have hg : ∀ j, IntegrableOn (g j) (Icc (-pi) pi) := by intro j by_cases hji : j = i · simpa [g, hji] using hi · simpa [g, hji] using integrableOn_jackson K rw [show (fun u : Fin d → ℝ ↦ |u i| * tensorJackson K d u) = fun u ↦ ∏ j, g j (u j) by funext u symm calc (∏ j, g j (u j)) = (∏ j, if j = i then |u j| else 1) * ∏ j, jackson K (u j) := by simp only [g, Finset.prod_mul_distrib] _ = |u i| * tensorJackson K d u := by simp [tensorJackson], integral_periodBox_prod g hg] have hmass : (∫ t in Icc (-pi) pi, jackson K t) = 1 := jackson_integral_eq_one K hK have hcoord : ∀ j, (∫ t in Icc (-pi) pi, g j t) = if j = i then (∫ t in Icc (-pi) pi, |t| * jackson K t) else 1 := by intro j by_cases hji : j = i <;> simp [g, hji, hmass] calc (∏ j, ∫ t in Icc (-pi) pi, g j t) = ∏ j, if j = i then (∫ t in Icc (-pi) pi, |t| * jackson K t) else 1 := Finset.prod_congr rfl fun j _ ↦ hcoord j _ = ∫ t in Icc (-pi) pi, |t| * jackson K t := by simp

theorem tensorJackson_second_moment_eq {d K : ℕ} (hK : 0 < K) (i : Fin d) : (∫ u in periodBox d, (u i) ^ 2 * tensorJackson K d u) = ∫ t in Icc (-pi) pi, t ^ 2 * jackson K t := by classical let g : Fin d → ℝ → ℝ := fun j t ↦ (if j = i then t ^ 2 else 1) * jackson K t have hi : IntegrableOn (fun t : ℝ ↦ t ^ 2 * jackson K t) (Icc (-pi) pi) := ((continuous_id.pow 2).mul (continuous_jackson K)).continuousOn.integrableOn_compact isCompact_Icc have hg : ∀ j, IntegrableOn (g j) (Icc (-pi) pi) := by intro j by_cases hji : j = i · simpa [g, hji] using hi · simpa [g, hji] using integrableOn_jackson K rw [show (fun u : Fin d → ℝ ↦ (u i) ^ 2 * tensorJackson K d u) = fun u ↦ ∏ j, g j (u j) by funext u symm calc (∏ j, g j (u j)) = (∏ j, if j = i then (u j) ^ 2 else 1) * ∏ j, jackson K (u j) := by simp only [g, Finset.prod_mul_distrib] _ = (u i) ^ 2 * tensorJackson K d u := by simp [tensorJackson], integral_periodBox_prod g hg] have hmass : (∫ t in Icc (-pi) pi, jackson K t) = 1 := jackson_integral_eq_one K hK have hcoord : ∀ j, (∫ t in Icc (-pi) pi, g j t) = if j = i then (∫ t in Icc (-pi) pi, t ^ 2 * jackson K t) else 1 := by intro j by_cases hji : j = i <;> simp [g, hji, hmass] calc (∏ j, ∫ t in Icc (-pi) pi, g j t) = ∏ j, if j = i then (∫ t in Icc (-pi) pi, t ^ 2 * jackson K t) else 1 := Finset.prod_congr rfl fun j _ ↦ hcoord j _ = ∫ t in Icc (-pi) pi, t ^ 2 * jackson K t := by simp

theorem tensorConvolution_nonneg {d K : ℕ} (hK : 0 < K) {f : (Fin d → ℝ) → ℝ} (hf : ∀ z ∈ normalizedCube d, 0 ≤ f z) (x : Fin d → ℝ) : 0 ≤ tensorConvolution K f x := by rw [tensorConvolution] exact integral_nonneg fun u ↦ mul_nonneg (hf _ (cosPoint_mem_normalizedCube _)) (tensorJackson_nonneg hK u)

theorem normalizedPoint_affinePoint {d : ℕ} (c r z : Fin d → ℝ) (hr : ∀ i, 0 < r i) : normalizedPoint c r (affinePoint c r z) = z := by funext i simp only [normalizedPoint, affinePoint] field_simp [ne_of_gt (hr i)] ring

theorem affinePoint_normalizedPoint {d : ℕ} (c r y : Fin d → ℝ) (hr : ∀ i, 0 < r i) : affinePoint c r (normalizedPoint c r y) = y := by funext i simp only [affinePoint, normalizedPoint] field_simp [ne_of_gt (hr i)] ring

theorem affinePoint_mem_centeredRectangle {d : ℕ} (c r z : Fin d → ℝ) (hr : ∀ i, 0 < r i) (hz : z ∈ normalizedCube d) : affinePoint c r z ∈ centeredRectangle c r := by intro i simp only [affinePoint] rw [add_sub_cancel_left, abs_mul, abs_of_pos (hr i)] exact mul_le_of_le_one_right (le_of_lt (hr i)) (abs_le.mpr (hz i))

theorem normalizedPoint_mem_normalizedCube {d : ℕ} (c r y : Fin d → ℝ) (hr : ∀ i, 0 < r i) (hy : y ∈ centeredRectangle c r) : normalizedPoint c r y ∈ normalizedCube d := by intro i rw [show normalizedPoint c r y i = (y i - c i) / r i by rfl, Set.mem_Icc] apply abs_le.mp rw [abs_div, abs_of_pos (hr i), div_le_one (hr i)] exact hy i

theorem mvPolynomial_affine_substitution_four (q : MvPolynomial (Fin 4) ℝ) (c r : Fin 4 → ℝ) (n : ℕ) (hr : ∀ i, 0 < r i) (hqcoord : ∀ m ∈ q.support, ∀ i, m i ≤ n) : ∃ p : MvPolynomial (Fin 4) ℝ, (∀ y, eval y p = eval (normalizedPoint c r y) q) ∧ (∀ m ∈ p.support, ∀ i, m i ≤ n) ∧ p.totalDegree ≤ q.totalDegree ∧ mvCoeffL1 p ≤ mvCoeffL1 q * ∏ i : Fin 4, (max 1 ((1 + |c i|) / r i)) ^ n := by classical let g : Fin 4 → MvPolynomial (Fin 4) ℝ := fun i => (MvPolynomial.X i - MvPolynomial.C (c i)) * MvPolynomial.C (r i)⁻¹ let p := MvPolynomial.bind₁ g q have hp_sum : p = ∑ m ∈ q.support, MvPolynomial.bind₁ g (monomial m (q.coeff m)) := by dsimp [p] conv_lhs => rw [q.as_sum] simp only [map_sum] have hcoord_term (m : Fin 4 →₀ ℕ) (a : ℝ) (i : Fin 4) : (MvPolynomial.bind₁ g (monomial m a)).degreeOf i ≤ m i := by rw [MvPolynomial.bind₁_monomial] calc (MvPolynomial.C a * ∏ j ∈ m.support, g j ^ m j : MvPolynomial (Fin 4) ℝ).degreeOf i ≤ (MvPolynomial.C a : MvPolynomial (Fin 4) ℝ).degreeOf i + (∏ j ∈ m.support, g j ^ m j : MvPolynomial (Fin 4) ℝ).degreeOf i := MvPolynomial.degreeOf_mul_le _ _ _ _ ≤ 0 + ∑ j ∈ m.support, (g j ^ m j : MvPolynomial (Fin 4) ℝ).degreeOf i := by gcongr · simp · exact MvPolynomial.degreeOf_prod_le _ _ _ _ ≤ ∑ j ∈ m.support, m j * (if i = j then 1 else 0) := by simp only [zero_add] gcongr with j hj exact (MvPolynomial.degreeOf_pow_le _ _ _).trans (Nat.mul_le_mul_left _ (by dsimp [g] exact affineVariable_degreeOf_le c r i j)) _ = m i := by by_cases hi : i ∈ m.support · rw [Finset.sum_eq_single i] · simp · intro j hj hji simp [Ne.symm hji] · exact fun h => (h hi).elim · have hmi : m i = 0 := Finsupp.notMem_support_iff.mp hi rw [hmi] apply Finset.sum_eq_zero intro j hj have hji : i ≠ j := by intro hij subst j exact hi hj simp [hji] have htotal_term (m : Fin 4 →₀ ℕ) (a : ℝ) : (MvPolynomial.bind₁ g (monomial m a)).totalDegree ≤ m.sum fun _ e => e := by rw [MvPolynomial.bind₁_monomial] calc (MvPolynomial.C a * ∏ j ∈ m.support, g j ^ m j : MvPolynomial (Fin 4) ℝ).totalDegree ≤ (MvPolynomial.C a : MvPolynomial (Fin 4) ℝ).totalDegree + (∏ j ∈ m.support, g j ^ m j : MvPolynomial (Fin 4) ℝ).totalDegree := MvPolynomial.totalDegree_mul _ _ _ ≤ 0 + ∑ j ∈ m.support, (g j ^ m j : MvPolynomial (Fin 4) ℝ).totalDegree := by gcongr · simp · exact MvPolynomial.totalDegree_finsetProd _ _ _ ≤ ∑ j ∈ m.support, m j := by simp only [zero_add] gcongr with j hj exact (MvPolynomial.totalDegree_pow _ _).trans (by simpa [g] using Nat.mul_le_mul_left (m j) (affineVariable_totalDegree_le c r j)) _ = m.sum fun _ e => e := by rfl refine ⟨p, ?_, ?_, ?_, ?_⟩ · intro y dsimp [p] rw [← MvPolynomial.aeval_eq_eval, MvPolynomial.aeval_bind₁, MvPolynomial.aeval_eq_eval] apply congrArg (fun z => eval z q) funext i simp [g, normalizedPoint, div_eq_mul_inv] · intro m hm i apply (MvPolynomial.monomial_le_degreeOf i hm).trans rw [hp_sum] refine (MvPolynomial.degreeOf_sum_le i q.support (fun m => MvPolynomial.bind₁ g (monomial m (q.coeff m)))).trans ?_ exact Finset.sup_le fun m hm => (hcoord_term m (q.coeff m) i).trans (hqcoord m hm i) · rw [hp_sum] refine (MvPolynomial.totalDegree_finsetSum q.support (fun m => MvPolynomial.bind₁ g (monomial m (q.coeff m)))).trans ?_ exact Finset.sup_le fun m hm => (htotal_term m (q.coeff m)).trans (MvPolynomial.le_totalDegree hm) · let A : Fin 4 → ℝ := fun i => (1 + |c i|) / r i let M : Fin 4 → ℝ := fun i => max 1 (A i) have hA (i : Fin 4) : 0 ≤ A i := by dsimp [A] exact div_nonneg (by positivity) (le_of_lt (hr i)) have hAM (i : Fin 4) : A i ≤ M i := by exact le_max_right _ _ have hM (i : Fin 4) : 1 ≤ M i := by exact le_max_left _ _ have hg_l1 (i : Fin 4) : mvCoeffL1 (g i) ≤ A i := by dsimp [g, A] calc mvCoeffL1 ((MvPolynomial.X i - MvPolynomial.C (c i)) * MvPolynomial.C (r i)⁻¹ : MvPolynomial (Fin 4) ℝ) ≤ mvCoeffL1 (MvPolynomial.X i - MvPolynomial.C (c i) : MvPolynomial (Fin 4) ℝ) * mvCoeffL1 (MvPolynomial.C (r i)⁻¹ : MvPolynomial (Fin 4) ℝ) := mvCoeffL1_mul_le _ _ _ ≤ (mvCoeffL1 (MvPolynomial.X i : MvPolynomial (Fin 4) ℝ) + mvCoeffL1 (-MvPolynomial.C (c i) : MvPolynomial (Fin 4) ℝ)) * mvCoeffL1 (MvPolynomial.C (r i)⁻¹ : MvPolynomial (Fin 4) ℝ) := by apply mul_le_mul_of_nonneg_right · simpa [sub_eq_add_neg] using mvCoeffL1_add_le (MvPolynomial.X i : MvPolynomial (Fin 4) ℝ) (-MvPolynomial.C (c i)) · unfold mvCoeffL1 positivity _ = (1 + |c i|) / r i := by rw [mvCoeffL1_X, mvCoeffL1_neg, mvCoeffL1_C, mvCoeffL1_C, abs_inv, abs_of_pos (hr i)] simp [div_eq_mul_inv] have hterm_l1 (m : Fin 4 →₀ ℕ) (a : ℝ) : mvCoeffL1 (MvPolynomial.bind₁ g (monomial m a)) ≤ |a| * ∏ i ∈ m.support, A i ^ m i := by rw [MvPolynomial.bind₁_monomial] calc mvCoeffL1 (MvPolynomial.C a * ∏ i ∈ m.support, g i ^ m i) ≤ mvCoeffL1 (MvPolynomial.C a : MvPolynomial (Fin 4) ℝ) * mvCoeffL1 (∏ i ∈ m.support, g i ^ m i) := mvCoeffL1_mul_le _ _ _ ≤ |a| * ∏ i ∈ m.support, mvCoeffL1 (g i ^ m i) := by rw [mvCoeffL1_C] exact mul_le_mul_of_nonneg_left (mvCoeffL1_finsetProd_le _ _) (abs_nonneg a) _ ≤ |a| * ∏ i ∈ m.support, mvCoeffL1 (g i) ^ m i := by apply mul_le_mul_of_nonneg_left _ (abs_nonneg a) apply Finset.prod_le_prod · intro i hi unfold mvCoeffL1 positivity · intro i hi exact mvCoeffL1_pow_le _ _ _ ≤ |a| * ∏ i ∈ m.support, A i ^ m i := by apply mul_le_mul_of_nonneg_left _ (abs_nonneg a) apply Finset.prod_le_prod · intro i hi exact pow_nonneg (by unfold mvCoeffL1; positivity) _ · intro i hi exact pow_le_pow_left₀ (by unfold mvCoeffL1; positivity) (hg_l1 i) _ have hfactor (m : Fin 4 →₀ ℕ) (hm : m ∈ q.support) : (∏ i ∈ m.support, A i ^ m i) ≤ ∏ i : Fin 4, M i ^ n := by calc (∏ i ∈ m.support, A i ^ m i) ≤ ∏ i ∈ m.support, M i ^ n := by apply Finset.prod_le_prod · intro i hi exact pow_nonneg (hA i) _ · intro i hi exact (pow_le_pow_left₀ (hA i) (hAM i) _).trans (pow_le_pow_right₀ (hM i) (hqcoord m hm i)) _ ≤ ∏ i : Fin 4, M i ^ n := by apply Finset.prod_le_prod_of_subset_of_one_le (Finset.subset_univ _) · intro i hi positivity · intro i hi hnot exact one_le_pow₀ (hM i) rw [hp_sum] calc mvCoeffL1 (∑ m ∈ q.support, MvPolynomial.bind₁ g (monomial m (q.coeff m))) ≤ ∑ m ∈ q.support, mvCoeffL1 (MvPolynomial.bind₁ g (monomial m (q.coeff m))) := mvCoeffL1_finsetSum_le _ _ _ ≤ ∑ m ∈ q.support, |q.coeff m| * ∏ i : Fin 4, M i ^ n := by gcongr with m hm exact (hterm_l1 m (q.coeff m)).trans (mul_le_mul_of_nonneg_left (hfactor m hm) (abs_nonneg _)) _ = mvCoeffL1 q * ∏ i : Fin 4, M i ^ n := by rw [← Finset.sum_mul] rfl _ = mvCoeffL1 q * ∏ i : Fin 4, (max 1 ((1 + |c i|) / r i)) ^ n := by rfl

theorem affineJackson_exists_mvPolynomial_four {K : ℕ} (hK : 0 < K) (c r : Fin 4 → ℝ) (hr : ∀ i, 0 < r i) (f : (Fin 4 → ℝ) → ℝ) (hf : ContinuousOn f (centeredRectangle c r)) : ∃ p q : MvPolynomial (Fin 4) ℝ, (∀ y, eval y p = eval (normalizedPoint c r y) q) ∧ (∀ x, eval (cosPoint x) q = tensorConvolution K (fun z => f (affinePoint c r z)) x) ∧ (∀ m ∈ p.support, ∀ i, m i ≤ 2 * (K - 1)) ∧ p.totalDegree ≤ 8 * (K - 1) := by /- Pull `f` back along `affinePoint`, proving continuity on `normalizedCube 4` with `ContinuousOn.comp` and `affinePoint_mem_centeredRectangle`. Apply `tensorConvolution_exists_mvPolynomial`, then apply `mvPolynomial_affine_substitution_four` to its output with `n = 2 * (K - 1)`. The substitution evaluation identity is exactly the first conjunct; its support and total-degree conclusions, together with `4 * (2 * (K - 1)) = 8 * (K - 1)`, discharge the remaining conjuncts. -/ have haff : Continuous (affinePoint c r) := by apply continuous_pi intro i exact continuous_const.add (continuous_const.mul (continuous_apply i)) have hpull : ContinuousOn (fun z => f (affinePoint c r z)) (normalizedCube 4) := hf.comp haff.continuousOn (fun z hz => affinePoint_mem_centeredRectangle c r z hr hz) obtain ⟨q, hqeval, hqcoord, hqtotal⟩ := tensorConvolution_exists_mvPolynomial hK (fun z => f (affinePoint c r z)) hpull obtain ⟨p, hpeval, hpcoord, hptotal, _⟩ := mvPolynomial_affine_substitution_four q c r (2 * (K - 1)) hr hqcoord refine ⟨p, q, hpeval, hqeval, hpcoord, ?_⟩ omega

theorem affineJackson_coeffBound_four {K : ℕ} (hK : 0 < K) (c r : Fin 4 → ℝ) (hr : ∀ i, 0 < r i) (f : (Fin 4 → ℝ) → ℝ) (B : ℝ) (hB : 0 ≤ B) (hf : ContinuousOn f (centeredRectangle c r)) (hbound : ∀ y ∈ centeredRectangle c r, |f y| ≤ B) : ∃ p q : MvPolynomial (Fin 4) ℝ, (∀ y, eval y p = eval (normalizedPoint c r y) q) ∧ (∀ x, eval (cosPoint x) q = tensorConvolution K (fun z => f (affinePoint c r z)) x) ∧ (∀ m ∈ p.support, ∀ i, m i ≤ 2 * (K - 1)) ∧ p.totalDegree ≤ 8 * (K - 1) ∧ mvCoeffL1 p ≤ (2 : ℝ) ^ (40 * K + 20) * B * ∏ i : Fin 4, (max 1 ((1 + |c i|) / r i)) ^ (2 * (K - 1)) := by /- Pull `f` back along `affinePoint`; rectangle boundedness restricts to cube boundedness by `affinePoint_mem_centeredRectangle`. Obtain `q` from `tensorConvolution_exists_mvPolynomial_four_coeffBound`, then substitute it using `mvPolynomial_affine_substitution_four` at degree `2 * (K - 1)`. Combine the two coefficient inequalities by multiplication with the nonnegative finite product. Reuse the substitution support/total-degree conclusions and the tensor evaluation identity without reconstructing a different representative. -/ have haff : Continuous (affinePoint c r) := by apply continuous_pi intro i exact continuous_const.add (continuous_const.mul (continuous_apply i)) have hpull : ContinuousOn (fun z => f (affinePoint c r z)) (normalizedCube 4) := hf.comp haff.continuousOn (fun z hz => affinePoint_mem_centeredRectangle c r z hr hz) have hbound_pull : ∀ z ∈ normalizedCube 4, |f (affinePoint c r z)| ≤ B := by intro z hz exact hbound (affinePoint c r z) (affinePoint_mem_centeredRectangle c r z hr hz) obtain ⟨q, hqeval, hqcoord, hqtotal, hqcoeff⟩ := tensorConvolution_exists_mvPolynomial_four_coeffBound hK (fun z => f (affinePoint c r z)) B hB hpull hbound_pull obtain ⟨p, hpeval, hpcoord, hptotal, hpcoeff⟩ := mvPolynomial_affine_substitution_four q c r (2 * (K - 1)) hr hqcoord refine ⟨p, q, hpeval, hqeval, hpcoord, ?_, ?_⟩ · omega · have hfactor : 0 ≤ ∏ i : Fin 4, (max 1 ((1 + |c i|) / r i)) ^ (2 * (K - 1)) := by positivity exact hpcoeff.trans (mul_le_mul_of_nonneg_right hqcoeff hfactor)

theorem tensorConvolution_exists_mvPolynomial {d K : ℕ} (hK : 0 < K) (f : (Fin d → ℝ) → ℝ) (hf : ContinuousOn f (normalizedCube d)) : ∃ p : MvPolynomial (Fin d) ℝ, (∀ x : Fin d → ℝ, eval (cosPoint x) p = tensorConvolution K f x) ∧ (∀ m ∈ p.support, ∀ i, m i ≤ 2 * (K - 1)) ∧ p.totalDegree ≤ d * (2 * (K - 1)) := by apply exists_mvPolynomial_of_coord_even_trig (q := tensorConvolution K f) · exact fun i x => tensorConvolution_coord_trig hK f hf x i · intro i x t have h := tensorConvolution_coord_even hK f hf (update x i t) i simpa [update] using h

theorem polynomial_cos_is_even_trigPoly {n : ℕ} (p : Polynomial ℝ) (hp : p.natDegree ≤ n) : IsTrigPolyLE n (fun t => p.eval (cos t)) ∧ Even (fun t => p.eval (cos t)) := by refine ⟨Causalean.Mathlib.Analysis.BernsteinSzegoTrig.cosComp_isTrigPolyLE p n hp, ?_⟩ intro t simp

theorem chebyshev_coeffL1_le (n : ℕ) : polyCoeffL1 (T ℝ (n : ℤ)) ≤ (3 : ℝ) ^ n := by induction n using Nat.twoStepInduction with | zero => change polyCoeffL1 (T ℝ 0) ≤ 1 rw [Polynomial.Chebyshev.T_zero, polyCoeffL1_eq_sum_range_of_natDegree_lt (1 : Polynomial ℝ) (m := 1) (by simp)] simp | one => norm_num only [cast_one, pow_one] rw [Polynomial.Chebyshev.T_one, polyCoeffL1_eq_sum_range_of_natDegree_lt Polynomial.X (m := 2) (by simp)] norm_num [Finset.sum_range_succ, Polynomial.coeff_X] | more n hn hn1 => have hT : T ℝ ((n + 2 : ℕ) : ℤ) = (2 : ℝ) • (Polynomial.X * T ℝ ((n + 1 : ℕ) : ℤ)) - T ℝ (n : ℤ) := by convert Polynomial.Chebyshev.T_add_two ℝ (n : ℤ) using 1 · norm_num · simp only [Polynomial.smul_eq_C_mul] norm_num rw [Polynomial.C_ofNat] ring rw [hT] calc polyCoeffL1 ((2 : ℝ) • (Polynomial.X * T ℝ ((n + 1 : ℕ) : ℤ)) - T ℝ (n : ℤ)) ≤ polyCoeffL1 ((2 : ℝ) • (Polynomial.X * T ℝ ((n + 1 : ℕ) : ℤ))) + polyCoeffL1 (T ℝ (n : ℤ)) := polyCoeffL1_sub_le _ _ _ = 2 * polyCoeffL1 (T ℝ ((n + 1 : ℕ) : ℤ)) + polyCoeffL1 (T ℝ (n : ℤ)) := by rw [polyCoeffL1_smul, polyCoeffL1_X_mul] norm_num _ ≤ 2 * (3 : ℝ) ^ (n + 1) + (3 : ℝ) ^ n := by gcongr _ = 7 * (3 : ℝ) ^ n := by rw [pow_succ] ring _ ≤ 9 * (3 : ℝ) ^ n := by gcongr norm_num _ = (3 : ℝ) ^ (n + 2) := by rw [show n + 2 = (n + 1) + 1 by omega, pow_succ, pow_succ] ring

theorem cosine_sum_exists_polynomial (n : ℕ) (a : ℕ → ℝ) : ∃ p : Polynomial ℝ, p.natDegree ≤ n ∧ (∀ t : ℝ, p.eval (cos t) = ∑ k ∈ range (n + 1), a k * cos ((k : ℝ) * t)) ∧ polyCoeffL1 p ≤ ∑ k ∈ range (n + 1), |a k| * (3 : ℝ) ^ k := by classical let p : Polynomial ℝ := ∑ k ∈ range (n + 1), Polynomial.C (a k) * T ℝ (k : ℤ) refine ⟨p, ?_, ?_, ?_⟩ · dsimp [p] apply Polynomial.natDegree_sum_le_of_forall_le intro k hk refine (Polynomial.natDegree_C_mul_le _ _).trans ?_ rw [Polynomial.Chebyshev.natDegree_T, Int.natAbs_natCast] exact Nat.le_of_lt_succ (Finset.mem_range.mp hk) · intro t dsimp [p] rw [Polynomial.eval_finsetSum] apply Finset.sum_congr rfl intro k _ rw [Polynomial.eval_C_mul, Polynomial.Chebyshev.T_real_cos] norm_num · dsimp [p] calc polyCoeffL1 (∑ k ∈ range (n + 1), Polynomial.C (a k) * T ℝ (k : ℤ)) ≤ ∑ k ∈ range (n + 1), polyCoeffL1 (Polynomial.C (a k) * T ℝ (k : ℤ)) := polyCoeffL1_sum_le _ _ _ = ∑ k ∈ range (n + 1), |a k| * polyCoeffL1 (T ℝ (k : ℤ)) := by apply Finset.sum_congr rfl intro k _ rw [Polynomial.C_mul', polyCoeffL1_smul] _ ≤ ∑ k ∈ range (n + 1), |a k| * (3 : ℝ) ^ k := by exact Finset.sum_le_sum fun k _ => mul_le_mul_of_nonneg_left (chebyshev_coeffL1_le k) (abs_nonneg (a k))