OAI/Probability/SKGap/Matrix/CorrectionTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.trace_frobenius line 14
2. lemma OAI.SKGapCutoff.Recipe.trace_small_diagonal line 22
3. lemma OAI.SKGapCutoff.Recipe.trace_small_mean line 32
4. def OAI.SKGapCutoff.Recipe.averageError line 39
5. lemma OAI.SKGapCutoff.Recipe.averageError_eq line 42
6. lemma OAI.SKGapCutoff.Recipe.trace_column_scaled line 50
7. lemma OAI.SKGapCutoff.Recipe.averageError_trace line 65
8. lemma OAI.SKGapCutoff.Recipe.primary_averageError_trace line 76