OAI/Analysis/KadisonKastler/AmplificationUnitaryBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The amplified unitary commutator estimate from a controlled free lift

  1. theorem OAI.KadisonKastler.unitary_commutator_le_of_free_lift line 36

    Source documentation

    With a controlled free Haar representative, all finite random choices can be made and eliminated. No row estimate is an assumption of this theorem.

    theorem unitary_commutator_le_of_free_lift
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τ : FaithfulTracialState (Algebra M))
    (D : TraceQuotientMap (matrixVonNeumannTrace (ι := Fin n) M τ) σ ω)
…

    Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixVonNeumannTrace