ProjectionJoinTrace.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite joins of projections and their trace bound. These elementary support identities are used to control countable unions of small spectral projections in the normal representation argument.

theorem OAI.KadisonSimilarity.trace_projection_le line 22

Source documentation

A positive trace is monotone in the algebraic projection order.

theorem trace_projection_le {A : Type*} [CStarAlgebra A]
    [PartialOrder A] [StarOrderedRing A] (τ : A →ₚ[ℂ] ℂ)
    (p q : A) (hp : IsStarProjection p) (hq : IsStarProjection q)
    (h : q * p = p) : (τ p).re ≤ (τ q).re := by
…

theorem OAI.KadisonSimilarity.trace_normalRangeSupport_le line 31

Source documentation

The range support has trace at most that of a prescribed right support.

theorem trace_normalRangeSupport_le (M : VonNeumannAlgebra H)
    (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
    (htr : ∀ a b, τ (a * b) = τ (b * a))
    (x p : M.toStarSubalgebra) (hp : IsStarProjection p) (hxp : x * p = x) :
    (τ (normalRangeSupport M x)).re ≤ (τ p).re := by
…

Mentions: OAI.KadisonSimilarity.normalRangeSupport

def OAI.KadisonSimilarity.projectionJoin line 45
Source documentation
Join formed from the orthogonal part of the second projection.
```
def projectionJoin (M : VonNeumannAlgebra H) (p q : M.toStarSubalgebra) :
    M.toStarSubalgebra := p + normalRangeSupport M ((1 - p) * q)
```
Mentions: OAI.KadisonSimilarity.normalRangeSupport
theorem OAI.KadisonSimilarity.projectionJoin_properties line 48

theorem OAI.KadisonSimilarity.trace_projectionJoin_le line 89

Source documentation

Subadditivity of the trace for a finite projection join.

theorem trace_projectionJoin_le (M : VonNeumannAlgebra H)
    (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
    (htr : ∀ a b, τ (a * b) = τ (b * a))
    (p q : M.toStarSubalgebra) (hq : IsStarProjection q) :
    (τ (projectionJoin M p q)).re ≤ (τ p).re + (τ q).re := by
…

Mentions: OAI.KadisonSimilarity.projectionJoin