Documentation

LeanPool.LiebThirring.Kinetic.ContractionState

One-particle insertion, contraction and projection on State #

Insert a fixed one-particle vector into coordinate i.

Contract coordinate i against the full spatial-and-spin one-particle vector.

source
noncomputable def LiebThirring.oneParticleInsertion {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) :
↥(RestState i q) →L[ℂ] State N q

Insert a fixed one-particle vector into coordinate i.

Equations
Instances For
    source
    noncomputable def LiebThirring.oneParticleContraction {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) :
    State N q →L[ℂ] ↥(RestState i q)

    Contract coordinate i against the full spatial-and-spin one-particle vector.

    Equations
    Instances For
      source
      theorem LiebThirring.oneParticleContraction_smul {N q : ℕ} (i : Fin N) (a : ℂ) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) :
      oneParticleContraction i (a • f) = star a • oneParticleContraction i f

      The concrete contraction is conjugate-linear in its one-particle vector.

      source
      theorem LiebThirring.oneParticleInsertion_adjoint {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) :
      ContinuousLinearMap.adjoint (oneParticleInsertion i f) = oneParticleContraction i f

      The concrete contraction is the adjoint of the concrete insertion.

      source
      theorem LiebThirring.oneParticleInsertion_norm {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (v : ↥(RestState i q)) :
      ‖(oneParticleInsertion i f) v‖ = ‖f‖ * ‖v‖

      Exact norm of insertion on the state carrier.

      source
      theorem LiebThirring.oneParticleContraction_norm_le {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (ψ : State N q) :
      ‖(oneParticleContraction i f) ψ‖ ≤ ‖f‖ * ‖ψ‖

      contraction contraction bound, with no antisymmetry or normalization assumption.

      source
      theorem LiebThirring.oneParticleContraction_zero {N q : ℕ} (i : Fin N) (ψ : State N q) :
      (oneParticleContraction i 0) ψ = 0

      The zero one-particle vector contracts every state to zero.

      source
      theorem LiebThirring.oneParticleCurrying_insertion {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (v : ↥(RestState i q)) :
      (oneParticleCurrying i) ((oneParticleInsertion i f) v) = (tensorInsertion f) v

      Currying the inserted state recovers the literal Hilbert-valued tensor.

      source
      theorem LiebThirring.oneParticleInsertion_ae {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (v : ↥(RestState i q)) :
      ∀ᵐ (x : Position), ∀ (s : Fin q), ∀ᵐ (y : OtherConfiguration i), ∀ (t : OtherSpinLabels i q), (↑↑((oneParticleInsertion i f) v) (insertParticle i x y)).ofLp (insertSpin i s t) = (↑↑f x).ofLp s * (↑↑v y).ofLp t

      The inserted state has the prescribed product amplitudes on a.e. slices.

      source
      noncomputable def LiebThirring.oneParticleProjection {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) :
      State N q →L[ℂ] State N q

      The rank-one lift obtained by inserting back after contraction. It is an orthogonal projection when the inserted one-particle vector is unit.

      Equations
      Instances For
        source
        theorem LiebThirring.oneParticleProjection_adjoint {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) :
        ContinuousLinearMap.adjoint (oneParticleProjection i f) = oneParticleProjection i f

        Every lifted rank-one operator is self-adjoint.

        source
        theorem LiebThirring.oneParticleProjection_inner {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (ψ φ : State N q) :
        inner ℂ ((oneParticleProjection i f) ψ) φ = inner ℂ ψ ((oneParticleProjection i f) φ)

        The symmetry identity needed by the finite projection sum estimate.

        source
        theorem LiebThirring.oneParticleContraction_insertion {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (hf : ‖f‖ = 1) (v : ↥(RestState i q)) :
        (oneParticleContraction i f) ((oneParticleInsertion i f) v) = v

        Contraction undoes insertion of a unit one-particle vector.

        source
        theorem LiebThirring.oneParticleProjection_idempotent {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (hf : ‖f‖ = 1) (ψ : State N q) :
        (oneParticleProjection i f) ((oneParticleProjection i f) ψ) = (oneParticleProjection i f) ψ

        Inserting a unit vector after contraction is idempotent.

        source
        theorem LiebThirring.oneParticleProjection_norm {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (hf : ‖f‖ = 1) (ψ : State N q) :
        ‖(oneParticleProjection i f) ψ‖ = ‖(oneParticleContraction i f) ψ‖

        Unit-vector projection and contraction have equal output norms.