OAI/Analysis/CircleDomains/Topology/RecursiveComponentShrink.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual recursively chosen shrinking homeomorphisms, with summable geometric forward and quotient-inverse displacement bounds.

  1. def OAI.CircleDomainRigidity.componentShrinkRadius line 11
  2. lemma OAI.CircleDomainRigidity.componentShrinkRadius_pos line 13
  3. lemma OAI.CircleDomainRigidity.exists_recursive_component_shrink line 17