OAI/Probability/SKGap/Stability/ImplicitFlip.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.ImplicitSystem.equations_balance line 13
  2. theorem OAI.SKGap.ImplicitSystem.implicit_difference_equation line 24
  3. theorem OAI.SKGap.ImplicitSystem.implicit_scaled_difference line 42
  4. lemma OAI.SKGap.ImplicitSystem.implicit_scalar_difference line 55
  5. def OAI.SKGap.ImplicitSystem.columnNorm line 75
  6. lemma OAI.SKGap.ImplicitSystem.columnNorm_nonneg line 77
  7. lemma OAI.SKGap.ImplicitSystem.columnNorm_sq line 79
  8. lemma OAI.SKGap.ImplicitSystem.columnNorm_add line 82
  9. lemma OAI.SKGap.ImplicitSystem.columnNorm_neg line 85
  10. lemma OAI.SKGap.ImplicitSystem.columnNorm_sub line 87
  11. lemma OAI.SKGap.ImplicitSystem.columnNorm_smul line 89
  12. lemma OAI.SKGap.ImplicitSystem.columnNorm_bound line 92
  13. lemma OAI.SKGap.ImplicitSystem.columnNorm_operator line 97
  14. lemma OAI.SKGap.ImplicitSystem.columnNorm_vector_scalar line 102
  15. lemma OAI.SKGap.ImplicitSystem.columnNorm_add_sub_sub_sub line 112
  16. lemma OAI.SKGap.ImplicitSystem.column_inverse_estimate line 122
  17. theorem OAI.SKGap.ImplicitSystem.implicit_columns_bound line 148
  18. lemma OAI.SKGapCutoff.Recipe.columnNorm_matrix line 185