Commit 2025-06-24 13:20 e268a252

feat: continuous Riemannian vector bundles (#26197) 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 continuously on the base point. We introduce a typeclass [IsContinuousRiemannianBundle F E] registering this property. Under this assumption, we show that the scalar product of two continuous maps into the same fibers of the bundle is a continuous function. If one wants to endow an existing vector bundle with a Riemannian metric, there is a subtlety: the inner product space structure on the fibers should give rise to a topology on the fibers which is defeq to the original one, to avoid diamonds. To do this, we introduce a class [RiemannianBundle E] containing the data of a scalar product on the fibers defining the same topology as the original one. Given this class, we can construct NormedAddCommGroup and InnerProductSpace instances on the fibers, compatible in a defeq way with the initial topology. If the data used to register the instance RiemannianBundle E depends continuously on the base point, we register automatically an instance of [IsContinuousRiemannianBundle F E] (and similarly if the data is smooth). The general theory should be built assuming [IsContinuousRiemannianBundle F E], while the [RiemannianBundle E] mechanism is only to build data in specific situations.