CommonPositionConjugationBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The tracial-conjugation bound in common position

The equality of basic constructions supplies the common right actions. All left and right unitary actions used in the norm-768 estimate are constructed here from the actual common subalgebra.

theorem OAI.KadisonKastler.norm_tracialConjugations_sub_le_of_commonPosition line 24

Source documentation

The norm-768 comparison with the common-action premises discharged by the basic-construction equality.

theorem norm_tracialConjugations_sub_le_of_commonPosition
    (hRM : R ≤ M) (hRN : R ≤ N)
    (τ : FaithfulTracialState (Algebra M)) (hτ : FiniteVectorTrace τ)
    (Ω : H) (hΩ : ‖Ω‖ = 1)
    (htrace : ∀ x : Algebra M, ‖x.val Ω‖ = traceTwoNorm τ x)
    (hcyclicM : DenseRange (fun x : Algebra M => x.val Ω))
    (hcyclicN : DenseRange (fun x : Algebra N => x.val Ω))
    (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H)
    (hJ₁ : Function.Involutive J₁) (hJ₂ : Function.Involutive J₂)
    (hM : ∀ x : Algebra M, J₁ (x.val Ω) = (star x).val Ω)
    (hN : ∀ x : Algebra N, J₂ (x.val Ω) = (star x).val Ω)
    (hirr : ∀ a : Algebra M,
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.traceTwoNorm