English
Given a Riemannian metric g on a fibre bundle, define for each fibre over b ∈ B an inner product on E_b by ⟨v,w⟩_b := g.inner b v w. This yields an inner product space structure on each fibre E_b, forming the core of an inner product on the bundle.
Русский
Для семейства скобок на волокне: если дан метрический риман на волокнах, то на каждом волокне E_b задаётся скалярным произведением ⟨v,w⟩_b := g.inner b v w, что на каждом волокне E_b даёт структуру пространства с скалярным произведением.
LaTeX
$$$$\text{For each } b\in B,\ \langle v,w\rangle_b := g.inner b v w,\qquad v,w\in E_b.$$$$
Lean4
/-- `Core structure associated to a family of inner products on the fibers of a fiber bundle. This
is an auxiliary construction to endow the fibers with an inner product space structure without
creating diamonds.
Warning: Do not use this `Core` structure if the space you are interested in already has a norm
instance defined on it, otherwise this will create a second non-defeq norm instance! -/
@[reducible]
noncomputable def toCore (g : RiemannianMetric E) (b : B) : InnerProductSpace.Core ℝ (E b)
where
inner v w := g.inner b v w
conj_inner_symm v w := g.symm b w v
re_inner_nonneg
v := by
rcases eq_or_ne v 0 with rfl | hv
· simp
· simpa using (g.pos b v hv).le
add_left v w x := by simp
smul_left c v := by simp
definite v h := by contrapose! h; exact (g.pos b v h).ne'
