OAI/Analysis/CircleDomains/Sobolev/CompactPhysicalFiberCoarea.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coarea for the actual distinct intersections of quotient arcs with compact physical slices. Length is measured before the coordinate change.

  1. theorem OAI.CircleDomainRigidity.pathImageCount_image_le_hausdorffZero line 20
  2. theorem OAI.CircleDomainRigidity.measurable_compactPhysicalFiberCount line 49
  3. theorem OAI.CircleDomainRigidity.compactPhysicalFiberCount_integral_le line 75
  4. theorem OAI.CircleDomainRigidity.mean_compactPhysicalFiberCount_integral_le line 94