English
The distance is symmetric: riemannianEDist I x y = riemannianEDist I y x.
Русский
Расстояние симметрично: d(x,y)=d(y,x).
LaTeX
$$riemannianEDist I x y = riemannianEDist I y x$$
Lean4
/-- The Riemannian edistance is bounded above by the length of any `C^1` path from `x` to `y`.
Here, we express this using a path defined on the whole real line, considered on
some interval `[a, b]`. -/
theorem riemannianEDist_le_pathELength {γ : ℝ → M} (hγ : ContMDiffOn 𝓘(ℝ) I 1 γ (Icc a b)) (ha : γ a = x) (hb : γ b = y)
(hab : a ≤ b) : riemannianEDist I x y ≤ pathELength I γ a b :=
by
let η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
have hη : ContMDiffOn 𝓘(ℝ) I 1 (γ ∘ η) (Icc 0 1) := by
apply hγ.comp
· rw [contMDiffOn_iff_contDiffOn]
exact η.contDiff.contDiffOn
· rw [← image_subset_iff, ContinuousAffineMap.coe_lineMap_eq, ← segment_eq_image_lineMap]
simp [hab]
let f : unitInterval → M := fun t ↦ (γ ∘ η) t
have hf : ContMDiff (𝓡∂ 1) I 1 f := by
rw [← contMDiffOn_comp_projIcc_iff]
apply hη.congr (fun t ht ↦ ?_)
simp only [Function.comp_apply, f, projIcc_of_mem, ht]
let g : Path x y := by refine ⟨⟨f, hf.continuous⟩, ?_, ?_⟩ <;> simp [f, η, ContinuousAffineMap.coe_lineMap_eq, ha, hb]
have A : riemannianEDist I x y ≤ ∫⁻ x, ‖mfderiv (𝓡∂ 1) I g x 1‖ₑ := by rw [riemannianEDist]; exact biInf_le _ hf
apply A.trans_eq
rw [lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc]
have E : pathELength I (g ∘ projIcc 0 1 zero_le_one) 0 1 = pathELength I (γ ∘ η) 0 1 :=
by
apply pathELength_congr (fun t ht ↦ ?_)
simp only [Function.comp_apply, ht, projIcc_of_mem]
rfl
rw [E, pathELength_comp_of_monotoneOn zero_le_one _ η.differentiableOn]
· simp [η, ContinuousAffineMap.coe_lineMap_eq]
· simpa [η, ContinuousAffineMap.coe_lineMap_eq] using hγ.mdifferentiableOn le_rfl
· apply (AffineMap.lineMap_mono hab).monotoneOn
