OAI/Analysis/CircleDomains/Topology/FixedDiskCutoffs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed source and target cutoffs are chosen before the near-extremal model, so their derivative constants do not depend on that model.

  1. theorem OAI.CircleDomainRigidity.exists_complex_disk_cutoff line 13
  2. theorem OAI.CircleDomainRigidity.exists_physical_disk_cutoff line 21