Restricting canonical midpoint germs to arbitrarily small geodesic neighborhoods.
theorem
PlanarMidpoint.IsShortGeodesic.mono_radius
{C : E → Coeff}
{σ r s : ℝ}
{p P Q : E}
{γ v : ℝ → E}
(h : IsShortGeodesic C σ p r P Q γ v)
(hrs : r ≤ s)
:
IsShortGeodesic C σ p s P Q γ v
theorem
PlanarMidpoint.arbitrarilyShortPairs_of_canonical
{Ω : Set E}
{C : E → Coeff}
{p : E}
(hlocal : LocalMidpointInvariance Ω C)
(hp : p ∈ Ω)
(hexists :
∀ σ ∈ {1, -1},
∀ r > 0,
∃ δ > 0,
∀ (P Q : E),
P ∈ Metric.ball p δ → Q ∈ Metric.ball p δ → ∃ (γ : ℝ → E) (v : ℝ → E), IsShortGeodesic C σ p r P Q γ v)
:
Canonical uniqueness identifies all sufficiently small representatives. The small-solution existence premise is supplied by the local BVP theorem.