OAI/Geometry/SurfaceImmersion/Atlas/GridIncrementEnvelope.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Polynomial envelopes for the full free/forced grid increment.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridInteractionCount line 10
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridInteractionCount_nonneg line 12
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridInteractionCount_mono line 15
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridIncrementSize line 20
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridIncrementError line 23
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridInteractionCount_polynomial line 29
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridIncrementSize_polynomial line 33
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridIncrementError_polynomial line 39
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridIncrementSize_bound line 51
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gridIncrementError_bound line 60