Local affine-parameter geodesic midpoints

The definition uses actual position and velocity curves satisfying the geodesic equation. Uniqueness is only asserted on the parameter interval and among short curves in the specified neighborhood. There is no regularity assumption on the dependence of the curves on their endpoints.

def PlanarMidpoint.IsGeodesicSegment (C : E → Coeff) (σ : ℝ) (γ v : ℝ → E) : Prop

Position and velocity curves satisfying the affine geodesic ODE on [0, 1].

Equations

• PlanarMidpoint.IsGeodesicSegment C σ γ v = ((∀ t ∈ Set.Icc 0 1, HasDerivAt γ (v t) t) ∧ ∀ t ∈ Set.Icc 0 1, HasDerivAt v (-σ • PlanarMidpoint.K (C (γ t)) (v t) (v t)) t)

def PlanarMidpoint.IsShortGeodesic (C : E → Coeff) (σ : ℝ) (p : E) (r : ℝ) (P Q : E) (γ v : ℝ → E) : Prop

A geodesic with prescribed endpoints and small position and velocity.

Equations

• PlanarMidpoint.IsShortGeodesic C σ p r P Q γ v = (PlanarMidpoint.IsGeodesicSegment C σ γ v ∧ γ 0 = P ∧ γ 1 = Q ∧ ∀ t ∈ Set.Icc 0 1, ‖γ t - p‖ < r ∧ ‖v t‖ < r)

def PlanarMidpoint.IsCanonicalLocalMidpoint (Ω : Set E) (C : E → Coeff) (σ : ℝ) (p : E) (r : ℝ) (W : Set (E × E)) (A : E → E → E) : Prop

A midpoint map supplied by the unique short geodesic near a diagonal point.

Equations

• One or more equations did not get rendered due to their size.

def PlanarMidpoint.LocalMidpointInvariance (Ω : Set E) (C : E → Coeff) : Prop

Complementarity of the canonical local midpoint maps of D+K and D-K near every diagonal point. The definition exposes the actual geodesic ODE.

Equations

• One or more equations did not get rendered due to their size.

def PlanarMidpoint.ArbitrarilyShortComplementaryPairs (C : E → Coeff) (p : E) : Prop

A formulation with arbitrarily small short curves, used only as an intermediate consequence of canonical midpoint invariance.

Equations

• One or more equations did not get rendered due to their size.