OAI/Geometry/SurfaceImmersion/Correction/ChartedUniformFree.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform size and full-linearization residuals for the actual free oscillation used by the charted mean construction.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.displacement line 21
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.displacement_smooth_support line 25
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_charted_free_bounds line 33