Fourier transform and bounded target maps

Bounded target maps commute with Fourier transform. Schwartz identities extend by unweighted L² density.

theorem LiebThirring.Fourier.fourier_postcomp {V : Type u_1} {H : Type u_2} {K : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (L : H →L[ℂ] K) (f : SchwartzMap V H) : FourierTransform.fourier ((SchwartzMap.postcompCLM L) f) = (SchwartzMap.postcompCLM L) (FourierTransform.fourier f)

A bounded complex target map commutes with the Schwartz Fourier transform.

theorem LiebThirring.Fourier.compLp_toLp {V : Type u_1} {H : Type u_2} {K : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (L : H →L[ℂ] K) (f : SchwartzMap V H) : L.compLp (f.toLp 2 MeasureTheory.volume) = ((SchwartzMap.postcompCLM L) f).toLp 2 MeasureTheory.volume

The bounded L² target map agrees with postcomposition on Schwartz maps.

theorem LiebThirring.Fourier.fourier_compLp {V : Type u_1} {H : Type u_2} {K : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (L : H →L[ℂ] K) (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : FourierTransform.fourier (L.compLp f) = L.compLp (FourierTransform.fourier f)

Fourier on L² commutes with every bounded complex map on the target.