Canonical short geodesics by a Dirichlet contraction

A bounded Dirichlet Green operator and a sufficiently small local Lipschitz constant produce a unique phase path in a closed ball about the constant zero-velocity path. This supplies the local endpoint problem.

def PlanarMidpoint.BallPath {T : Type u_1} {V : Type u_2} [TopologicalSpace T] [CompactSpace T] [NormedAddCommGroup V] (p : V) (r : ℝ) : Set C(T, V)

Continuous paths restricted to one complete closed sup-norm ball.

Equations

• PlanarMidpoint.BallPath p r = Metric.closedBall (ContinuousMap.const T p) r

theorem PlanarMidpoint.path_mem_ball {T : Type u_1} {V : Type u_2} [TopologicalSpace T] [CompactSpace T] [NormedAddCommGroup V] {p : V} {r : ℝ} (y : ↑(BallPath p r)) (t : T) : ↑y t ∈ Metric.closedBall p r

def PlanarMidpoint.composeBallPath {T : Type u_1} {V : Type u_2} {W : Type u_3} [TopologicalSpace T] [CompactSpace T] [NormedAddCommGroup V] [NormedAddCommGroup W] {p : V} {r : ℝ} {F : V → W} {L : NNReal} (hF : LipschitzOnWith L F (Metric.closedBall p r)) (y : ↑(BallPath p r)) : C(T, W)

Composition is continuous because the path stays in the region where its vector field is Lipschitz.

Equations

• PlanarMidpoint.composeBallPath hF y = { toFun := F ∘ ⇑↑y, continuous_toFun := ⋯ }

theorem PlanarMidpoint.exists_unique_green_path {T : Type u_1} {V : Type u_2} {W : Type u_3} [TopologicalSpace T] [CompactSpace T] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [NormedSpace ℝ W] (G : C(T, W) →L[ℝ] C(T, V)) (p : V) (r : ℝ) (hr : 0 ≤ r) (F : V → W) (L : NNReal) (hF : LipschitzOnWith L F (Metric.closedBall p r)) (hFp : F p = 0) (hsmall : ‖G‖ * ↑L ≤ 1 / 2) (a : C(T, V)) (ha : dist a (ContinuousMap.const T p) ≤ r / 2) : ∃! y : ↑(BallPath p r), ↑y = a + G (composeBallPath hF y)

Banach's theorem for the nonlinear Dirichlet equation in phase-path space.

def PlanarMidpoint.affinePhase (P Q : E) : PhasePath

The position and velocity of the affine chord joining two endpoints.

Equations

• PlanarMidpoint.affinePhase P Q = { toFun := fun (t : ↑PlanarMidpoint.UnitInterval) => (P + ↑t • (Q - P), Q - P), continuous_toFun := ⋯ }

theorem PlanarMidpoint.affinePhase_near (p P Q : E) {r : ℝ} (hr : 0 ≤ r) (hP : dist P p ≤ r / 8) (hQ : dist Q p ≤ r / 8) : dist (affinePhase P Q) (ContinuousMap.const ↑UnitInterval (p, 0)) ≤ r / 2

noncomputable def PlanarMidpoint.bvpPosition (P Q : E) (a : AccelerationPath) (t : ℝ) : E

The affine endpoint chord plus the zero-endpoint Green correction.

Equations

• PlanarMidpoint.bvpPosition P Q a t = P + t • (Q - P) + PlanarMidpoint.greenPosition a t

noncomputable def PlanarMidpoint.bvpVelocity (P Q : E) (a : AccelerationPath) (t : ℝ) : E

The endpoint secant plus the velocity of the Green correction.

Equations

• PlanarMidpoint.bvpVelocity P Q a t = Q - P + PlanarMidpoint.greenVelocity a t

@[simp]

theorem PlanarMidpoint.bvpPosition_zero (P Q : E) (a : AccelerationPath) : bvpPosition P Q a 0 = P

