English
Let F be a real vector space with an inner product. The tangent spaces T_xF are identified with F, and the standard inner product induces a smooth Riemannian metric on the tangent bundle at every point, i.e., g_x(v,w) = ⟪v,w⟫ for v,w ∈ T_xF.
Русский
Пусть F — вещественное векторное пространство с вложенным скалярным произведением. Тангенциальные пространства T_xF естественным образом идентифицируются с F, и стандартное скалярное произведение порождает гладкую римманову метрику на касательном расслоении: g_x(v,w) = ⟪v,w⟫.
LaTeX
$$$$\\text{Let }F\\text{ be a real inner product space. Then the tangent bundle }T F\\text{ carries the standard smooth metric }g\\text{ given by }g_x(v,w)=\\langle v,w\\rangle\\text{ for }v,w\\in T_xF.$$$$
Lean4
/-- The standard Riemannian metric on a vector space with an inner product, given by this inner
product on each tangent space. -/
noncomputable def riemannianMetricVectorSpace :
ContMDiffRiemannianMetric 𝓘(ℝ, F) ω F (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x)
where
inner x := (innerSL ℝ (E := F) : F →L[ℝ] F →L[ℝ] ℝ)
symm x v w := real_inner_comm _ _
pos x v hv := real_inner_self_pos.2 hv
isVonNBounded
x := by
change IsVonNBounded ℝ {v : F | ⟪v, v⟫ < 1}
have : Metric.ball (0 : F) 1 = {v : F | ⟪v, v⟫ < 1} := by
ext v
simp only [Metric.mem_ball, dist_zero_right, norm_eq_sqrt_re_inner (𝕜 := ℝ), RCLike.re_to_real, Set.mem_setOf_eq]
conv_lhs => rw [show (1 : ℝ) = √1 by simp]
rw [Real.sqrt_lt_sqrt_iff]
exact real_inner_self_nonneg
rw [← this]
exact NormedSpace.isVonNBounded_ball ℝ F 1
contMDiff := by
intro x
rw [contMDiffAt_section]
convert contMDiffAt_const (c := innerSL ℝ)
ext v w
simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates, Trivialization.linearMapAt_apply, TangentSpace]
