OAI/Geometry/SurfaceImmersion/Primitive/VelocityAngleInterpolation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.CollarVelocity.blendedAngle line 11
2. lemma OAI.ClosedSurfaceR4.CollarVelocity.hasDerivAt_blendedAngle line 14
3. lemma OAI.ClosedSurfaceR4.CollarVelocity.blended_speed_positive line 25
4. lemma OAI.ClosedSurfaceR4.CollarVelocity.blended_deriv_eq_zero_iff line 36

   Source documentation

   All interpolation parameters preserve the same two stationary positions.

   lemma blended_deriv_eq_zero_iff {a A s : ℝ} (ha : 0 < a) (hA : 0 < A)
       (hs : 0 ≤ s) (hs1 : s ≤ 1) (h t : ℝ) :
       deriv (blendedAngle a A s h) t = 0 ↔ Real.sin t = 0 := by
   …

   Mentions: OAI.ClosedSurfaceR4.CollarVelocity.blendedAngle

5. lemma OAI.ClosedSurfaceR4.CollarVelocity.blendedAngle_zero line 42
6. lemma OAI.ClosedSurfaceR4.CollarVelocity.blendedAngle_pi line 47
7. lemma OAI.ClosedSurfaceR4.CollarVelocity.interior_angle_covers line 53

   Source documentation

   The interior angle covers every direction once its amplitude exceeds pi.

   lemma interior_angle_covers {A β : ℝ} (hA : Real.pi ≤ A)
       (hβ : β ∈ Set.Icc (-Real.pi) Real.pi) :
       ∃ t ∈ Set.Icc (0 : ℝ) Real.pi, A * Real.cos t = β := by
   …