VectorSupportProjection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The support projection of a represented vector state

The support is the projection onto the closed commutant orbit. The orbit construction proves its minimality and faithfulness on the supported corner.

theorem OAI.KadisonKastler.commutantOrbitProjection_mem line 19
def OAI.KadisonKastler.vectorSupportProjection line 28
theorem OAI.KadisonKastler.vectorSupportProjection_apply line 34
theorem OAI.KadisonKastler.mul_vectorSupport_eq_zero line 39
Source documentation
An operator killing the vector kills its supported corner.
```
theorem mul_vectorSupport_eq_zero (M : VonNeumannAlgebra H) (ξ : H)
    (a : Algebra M) (ha : a.val ξ = 0) :
    a.val * (vectorSupportProjection M ξ).val.val = 0 := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.vectorSupportProjection
theorem OAI.KadisonKastler.vectorSupport_faithful_corner line 54

theorem OAI.KadisonKastler.vectorSupport_minimal line 61

Source documentation

A projection fixing the vector dominates its support.

theorem vectorSupport_minimal (M : VonNeumannAlgebra H) (ξ : H)
    (p : AlgebraProjection M) (hp : p.val.val ξ = ξ) :
    (vectorSupportProjection M ξ).val.val * p.val.val =
      (vectorSupportProjection M ξ).val.val := by
…

Mentions: OAI.KadisonKastler.vectorSupportProjection

theorem OAI.KadisonKastler.vectorSupport_commutes_of_right_vectors line 80

Source documentation

Central vectors have supports commuting with their left algebra.

theorem vectorSupport_commutes_of_right_vectors (M N : VonNeumannAlgebra H)
    (hNM : N ≤ M) (ξ : H)
    (hright : ∀ a : Algebra N, ∃ b : Algebra M.commutant, a.val ξ = b.val ξ)
    (a : Algebra N) :
    (vectorSupportProjection M ξ).val.val * a.val =
      a.val * (vectorSupportProjection M ξ).val.val := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.vectorSupportProjection