OAI/Analysis/CircleDomains/Topology/LimitSphereExtension.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Extending a principally normalized limit across infinity

The uniform principal remainder does more than prevent a constant limit: it gives continuity on the sphere and chart derivative one at infinity. This step needs no further analytic input.

  1. def OAI.CircleDomainRigidity.extendAtInfinity line 20
  2. theorem OAI.CircleDomainRigidity.extendAtInfinity_infty line 23
  3. theorem OAI.CircleDomainRigidity.extendAtInfinity_coe line 26
  4. theorem OAI.CircleDomainRigidity.principal_remainder_tendsto_zero line 29
  5. theorem OAI.CircleDomainRigidity.principal_tendsto_cobounded line 34
  6. theorem OAI.CircleDomainRigidity.continuousAt_extendAtInfinity_infty line 51
  7. theorem OAI.CircleDomainRigidity.hasDerivAt_extendAtInfinity_chart line 62
  8. theorem OAI.CircleDomainRigidity.isConformalAt_extendAtInfinity_infty line 94
  9. theorem OAI.CircleDomainRigidity.isPrincipalNormalized_extendAtInfinity line 100