RelativePositiveDecomposition.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Positive decomposition inside a finite-matrix central space

Orthogonal positive parts of a central vector remain central: the positive central projection cannot discard a common nonzero component of those parts. Their support projections therefore belong to the relative commutant.

theorem OAI.KadisonKastler.positiveCone_parts_mem_centralVectorSpace line 26
theorem OAI.KadisonKastler.exists_relative_positive_decomposition line 76
theorem OAI.KadisonKastler.vectorSupportProjection_mem_relative line 98
Source documentation
The support of a matrix-central vector lies in the relative commutant.
```
theorem vectorSupportProjection_mem_relative
    (E : MatrixUnitSystem ι (Algebra M))
    (J : H ≃ₗᵢ⋆[ℂ] H)
    (hright : ∀ a : Algebra M, conjugationOperator J a.val ∈ M.commutant)
    (α : H) (hα : α ∈ centralVectorSpace (matrixUnitConcreteAlgebra E) J) :
    (vectorSupportProjection M α).val.val ∈ E.relativeVonNeumann := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.centralVectorSpace, OAI.KadisonKastler.matrixUnitConcreteAlgebra, OAI.KadisonKastler.vectorSupportProjection