OAI/Analysis/CircleDomains/Reflection/AnnularReflectionInjection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The explicit annular reflection preserves injectivity and keeps uniform bounds from the exterior side.

  1. lemma OAI.CircleDomainRigidity.annularCircleReflect_outer_iff line 12
  2. lemma OAI.CircleDomainRigidity.injOn_annularCircleReflect line 31
  3. lemma OAI.CircleDomainRigidity.annularCircleReflect_norm_le line 51