OAI/Analysis/CircleDomains/Reflection/ReflectedFractionalLinear.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual reflected conjugate is fractional linear. Moving its pole to infinity produces an entire plane homeomorphism, so Liouville's theorem supplies its affine formula.

  1. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.poleNormalized_differentiableAt_ne_zero line 17
  2. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.poleNormalized_holomorphic line 28
  3. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedLimit_fractional_linear line 41