OAI/Analysis/CircleDomains/Reflection/AnalyticJordanPhysicalContinuation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The continuation of a circularization map on an open neighborhood in the original source plane, with the chart inverse constructed.

  1. lemma OAI.CircleDomainRigidity.analytic_jordan_physical_continuation_sides line 13
  2. lemma OAI.CircleDomainRigidity.analytic_jordan_physical_continuation line 75