OAI/Analysis/KadisonKastler/AmplificationWordLimits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.negative_amplification_word_limit line 50

   Source documentation

   The negative randomized word has eventual drift at most 66δ.

   theorem negative_amplification_word_limit (z : Generator.FiniteHilbert (Fin n) H) :
       ∀ ε > 0, ∀ᶠ j in (ω : Filter ℕ),
         let T := hilbertMatrix (diagonalAmplification (n := Fin n) h)
   …

   Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification

2. theorem OAI.KadisonKastler.positive_amplification_word_limit line 73

   Source documentation

   The positive randomized word has eventual drift 68δ on the moving vector.

   theorem positive_amplification_word_limit
       (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
   …

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