English
A continuous Riemannian metric g on a fibre bundle F E induces a fibrewise Riemannian metric on E, defined by ⟨v,w⟩_b := g.inner b v w for each fibre E_b; the resulting family defines a RiemannianMetric E.
Русский
Непрерывная риманова метрка g на волокне F→E порождает риманову метрикой на каждом волокне E_b: ⟨v,w⟩_b := g.inner b v w; полученная семья образует RiemannianMetric E.
LaTeX
$$$$\langle v,w\rangle_b := g.inner b v w \, (v,w \in E_b),\quad \text{the family } (\langle\cdot,\cdot\rangle_b)_b \text{ defines a fibrewise Riemannian metric.}$$$$
Lean4
/-- A continuous Riemannian metric is in particular a Riemannian metric. -/
def toRiemannianMetric (g : ContinuousRiemannianMetric F E) : RiemannianMetric E
where
inner := g.inner
symm := g.symm
pos := g.pos
isVonNBounded := g.isVonNBounded
continuousAt
b := by
-- Continuity of bilinear maps is only true on normed spaces. As `F` is a normed space by
-- assumption, we transfer everything to `F` and argue there.
let e : E b ≃L[ℝ] F :=
Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E b) _ (FiberBundle.mem_baseSet_trivializationAt' b)
let m : (E b →L[ℝ] E b →L[ℝ] ℝ) ≃L[ℝ] (F →L[ℝ] F →L[ℝ] ℝ) :=
e.arrowCongr (e.arrowCongr (ContinuousLinearEquiv.refl ℝ ℝ))
have A (v : E b) : g.inner b v v = ((fun w ↦ m (g.inner b) w w) ∘ e) v := by simp [m]
simp only [A]
fun_prop
