Documentation

LeanPool.LiebThirring.Assembly.RealFormSlices

Full-spin one-particle L² slices #

Spatial currying without spin regrouping gives the slices on which the one-body Hardy estimate is applied. Spin regrouping is an isometry, so the partial Fourier weighted norm is exactly the landed particle Fourier energy.

source
theorem LiebThirring.Assembly.instFactNeENNRealOfNatTop_leanPool :
Fact (2 ≠ ⊤)
source
noncomputable def LiebThirring.Assembly.realFormParticleCurrying {N q : ℕ} (i : Fin N) (ψ : State N q) :
↥(MeasureTheory.Lp (↥(MeasureTheory.Lp (SpinAmplitudes N q) 2 MeasureTheory.volume)) 2 MeasureTheory.volume)

Spatial currying with the complete spin amplitude retained in each slice.

Equations
Instances For
    source
    theorem LiebThirring.Assembly.realFormParticleCurrying_ae {N q : ℕ} (i : Fin N) (ψ : State N q) :
    ∀ᵐ (x : Position) (y : OtherConfiguration i), ↑↑(↑↑(realFormParticleCurrying i ψ) x) y = ↑↑ψ (insertParticle i x y)

    The full-spin curried representative is the inserted state.

    source
    theorem LiebThirring.Assembly.realFormParticleCurrying_norm {N q : ℕ} (i : Fin N) (ψ : State N q) :
    ‖realFormParticleCurrying i ψ‖ = ‖ψ‖

    Spatial currying preserves the original L² norm.

    source
    noncomputable def LiebThirring.Assembly.realFormSpinRegrouping {N q : ℕ} (i : Fin N) :
    ↥(MeasureTheory.Lp (SpinAmplitudes N q) 2 MeasureTheory.volume) ≃ₗᵢ[ℂ] OneParticleFiber i q

    Regroup the complete spin slice into the landed one-particle fiber.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LiebThirring.Assembly.realFormSpinRegrouping_ae {N q : ℕ} (i : Fin N) (v : ↥(MeasureTheory.Lp (SpinAmplitudes N q) 2 MeasureTheory.volume)) (s : Fin q) :
      ∀ᵐ (y : OtherConfiguration i), ∀ (t : OtherSpinLabels i q), (↑↑(((realFormSpinRegrouping i) v).ofLp s) y).ofLp t = (↑↑v y).ofLp (insertSpin i s t)

      The representative formula for spin regrouping.

      source
      theorem LiebThirring.Assembly.realFormSpinRegrouping_compLp {N q : ℕ} (i : Fin N) (ψ : State N q) :
      (↑↑(realFormSpinRegrouping i)).compLp (realFormParticleCurrying i ψ) = (oneParticleCurrying i) ψ

      Full-spin currying and the currying currying differ only by a target isometry.

      source
      theorem LiebThirring.Assembly.realFormParticleCurrying_fourier_regrouping {N q : ℕ} (i : Fin N) (ψ : State N q) :
      (↑↑(realFormSpinRegrouping i)).compLp (FourierTransform.fourier (realFormParticleCurrying i ψ)) = FourierTransform.fourier ((oneParticleCurrying i) ψ)

      Spin regrouping commutes with the spatial partial Fourier transform.

      source
      theorem LiebThirring.Assembly.realFormParticleCurrying_fourier_energy {N q : ℕ} (i : Fin N) (ψ : State N q) :
      ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖↑↑(FourierTransform.fourier (realFormParticleCurrying i ψ)) ξ‖₊ ^ 2 = particleFourierEnergy ψ i

      Partial Fourier kinetic mass of the full-spin slices is the particle energy.

      source
      theorem LiebThirring.Assembly.realFormParticleSlices_ae {N q : ℕ} (i : Fin N) (ψ : State N q) :
      ∀ᵐ (y : OtherConfiguration i) (x : Position), ↑↑(↑↑(realFormSwapCurrying (realFormParticleCurrying i ψ)) y) x = ↑↑ψ (insertParticle i x y)

      In the opposite order, each remaining-coordinate slice is the original state as a function of the selected particle position.