OAI/Analysis/CircleDomains/Selection/AnnularRadii.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A concrete decreasing sequence of separated transition radii.

  1. def OAI.CircleDomainRigidity.annularRadius line 11
  2. theorem OAI.CircleDomainRigidity.annularRadius_pos line 13
  3. theorem OAI.CircleDomainRigidity.annularRadius_antitone line 16
  4. theorem OAI.CircleDomainRigidity.annularRadius_separated line 21
  5. theorem OAI.CircleDomainRigidity.annularRadius_outer line 32
  6. theorem OAI.CircleDomainRigidity.annular_cutoff_derivatives_disjoint line 39