OAI/Geometry/SurfaceImmersion/Whitney/CollarVelocityReparam.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The collar velocity has the desired uniform mean after reparametrization.

  1. def OAI.ClosedSurfaceR4.CollarVelocity.reparamX line 12
  2. def OAI.ClosedSurfaceR4.CollarVelocity.reparamY line 13
  3. lemma OAI.ClosedSurfaceR4.CollarVelocity.reparamX_smooth line 15
  4. lemma OAI.ClosedSurfaceR4.CollarVelocity.reparamY_smooth line 18
  5. lemma OAI.ClosedSurfaceR4.CollarVelocity.reparam_unit line 21
  6. lemma OAI.ClosedSurfaceR4.CollarVelocity.reparamX_periodic line 24
  7. lemma OAI.ClosedSurfaceR4.CollarVelocity.reparamY_periodic line 29
  8. lemma OAI.ClosedSurfaceR4.CollarVelocity.reparamX_zero line 34
  9. lemma OAI.ClosedSurfaceR4.CollarVelocity.reparamY_zero line 35
  10. lemma OAI.ClosedSurfaceR4.CollarVelocity.mean_reparam line 37
  11. lemma OAI.ClosedSurfaceR4.CollarVelocity.mean_reparamX line 58
  12. lemma OAI.ClosedSurfaceR4.CollarVelocity.mean_reparamY line 63
  13. theorem OAI.ClosedSurfaceR4.CollarVelocity.reparametrized_velocity_means line 68

    Source documentation

    The unweighted reparametrized velocity has exactly the required mean.

    theorem reparametrized_velocity_means {R v a : ℝ} (hR : 0 < R) (hv : 0 < v)
    (hquad : R ^ 2 = v ^ 2 + a ^ 2) :
    circleMean (fun θ => R * reparamX (amplitude R v a) θ) = v ∧
    circleMean (fun θ => R * reparamY (amplitude R v a) θ) = 0 := by
…

    Mentions: OAI.ClosedSurfaceR4.CollarVelocity.circleMean, OAI.ClosedSurfaceR4.CollarVelocity.reparamX, OAI.ClosedSurfaceR4.CollarVelocity.amplitude, OAI.ClosedSurfaceR4.CollarVelocity.reparamY