Orthogonal covariance of the L² Fourier transform

Orthogonal changes of spatial coordinates commute with the L² Fourier transform, by the integral formula and Schwartz density.

theorem LiebThirring.Fourier.fourier_comp_isometry {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : V ≃ₗᵢ[ℝ] V) (f : SchwartzMap V H) : FourierTransform.fourier ((SchwartzMap.compCLMOfContinuousLinearEquiv ℂ ↑A) f) = (SchwartzMap.compCLMOfContinuousLinearEquiv ℂ ↑A) (FourierTransform.fourier f)

Schwartz Fourier covariance under an orthogonal change of variables.

theorem LiebThirring.Fourier.compMeasurePreserving_toLp {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : V ≃ₗᵢ[ℝ] V) (f : SchwartzMap V H) : (MeasureTheory.Lp.compMeasurePreserving ⇑A ⋯) (f.toLp 2 MeasureTheory.volume) = ((SchwartzMap.compCLMOfContinuousLinearEquiv ℂ ↑A) f).toLp 2 MeasureTheory.volume

The measure-preserving L² pullback agrees with composition on Schwartz maps.

theorem LiebThirring.Fourier.fourier_compMeasurePreserving {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : V ≃ₗᵢ[ℝ] V) (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : FourierTransform.fourier ((MeasureTheory.Lp.compMeasurePreserving ⇑A ⋯) f) = (MeasureTheory.Lp.compMeasurePreserving ⇑A ⋯) (FourierTransform.fourier f)

Fourier on L² commutes with orthogonal spatial pullback.