OAI/Geometry/SurfaceImmersion/Correction/ChartedFreeFamily.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual finite free oscillation and its original-coordinate linear residual. The constants precede the immersion and scales.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.chartedFreeSum line 21
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.chartedFreeSum_eq line 26
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.chartedFreeSum_smooth_support line 30
  4. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_charted_free_family line 45
  5. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_charted_free_family_all_inputs line 89