OAI/Analysis/CircleDomains/Selection/GeometricIndexPeriod.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Deck translation adds the corresponding integer to the actual ray index and hence to its expectation.

  1. theorem OAI.CircleDomainRigidity.translatedHalfPlaneRay_curve_add line 15
  2. theorem OAI.CircleDomainRigidity.rayRightIndices_translate_iff line 23
  3. theorem OAI.CircleDomainRigidity.geometricRayIndex_translate line 47
  4. def OAI.CircleDomainRigidity.ClosedUpperHalfPlane.translate line 62
  5. theorem OAI.CircleDomainRigidity.meanGeometricIndex_translate line 65