OAI/Analysis/CircleDomains/Reflection/MovingCircleReflection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reflection into a moving target circle. The unnormalized bound does not divide by its radius, so it remains useful along degenerating disks.

  1. def OAI.CircleDomainRigidity.circleReflectionExtension line 12
  2. lemma OAI.CircleDomainRigidity.circleReflectionExtension_outer line 15
  3. lemma OAI.CircleDomainRigidity.normalized_circle_norm line 22
  4. lemma OAI.CircleDomainRigidity.circleReflectionExtension_differentiableOn line 26
  5. lemma OAI.CircleDomainRigidity.circleReflectionExtension_norm_le line 51