OAI/Geometry/SurfaceImmersion/Atlas/AtlasPhaseJetBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted two-jet estimates in a fixed phase chart from the global input norm.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseChart_twoJet_bound line 17