OAI/Geometry/SurfaceImmersion/Whitney/CollarVelocity.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

An explicit small circular arc and positive averaging density. This gives an alternative collar construction without solving a squared-amplitude equation.

  1. def OAI.ClosedSurfaceR4.CollarVelocity.arcX line 13

    Source documentation

    Rational parametrization of a small arc around (1,0).

    def arcX (a t : ℝ) : ℝ := (1 - (a * Real.cos t) ^ 2) / (1 + (a * Real.cos t) ^ 2)
  2. def OAI.ClosedSurfaceR4.CollarVelocity.arcY line 14
  3. def OAI.ClosedSurfaceR4.CollarVelocity.density line 17

    Source documentation

    A positive density that makes the two mean constraints elementary.

    def density (a t : ℝ) : ℝ := (1 + (a * Real.cos t) ^ 2) / (1 + a ^ 2 / 2)
  4. lemma OAI.ClosedSurfaceR4.CollarVelocity.arcDen_pos line 19
  5. lemma OAI.ClosedSurfaceR4.CollarVelocity.densityDen_pos line 20
  6. lemma OAI.ClosedSurfaceR4.CollarVelocity.arc_unit line 22
  7. lemma OAI.ClosedSurfaceR4.CollarVelocity.density_pos line 27
  8. lemma OAI.ClosedSurfaceR4.CollarVelocity.density_mul_arcX line 30
  9. lemma OAI.ClosedSurfaceR4.CollarVelocity.density_mul_arcY line 35
  10. lemma OAI.ClosedSurfaceR4.CollarVelocity.arcX_zero line 40
  11. lemma OAI.ClosedSurfaceR4.CollarVelocity.arcY_zero line 41
  12. lemma OAI.ClosedSurfaceR4.CollarVelocity.density_zero line 42
  13. lemma OAI.ClosedSurfaceR4.CollarVelocity.arcX_smooth line 44
  14. lemma OAI.ClosedSurfaceR4.CollarVelocity.arcY_smooth line 49
  15. lemma OAI.ClosedSurfaceR4.CollarVelocity.density_smooth line 54
  16. lemma OAI.ClosedSurfaceR4.CollarVelocity.arcX_periodic line 59
  17. lemma OAI.ClosedSurfaceR4.CollarVelocity.arcY_periodic line 63
  18. lemma OAI.ClosedSurfaceR4.CollarVelocity.density_periodic line 67