OAI/GroupTheory/SimpleAmenable/PolygonGeometry/GoodRowSeparators.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.flagSeparates_near_row line 18
  2. theorem OAI.SimpleAmenable.directionNoCutProbability_eq_one line 29
  3. theorem OAI.SimpleAmenable.separatorMatrix_eq_one_on_good_row line 47
  4. theorem OAI.SimpleAmenable.squareFlag_cutForm_bound line 61
  5. def OAI.SimpleAmenable.flagBadSeparatorRow line 75
  6. theorem OAI.SimpleAmenable.flagBadSeparatorRow_card_bound line 79
  7. def OAI.SimpleAmenable.unitTent line 116
  8. theorem OAI.SimpleAmenable.unitTent_bounds line 118
  9. theorem OAI.SimpleAmenable.unitTent_lipschitz line 123
  10. theorem OAI.SimpleAmenable.unitTent_zero line 132
  11. theorem OAI.SimpleAmenable.unitTent_compact line 135
  12. theorem OAI.SimpleAmenable.unitTent_integral line 142
  13. def OAI.SimpleAmenable.doubleUnitTent line 168
  14. theorem OAI.SimpleAmenable.doubleUnitTent_bounds line 170
  15. theorem OAI.SimpleAmenable.doubleUnitTent_lipschitz line 174
  16. theorem OAI.SimpleAmenable.doubleUnitTent_zero line 190
  17. theorem OAI.SimpleAmenable.doubleUnitTent_integral line 201
  18. def OAI.SimpleAmenable.pairedUnitTent line 206
  19. theorem OAI.SimpleAmenable.pairedUnitTent_bounds line 209
  20. theorem OAI.SimpleAmenable.unit_mul_sub_bound line 215
  21. theorem OAI.SimpleAmenable.pairedUnitTent_lipschitz line 222
  22. theorem OAI.SimpleAmenable.pairedUnitTent_zero line 237
  23. theorem OAI.SimpleAmenable.pairedUnitTent_integrable line 244
  24. theorem OAI.SimpleAmenable.pairedUnitTent_integral line 250
  25. theorem OAI.SimpleAmenable.pairedQuadratic_tent_mass line 255