OAI/GroupTheory/SimpleAmenable/RandomFields/SignalGoodRows.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.finset_sum_eq_of_zero_outside line 15
  2. theorem OAI.SimpleAmenable.flagSignal_good_row_constants line 22
  3. def OAI.SimpleAmenable.flagBoxFinset line 67
  4. theorem OAI.SimpleAmenable.mem_flagBoxFinset line 70
  5. theorem OAI.SimpleAmenable.flagAveragingMatrix_box_support line 74
  6. theorem OAI.SimpleAmenable.flagSignal_box_support line 85
  7. theorem OAI.SimpleAmenable.flagBoxFinset_card_quadratic line 107
  8. def OAI.SimpleAmenable.flagVolumeConstant line 126
  9. def OAI.SimpleAmenable.flagExceptionalConstant line 127
  10. def OAI.SimpleAmenable.flagRowSumConstant line 130
  11. theorem OAI.SimpleAmenable.flag_good_bad_energy line 132