OAI/Geometry/SurfaceImmersion/Whitney/CollarVelocityTurns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact turning positions for the collar arc, including after reparametrization.

  1. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_of_sin_eq_zero line 10
  2. lemma OAI.ClosedSurfaceR4.CollarVelocity.inverseClock_of_sin_eq_zero line 13
  3. lemma OAI.ClosedSurfaceR4.CollarVelocity.sin_inverseClock_eq_zero_iff line 18
  4. lemma OAI.ClosedSurfaceR4.CollarVelocity.deriv_angle_eq_zero_iff_sin line 28
  5. theorem OAI.ClosedSurfaceR4.CollarVelocity.angle_two_turns line 33

    Source documentation

    There are precisely two turns in one half-open period.

    theorem angle_two_turns {a θ : ℝ} (ha : a ≠ 0) (hθ : θ ∈ Set.Ico 0 (2 * Real.pi)) :
    deriv (angle a) θ = 0 ↔ θ = 0 ∨ θ = Real.pi := by
…

    Mentions: OAI.ClosedSurfaceR4.CollarVelocity.angle

  6. lemma OAI.ClosedSurfaceR4.CollarVelocity.angle_zero line 49
  7. lemma OAI.ClosedSurfaceR4.CollarVelocity.angle_pi line 52