OAI/Probability/SKGap/Localization/LocalExtraction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Static.tested_l2_to_star line 13
2. lemma OAI.SKGapCutoff.Static.local_source_extract line 26
3. lemma OAI.SKGapCutoff.Recipe.StartedMatrixEvent.mono_budget line 53
4. lemma OAI.SKGapCutoff.Recipe.residualCutoff_uniform_gradient line 68
5. theorem OAI.SKGapCutoff.Recipe.buffered_root_direction_weak line 106