OAI/Probability/SKGap/Stability/OrdinaryWordEvent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.wordBounded_lift line 15
2. def OAI.SKGapCutoff.Recipe.WordSeminormBound line 25
3. lemma OAI.SKGapCutoff.Recipe.wordSeminormBound_diagram line 29
4. lemma OAI.SKGapCutoff.Recipe.offDiagonalSeminorm_sub_diagonal line 32
5. lemma OAI.SKGapCutoff.Recipe.matrixWord_opNorm line 39
6. lemma OAI.SKGapCutoff.Recipe.wordSeminormBound_test line 54
7. theorem OAI.SKGapCutoff.Recipe.ordinary_word_event line 63