OAI/Probability/SKGap/Localization/UniformStarted.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.errorBudget_mono line 21
2. theorem OAI.SKGapCutoff.Recipe.uniform_started_control line 33
3. theorem OAI.SKGapCutoff.Recipe.local_uniform_auxiliary_mean line 94
4. theorem OAI.SKGapCutoff.Recipe.finite_started_control line 122