TracialRightSupportDischarge.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Right support trace bounds from the constructed polar partial isometry

theorem OAI.KadisonSimilarity.trace_initial_le_leftSupport line 15

Source documentation

Trace comparison needs only traciality and positivity once the polar partial isometry has been constructed.

theorem trace_initial_le_leftSupport {A : Type*} [CStarAlgebra A] [PartialOrder A]
    [StarOrderedRing A] (τ : A →ₚ[ℂ] ℂ) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (v q : A) (hq : IsStarProjection q) (hv : IsStarProjection (v * star v))
    (hqv : q * v = v) : (τ (star v * v)).re ≤ (τ q).re := by
…

theorem OAI.KadisonSimilarity.exists_rightSupport_trace_le line 38

Source documentation

The constructed right support has trace no larger than any containing left support. No normality of the tracial positive functional is used.

theorem exists_rightSupport_trace_le
    (τ : P.toStarSubalgebra →ₚ[ℂ] ℂ) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (q x : P.toStarSubalgebra) (hq : IsStarProjection q) (hqx : q * x = x) :
    ∃ r : P.toStarSubalgebra, IsStarProjection r ∧ (τ r).re ≤ (τ q).re ∧ x * r = x := by
…

theorem OAI.KadisonSimilarity.tracialRightSupportInput line 81

Source documentation

Discharge of the exact support input used in propagation.

theorem tracialRightSupportInput
    (τ : P.toStarSubalgebra →ₚ[ℂ] ℂ) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (q : P.toStarSubalgebra) (hq : IsStarProjection q)
    (A : StarSubalgebra ℂ P.toStarSubalgebra) :
    TracialRightSupportInput (fun a => (τ a).re) q A := by
…

Mentions: OAI.KadisonSimilarity.TracialRightSupportInput