OAI/Geometry/SurfaceImmersion/Correction/CombinedZeroMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identify the actual local quadratic zero phase with the leading tensor plus the combined mean correction.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.seedQuadraticMeanTensor line 16
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.seedQuadraticMeanTensor_eq line 29
  3. def OAI.ClosedSurfaceR4.PhaseMean.localQuadraticMean line 55
  4. lemma OAI.ClosedSurfaceR4.PhaseMean.localQuadraticMean_eq line 63