VelocityPlane.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The normal-plane projection used in the velocity-circle construction.

abbrev OAI.ClosedSurfaceR4.VelocityPlane.Space line 11
def OAI.ClosedSurfaceR4.VelocityPlane.tangentPlane line 13
def OAI.ClosedSurfaceR4.VelocityPlane.oldNormal line 16
def OAI.ClosedSurfaceR4.VelocityPlane.velocityPlane line 18
lemma OAI.ClosedSurfaceR4.VelocityPlane.left_mem_tangent line 20
lemma OAI.ClosedSurfaceR4.VelocityPlane.right_mem_tangent line 23
lemma OAI.ClosedSurfaceR4.VelocityPlane.coefficients_eq_zero line 26
theorem OAI.ClosedSurfaceR4.VelocityPlane.projection_kernel_on_oldNormal line 34
Source documentation
A nonzero longitudinal Hessian coefficient makes projection onto the new velocity plane injective on the old normal plane.
```
theorem projection_kernel_on_oldNormal {X Y B C n : Space} {a b : ℝ}
    (hXY : LinearIndependent ℝ ![X, Y]) (ha : a ≠ 0)
    (hB : B ∈ oldNormal X Y) (hC : C = a • X + b • Y + B)
    (hn : n ∈ oldNormal X Y)
    (hp : (velocityPlane Y C).starProjection n = 0) : n = 0 := by
…
```
Mentions: OAI.ClosedSurfaceR4.VelocityPlane.Space, OAI.ClosedSurfaceR4.VelocityPlane.oldNormal, OAI.ClosedSurfaceR4.VelocityPlane.velocityPlane
theorem OAI.ClosedSurfaceR4.VelocityPlane.projection_injective_on_oldNormal line 64
theorem OAI.ClosedSurfaceR4.VelocityPlane.projected_normal_ne_zero line 74
theorem OAI.ClosedSurfaceR4.VelocityPlane.projected_second_form line 83
Source documentation
The projected old second form points oppositely to the projected longitudinal tangent when the longitudinal Hessian coefficient is positive.
```
theorem projected_second_form {X Y B C : Space} {a b : ℝ}
    (hC : C = a • X + b • Y + B) :
    (velocityPlane Y C).starProjection B =
      -a • (velocityPlane Y C).starProjection X := by
…
```
Mentions: OAI.ClosedSurfaceR4.VelocityPlane.Space, OAI.ClosedSurfaceR4.VelocityPlane.velocityPlane

theorem OAI.ClosedSurfaceR4.VelocityPlane.leading_metric line 106

Source documentation

Replacing the projected velocity by a longer vector in the same plane adds precisely a rank-one term to the metric.

theorem leading_metric {X Y C V : Space} {a : ℝ}
    (hV : V ∈ velocityPlane Y C)
    (hR : ‖V‖ ^ 2 = ‖(velocityPlane Y C).starProjection X‖ ^ 2 + a ^ 2) :
    ‖X - (velocityPlane Y C).starProjection X + V‖ ^ 2 = ‖X‖ ^ 2 + a ^ 2 ∧
      inner ℝ (X - (velocityPlane Y C).starProjection X + V) Y = inner ℝ X Y := by
…

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