OAI/Geometry/SurfaceImmersion/Primitive/AtlasJetProfiles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact jet ranges and coefficient bounds derived from the actual atlas input norms.

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