OAI/Probability/SKGap/Localization/BufferedFlip.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.vector_column_opNorm line 15
2. lemma OAI.SKGapCutoff.Recipe.vector_flip_opNorm line 22
3. lemma OAI.SKGapCutoff.Recipe.vector_flip_buffer line 30
4. lemma OAI.SKGapCutoff.Recipe.residualCutoff_flip_buffer line 42
5. lemma OAI.SKGapCutoff.Recipe.auxiliary_derivative line 67
6. lemma OAI.SKGapCutoff.Recipe.primary_literal_derivative_diagnostics line 73
7. theorem OAI.SKGapCutoff.Recipe.stable_selected_initial_diagnostics line 116