OAI/Analysis/CircleDomains/Topology/CompactDiskRayBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The bounded-depth part of a compact family of disk rays lies in a common initial time interval, on which the angular lifts are uniformly bounded.

  1. def OAI.CircleDomainRigidity.puncturedArgument line 16
  2. theorem OAI.CircleDomainRigidity.compact_disk_rays_uniform_tail line 22
  3. theorem OAI.CircleDomainRigidity.compact_disk_rays_initial_angle_bound line 57