a is a Schwartz Function

The purpose of this file is to prove that a is a Schwartz function. It collects results stated elsewhere and presents them concisely.

a is smooth.

There is no reference for this in the blueprint. The idea is to use integrability to differentiate inside the integrals. The proof path I have in mind is the following.

We need to use the Leibniz Integral Rule to differentiate under the integral sign. This is stated as hasDerivAt_integral_of_dominated_loc_of_deriv_le in Mathlib.Analysis.Calculus.ParametricIntegral

theorem MagicFunction.a.SchwartzProperties.I₁'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.I₁'

theorem MagicFunction.a.SchwartzProperties.I₂'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.I₂'

theorem MagicFunction.a.SchwartzProperties.I₃'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.I₃'

theorem MagicFunction.a.SchwartzProperties.I₄'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.I₄'

theorem MagicFunction.a.SchwartzProperties.I₅'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.I₅'

theorem MagicFunction.a.SchwartzProperties.I₆'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.I₆'

a decays faster than any inverse power of the norm squared.

We follow the proof of Proposition 7.8 in the blueprint.

theorem MagicFunction.a.SchwartzProperties.I₁'_decay' (k n : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n RealIntegrals.I₁' x‖ ≤ C

theorem MagicFunction.a.SchwartzProperties.I₂'_decay' (k n : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n RealIntegrals.I₂' x‖ ≤ C

theorem MagicFunction.a.SchwartzProperties.I₃'_decay' (k n : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n RealIntegrals.I₃' x‖ ≤ C

theorem MagicFunction.a.SchwartzProperties.I₄'_decay' (k n : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n RealIntegrals.I₄' x‖ ≤ C

theorem MagicFunction.a.SchwartzProperties.I₅'_decay' (k n : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n RealIntegrals.I₅' x‖ ≤ C

theorem MagicFunction.a.SchwartzProperties.I₆'_decay' (k n : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n RealIntegrals.I₆' x‖ ≤ C

noncomputable def MagicFunction.a.SchwartzIntegrals.I₁' : SchwartzMap ℝ ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MagicFunction.a.SchwartzIntegrals.I₂' : SchwartzMap ℝ ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MagicFunction.a.SchwartzIntegrals.I₃' : SchwartzMap ℝ ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MagicFunction.a.SchwartzIntegrals.I₄' : SchwartzMap ℝ ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MagicFunction.a.SchwartzIntegrals.I₅' : SchwartzMap ℝ ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MagicFunction.a.SchwartzIntegrals.I₆' : SchwartzMap ℝ ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MagicFunction.a.SchwartzIntegrals.I₁ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.a.SchwartzIntegrals.I₁ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.a.SchwartzIntegrals.I₁'

noncomputable def MagicFunction.a.SchwartzIntegrals.I₂ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.a.SchwartzIntegrals.I₂ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.a.SchwartzIntegrals.I₂'

noncomputable def MagicFunction.a.SchwartzIntegrals.I₃ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.a.SchwartzIntegrals.I₃ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.a.SchwartzIntegrals.I₃'

noncomputable def MagicFunction.a.SchwartzIntegrals.I₄ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.a.SchwartzIntegrals.I₄ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.a.SchwartzIntegrals.I₄'

noncomputable def MagicFunction.a.SchwartzIntegrals.I₅ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.a.SchwartzIntegrals.I₅ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.a.SchwartzIntegrals.I₅'

noncomputable def MagicFunction.a.SchwartzIntegrals.I₆ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.a.SchwartzIntegrals.I₆ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.a.SchwartzIntegrals.I₆'

noncomputable def MagicFunction.FourierEigenfunctions.a' : SchwartzMap ℝ ℂ

The radial component of the +1-Fourier Eigenfunction of Viazovska's Magic Function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MagicFunction.FourierEigenfunctions.a'_toFun_re (a : ℝ) : (a' a).re = (MagicFunction.a.SchwartzIntegrals.I₁' a).re + (MagicFunction.a.SchwartzIntegrals.I₂' a).re + (MagicFunction.a.SchwartzIntegrals.I₃' a).re + (MagicFunction.a.SchwartzIntegrals.I₄' a).re + (MagicFunction.a.SchwartzIntegrals.I₅' a).re + (MagicFunction.a.SchwartzIntegrals.I₆' a).re

@[simp]

theorem MagicFunction.FourierEigenfunctions.a'_toFun_im (a : ℝ) : (a' a).im = (MagicFunction.a.SchwartzIntegrals.I₁' a).im + (MagicFunction.a.SchwartzIntegrals.I₂' a).im + (MagicFunction.a.SchwartzIntegrals.I₃' a).im + (MagicFunction.a.SchwartzIntegrals.I₄' a).im + (MagicFunction.a.SchwartzIntegrals.I₅' a).im + (MagicFunction.a.SchwartzIntegrals.I₆' a).im

noncomputable def MagicFunction.FourierEigenfunctions.a : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

The +1-Fourier Eigenfunction of Viazovska's Magic Function.

Equations

• MagicFunction.FourierEigenfunctions.a = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.FourierEigenfunctions.a'

@[simp]

theorem MagicFunction.FourierEigenfunctions.a_toFun_re (a✝ : EuclideanSpace ℝ (Fin 8)) : (a a✝).re = (a.SchwartzIntegrals.I₁' (‖a✝‖ ^ 2)).re + (a.SchwartzIntegrals.I₂' (‖a✝‖ ^ 2)).re + (a.SchwartzIntegrals.I₃' (‖a✝‖ ^ 2)).re + (a.SchwartzIntegrals.I₄' (‖a✝‖ ^ 2)).re + (a.SchwartzIntegrals.I₅' (‖a✝‖ ^ 2)).re + (a.SchwartzIntegrals.I₆' (‖a✝‖ ^ 2)).re

@[simp]

theorem MagicFunction.FourierEigenfunctions.a_toFun_im (a✝ : EuclideanSpace ℝ (Fin 8)) : (a a✝).im = (a.SchwartzIntegrals.I₁' (‖a✝‖ ^ 2)).im + (a.SchwartzIntegrals.I₂' (‖a✝‖ ^ 2)).im + (a.SchwartzIntegrals.I₃' (‖a✝‖ ^ 2)).im + (a.SchwartzIntegrals.I₄' (‖a✝‖ ^ 2)).im + (a.SchwartzIntegrals.I₅' (‖a✝‖ ^ 2)).im + (a.SchwartzIntegrals.I₆' (‖a✝‖ ^ 2)).im

theorem MagicFunction.FourierEigenfunctions.a_eq_sum_integrals_RadialFunctions : ⇑a = a.RadialFunctions.I₁ + a.RadialFunctions.I₂ + a.RadialFunctions.I₃ + a.RadialFunctions.I₄ + a.RadialFunctions.I₅ + a.RadialFunctions.I₆

theorem MagicFunction.FourierEigenfunctions.a_eq_sum_integrals_SchwartzIntegrals : a = a.SchwartzIntegrals.I₁ + a.SchwartzIntegrals.I₂ + a.SchwartzIntegrals.I₃ + a.SchwartzIntegrals.I₄ + a.SchwartzIntegrals.I₅ + a.SchwartzIntegrals.I₆

theorem MagicFunction.FourierEigenfunctions.a'_eq_sum_RealIntegrals : ⇑a' = a.RealIntegrals.I₁' + a.RealIntegrals.I₂' + a.RealIntegrals.I₃' + a.RealIntegrals.I₄' + a.RealIntegrals.I₅' + a.RealIntegrals.I₆'