PositiveNormalParts.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Positive normal and singular parts

The normal-vector projection splits a positive functional into positive normal and singular parts. In particular, any positive functional dominated by a normal positive functional is normal. This supplies the normality criterion for order intervals in the predual compactness argument.

lemma OAI.BoundedHochschild.KadisonRingrose.normalPart_diagonal line 33
lemma OAI.BoundedHochschild.KadisonRingrose.normalComplement_diagonal line 50
def OAI.BoundedHochschild.KadisonRingrose.positiveNormalPart line 77
Source documentation
The positive normal part, realized by a projected GNS vector.
```
def positiveNormalPart (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (ψ : M →ₚ[ℂ] ℂ) :
    M →ₚ[ℂ] ℂ :=
…
```
def OAI.BoundedHochschild.KadisonRingrose.positiveSingularPart line 83
Source documentation
The remaining positive part, realized by the complementary GNS vector.
```
def positiveSingularPart (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (ψ : M →ₚ[ℂ] ℂ) :
    M →ₚ[ℂ] ℂ :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.positiveNormalPart_eq line 88
lemma OAI.BoundedHochschild.KadisonRingrose.positiveSingularPart_eq line 95
lemma OAI.BoundedHochschild.KadisonRingrose.positiveNormalPart_normal line 103

theorem OAI.BoundedHochschild.KadisonRingrose.positive_normal_of_dominated line 109

Source documentation

Domination by a positive normal functional forces normality.

theorem positive_normal_of_dominated (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (χ ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ)
    (hle : ∀ a : M, 0 ≤ a → χ a ≤ ψ a) : TraceInPredual e χ := by
…

Mentions: OAI.BoundedHochschild.TraceInPredual