AdditivePositiveSupport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Support projections for completely additive positive functionals.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_additive_positive_support line 22
Source documentation
Complete additivity supplies a support projection without assuming normality in advance. This is used in proving the normality criterion.
```
theorem exists_additive_positive_support (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (ψ : M →ₚ[ℂ] ℂ) (hψ : CompletelyAdditive (positiveFunctionalCLM ψ)) :
    ∃ p : M, IsStarProjection p ∧ ψ p = ψ 1 ∧
      ∀ q : M, IsStarProjection q → q ≤ p → ψ q = 0 → q = 0 := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.CompletelyAdditive, OAI.BoundedHochschild.KadisonRingrose.positiveFunctionalCLM