OAI/Geometry/SurfaceImmersion/Correction/ConjugatedPolynomialOperator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The oscillatory estimates apply to the actual conjugated polynomial linearization on supported smooth fields.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.iteratedDirectional_zero line 16
  2. def OAI.ClosedSurfaceR4.JetPolynomial.singlePhase line 23
  3. def OAI.ClosedSurfaceR4.JetPolynomial.singleDirection line 24
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.singlePhase_smooth line 26
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.singleDirection_smooth line 34
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.single_oscillatoryData line 42
  7. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.conjugatedVariationLM line 58
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.conjugatedVariationLM_apply line 67