Commit 2025-11-19 10:28 5db554c9

View on Github →

feat: local frame induced by a vector bundle trivialisation (#31788) We construct local frames on a vector from local trivialisations. The former constructs, given a trivialisation e of the vector bundle and a basis of the model fibre, Basis.localFrame is a local frame on e.baseSet. Future PRs will

define the coefficients of a section w.r.t. this local frame (and related smoothness of a section to the smoothness of its coefficients),
will use this to define the local extension of a tangent vector to a vector field near a point. From the path towards geodesics and the Levi-Civita connection.

Estimated changes

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

modified theorem IsLocalFrameOn.contMDiffAt_of_coeff

modified theorem IsLocalFrameOn.contMDiffAt_of_coeff_aux

modified theorem IsLocalFrameOn.contMDiffOn_of_coeff

modified theorem IsLocalFrameOn.eq_iff_coeff

added def IsLocalFrameOn.fintype_of_finiteDimensional

modified theorem IsLocalFrameOn.mdifferentiableAt_of_coeff

modified theorem IsLocalFrameOn.mdifferentiableAt_of_coeff_aux

modified theorem IsLocalFrameOn.mdifferentiableOn_of_coeff

added def Trivialization.basisAt

added theorem Trivialization.contMDiffOn_localFrame_baseSet

added theorem Trivialization.isLocalFrameOn_localFrame_baseSet

added def Trivialization.localFrame

added theorem Trivialization.localFrame_apply_of_mem_baseSet

added theorem Trivialization.localFrame_apply_of_notMem

added theorem contMDiffAt_localFrame_of_mem