OAI/Analysis/CircleDomains/Reflection/SmoothReflectedApproximation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The conjugated smooth reflections are smooth on every fixed compact set off the limiting pole, after a finite initial segment.

  1. lemma OAI.CircleDomainRigidity.roundReflectionPlane_contDiffAt line 13
  2. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedApproximation_contDiffAt line 27
  3. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.eventually_reflectedApproximation_contDiffOn line 35