OAI/Probability/SKGap/Matrix/PrimaryWordEventBinding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.WordSeminormBound.mono line 15
2. def OAI.SKGapCutoff.Recipe.primaryEventBudget line 19
3. lemma OAI.SKGapCutoff.Recipe.primaryEventBudget_nonneg line 21
4. lemma OAI.SKGapCutoff.Recipe.wordEvent_formal line 25
5. def OAI.SKGapCutoff.Recipe.RecipeMatrixEvent line 51
6. lemma OAI.SKGapCutoff.Recipe.wordEvent_recipeEvent line 56