OAI/Analysis/CircleDomains/Reflection/CircleSchwarzReflection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local holomorphic continuation across a real interval whose image lies on a circle. The continuation is constructed by Cayley coordinates and the proved real-axis reflection principle.

  1. lemma OAI.CircleDomainRigidity.exists_local_circle_reflection line 14