OAI/Analysis/CircleDomains/Selection/GeometricRayIndex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual greatest-translate index. Compact strip bounds prove that the defining set is nonempty and bounded above, uniformly over the arc law.

  1. def OAI.CircleDomainRigidity.rayJordan line 15
  2. theorem OAI.CircleDomainRigidity.rayJordan_spec line 19
  3. def OAI.CircleDomainRigidity.rayRightIndices line 24
  4. def OAI.CircleDomainRigidity.geometricRayIndex line 28
  5. theorem OAI.CircleDomainRigidity.compact_ray_indices_bounded line 31
  6. theorem OAI.CircleDomainRigidity.rayRightIndices_nonempty_bddAbove line 53
  7. theorem OAI.CircleDomainRigidity.geometricRayIndex_isGreatest line 64
  8. theorem OAI.CircleDomainRigidity.compact_geometricRayIndex_bound line 70