OAI/NumberTheory/CubicMoment/Theta/CubicThetaEuclideanSmoothing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Smooth approximation of compact C1 coordinate functions, controlling both the value and the actual first derivative.

  1. def OAI.CubicFirstMoment.cubicThetaCoordinateSmooth line 17
  2. lemma OAI.CubicFirstMoment.cubicThetaCoordinateSmooth_contDiff line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaCoordinateSmooth_compact line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaCoordinateSmooth_support line 31
  5. lemma OAI.CubicFirstMoment.cubicThetaCoordinateSmooth_fderiv line 40
  6. lemma OAI.CubicFirstMoment.cubicThetaCoordinateSmooth_exists line 50