OAI/Analysis/CircleDomains/Sobolev/StereographicDerivativeBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Decay of the derivative of the fixed inverse stereographic map. This supplies the spherical weight missing from a compact-chart bound.

  1. theorem OAI.CircleDomainRigidity.stereoInvFunAux_eq_centered line 16
  2. theorem OAI.CircleDomainRigidity.stereographic_scalar_bound line 28
  3. theorem OAI.CircleDomainRigidity.stereoInvFunAux_fderiv_apply line 41
  4. theorem OAI.CircleDomainRigidity.norm_stereoInvFunAux_fderiv_apply line 72