OAI/Probability/SKGap/Localization/DisorderRecipeEvent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.continuous_matrixLetter line 15
2. lemma OAI.SKGapCutoff.Recipe.continuous_matrixWord line 19
3. lemma OAI.SKGapCutoff.Recipe.isClosed_wordSeminormBound line 28
4. lemma OAI.SKGapCutoff.Recipe.disorder_closed_matrix_event line 48
5. lemma OAI.SKGapCutoff.Recipe.disorder_word_event line 59
6. lemma OAI.SKGapCutoff.Recipe.disorder_norm_event line 70
7. theorem OAI.SKGapCutoff.Recipe.disorder_fixed_norm_recipe_probability line 80