OAI/Geometry/SurfaceImmersion/Correction/ArbitraryPhasePolynomial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The polynomial conjugation estimate and its real realization for an arbitrary smooth phase, before changing to a first-coordinate chart.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.phaseCoordinatePolynomialOperator line 16
  2. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.phaseCoordinatePolynomialOperator_bounds line 26
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.phaseCoordinatePolynomialOperator_realization line 55