OAI/Analysis/KadisonKastler/TracialVarianceControl.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_unitary_trace_variance_control line 18

   Source documentation

   Scalar averaging in the trace Hilbert space gives one unitary detecting at least half the distance to the scalar trace.

   theorem exists_unitary_trace_variance_control
       (hM : Generator.IsII1Factor M.toStarSubalgebra) (x : Algebra M) :
       ∃ u : unitary (Algebra M),
         traceTwoNorm (concreteFactorTrace hM)
           (x - (concreteFactorTrace hM).toLinearMap x • (1 : Algebra M)) ≤
         2 * traceTwoNorm (concreteFactorTrace hM) ((u : Algebra M) * x - x * u) := by
   …

   Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.concreteFactorTrace