OAI/Geometry/SurfaceImmersion/Correction/PolynomialMeanDifference.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Difference identity for the actual polynomial zero-phase mean.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticMeanPair_sub_left line 10
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticMeanPair_sub_right line 21
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticMeanCoefficient_difference line 32