OAI/Geometry/SurfaceImmersion/Correction/AtlasSupportedPolynomialQuadratic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.second_variation_zero_of_notMem line 29

   Source documentation

   A quadratic variation vanishes wherever its varying field vanishes as a germ.

   lemma second_variation_zero_of_notMem (e : Expression) (G : Base → JetPolynomial.Space)
       {H : Base → JetPolynomial.Space} {p : Base} (hp : p ∉ tsupport H) (t : ℝ) :
       (e.variations 1).eval ![G,H,H,0] (p,t) = 0 := by
   …

   Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Space

2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialQuadratic_zero_of_notMem line 48
3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.supported_polynomial_quadratic line 78
4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restored_polynomial_quadratic line 122