OAI/Geometry/SurfaceImmersion/Atlas/WeightedInverseSqrt.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial weighted bounds for normalization by a positive square root.

  1. lemma OAI.ClosedSurfaceR4.WeightedEstimates.norm_iteratedFDerivWithin_inverse_half line 11
  2. lemma OAI.ClosedSurfaceR4.WeightedEstimates.inverse_half_power_bound line 18
  3. theorem OAI.ClosedSurfaceR4.WeightedEstimates.weighted_inverse_sqrt line 38