OAI/Analysis/CircleDomains/Sobolev/SmoothRadialShrink.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A smooth ambient radial contraction, fixed outside the larger disk. It supplies the local shrinking step for analytic Jordan caps.

  1. def OAI.CircleDomainRigidity.radialShrinkFactor line 15
  2. def OAI.CircleDomainRigidity.radialShrink line 18
  3. lemma OAI.CircleDomainRigidity.radialShrinkFactor_pos line 21
  4. lemma OAI.CircleDomainRigidity.radialShrinkFactor_monotone line 27
  5. lemma OAI.CircleDomainRigidity.radialShrinkRadius_strictMono line 40
  6. lemma OAI.CircleDomainRigidity.radialShrink_norm line 50
  7. lemma OAI.CircleDomainRigidity.radialShrink_inner line 54
  8. lemma OAI.CircleDomainRigidity.radialShrink_outer line 62
  9. lemma OAI.CircleDomainRigidity.radialShrink_contDiff line 70
  10. lemma OAI.CircleDomainRigidity.radialShrink_injective line 78
  11. lemma OAI.CircleDomainRigidity.radialShrink_surjective line 87
  12. def OAI.CircleDomainRigidity.smoothRadialShrinkHomeomorph line 121