Fourier factorization on particle tensors

The insertion phase splits into the selected and remaining spatial phases.

The literal full-state representative of a separated particle tensor.

theorem LiebThirring.inner_insertParticle {N : ℕ} (i : Fin N) (x ξ : Position) (y η : OtherConfiguration i) : inner ℝ (insertParticle i x y) (insertParticle i ξ η) = inner ℝ x ξ + inner ℝ y η

The insertion phase splits into the selected and remaining spatial phases.

noncomputable def LiebThirring.particleTensorFunction {N q : ℕ} (i : Fin N) (f : Position → EuclideanSpace ℂ (Fin q)) (v : OtherConfiguration i → EuclideanSpace ℂ (OtherSpinLabels i q)) (X : Configuration N) : SpinAmplitudes N q

The literal full-state representative of a separated particle tensor.

Equations

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

theorem LiebThirring.particleTensorFunction_insert {N q : ℕ} (i : Fin N) (f : Position → EuclideanSpace ℂ (Fin q)) (v : OtherConfiguration i → EuclideanSpace ℂ (OtherSpinLabels i q)) (x : Position) (y : OtherConfiguration i) (s : Fin q) (t : OtherSpinLabels i q) : (particleTensorFunction i f v (insertParticle i x y)).ofLp (insertSpin i s t) = (f x).ofLp s * (v y).ofLp t

Exact regrouped tensor evaluation on inserted spatial coordinates.

theorem LiebThirring.integrable_particleTensorFunction {N q : ℕ} (i : Fin N) {f : Position → EuclideanSpace ℂ (Fin q)} {v : OtherConfiguration i → EuclideanSpace ℂ (OtherSpinLabels i q)} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hv : MeasureTheory.Integrable v MeasureTheory.volume) : MeasureTheory.Integrable (particleTensorFunction i f v) MeasureTheory.volume

A product of integrable spatial factors gives an integrable full tensor.

theorem LiebThirring.fourier_particleTensorFunction {N q : ℕ} (i : Fin N) {f : Position → EuclideanSpace ℂ (Fin q)} {v : OtherConfiguration i → EuclideanSpace ℂ (OtherSpinLabels i q)} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hv : MeasureTheory.Integrable v MeasureTheory.volume) (ξ : Position) (η : OtherConfiguration i) : FourierTransform.fourier (particleTensorFunction i f v) (insertParticle i ξ η) = particleTensorFunction i (FourierTransform.fourier f) (FourierTransform.fourier v) (insertParticle i ξ η)

The full Fourier integral of a separated particle tensor is the tensor of its two Fourier integrals.

theorem LiebThirring.stronglyMeasurable_particleTensorFunction {N q : ℕ} (i : Fin N) (f : SchwartzMap Position (EuclideanSpace ℂ (Fin q))) (v : SchwartzMap (OtherConfiguration i) (EuclideanSpace ℂ (OtherSpinLabels i q))) : MeasureTheory.StronglyMeasurable (particleTensorFunction i ⇑f ⇑v)

Smooth factors give a strongly measurable literal tensor representative.

theorem LiebThirring.oneParticleInsertion_toLp_ae {N q : ℕ} (i : Fin N) (f : SchwartzMap Position (EuclideanSpace ℂ (Fin q))) (v : SchwartzMap (OtherConfiguration i) (EuclideanSpace ℂ (OtherSpinLabels i q))) : ↑↑((oneParticleInsertion i (f.toLp 2 MeasureTheory.volume)) (v.toLp 2 MeasureTheory.volume)) =ᵐ[MeasureTheory.volume] particleTensorFunction i ⇑f ⇑v

The concrete State insertion is the literal smooth tensor almost everywhere.

theorem LiebThirring.fourier_oneParticleInsertion_toLp {N q : ℕ} (i : Fin N) (f : SchwartzMap Position (EuclideanSpace ℂ (Fin q))) (v : SchwartzMap (OtherConfiguration i) (EuclideanSpace ℂ (OtherSpinLabels i q))) : FourierTransform.fourier ((oneParticleInsertion i (f.toLp 2 MeasureTheory.volume)) (v.toLp 2 MeasureTheory.volume)) = (oneParticleInsertion i ((FourierTransform.fourier f).toLp 2 MeasureTheory.volume)) ((FourierTransform.fourier v).toLp 2 MeasureTheory.volume)

Full L² Fourier carries a smooth inserted tensor to the Fourier-factor tensor.