OAI/GroupTheory/SimpleAmenable/RandomFields/WeightedAveragingError.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.weighted_average_error line 16
  2. theorem OAI.SimpleAmenable.squared_error_good_bad line 44
  3. theorem OAI.SimpleAmenable.flagSignalDifference_add_constant line 72
  4. theorem OAI.SimpleAmenable.flagSignalDifference_vector_chart line 78
  5. theorem OAI.SimpleAmenable.flagSignalDifference_chart_variation line 88
  6. theorem OAI.SimpleAmenable.planeTent_scaled_near line 113
  7. def OAI.SimpleAmenable.flagGoodRow line 129
  8. theorem OAI.SimpleAmenable.flagGoodRow_interior line 133
  9. theorem OAI.SimpleAmenable.flagRowTent_nonneg line 152
  10. theorem OAI.SimpleAmenable.flagRowTent_ne_zero_iff line 159
  11. theorem OAI.SimpleAmenable.flagRowTent_separator_one line 165
  12. theorem OAI.SimpleAmenable.flagNormalization line 174
  13. theorem OAI.SimpleAmenable.flagAveragingMatrix_eq_rowTent line 180
  14. theorem OAI.SimpleAmenable.flagAveragingMatrix_good_action line 189
  15. theorem OAI.SimpleAmenable.flagAveragingMatrix_good_row_error line 205