OAI/Geometry/SurfaceImmersion/Correction/NormalizedLinearModel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual first-order transverse model in normalized coordinates.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedAxisPolynomial line 12
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalTransverse line 14
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedLinearModel line 16
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedAxisPolynomial_smooth line 19
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalTransverse_smooth line 25
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedLinearModel_smooth line 29
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedLinearModel_axis line 34
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedAxisPolynomial_hasFDerivAt line 38
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedLinearModel_fderiv_axis line 52