Viazovska's Magic Function

In this file, we define Viazovska's magic funtction g.

noncomputable def g : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ

The Magic Function, g.

Equations

• g = (↑Real.pi * Complex.I / 8640) • MagicFunction.FourierEigenfunctions.a + (Complex.I / (240 * ↑Real.pi)) • MagicFunction.FourierEigenfunctions.b

theorem g_zero : g 0 = 1

theorem fourier_g_zero : (FourierTransform.fourier g) 0 = 1

theorem g_zero_eq_fourier_g_zero : g 0 = (FourierTransform.fourier g) 0

noncomputable def A (t : ℝ) : ℂ

Equations

• A t = -↑t ^ 2 * φ₀'' (Complex.I / ↑t) - 36 * ↑Real.pi ^ (-2) * ψI' (Complex.I * ↑t)

noncomputable def B (t : ℝ) : ℂ

Equations

• B t = -↑t ^ 2 * φ₀'' (Complex.I / ↑t) + 36 * ↑Real.pi ^ (-2) * ψI' (Complex.I * ↑t)

theorem A_eq {t : ℝ} (ht : 0 < t) : A t = -↑t ^ 2 * φ₀ { coe := Complex.I / ↑t, coe_im_pos := ⋯ } - 36 * ↑Real.pi ^ (-2) * ψI { coe := Complex.I * ↑t, coe_im_pos := ⋯ }

theorem B_eq {t : ℝ} (ht : 0 < t) : B t = -↑t ^ 2 * φ₀ { coe := Complex.I / ↑t, coe_im_pos := ⋯ } + 36 * ↑Real.pi ^ (-2) * ψI { coe := Complex.I * ↑t, coe_im_pos := ⋯ }

theorem g_eq_integral_A {x : EuclideanSpace ℝ (Fin 8)} (hx : √2 < ‖x‖) : g x = ↑Real.pi / 2160 * ↑(Real.sin (Real.pi * ‖x‖ ^ 2 / 2)) ^ 2 * ∫ (t : ℝ) in Set.Ioi 0, A t * ↑(Real.exp (-Real.pi * ‖x‖ ^ 2 * t))

Integral representation of g in terms of A.

theorem g_Fourier_eq_integral_B {x : EuclideanSpace ℝ (Fin 8)} (hx : 0 < ‖x‖) : (FourierTransform.fourier g) x = ↑Real.pi / 2160 * ↑(Real.sin (Real.pi * ‖x‖ ^ 2 / 2)) ^ 2 * ∫ (t : ℝ) in Set.Ioi 0, B t * ↑(Real.exp (-Real.pi * ‖x‖ ^ 2 * t))

Integral representation of Fourier transform of g in terms of B.

theorem A_neg {t : ℝ} (ht : 0 < t) : (A t).re < 0

A is negative on (0, ∞).

theorem B_pos {t : ℝ} (ht : 0 < t) : 0 < (B t).re

B is positive on (0, ∞).

theorem g_nonpos {x : EuclideanSpace ℝ (Fin 8)} (hx : √2 ≤ ‖x‖) : (g x).re ≤ 0

g is nonpositive outside of the ball of radius √2.

theorem g_Fourier_nonneg (x : EuclideanSpace ℝ (Fin 8)) : 0 ≤ ((FourierTransform.fourier g) x).re

Fourier transform of g is nonnegative everywhere.