OAI/Analysis/CircleDomains/Reflection/AnalyticStraighteningResidual.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual pulled-back principal approximants have antiholomorphic error tending strongly to zero on the original analytic domain.

  1. def OAI.CircleDomainRigidity.AnalyticReflectionData.straighteningApproximation line 19
  2. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.exists_straightening_residual line 22