OAI/Analysis/CircleDomains/Modulus/RayIndexOscillation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Near an interior point, a simple lifted ray has index jump at most one. The jump is zero when the projected point misses the arc.

  1. theorem OAI.CircleDomainRigidity.geometricRayIndex_on_translated_ray line 14
  2. theorem OAI.CircleDomainRigidity.rayInterior_of_index_lt_of_avoids line 37
  3. theorem OAI.CircleDomainRigidity.eventually_geometricRayIndex_bounds line 58
  4. theorem OAI.CircleDomainRigidity.eventually_geometricRayIndex_pair_difference line 99