Density of smooth one-particle tensors #
Continuous linear maps out of a finite-spin normed-space-valued L² space are determined by their
values on elementary tensors.
Applying a linear isometry componentwise to the normed factor of an elementary tensor is the same as applying it before insertion.
theorem
LiebThirring.continuousLinearMap_ext_tensorInsertion
{ι : Type u_1}
{α : Type u_2}
{H : Type u_3}
{K : Type u_4}
[Fintype ι]
[MeasurableSpace α]
[NormedAddCommGroup H]
[NormedSpace ℂ H]
[NormedAddCommGroup K]
[NormedSpace ℂ K]
{μ : MeasureTheory.Measure α}
(A B : ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => H) 2 μ) →L[ℂ] K)
(h :
∀ (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) (v : H), A ((tensorInsertion f) v) = B ((tensorInsertion f) v))
:
Continuous linear maps out of a finite-spin normed-space-valued L² space are
determined by their values on elementary tensors.
theorem
LiebThirring.piLpCongrRight_compLp_tensorInsertion
{ι : Type u_1}
{α : Type u_2}
[Fintype ι]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{E : Type u_5}
{F : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(T : E ≃ₗᵢ[ℂ] F)
(f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ))
(v : E)
:
(↑↑(LinearIsometryEquiv.piLpCongrRight 2 fun (x : ι) => T)).compLp ((tensorInsertion f) v) = (tensorInsertion f) (T v)
Applying a linear isometry componentwise to the normed-space-valued factor of an elementary tensor is the same as applying it before insertion.
theorem
LiebThirring.continuousLinearMap_ext_oneParticleInsertion_schwartz
{K : Type u_4}
[NormedAddCommGroup K]
[NormedSpace ℂ K]
{N q : ℕ}
(i : Fin N)
(A B : State N q →L[ℂ] K)
(h :
∀ (f : SchwartzMap Position (EuclideanSpace ℂ (Fin q)))
(v : SchwartzMap (OtherConfiguration i) (EuclideanSpace ℂ (OtherSpinLabels i q))),
A ((oneParticleInsertion i (f.toLp 2 MeasureTheory.volume)) (v.toLp 2 MeasureTheory.volume)) = B ((oneParticleInsertion i (f.toLp 2 MeasureTheory.volume)) (v.toLp 2 MeasureTheory.volume)))
:
Continuous linear maps out of the state space are determined by one-particle insertions whose two factors are Schwartz maps.