OAI/Geometry/SurfaceImmersion/Primitive/SupportedPrimitiveExpansion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite recursion supplies the same supported coefficients for the actual primitive and its full tensor remainder. Both losses are fixed before the differentiation order and before the slow map.

  1. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.supported_primitive_expansion line 15