Commit 2025-07-04 20:03 2aea8b5b

feat: smooth Riemannian bundles (#26506) Given a vector bundle over a manifold whose fibers are all endowed with a scalar product, we say that this bundle is Riemannian if the scalar product depends smoothly on the base point. We introduce a typeclass [IsContMDiffRiemannianBundle IB n F E] registering this property. Under this assumption, we show that the scalar product of two smooth maps into the same fibers of the bundle is a smooth function. If the fibers of a bundle E have a preexisting topology (like the tangent bundle), one can not assume additionally [∀ b, InnerProductSpace ℝ (E b)] as this would create diamonds. Instead, use [RiemannianBundle E], which endows the fibers with a scalar product while ensuring that there is no diamond. We provide a constructor for [RiemannianBundle E] from a smooth family of metrics, which registers automatically [IsContMDiffRiemannianBundle IB n F E]