OAI/Geometry/Cannon/Modulus/LocalSubdisk.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonRadialEnergy.local_subdisk line 14
  2. theorem OAI.CannonRadialEnergy.local_disjoint_disk_square_budget line 40
  3. theorem OAI.CannonRadialEnergy.active_local_disk_square_budget line 53
  4. lemma OAI.CannonLocalPacking.compact_subset_closedBall_of_frontier_subset line 73
  5. lemma OAI.CannonLocalPacking.tile_ball_dichotomy line 84
  6. lemma OAI.CannonLocalPacking.tile_max_disk_control line 104
  7. lemma OAI.CannonLocalPacking.frontier_disk_charge line 120
  8. lemma OAI.CannonLocalPacking.clipped_tile_control line 146
  9. lemma OAI.CannonLocalPacking.sum_indicator_le_one line 164
  10. lemma OAI.CannonLocalPacking.incidence_sum_le line 181
  11. theorem OAI.CannonLocalPacking.local_active_tile_square_budget line 195
  12. theorem OAI.CannonTileTopology.selected_tile_budget line 261
  13. theorem OAI.CannonTileTopology.pole_chart_tile_budget line 323