OAI/Geometry/SurfaceImmersion/Correction/JetPolynomialIntegral.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Angular derivatives, averaging, and normalized primitives act only on smooth low-jet coefficients, preserving polynomial jet order and scale loss.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_slice_smooth line 16
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.angle line 26
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.mean line 28
  4. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.primitive line 31
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_angle line 34
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_mean line 38
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_primitive line 45
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_angle line 49
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_angle line 50
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_mean line 51
  11. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_mean line 52
  12. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_primitive line 53
  13. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_primitive line 54
  14. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_angle line 56
  15. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_mean line 72
  16. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.normalizedPrimitive_const_mul line 87
  17. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.normalizedPrimitive_add line 92
  18. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_primitive line 104