The Fourier Eigenfunction Property of a

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

theorem MagicFunction.a.Fourier.fourier_involution {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : SchwartzMap V E) : ⇑((FourierTransform.fourierCLE ℂ (SchwartzMap V E)) ((FourierTransform.fourierCLE ℂ (SchwartzMap V E)) f)) = fun (x : V) => f (-x)

theorem MagicFunction.a.Fourier.radial_inversion {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : SchwartzMap V E) (hf : Function.Even ⇑f) : (FourierTransform.fourierCLE ℂ (SchwartzMap V E)) ((FourierTransform.fourierCLE ℂ (SchwartzMap V E)) f) = f

theorem MagicFunction.a.Fourier.perm_I₁_I₂ : (FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) (SchwartzIntegrals.I₁ + SchwartzIntegrals.I₂) = SchwartzIntegrals.I₃ + SchwartzIntegrals.I₄

theorem MagicFunction.a.Fourier.perm_I₅ : (FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) SchwartzIntegrals.I₅ = SchwartzIntegrals.I₆

theorem MagicFunction.a.Fourier.perm_₃_I₄ : (FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) (SchwartzIntegrals.I₃ + SchwartzIntegrals.I₄) = SchwartzIntegrals.I₁ + SchwartzIntegrals.I₂

theorem MagicFunction.a.Fourier.perm_I₆ : (FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) SchwartzIntegrals.I₆ = SchwartzIntegrals.I₅

theorem MagicFunction.a.Fourier.eig_a : (FourierTransform.fourierCLE ℂ (SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂ)) FourierEigenfunctions.a = FourierEigenfunctions.a