Geodesic phase equation

A geodesic for the connection D + σ K is an integral curve of the phase field (x,v) ↦ (v, -σ K_x(v,v)). This file proves local initial-value existence from smooth coefficients. It does not assume parameter regularity.

@[reducible, inline]

abbrev PlanarMidpoint.Phase : Type

Position and velocity in the product normed phase space.

Equations

• PlanarMidpoint.Phase = (PlanarMidpoint.E × PlanarMidpoint.E)

def PlanarMidpoint.phaseField (C : E → Coeff) (σ : ℝ) (z : Phase) : Phase

The acceleration field of the affine geodesic equation.

Equations

• PlanarMidpoint.phaseField C σ z = (z.2, -σ • PlanarMidpoint.K (C z.1) z.2 z.2)

theorem PlanarMidpoint.contDiffAt_K {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] {n : WithTop ℕ∞} {c : A → Coeff} {u v : A → E} {x : A} (hc : ContDiffAt ℝ n c x) (hu : ContDiffAt ℝ n u x) (hv : ContDiffAt ℝ n v x) : ContDiffAt ℝ n (fun (y : A) => K (c y) (u y) (v y)) x

theorem PlanarMidpoint.contDiffAt_phaseField {C : E → Coeff} {p v : E} {n : WithTop ℕ∞} (hC : ContDiffAt ℝ n C p) (σ : ℝ) : ContDiffAt ℝ n (phaseField C σ) (p, v)

theorem PlanarMidpoint.exists_local_geodesic {C : E → Coeff} {p v : E} (hC : ContDiffAt ℝ 1 C p) (σ t₀ : ℝ) : ∃ (z : ℝ → Phase), z t₀ = (p, v) ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt z (phaseField C σ (z t)) t

theorem PlanarMidpoint.geodesic_components {C : E → Coeff} {σ : ℝ} {z : ℝ → Phase} {t : ℝ} (hz : HasDerivAt z (phaseField C σ (z t)) t) : HasDerivAt (fun (s : ℝ) => (z s).1) (z t).2 t ∧ HasDerivAt (fun (s : ℝ) => (z s).2) (-σ • K (C (z t).1) (z t).2 (z t).2) t

theorem PlanarMidpoint.local_geodesic_unique {C : E → Coeff} {p v : E} {σ t₀ : ℝ} (hC : ContDiffAt ℝ 1 C p) {z w : ℝ → Phase} (hz₀ : z t₀ = (p, v)) (hw₀ : w t₀ = (p, v)) (hz : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt z (phaseField C σ (z t)) t) (hw : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt w (phaseField C σ (w t)) t) : z =ᶠ[nhds t₀] w

Two actual geodesics with the same initial phase have the same local germ.

@[simp]

theorem PlanarMidpoint.phaseField_zero (C : E → Coeff) (σ : ℝ) (p : E) : phaseField C σ (p, 0) = 0

theorem PlanarMidpoint.constant_geodesic (C : E → Coeff) (σ : ℝ) (p : E) (t : ℝ) : HasDerivAt (fun (x : ℝ) => (p, 0)) (phaseField C σ (p, 0)) t

The constant curve is the geodesic with zero initial velocity.

theorem PlanarMidpoint.hasStrictFDerivAt_acceleration_zero {C : E → Coeff} {p : E} (hC : ContDiffAt ℝ 1 C p) (σ : ℝ) : HasStrictFDerivAt (fun (z : Phase) => -σ • K (C z.1) z.2 z.2) 0 (p, 0)

The acceleration has zero strict derivative at every zero-velocity phase. Consequently its local Lipschitz constant can be made arbitrarily small.