OAI/Geometry/SurfaceImmersion/Whitney/CollarDensityMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact unit-period moment equations for the prescribed collar density.

  1. def OAI.ClosedSurfaceR4.CollarVelocity.unitDensity line 12
  2. lemma OAI.ClosedSurfaceR4.CollarVelocity.unitDensity_smooth line 14
  3. lemma OAI.ClosedSurfaceR4.CollarVelocity.unitDensity_pos line 17
  4. lemma OAI.ClosedSurfaceR4.CollarVelocity.unitDensity_periodic line 19
  5. lemma OAI.ClosedSurfaceR4.CollarVelocity.unitDensity_zero line 25
  6. lemma OAI.ClosedSurfaceR4.CollarVelocity.blendedPath_collar line 27
  7. lemma OAI.ClosedSurfaceR4.CollarVelocity.collar_density_moments line 31