CollarVelocityVector.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual collar velocity in an orthonormal frame of the velocity plane.

def OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop line 13
lemma OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop_average line 19
lemma OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop_norm_sq line 38
lemma OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop_mem line 55

theorem OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop_leading_metric line 61

Source documentation

The collar loop gives the exact leading metric required by the primitive addition.

theorem vectorLoop_leading_metric {X Y C e₁ e₂ : Space} {R v a : ℝ}
    (h₁ : ‖e₁‖ = 1) (h₂ : ‖e₂‖ = 1) (horth : inner ℝ e₁ e₂ = 0)
    (hp₁ : e₁ ∈ VelocityPlane.velocityPlane Y C)
    (hp₂ : e₂ ∈ VelocityPlane.velocityPlane Y C)
    (hproj : (VelocityPlane.velocityPlane Y C).starProjection X = v • e₁)
    (hquad : R ^ 2 = v ^ 2 + a ^ 2) (t : Period) :
    ‖X - v • e₁ + vectorLoop e₁ e₂ R v a t‖ ^ 2 = ‖X‖ ^ 2 + a ^ 2 ∧
      inner ℝ (X - v • e₁ + vectorLoop e₁ e₂ R v a t) Y = inner ℝ X Y := by
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.VelocityPlane.velocityPlane, OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop

lemma OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop_zero_amplitude line 76