OAI/Geometry/SurfaceImmersion/Correction/ChartedMetricMean.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Global supported metric mean fields for the actual charted free seed.

  1. lemma OAI.ClosedSurfaceR4.RealModes.normalizedPerturbedMean_smooth_general line 13
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.metricMeanFieldInChart line 30
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.metricMeanField line 41
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.metricMeanField_apply line 45
  5. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.metricMeanField_bound line 50