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 : ((SchwartzMap.fourierTransformCLE ℂ) g) 0 = 1

theorem g_zero_eq_fourier_g_zero : g 0 = ((SchwartzMap.fourierTransformCLE ℂ) g) 0