English
For a finite-dimensional real vector space F, the model self with corners F carries an IsRiemannianManifold structure with the standard inner product.
Русский
Для конечномерного вещественного векторного пространства F модель self с углами поддерживает структуру IsRiemannianManifold с использованием стандартного скалярного произведения.
LaTeX
$$$$\\text{IsRiemannianManifold}(\\,\\mathcal{I}(\\mathbb{R},F)\\,)\\;F.$$$
Lean4
theorem lintegral_fderiv_lineMap_eq_edist {x y : E} :
∫⁻ t in Icc 0 1, ‖fderivWithin ℝ (ContinuousAffineMap.lineMap (R := ℝ) x y) (Icc 0 1) t 1‖ₑ = edist x y :=
by
have : edist x y = ∫⁻ t in Icc (0 : ℝ) 1, ‖y - x‖ₑ := by simp [edist_comm x y, edist_eq_enorm_sub]
rw [this]
apply setLIntegral_congr_fun measurableSet_Icc (fun z hz ↦ ?_)
rw [show y - x = fderiv ℝ (ContinuousAffineMap.lineMap (R := ℝ) x y) z 1 by simp]
congr
exact fderivWithin_eq_fderiv (uniqueDiffOn_Icc zero_lt_one _ hz) (ContinuousAffineMap.differentiableAt _)
