OAI/Probability/SKGap/Stability/ImplicitFrobenius.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.ImplicitSystem.columnNorm_compare line 16
2. lemma OAI.SKGap.ImplicitSystem.columnNorm_inner_common line 23
3. lemma OAI.SKGap.ImplicitSystem.columnNorm_inner_variable line 29
4. lemma OAI.SKGap.ImplicitSystem.normalized_coefficient_difference line 36
5. lemma OAI.SKGap.ImplicitSystem.normalized_scalar_difference line 53
6. theorem OAI.SKGap.ImplicitSystem.implicit_frobenius_estimate line 76
7. lemma OAI.SKGapCutoff.Recipe.frobenius_by_rows line 148
8. lemma OAI.SKGapCutoff.Recipe.coefficient_diagonal_columns line 156