Fourier invariance of tensor contraction

Outer Fourier transforms preserve the contraction against a spatial-and-spin one-particle vector. These identities hold for arbitrary complete complex Hilbert fibers and require no integrability beyond L².

theorem LiebThirring.Fourier.fourier_tensorInsertion {V : Type u_1} {ι : Type u_2} {H : Type u_3} [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 MeasureTheory.volume)) (v : H) : FourierTransform.fourier ((tensorInsertion f) v) = (tensorInsertion (FourierTransform.fourier f)) v

Outer Fourier transforms act on the spatial factor of a tensor insertion.

theorem LiebThirring.Fourier.tensorContraction_fourier {V : Type u_1} {ι : Type u_2} {H : Type u_3} [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 MeasureTheory.volume)) (h : ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => H) 2 MeasureTheory.volume)) : (tensorContraction (FourierTransform.fourier f)) (FourierTransform.fourier h) = (tensorContraction f) h

Simultaneous outer Fourier transforms leave tensor contraction unchanged.