OAI/GroupTheory/SimpleAmenable/Amenability/BarrierAlgorithm.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.barrierSitePoint line 15
  2. theorem OAI.SimpleAmenable.flagSite_eq_of_track_point line 18
  3. def OAI.SimpleAmenable.barrierMarkedParameters line 24
  4. def OAI.SimpleAmenable.barrierSubdivision line 31
  5. def OAI.SimpleAmenable.barrierActivation line 36
  6. def OAI.SimpleAmenable.ConsecutiveSubdivision line 42
  7. def OAI.SimpleAmenable.barrierActiveIntervals line 45
  8. theorem OAI.SimpleAmenable.barrierActivation_at_site line 54
  9. theorem OAI.SimpleAmenable.mem_barrierSubdivision_bounds line 69
  10. theorem OAI.SimpleAmenable.barrierSubdivision_start_site line 86
  11. def OAI.SimpleAmenable.BarrierLineIndex line 103
  12. def OAI.SimpleAmenable.barrierLineIndexFintype line 105
  13. def OAI.SimpleAmenable.sampledBarriers line 111
  14. theorem OAI.SimpleAmenable.sampledBarriers_supported line 118
  15. def OAI.SimpleAmenable.sampledPolygonPartition line 126
  16. theorem OAI.SimpleAmenable.barrierLinePoint_continuous line 134
  17. theorem OAI.SimpleAmenable.sampledBarriers_closed line 139