OAI/Geometry/CylinderCovering/Nilpotent/RetainedArea.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CylinderCovering.NilpotentRate.box line 10
  2. def OAI.CylinderCovering.NilpotentRate.openBox line 13
  3. lemma OAI.CylinderCovering.NilpotentRate.box_eq line 16
  4. lemma OAI.CylinderCovering.NilpotentRate.openBox_eq line 22
  5. lemma OAI.CylinderCovering.NilpotentRate.box_volume line 28
  6. lemma OAI.CylinderCovering.NilpotentRate.openBox_volume line 40
  7. lemma OAI.CylinderCovering.NilpotentRate.box_compact line 52
  8. lemma OAI.CylinderCovering.NilpotentRate.openBox_open line 57
  9. def OAI.CylinderCovering.NilpotentRate.indexCoord line 63
  10. lemma OAI.CylinderCovering.NilpotentRate.integerVector_apply line 65
  11. lemma OAI.CylinderCovering.NilpotentRate.tile_eq_rotated_box line 69
  12. lemma OAI.CylinderCovering.NilpotentRate.rotated_volume line 94
  13. lemma OAI.CylinderCovering.NilpotentRate.tile_area line 107
  14. lemma OAI.CylinderCovering.NilpotentRate.tile_compact line 113
  15. def OAI.CylinderCovering.NilpotentRate.openTile line 118
  16. lemma OAI.CylinderCovering.NilpotentRate.openTile_subset line 121
  17. lemma OAI.CylinderCovering.NilpotentRate.openTile_area line 126
  18. lemma OAI.CylinderCovering.NilpotentRate.openTile_open line 132
  19. lemma OAI.CylinderCovering.NilpotentRate.openTile_disjoint line 136
  20. lemma OAI.CylinderCovering.NilpotentRate.sum_tile_area_le_container line 155
  21. lemma OAI.CylinderCovering.NilpotentRate.unitSquare_norm_le line 171
  22. lemma OAI.CylinderCovering.NilpotentRate.tile_dist_center_le line 182
  23. lemma OAI.CylinderCovering.NilpotentRate.tile_center_mem line 191
  24. def OAI.CylinderCovering.NilpotentRate.coarseCenter line 197
  25. lemma OAI.CylinderCovering.NilpotentRate.cell_eq_box line 200
  26. lemma OAI.CylinderCovering.NilpotentRate.retained_tile_subset_box line 222
  27. lemma OAI.CylinderCovering.NilpotentRate.retained_tile_area_bound line 249
  28. lemma OAI.CylinderCovering.NilpotentRate.retained_fine_area_bound line 260
  29. lemma OAI.CylinderCovering.NilpotentRate.openTile_ae_eq_tile line 267
  30. lemma OAI.CylinderCovering.NilpotentRate.tile_aedisjoint line 277
  31. lemma OAI.CylinderCovering.NilpotentRate.finite_tile_union_area line 283