CompleteAdditivity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

This is the complete-additivity condition of Ringrose, Section 4 (Takesaki's normality criterion), expressed through the net of finite partial sums.

def OAI.BoundedHochschild.KadisonRingrose.CompletelyAdditive line 28
Source documentation
Preservation of arbitrary orthogonal projection sums. The index universe need only contain the set of projections of the algebra.
```
def CompletelyAdditive (F : StrongDual ℂ M) : Prop :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.normal_completelyAdditive line 35
lemma OAI.BoundedHochschild.KadisonRingrose.CompletelyAdditive.add line 48
lemma OAI.BoundedHochschild.KadisonRingrose.CompletelyAdditive.sub line 56
theorem OAI.BoundedHochschild.KadisonRingrose.exists_nonnegative_projection_corner line 66
Source documentation
A completely additive hermitian functional has a maximal positive projection corner inside any given projection (Ringrose, Lemma 4.1). Here positivity is first recorded on subprojections.
```
theorem exists_nonnegative_projection_corner (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (F : StrongDual ℂ M) (hF : CompletelyAdditive F) {E : M} (hE : IsStarProjection E) :
    ∃ p : M, IsStarProjection p ∧ p ≤ E ∧ (F E).re ≤ (F p).re ∧
      ∀ q : M, IsStarProjection q → q ≤ p → 0 ≤ (F q).re := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.CompletelyAdditive