Interchanging L² slices and partial Fourier transformation

Product currying supplies genuine L² classes in both orders. The interchange of a partial Fourier transform is proved on scalar tensors and extended by L² density; it does not assert pointwise Fourier integration for an L² state.

noncomputable def LiebThirring.Assembly.realFormSwapCurrying {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)] : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 MeasureTheory.volume) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) 2 ν)

Interchange the outer spatial variable and the remaining L² variable.

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.Assembly.realFormSwapCurrying_apply {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)] (u : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 MeasureTheory.volume)) : realFormSwapCurrying u = l2Curry ((l2PullbackEquiv MeasurableEquiv.prodComm ⋯) (l2CurryLinearIsometryEquiv.symm u))

Exchanging slices is currying the swapped product class.

theorem LiebThirring.Assembly.realFormSwapCurrying_ae_uncurry {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)] (u : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 MeasureTheory.volume)) : ∀ᵐ (y : α) ∂ν, ∀ᵐ (x : Position), ↑↑(↑↑(realFormSwapCurrying u) y) x = ↑↑(l2CurryLinearIsometryEquiv.symm u) (x, y)

The exchanged class agrees with the uncurried product representative, in the order needed to apply the one-body estimate on each remaining slice.

theorem LiebThirring.Assembly.realFormSwapCurrying_weighted_norm_sq {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)] (u : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 MeasureTheory.volume)) (w : Position → ENNReal) (hw : Measurable w) : ∫⁻ (y : α), ∫⁻ (x : Position), w x * ‖↑↑(↑↑(realFormSwapCurrying u) y) x‖ₑ ^ 2 ∂ν = ∫⁻ (x : Position), w x * ‖↑↑u x‖ₑ ^ 2

Weighted spatial mass is unchanged by exchanging the slice order.

noncomputable def LiebThirring.Assembly.realFormScalarInsertion {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : E →L[ℂ] ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)

Scalar tensor insertion into a Hilbert-valued spatial L² space.

Equations

• LiebThirring.Assembly.realFormScalarInsertion f = (ContinuousLinearMap.compLpL₂ 2 MeasureTheory.volume (ContinuousLinearMap.lsmul ℂ ℂ).flip).flip f

theorem LiebThirring.Assembly.realFormScalarInsertion_ae {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (v : E) : ↑↑((realFormScalarInsertion f) v) =ᵐ[MeasureTheory.volume] fun (x : Position) => ↑↑f x • v

theorem LiebThirring.Assembly.realFormSwapCurrying_tensor {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (v : ↥(MeasureTheory.Lp E 2 ν)) : realFormSwapCurrying ((ContinuousLinearMap.toSpanSingleton ℂ v).compLp f) = (realFormScalarInsertion f).compLp v

Slice interchange on an elementary scalar tensor.

theorem LiebThirring.Assembly.realFormSwapCurrying_fourier {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)] (u : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 MeasureTheory.volume)) : realFormSwapCurrying (FourierTransform.fourier u) = (↑↑(MeasureTheory.Lp.fourierTransformₗᵢ Position E)).compLp (realFormSwapCurrying u)

Partial Fourier transformation commutes with exchanging the slice order.

theorem LiebThirring.Assembly.realFormSwapCurrying_fourier_weighted_norm_sq {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)] (u : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 MeasureTheory.volume)) (w : Position → ENNReal) (hw : Measurable w) : ∫⁻ (y : α), ∫⁻ (ξ : Position), w ξ * ‖↑↑(FourierTransform.fourier (↑↑(realFormSwapCurrying u) y)) ξ‖ₑ ^ 2 ∂ν = ∫⁻ (ξ : Position), w ξ * ‖↑↑(FourierTransform.fourier u) ξ‖ₑ ^ 2

The integral of the slice Fourier energies is the outer partial Fourier energy.

theorem LiebThirring.Assembly.realFormTargetIsometry_weighted_norm_sq {H : Type u_3} {K : Type u_4} [NormedAddCommGroup H] [NormedSpace ℂ H] [NormedAddCommGroup K] [NormedSpace ℂ K] (A : H ≃ₗᵢ[ℂ] K) (u : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (w : Position → ENNReal) : ∫⁻ (x : Position), w x * ↑‖↑↑((↑↑A).compLp u) x‖₊ ^ 2 = ∫⁻ (x : Position), w x * ↑‖↑↑u x‖₊ ^ 2

Target isometries preserve all weighted extended L² masses.