OAI/Geometry/SurfaceImmersion/Correction/JetPolynomialScalar.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Scalar polynomial representations of the finite metric coefficients.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.Represents line 12
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.scale line 16
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.sumFinset line 19
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_scale line 22
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_scale line 25
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_scale line 26
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_scale line 28
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.represents_add line 31
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.represents_scale line 37
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.represents_fluct line 43
  11. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.represents_sumFinset line 53
  12. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_sumFinset line 63
  13. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_sumFinset_le line 69
  14. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_sumFinset_le line 75
  15. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.represents_dot line 81