PositiveConeFaithfulApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Faithful positive perturbations in the original Hilbert space

Adding a positive vector to a separating positive vector preserves separation. A small positive multiple of the reference vector therefore approximates any cone vector by cyclic separating cone vectors.

theorem OAI.KadisonKastler.positiveCone_separating_add line 30
theorem OAI.KadisonKastler.cyclic_of_separating_of_conjugation_fixed line 57
Source documentation
For a conjugation exchanging the two algebras, a fixed separating vector is cyclic on the same representation.
```
theorem cyclic_of_separating_of_conjugation_fixed
    (hleft : ∀ a : Algebra M.commutant, conjugationOperator J a.val ∈ M)
    {η : H} (hη : J η = η) (hs : Function.Injective (algebraVectorMap M η)) :
    DenseRange (algebraVectorMap M η) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.algebraVectorMap
theorem OAI.KadisonKastler.exists_positiveCone_cyclic_separating_near line 81