OAI/Geometry/SurfaceImmersion/Atlas/QuadraticJetCutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The local quadratic correction in the finite-point spherical preparation. The cutoff leaves its prescribed second jet unchanged.

  1. def OAI.ClosedSurfaceR4.SphericalJets.quadraticCorrection line 12
  2. lemma OAI.ClosedSurfaceR4.SphericalJets.quadraticCorrection_smooth line 15
  3. lemma OAI.ClosedSurfaceR4.SphericalJets.quadraticCorrection_fderiv line 21
  4. lemma OAI.ClosedSurfaceR4.SphericalJets.quadraticCorrection_second line 34
  5. def OAI.ClosedSurfaceR4.SphericalJets.cutoffQuadratic line 45
  6. lemma OAI.ClosedSurfaceR4.SphericalJets.cutoffQuadratic_smooth line 48
  7. lemma OAI.ClosedSurfaceR4.SphericalJets.cutoffQuadratic_germ line 52
  8. lemma OAI.ClosedSurfaceR4.SphericalJets.cutoffQuadratic_jets line 57
  9. lemma OAI.ClosedSurfaceR4.SphericalJets.cutoffQuadratic_tsupport line 69
  10. lemma OAI.ClosedSurfaceR4.SphericalJets.cutoffQuadratic_compact line 76