OAI/Geometry/SurfaceImmersion/Primitive/BoundedPrimitiveAmplitude.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform inverse and amplitude bounds from the fixed reference size and positive coefficient margin. Inactive chart coefficients need not vary continuously.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundedPrimitiveReference line 30
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundedPrimitiveReference_compact line 34
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundedPrimitiveReference_good line 46
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.bounded_primitive_amplitude_C1 line 54