@[simp]

theorem PlanarMidpoint.bvpPosition_one (P Q : E) (a : AccelerationPath) : bvpPosition P Q a 1 = Q

theorem PlanarMidpoint.hasDerivAt_bvpPosition (P Q : E) (a : AccelerationPath) (t : ℝ) : HasDerivAt (bvpPosition P Q a) (bvpVelocity P Q a t) t

theorem PlanarMidpoint.hasDerivAt_bvpVelocity (P Q : E) (a : AccelerationPath) (t : ℝ) : HasDerivAt (bvpVelocity P Q a) (pathExtend a t) t

theorem PlanarMidpoint.fixed_green_isGeodesic (C : E → Coeff) (σ : ℝ) (p P Q : E) (r : ℝ) {L : NNReal} (hF : LipschitzOnWith L (fun (z : Phase) => -σ • K (C z.1) z.2 z.2) (Metric.closedBall (p, 0) r)) (y : ↑(BallPath (p, 0) r)) (hy : ↑y = affinePhase P Q + greenOperator (composeBallPath hF y)) : IsGeodesicSegment C σ (bvpPosition P Q (composeBallPath hF y)) (bvpVelocity P Q (composeBallPath hF y)) ∧ ∀ (t : ℝ) (ht : t ∈ UnitInterval), (bvpPosition P Q (composeBallPath hF y) t, bvpVelocity P Q (composeBallPath hF y) t) = ↑y ⟨t, ht⟩

A fixed phase path produces an actual geodesic with the prescribed endpoints.

def PlanarMidpoint.segmentPhasePath {C : E → Coeff} {σ : ℝ} {γ v : ℝ → E} (hg : IsGeodesicSegment C σ γ v) : PhasePath

The phase path of an actual geodesic, restricted to the parameter interval.

Equations

• PlanarMidpoint.segmentPhasePath hg = { toFun := fun (t : ↑PlanarMidpoint.UnitInterval) => (γ ↑t, v ↑t), continuous_toFun := ⋯ }

theorem PlanarMidpoint.short_path_mem {C : E → Coeff} {σ : ℝ} {p P Q : E} {r : ℝ} (hr : 0 ≤ r) {γ v : ℝ → E} (h : IsShortGeodesic C σ p r P Q γ v) : segmentPhasePath ⋯ ∈ Metric.closedBall (ContinuousMap.const ↑UnitInterval (p, 0)) r

theorem PlanarMidpoint.actual_geodesic_is_fixed {C : E → Coeff} {σ : ℝ} {p P Q : E} {r : ℝ} (hr : 0 ≤ r) {L : NNReal} (hF : LipschitzOnWith L (fun (z : Phase) => -σ • K (C z.1) z.2 z.2) (Metric.closedBall (p, 0) r)) {γ v : ℝ → E} (h : IsShortGeodesic C σ p r P Q γ v) : have y := ⟨segmentPhasePath ⋯, ⋯⟩; ↑y = affinePhase P Q + greenOperator (composeBallPath hF y)

Every actual short geodesic satisfies the same Green fixed-point equation.

theorem PlanarMidpoint.exists_unique_short_geodesic {C : E → Coeff} {p : E} (hC : ContDiffAt ℝ 1 C p) (σ η : ℝ) (hη : 0 < η) : ∃ r > 0, r ≤ η ∧ ∃ δ > 0, ∀ (P Q : E), P ∈ Metric.ball p δ → Q ∈ Metric.ball p δ → ∃ (γ : ℝ → E) (v : ℝ → E), IsShortGeodesic C σ p r P Q γ v ∧ ∀ (γ' v' : ℝ → E), IsShortGeodesic C σ p r P Q γ' v' → ∀ t ∈ UnitInterval, γ' t = γ t ∧ v' t = v t

Every sufficiently close pair of endpoints has a unique short geodesic. The permitted phase radius can be chosen below any prescribed positive size.