OAI/Geometry/SurfaceImmersion/Primitive/VelocityNormalGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The angular derivative contributes only to the complementary normal component.

  1. def OAI.ClosedSurfaceR4.VelocityFrame.direction line 12
  2. def OAI.ClosedSurfaceR4.VelocityFrame.angularDirection line 13
  3. lemma OAI.ClosedSurfaceR4.VelocityFrame.direction_unit line 15
  4. lemma OAI.ClosedSurfaceR4.VelocityFrame.angularDirection_unit line 22
  5. lemma OAI.ClosedSurfaceR4.VelocityFrame.direction_angular_perp line 30
  6. lemma OAI.ClosedSurfaceR4.VelocityFrame.angularDirection_perp line 38
  7. lemma OAI.ClosedSurfaceR4.VelocityFrame.dot_normalPart_eq line 42
  8. lemma OAI.ClosedSurfaceR4.VelocityFrame.dot_leadingTangent_zero line 46
  9. lemma OAI.ClosedSurfaceR4.VelocityFrame.angularDirection_normal_perp line 52
  10. lemma OAI.ClosedSurfaceR4.VelocityFrame.first_normal_derivative_independent line 71

    Source documentation

    The first normal coefficient does not contain the angular derivative.

    lemma first_normal_derivative_independent {W m n : Vec} (hmn : m ⬝ᵥ n = 0) (R d : ℝ) :
    (W + (R * d) • m) ⬝ᵥ n = W ⬝ᵥ n := by
…
  11. lemma OAI.ClosedSurfaceR4.VelocityFrame.second_normal_derivative line 76

    Source documentation

    The complementary normal coefficient contains that derivative with coefficient R.

    lemma second_normal_derivative {W m : Vec} (hm : m ⬝ᵥ m = 1) (R d : ℝ) :
    (W + (R * d) • m) ⬝ᵥ m = R * d + W ⬝ᵥ m := by
…