OAI/Geometry/SurfaceImmersion/Correction/ChartedAdjustedMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual original-coordinate quadratic mean after finite substitution. The threshold in this statement still concerns fixed scale data.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.chartedFamilyMean_smooth line 20
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.charted_quadratic_mean_residual line 24
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.finite_charted_adjusted_quadratic_mean line 39