OAI/Analysis/CircleDomains/Probability/PhysicalSliceOccupation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The physical occupation measure controls compact physical slices. A local inverse chart bound suffices; no regularity of the Jordan coordinate change is used.

  1. theorem OAI.CircleDomainRigidity.physical_chart_image_subset line 19
  2. theorem OAI.CircleDomainRigidity.compact_chart_length_le_occupation line 39
  3. theorem OAI.CircleDomainRigidity.mean_compactChartFiberCount_le_occupation line 77