OAI/Geometry/SurfaceImmersion/Correction/PolynomialForcingRepresentation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The polynomial right-hand sides coincide with those in the actual triangular metric-cancellation recursion.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_mixedForcing line 14
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_longitudinalForcing line 30
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_transverseForcing line 43