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) : ⇑((SchwartzMap.fourierTransformCLE ℂ) ((SchwartzMap.fourierTransformCLE ℂ) 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) : (SchwartzMap.fourierTransformCLE ℂ) ((SchwartzMap.fourierTransformCLE ℂ) f) = f

theorem MagicFunction.a.Fourier.perm_I₁_I₂ : (SchwartzMap.fourierTransformCLE ℂ) (SchwartzIntegrals.I₁ + SchwartzIntegrals.I₂) = SchwartzIntegrals.I₃ + SchwartzIntegrals.I₄

theorem MagicFunction.a.Fourier.perm_I₅ : (SchwartzMap.fourierTransformCLE ℂ) SchwartzIntegrals.I₅ = SchwartzIntegrals.I₆

theorem MagicFunction.a.Fourier.perm_₃_I₄ : (SchwartzMap.fourierTransformCLE ℂ) (SchwartzIntegrals.I₃ + SchwartzIntegrals.I₄) = SchwartzIntegrals.I₁ + SchwartzIntegrals.I₂

theorem MagicFunction.a.Fourier.perm_I₆ : (SchwartzMap.fourierTransformCLE ℂ) SchwartzIntegrals.I₆ = SchwartzIntegrals.I₅

theorem MagicFunction.a.Fourier.eig_a : (SchwartzMap.fourierTransformCLE ℂ) FourierEigenfunctions.a = FourierEigenfunctions.a