OAI/Analysis/CircleDomains/Topology/MeanIndexBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual mean index has the previously constructed positive Stieltjes boundary coordinate for the actual starting-angle law.

  1. theorem OAI.CircleDomainRigidity.translatedHalfPlaneRay_start line 16
  2. theorem OAI.CircleDomainRigidity.geometricRayIndex_boundary_of_avoids line 27
  3. def OAI.CircleDomainRigidity.compactArcStartingAngleLaw line 39
  4. theorem OAI.CircleDomainRigidity.measurable_compactArcStartingAngle line 42
  5. theorem OAI.CircleDomainRigidity.meanGeometricIndex_boundary line 46