Documentation

SpherePacking.MagicFunction.b.Eigenfunction

The Fourier Eigenfunction Property of b #

This file establishes that the function b is a -1-eigenfunction of the Fourier transform.

source
theorem MagicFunction.b.Fourier.perm_J₁_J₂ :
(FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) (SchwartzIntegrals.J₁ + SchwartzIntegrals.J₂) = -(SchwartzIntegrals.J₃ + SchwartzIntegrals.J₄)
source
theorem MagicFunction.b.Fourier.perm_J₅ :
(FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) SchwartzIntegrals.J₅ = -SchwartzIntegrals.J₆
source
theorem MagicFunction.b.Fourier.perm_₃_J₄ :
(FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) (SchwartzIntegrals.J₃ + SchwartzIntegrals.J₄) = -(SchwartzIntegrals.J₁ + SchwartzIntegrals.J₂)
source
theorem MagicFunction.b.Fourier.perm_J₆ :
(FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) SchwartzIntegrals.J₆ = -SchwartzIntegrals.J₅
source
theorem MagicFunction.b.Fourier.eig_b :
(FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) FourierEigenfunctions.b = -FourierEigenfunctions.b