PositiveCompleteAdditivity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Complete additivity implies normality for positive functionals

The positive-functional case of Takesaki's criterion, as proved in Ringrose, Lectures on the trace in a finite von Neumann algebra, Lemmas 4.1--4.3. Only this case is needed for the normal-state orbit in the trace construction.

lemma OAI.BoundedHochschild.KadisonRingrose.positiveFunctional_zero_of_one_zero line 27
lemma OAI.BoundedHochschild.KadisonRingrose.exists_normal_positive_larger_on_projection line 35
theorem OAI.BoundedHochschild.KadisonRingrose.positive_normal_of_completelyAdditive line 56
Source documentation
A positive completely additive functional is normal.
```
theorem positive_normal_of_completelyAdditive (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (ψ : M →ₚ[ℂ] ℂ) (hψ : CompletelyAdditive (positiveFunctionalCLM ψ)) :
    TraceInPredual e ψ := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.CompletelyAdditive, OAI.BoundedHochschild.KadisonRingrose.positiveFunctionalCLM, OAI.BoundedHochschild.TraceInPredual