English
The model-with-corners self of a real inner-product space F is a Riemannian manifold with its standard metric.
Русский
Модель с углами для вещественного пространства с скалярным произведением образует римманово многообразие с обычной метрикой.
LaTeX
$$$$\\text{IsRiemannianManifold}(\\text{modelWithCornersSelf}(\\mathbb{R},F))\\ F.$$$$
Lean4
/-- An inner product vector space is a Riemannian manifold, i.e., the distance between two points
is the infimum of the lengths of paths between these points. -/
instance : IsRiemannianManifold 𝓘(ℝ, F) F :=
by
refine ⟨fun x y ↦ le_antisymm ?_ ?_⟩
· simp only [riemannianEDist, le_iInf_iff]
intro γ hγ
let e : ℝ → F := γ ∘ (projIcc 0 1 zero_le_one)
have D : ContDiffOn ℝ 1 e (Icc 0 1) := contMDiffOn_iff_contDiffOn.mp (hγ.comp_contMDiffOn contMDiffOn_projIcc)
rw [lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, pathELength_eq_lintegral_mfderivWithin_Icc]
simp only [mfderivWithin_eq_fderivWithin, enorm_tangentSpace_vectorSpace]
conv_lhs => rw [edist_comm, edist_eq_enorm_sub, show x = e 0 by simp [e], show y = e 1 by simp [e]]
exact (enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc D zero_le_one).trans_eq rfl
· let γ := ContinuousAffineMap.lineMap (R := ℝ) x y
have : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) γ 0 1 :=
by
apply
riemannianEDist_le_pathELength ?_ (by simp [γ, ContinuousAffineMap.coe_lineMap_eq])
(by simp [γ, ContinuousAffineMap.coe_lineMap_eq]) zero_le_one
rw [contMDiffOn_iff_contDiffOn]
exact γ.contDiff.contDiffOn
apply this.trans_eq
rw [pathELength_eq_lintegral_mfderivWithin_Icc]
simp only [mfderivWithin_eq_fderivWithin, enorm_tangentSpace_vectorSpace]
exact lintegral_fderiv_lineMap_eq_edist
