PositiveCompression.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Normality of positive functionals localized to a projection corner.

def OAI.BoundedHochschild.KadisonRingrose.compressionPositive line 22
Source documentation
Two-sided compression of a positive functional.
```
def compressionPositive {p : M} (hp : IsStarProjection p) (ψ : M →ₚ[ℂ] ℂ) : M →ₚ[ℂ] ℂ where
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.compressionPositive_clm line 30
lemma OAI.BoundedHochschild.KadisonRingrose.compressionPositive_one line 35
lemma OAI.BoundedHochschild.KadisonRingrose.compressionPositive_normal line 40
theorem OAI.BoundedHochschild.KadisonRingrose.singular_zero_of_normal_compression line 51
Source documentation
A singular positive functional has zero mass on every corner where its compression is normal.
```
theorem singular_zero_of_normal_compression (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p : M} (hp : IsStarProjection p) (ψ : M →ₚ[ℂ] ℂ)
    (hs : scalarNormalPart e (positiveFunctionalCLM ψ) = 0)
    (hn : TraceInPredual e (compressionPositive hp ψ)) : ψ p = 0 := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.positiveFunctionalCLM, OAI.BoundedHochschild.TraceInPredual, OAI.BoundedHochschild.KadisonRingrose.compressionPositive
theorem OAI.BoundedHochschild.KadisonRingrose.compression_normal_of_projection_dominance line 66
Source documentation
Domination on the projections of a corner suffices to make a positive compression normal when the dominating functional is normal.
```
theorem compression_normal_of_projection_dominance (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p : M} (hp : IsStarProjection p) (χ ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ)
    (hle : ∀ q : M, IsStarProjection q → q ≤ p → χ q ≤ ψ q) :
    TraceInPredual e (compressionPositive hp χ) := by
…
```
Mentions: OAI.BoundedHochschild.TraceInPredual, OAI.BoundedHochschild.KadisonRingrose.compressionPositive