OAI/Analysis/CircleDomains/Selection/OffsetRegions.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Geometry and energy monotonicity for the actual regions obtained by moving finitely many round boundaries a common positive distance.

  1. theorem OAI.CircleDomainRigidity.offset_closed_region_subset line 15
  2. theorem OAI.CircleDomainRigidity.offset_open_region_subset line 29
  3. theorem OAI.CircleDomainRigidity.circle_energy_mono line 39