Commit 2025-09-27 12:35 79c7feb2

View on Github →

feat: finsum and locally finite sums of differentiable sections are differentiable (#29686) Mirrors analogous API for C^n sections; this is added mostly for completeness. Follow-up to #26871. Hence, this also originated from our work towards the path towards geodesics and the Levi-Civita connection.

Estimated changes

Modified Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

added theorem MDifferentiableWithinAt.congr'

Modified Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

added theorem MDifferentiable.finsum_section_of_locallyFinite

added theorem MDifferentiable.sum_section_of_locallyFinite

added theorem MDifferentiableAt.finsum_section_of_locallyFinite

added theorem MDifferentiableAt.sum_section_of_locallyFinite

added theorem MDifferentiableOn.finsum_section_of_locallyFinite

added theorem MDifferentiableOn.smul_section_of_tsupport

added theorem MDifferentiableOn.sum_section_of_locallyFinite

added theorem MDifferentiableWithinAt.finsum_section_of_locallyFinite

added theorem MDifferentiableWithinAt.sum_section_of_locallyFinite