b is a Schwartz Function

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

b 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.b.SchwartzProperties.J₁'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.J₁'

theorem MagicFunction.b.SchwartzProperties.J₂'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.J₂'

theorem MagicFunction.b.SchwartzProperties.J₃'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.J₃'

theorem MagicFunction.b.SchwartzProperties.J₄'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.J₄'

theorem MagicFunction.b.SchwartzProperties.J₅'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.J₅'

theorem MagicFunction.b.SchwartzProperties.J₆'_smooth' : ContDiff ℝ (↑⊤) RealIntegrals.J₆'

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

We follow the proof of Proposition 7.8 in the blueprint.

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

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

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

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

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

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

def MagicFunction.b.SchwartzIntegrals.J₁' : SchwartzMap ℝ ℂ

Equations

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

def MagicFunction.b.SchwartzIntegrals.J₂' : SchwartzMap ℝ ℂ

Equations

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

def MagicFunction.b.SchwartzIntegrals.J₃' : SchwartzMap ℝ ℂ

Equations

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

def MagicFunction.b.SchwartzIntegrals.J₄' : SchwartzMap ℝ ℂ

Equations

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

def MagicFunction.b.SchwartzIntegrals.J₅' : SchwartzMap ℝ ℂ

Equations

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

def MagicFunction.b.SchwartzIntegrals.J₆' : SchwartzMap ℝ ℂ

Equations

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

def MagicFunction.b.SchwartzIntegrals.J₁ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.b.SchwartzIntegrals.J₁ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.b.SchwartzIntegrals.J₁'

def MagicFunction.b.SchwartzIntegrals.J₂ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.b.SchwartzIntegrals.J₂ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.b.SchwartzIntegrals.J₂'

def MagicFunction.b.SchwartzIntegrals.J₃ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.b.SchwartzIntegrals.J₃ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.b.SchwartzIntegrals.J₃'

def MagicFunction.b.SchwartzIntegrals.J₄ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.b.SchwartzIntegrals.J₄ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.b.SchwartzIntegrals.J₄'

def MagicFunction.b.SchwartzIntegrals.J₅ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.b.SchwartzIntegrals.J₅ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.b.SchwartzIntegrals.J₅'

def MagicFunction.b.SchwartzIntegrals.J₆ : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

Equations

• MagicFunction.b.SchwartzIntegrals.J₆ = schwartzMap_multidimensional_of_schwartzMap_real (EuclideanSpace ℝ (Fin 8)) MagicFunction.b.SchwartzIntegrals.J₆'

def MagicFunction.FourierEigenfunctions.b' : 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.b'_toFun_im (a : ℝ) : (b' a).im = (b.SchwartzIntegrals.J₁' a).im + (b.SchwartzIntegrals.J₂' a).im + (b.SchwartzIntegrals.J₃' a).im + (b.SchwartzIntegrals.J₄' a).im + (b.SchwartzIntegrals.J₅' a).im + (b.SchwartzIntegrals.J₆' a).im

@[simp]

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

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

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

Equations

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

@[simp]

theorem MagicFunction.FourierEigenfunctions.b_toFun_im (x : EuclideanSpace ℝ (Fin 8)) : (b x).im = (b.SchwartzIntegrals.J₁' (‖x‖ ^ 2)).im + (b.SchwartzIntegrals.J₂' (‖x‖ ^ 2)).im + (b.SchwartzIntegrals.J₃' (‖x‖ ^ 2)).im + (b.SchwartzIntegrals.J₄' (‖x‖ ^ 2)).im + (b.SchwartzIntegrals.J₅' (‖x‖ ^ 2)).im + (b.SchwartzIntegrals.J₆' (‖x‖ ^ 2)).im

@[simp]

theorem MagicFunction.FourierEigenfunctions.b_toFun_re (x : EuclideanSpace ℝ (Fin 8)) : (b x).re = (b.SchwartzIntegrals.J₁' (‖x‖ ^ 2)).re + (b.SchwartzIntegrals.J₂' (‖x‖ ^ 2)).re + (b.SchwartzIntegrals.J₃' (‖x‖ ^ 2)).re + (b.SchwartzIntegrals.J₄' (‖x‖ ^ 2)).re + (b.SchwartzIntegrals.J₅' (‖x‖ ^ 2)).re + (b.SchwartzIntegrals.J₆' (‖x‖ ^ 2)).re

theorem MagicFunction.FourierEigenfunctions.b_eq_sum_integrals_RadialFunctions : ⇑b = b.RadialFunctions.J₁ + b.RadialFunctions.J₂ + b.RadialFunctions.J₃ + b.RadialFunctions.J₄ + b.RadialFunctions.J₅ + b.RadialFunctions.J₆

theorem MagicFunction.FourierEigenfunctions.b_eq_sum_integrals_SchwartzIntegrals : b = b.SchwartzIntegrals.J₁ + b.SchwartzIntegrals.J₂ + b.SchwartzIntegrals.J₃ + b.SchwartzIntegrals.J₄ + b.SchwartzIntegrals.J₅ + b.SchwartzIntegrals.J₆

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