OAI/Analysis/CircleDomains/Selection/MeanGeometricIndex.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Averaging the actual geometric index of a compact arc law. Uniform bounds come from the ray geometry, rather than a domination hypothesis.

  1. abbrev OAI.CircleDomainRigidity.ClosedUpperHalfPlane line 15
  2. def OAI.CircleDomainRigidity.meanGeometricIndex line 17
  3. theorem OAI.CircleDomainRigidity.integrable_geometricRayIndex line 22
  4. theorem OAI.CircleDomainRigidity.rayIndexDomain_of_projection_avoids line 37
  5. theorem OAI.CircleDomainRigidity.continuousAt_geometricRayIndex_of_avoids line 47
  6. theorem OAI.CircleDomainRigidity.continuousAt_meanGeometricIndex line 65