OAI/Analysis/CircleDomains/Selection/VerticalRayAvoidance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The common angular strip bound makes all sufficiently far translates miss each vertical segment to the real boundary.

  1. theorem OAI.CircleDomainRigidity.vertical_im_nonneg line 14
  2. def OAI.CircleDomainRigidity.verticalCayleyPath line 18
  3. theorem OAI.CircleDomainRigidity.verticalCayleyPath_norm_le line 25
  4. theorem OAI.CircleDomainRigidity.verticalCayleyPath_zero line 28
  5. theorem OAI.CircleDomainRigidity.verticalCayleyPath_one line 31
  6. theorem OAI.CircleDomainRigidity.verticalCayleyPath_common_strip_bound line 35
  7. theorem OAI.CircleDomainRigidity.verticalCayleyPath_ray_intersection_strip_bound line 74
  8. theorem OAI.CircleDomainRigidity.verticalCayleyPath_ray_intersection_bound line 84
  9. theorem OAI.CircleDomainRigidity.far_translates_miss_verticalCayleyPath line 93