OAI/Geometry/SurfaceImmersion/Correction/PolynomialDiagonalVariations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The first three actual parameter derivatives of a polynomial along a map variation are its mixed variations with all directions equal.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.diagonalFamily line 15
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.diagonalFamily_smooth line 18
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.diagonalFamily_succ line 23
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.diagonal_angleDerivative line 25
  5. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.affinePolynomial line 37
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.affinePolynomial_smooth line 40
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.affinePolynomial_first line 45
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.affinePolynomial_second line 52
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.affinePolynomial_third line 61