The action of a geodesic segment

A constant-speed geodesic has constant metric derivative on the interior of its parameter interval. Consequently its p-action is exactly the pth power of the distance between its endpoints. This is the pathwise identity used when dynamic plans are concentrated on minimizing geodesics.

Conversely, the Hölder estimate bounds the p-action of every absolutely continuous curve on [0, 1] below by d(γ 0, γ 1) ^ p, and for 1 < p the curves attaining this bound are exactly the constant-speed geodesic segments (AbsolutelyContinuousOnInterval.isGeodesicSegment_of_curveAction_le). This rigidity is what forces the paths of a dynamic plan of minimal action to be geodesics. It fails for p = 1, where every monotone reparametrisation of a geodesic has the same action.

theorem TauCeti.IsGeodesicSegment.metricDerivative_eq {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : metricDerivative γ t = ENNReal.ofReal (dist x y)

On the interior of its parameter interval, a constant-speed geodesic segment has metric derivative equal to the distance between its endpoints.

theorem TauCeti.IsGeodesicSegment.curveAction_eq {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) (p : ℝ) : curveAction p γ 0 1 = ENNReal.ofReal (dist x y) ^ p

The p-action of a constant-speed geodesic segment is the pth power of the distance between its endpoints. The values of the metric derivative at the two endpoints do not affect the integral.

theorem TauCeti.IsGeodesicSegment.absolutelyContinuousOnInterval {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) : AbsolutelyContinuousOnInterval γ 0 1

A geodesic segment is absolutely continuous on [0, 1], being Lipschitz there.

theorem AbsolutelyContinuousOnInterval.curveAction_zero_eq_mul_of_curveAction_le {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {p : ℝ} (hγ : AbsolutelyContinuousOnInterval γ 0 1) (hp : 1 < p) (h : TauCeti.curveAction p γ 0 1 ≤ edist (γ 0) (γ 1) ^ p) {s : ℝ} (hs : s ∈ Set.Icc 0 1) : TauCeti.curveAction p γ 0 s = ENNReal.ofReal (s * dist (γ 0) (γ 1) ^ p)

Minimal action is spent at a constant rate. For 1 < p, if a curve absolutely continuous on [0, 1] has p-action at most d(γ 0, γ 1) ^ p, then its p-action on [0, s] is s * d(γ 0, γ 1) ^ p for every s ∈ [0, 1].

theorem AbsolutelyContinuousOnInterval.isGeodesicSegment_of_curveAction_le {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {p : ℝ} (hγ : AbsolutelyContinuousOnInterval γ 0 1) (hp : 1 < p) (h : TauCeti.curveAction p γ 0 1 ≤ edist (γ 0) (γ 1) ^ p) : TauCeti.IsGeodesicSegment γ (γ 0) (γ 1)

Curves of minimal action are geodesics. For 1 < p, an absolutely continuous curve on [0, 1] whose p-action is at most d(γ 0, γ 1) ^ p is a constant-speed geodesic segment from γ 0 to γ 1. Together with the Hölder estimate and IsGeodesicSegment.curveAction_eq, the geodesic segments are exactly the absolutely continuous curves on [0, 1] attaining the lower bound d(γ 0, γ 1) ^ p ≤ A_p(γ).