OAI/Analysis/CircleDomains/Reflection/ReflectedLimitHolomorphic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual principal map conjugates every generating circular reflection to an antiholomorphic map away from its one pole. Vanishing smooth coefficient defects give the local Morera identity.

  1. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedLimit_holomorphic line 19