VelocityCircleLift.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Lift a normalized planar loop to the actual four-dimensional velocity plane, retaining its exact mean, length, and leading metric.

def OAI.ClosedSurfaceR4.VelocityFrame.planeLift line 15
Source documentation
The fixed orthonormal-plane inclusion, written as a continuous linear map.
```
def planeLift (e₁ e₂ : Vec) : LoopDensity.Plane →L[ℝ] Vec :=
…
```
Mentions: OAI.ClosedSurfaceR4.LoopDensity.Plane
lemma OAI.ClosedSurfaceR4.VelocityFrame.planeLift_apply line 18
lemma OAI.ClosedSurfaceR4.VelocityFrame.planeLift_unit line 21
lemma OAI.ClosedSurfaceR4.VelocityFrame.planeLift_perp line 30
lemma OAI.ClosedSurfaceR4.VelocityFrame.planeLift_scaled_length line 34
lemma OAI.ClosedSurfaceR4.VelocityFrame.planeLift_mean line 42

theorem OAI.ClosedSurfaceR4.VelocityFrame.real_leading_metric line 52

Source documentation

The real coordinate form of the leading rank-one metric identity.

theorem real_leading_metric {X Y C V : Vec} {a : ℝ}
    (hD : gramDet Y C ≠ 0) (hYV : Y ⬝ᵥ V = 0) (hCV : C ⬝ᵥ V = 0)
    (hR : V ⬝ᵥ V = realNormalPart Y C X ⬝ᵥ realNormalPart Y C X + a ^ 2) :
    leadingTangent X Y C V ⬝ᵥ leadingTangent X Y C V = X ⬝ᵥ X + a ^ 2 ∧
      leadingTangent X Y C V ⬝ᵥ Y = X ⬝ᵥ Y := by
…

Mentions: OAI.ClosedSurfaceR4.VelocityFrame.leadingTangent