OAI/Geometry/SurfaceImmersion/Primitive/VelocityNormalNonvanishing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The old second derivative has a nonzero normal component after changing velocity.

  1. lemma OAI.ClosedSurfaceR4.VelocityFrame.gram_ne_zero_of_projection line 12
  2. lemma OAI.ClosedSurfaceR4.VelocityFrame.normalPart_ne_zero_of_projection line 28
  3. def OAI.ClosedSurfaceR4.VelocityFrame.leadingTangent line 50
  4. lemma OAI.ClosedSurfaceR4.VelocityFrame.leadingTangent_projection line 52
  5. theorem OAI.ClosedSurfaceR4.VelocityFrame.leading_normal_nondegenerate line 63

    Source documentation

    Neither the leading tangent pair nor the normal component of C degenerates.

    theorem leading_normal_nondegenerate {X Y C V : Vec} (hD : gramDet Y C ≠ 0)
    (hYV : Y ⬝ᵥ V = 0) (hCV : C ⬝ᵥ V = 0) (hV : V ≠ 0) :
    gramDet (leadingTangent X Y C V) Y ≠ 0 ∧
      realNormalPart (leadingTangent X Y C V) Y C ≠ 0 := by
…

    Mentions: OAI.ClosedSurfaceR4.VelocityFrame.leadingTangent