OAI/Analysis/CircleDomains/Reflection/ReflectedApproximationLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual conjugated smooth reflections converge locally uniformly off the limiting pole. This follows from both retained principal-map limits.

  1. lemma OAI.CircleDomainRigidity.locallyUniform_joint_tendsto line 13
  2. def OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedLimit line 22
  3. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedLimit_continuousAt line 25
  4. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedApproximation_tendsto line 34