OAI/Analysis/CircleDomains/Probability/PhysicalImageOccupation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

General physical paths pay for the Hausdorff measure of their images. Together with the opposite simple-arc bound this makes erasing loops decrease physical occupation, including for arbitrary measurable densities.

  1. def OAI.CircleDomainRigidity.physicalStageImage line 20
  2. lemma OAI.CircleDomainRigidity.physicalSubpath_range line 25
  3. lemma OAI.CircleDomainRigidity.physicalStageImage_subset line 41
  4. lemma OAI.CircleDomainRigidity.monotone_physicalStageImage line 50
  5. lemma OAI.CircleDomainRigidity.iUnion_physicalStageImage line 80
  6. lemma OAI.CircleDomainRigidity.physicalStageImage_hausdorff_le line 92
  7. theorem OAI.CircleDomainRigidity.physical_image_hausdorff_le_occupation line 111
  8. theorem OAI.CircleDomainRigidity.simple_subarc_physical_length_le line 122
  9. theorem OAI.CircleDomainRigidity.simple_subarc_physical_occupation_le line 140