OAI/Analysis/KadisonKastler/RecoveryFamilyNormalization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalization over all the finite choices in the recovery rows

  1. theorem OAI.KadisonKastler.finiteRMS_independent_family line 15
  2. theorem OAI.KadisonKastler.recoveryForwardFamily_finiteRMS line 37

    Source documentation

    Averaging the forward rows over the independent unitary choice retains exactly the norm of the tested vector.

    theorem recoveryForwardFamily_finiteRMS (M : VonNeumannAlgebra H)
    (v : Θ → unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…

    Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann

  3. theorem OAI.KadisonKastler.recoveryBackwardFamily_finiteRMS line 47

    Source documentation

    The full backward row family has the same exact normalization.

    theorem recoveryBackwardFamily_finiteRMS (M : VonNeumannAlgebra H)
    (v : Θ → unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…

    Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann