English
The extended Riemannian distance between two points is the infimum of the lengths of all C^1 paths joining them, measured by an extended norm on tangent spaces.
Русский
Расстояние Римана векторного параграфа между двумя точками — это инфимум длин всех гладких путей между ними, измеряемых расширенной нормой на касательных пространствах.
LaTeX
$$riemannianEDist I x y = \\inf_{\\gamma} \\; ( length of γ )$$
Lean4
/-- The length of a path in a manifold is invariant under a monotone reparametrization. -/
theorem pathELength_comp_of_monotoneOn {f : ℝ → ℝ} (h : a ≤ b) (hf : MonotoneOn f (Icc a b))
(h'f : DifferentiableOn ℝ f (Icc a b)) (hγ : MDifferentiableOn 𝓘(ℝ) I γ (Icc (f a) (f b))) :
pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b) :=
by
rcases h.eq_or_lt with rfl | h
· simp
have f_im : f '' (Icc a b) = Icc (f a) (f b) := h'f.continuousOn.image_Icc_of_monotoneOn h.le hf
simp only [pathELength_eq_lintegral_mfderivWithin_Icc, ← f_im]
have B (t) (ht : t ∈ Icc a b) : HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t :=
(h'f t ht).hasDerivWithinAt
rw [lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn measurableSet_Icc B hf]
apply setLIntegral_congr_fun measurableSet_Icc (fun t ht ↦ ?_)
have :
(mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t) =
(mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t)) ∘L mfderivWithin 𝓘(ℝ) 𝓘(ℝ) f (Icc a b) t :=
by
rw [← f_im] at hγ ⊢
apply mfderivWithin_comp
· apply hγ _ (mem_image_of_mem _ ht)
· rw [mdifferentiableWithinAt_iff_differentiableWithinAt]
exact h'f _ ht
· exact subset_preimage_image _ _
· rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
exact uniqueDiffOn_Icc h _ ht
rw [this]
simp only [Function.comp_apply, ContinuousLinearMap.coe_comp']
have : mfderivWithin 𝓘(ℝ) 𝓘(ℝ) f (Icc a b) t 1 = derivWithin f (Icc a b) t • (1 : TangentSpace 𝓘(ℝ) (f t)) :=
by
simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
rfl
rw [this]
have : 0 ≤ derivWithin f (Icc a b) t := hf.derivWithin_nonneg
simp only [map_smul, enorm_smul, ← Real.enorm_of_nonneg this, f_im]
