[placeholder PR uniting ongoing work on connections and geodesics]

[grunweg]

---

• depends on: [Merged by Bors] - feat: mfderiv_smul #34263
• depends on: feat(Manifold/VectorBundle): tensoriality construction #36277
• depends on: [Merged by Bors] - feat: covariant derivatives on vector bundles #36279
• depends on: [Merged by Bors] - feat: torsion of an affine connection #36285
• depends on: [Merged by Bors] - feat: metric connections #36299
• depends on: [Merged by Bors] - feat: continuousLinearMapAt_apply_of_mem #37537
• depends on: [Merged by Bors] - feat(Tactic/ToFun): allow configuring the name of the generated declaration #34257
• depends on: [Merged by Bors] - feat(fun_prop): allow fun_prop to call discharger on ModelWithCorners #39226
• depends on: [Merged by Bors] - feat: mfderivWithin_{add,neg,sub} #39451
• depends on: [Merged by Bors] - chore: rename extDerivFun to mvfderiv #39485
• depends on: [Merged by Bors] - feat: add and use custom (d)elaborators for mvfderiv, add basic API lemmas #39554
• depends on: [Merged by Bors] - feat: add mvfderivWithin with (d)elaborators and basic API #39513
• depends on: [Merged by Bors] - fix(Geometry/Manifold/Notation): typo in MDiffAt delaborator #39486
• depends on: [Merged by Bors] - feat: the Levi-Civita connection on a manifold #36845
• depends on: [Merged by Bors] - feat: sections of a fiber bundle with Subsingleton fiber are smooth and differentiable #41027
• depends on: [Merged by Bors] - chore(Geometry/Manifold/VectorBundle/Basic): consolidate open statements #42496
• depends on: [Merged by Bors] - feat: add contDiffWithinAt_clm_apply #42497
• depends on: feat: ContMDiff.clm_bundle_of_apply and friends #43042

[github-actions]

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title does not contain a colon

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"

[github-actions]

PR summary e1c5ca8741

Import changes exceeding 2%

%	File
+16.04%	Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
+16.46%	Mathlib.Geometry.Manifold.VectorBundle.Hom

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Manifold.VectorBundle.Hom	2260	2632	+372 (+16.46%)
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic	2269	2633	+364 (+16.04%)

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.Riemannian.Basic	35
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita	279
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric	349
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion	350
Mathlib.Geometry.Manifold.GroupLieAlgebra Mathlib.Geometry.Manifold.VectorBundle.Riemannian	358
Mathlib.Geometry.Manifold.VectorField.LieBracket Mathlib.Geometry.Manifold.VectorField.Pullback	359
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic	364
Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.VectorBundle.Hom	372
Mathlib.Geometry.Manifold.VectorBundle.Unused (new file)	2259
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.IntegralCurvePrelim (new file)	2261
Mathlib.Geometry.Manifold.VectorBundle.TensorialityNextGen (new file)	2267
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Prelim (new file) Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.TrivPrelim (new file)	2271
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Trivial (new file) Mathlib.Geometry.Manifold.VectorBundle.GramSchmidtOrtho (new file)	2635
Mathlib.Geometry.Manifold.VectorBundle.OrthonormalFrame (new file)	2636
Mathlib.Geometry.Manifold.Riemannian.ExistsRiemannianMetric (new file)	2637
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion2 (new file)	2643
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Ehresmann (new file)	2645
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Lift (new file)	2646
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Geodesics (new file)	2649
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.ChristoffelSymbols (new file)	2651
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Curvature (new file)	2670

---

Declarations diff (regex)

+ Bundle.TotalSpace.proj_mk'
+ Bundle.Trivialization.ContMDiffAt_symm
+ Bundle.Trivialization.contMDiffAt_symm_const
+ Bundle.Trivialization.contMDiffWithinAt_apply
+ ChristoffelSymbol
+ ChristoffelSymbol.sum_eq
+ ContMDiff.clm_bundle_of_apply
+ ContMDiff.clm_bundle_of_apply'
+ ContMDiff.smul_section_of_tsupport'
+ ContMDiffAt.clm_bundle_apply_trivial_source
+ ContMDiffAt.clm_bundle_apply_trivial_target
+ ContMDiffAt.clm_bundle_of_apply
+ ContMDiffAt.clm_bundle_of_apply'
+ ContMDiffCovariantDerivativeOn'
+ ContMDiffCovariantDerivativeOn'.contMDiffAt_of_isOpen
+ ContMDiffCovariantDerivativeOn'.mdifferentiableAt_of_eventually
+ ContMDiffCovariantDerivativeOn'.mdifferentiableWithinAt_of_eventually
+ ContMDiffCovariantDerivativeOn.contMDiff'
+ ContMDiffCovariantDerivativeOn.contMDiffCovariantDerivativeOn'
+ ContMDiffCovariantDerivativeOn.contMDiffCovariantDerivativeOn''
+ ContMDiffCovariantDerivativeOn.contMDiffCovariantDerivativeOn'''
+ ContMDiffOn.clm_bundle_of_apply
+ ContMDiffOn.clm_bundle_of_apply'
+ ContMDiffWithinAt.clm_bundle_of_apply
+ ContMDiffWithinAt.clm_bundle_of_apply'
+ ContMDiffWithinAt.orthogonalProjection
+ CovariantDerivative.geodVF
+ CovariantDerivative.geodVF_horiz
+ CovariantDerivative.isGeod
+ CovariantDerivative.isGeodAt
+ CovariantDerivative.isGeodAt_iff_horiz
+ CovariantDerivative.isGeodAt_iff_proj
+ CovariantDerivative.lift_vec
+ CovariantDerivative.lift_vec_apply
+ CovariantDerivative.lift_vec_eq
+ CovariantDerivative.lift_vec_eq_iff
+ CovariantDerivative.lift_vec_eq_iff'
+ CovariantDerivative.lift_vec_mem_horiz
+ CovariantDerivative.mfderiv_proj_lift_vec
+ CovariantDerivative.orbit_geodVF
+ CovariantDerivative.proj_geodVF
+ CovariantDerivative.proj_lift_vec
+ Function.dcomp'
+ HasMFDerivWithinAt.smul
+ IsCovariantDerivativeOn.fst_comp_lift_vec
+ IsCovariantDerivativeOn.lift_vec
+ IsCovariantDerivativeOn.lift_vec_apply
+ IsCovariantDerivativeOn.lift_vec_eq_iff
+ IsCovariantDerivativeOn.lift_vec_mem_horiz
+ IsCovariantDerivativeOn.projection_lift_vec
+ IsLocalFrameOn.gramSchmidtNormed
+ IsMIntegralCurveAt.acceleration
+ IsMIntegralCurveAt.eventually_acceleration
+ IsMIntegralCurveAt.eventually_isMIntegralCurveAt
+ IsMIntegralCurveAt.mdifferentiableAt
+ IsMIntegralCurveAt.mfderiv
+ IsMIntegralCurveAt.proj_acceleration
+ IsMIntegralCurveAt.velocity_eventuallyEq
+ IsMIntegralCurveAt_iff_mfderiv
+ IsOpen.contMDiffAt
+ IsOrthonormalFrameOn
+ IsOrthonormalFrameOn.gramSchmidtNormed
+ IsOrthonormalFrameOn.mono
+ IsOrthonormalFrameOn.of_le
+ IsTorsionFreeOn
+ LeviCivitaConnection.christoffelSymbol_symm
+ LinearEquiv.comap_isCompl
+ LinearMap.comap_isCompl
+ MDiffAtPkg
+ RegPkg
+ Tensorial
+ TensorialAt.apply_clm
+ TensorialAt.contMDiff_mkHom
+ V
+ W
+ _root_.Bundle.Trivial.contMDiffOn_iff
+ _root_.Bundle.Trivial.mdifferentiableAt_iff
+ _root_.Bundle.Trivialization.isOrthonormalFrameOn_orthonormalFrame_baseSet
+ _root_.Bundle.vert
+ _root_.CovariantDerivative.exists_one_form
+ _root_.IsCovariantDerivativeOn.congr_iff_christoffelSymbol_eq
+ _root_.IsCovariantDerivativeOn.congr_of_christoffelSymbol_eq
+ _root_.contMDiffAt_orthonormalFrame_of_mem
+ _root_.mdifferentiableAt_orthonormalFrame_of_mem
+ _root_.mdifferentiableAt_section_trivial_iff
+ _root_.mdifferentiableAt_total_trivial_iff
+ apply_funToSec
+ apply_total_eventuallyEq
+ aux
+ aux_special
+ aux_tvs
+ baseSet_mem_nhds
+ baseSet_prod_univ_mem_nhds
+ bijective_deriv
+ bijective_symm
+ christoffelSymbol_zero
+ christoffelSymbol_zero_apply
+ coe_gramSchmidtBasis
+ coe_gramSchmidtNormedBasis
+ coe_proj
+ coeff_eq_inner
+ comap_trivializationAt_horiz
+ comap_vert
+ comp_invFun_eventuallyEq
+ condition
+ condition1
+ condition2
+ congr_of_eq_one_jet
+ const
+ contMDiffAt_aux
+ contMDiffAt_coeff
+ contMDiffAt_iff_coeff
+ contMDiffAt_iff_inner
+ contMDiffAt_symm_of_memTrivializationAtlas
+ contMDiffOn_coeff
+ contMDiffOn_iff_coeff
+ contMDiffOn_iff_inner
+ contMDiffOn_localExtensionOn
+ contMDiffOn_one_form
+ contMDiffOn_orthonormalFrame_baseSet
+ contMDiffOn_symm_of_memTrivializationAtlas
+ contMDiffWithinAt_aux
+ contMDiffWithinAt_coeff
+ contMDiffWithinAt_inner
+ contMDiff_localSection
+ convex_condition
+ convex_condition1
+ convex_condition2
+ coordChangeL_coordChangeL
+ cov_eq_proj
+ curvatureEndomorphismTensor
+ curvatureEndomorphismTensor_self
+ curvatureEndomorphismTensor_swap
+ curvatureTensorAux
+ curvatureTensorAux_tensorial₁
+ curvatureTensorAux_tensorial₂
+ curvatureTensorAux_tensorial₃
+ deriv
+ derivInv
+ derivInv_deriv
+ derivInv_deriv_apply
+ deriv_derivInv
+ deriv_derivInv_apply
+ eq_of
+ eq_one_form
+ eq_one_form_lemming
+ eq_product_apply
+ eventually
+ exists_bumpFunction
+ exists_contMDiff_extension
+ exists_contMDiff_of_one_form
+ exists_map_of
+ exists_one_form
+ foo
+ foo_aux
+ foo_aux_prop
+ foobar
+ fromTangentSpace_mfderiv_add
+ fromTangentSpace_mfderiv_add_apply
+ fst_comp_eventuallyEq
+ funToSec
+ funToSec_congr
+ funToSec_map_add
+ funToSec_map_add_eventuallyEq
+ funToSec_map_smul
+ funToSec_map_smul_const
+ funToSec_map_zero
+ funToSec_map_zero_eventuallyEq
+ funToSec_proj_eq
+ funToSec_secToFun
+ funToSec_secToFun_eventually_eq
+ gramSchmidt
+ gramSchmidtBasis
+ gramSchmidtNormed
+ gramSchmidtNormedBasis
+ gramSchmidtNormed_apply_of_orthogonal
+ gramSchmidtNormed_apply_of_orthonormal
+ gramSchmidtNormed_coe
+ gramSchmidtNormed_contMDiff
+ gramSchmidtNormed_contMDiffAt
+ gramSchmidtNormed_contMDiffOn
+ gramSchmidtNormed_contMDiffWithinAt
+ gramSchmidtNormed_linearIndependent
+ gramSchmidtNormed_orthonormal
+ gramSchmidtNormed_orthonormal'
+ gramSchmidtNormed_unit_length
+ gramSchmidtNormed_unit_length'
+ gramSchmidtNormed_unit_length_coe
+ gramSchmidtOrthonormalBasis
+ gramSchmidtOrthonormalBasis_apply_of_orthonormal
+ gramSchmidtOrthonormalBasis_coe
+ gramSchmidt_apply
+ gramSchmidt_bot
+ gramSchmidt_contMDiff
+ gramSchmidt_contMDiffAt
+ gramSchmidt_contMDiffOn
+ gramSchmidt_contMDiffWithinAt
+ gramSchmidt_def
+ gramSchmidt_def'
+ gramSchmidt_def''
+ gramSchmidt_inv_triangular
+ gramSchmidt_linearIndependent
+ gramSchmidt_mem_span
+ gramSchmidt_ne_zero
+ gramSchmidt_ne_zero_coe
+ gramSchmidt_of_orthogonal
+ gramSchmidt_orthogonal
+ gramSchmidt_pairwise_orthogonal
+ gramSchmidt_zero
+ hloc_TODO
+ hoge
+ injective_mfderiv_of_eventually_leftInverse
+ injective_symm
+ instance (f : F) : CoeOut (TangentSpace 𝓘(ℝ, F) f) F
+ instance (x : B) : AddCommGroup (W E x) := by
+ instance (x : B) : ContinuousAdd (V E x) := by
+ instance (x : B) : ContinuousSMul ℝ (V E x) := by
+ instance (x : B) : IsTopologicalAddGroup (V E x) := by
+ instance (x : B) : Module ℝ (V E x) := by
+ instance (x : B) : Module ℝ (W E x) := by
+ instance (x : B) : TopologicalSpace (W E x) := by
+ instance : (x : B) → AddCommGroup (V E x) := by
+ instance : (x : B) → TopologicalSpace (V E x) := by
+ instance : ContMDiffVectorBundle n (F →L[ℝ] F →L[ℝ] ℝ) (W E) IB := by
+ instance : ContMDiffVectorBundle n (F →L[ℝ] ℝ) (V E) IB := by
+ instance : FiberBundle (F →L[ℝ] F →L[ℝ] ℝ) (W E) := by
+ instance : FiberBundle (F →L[ℝ] ℝ) (V E) := by
+ instance : TopologicalSpace (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) (W E)) := by
+ instance : TopologicalSpace (TotalSpace (F →L[ℝ] ℝ) (V E)) := by
+ instance : VectorBundle ℝ (F →L[ℝ] F →L[ℝ] ℝ) (W E) := by
+ instance : VectorBundle ℝ (F →L[ℝ] ℝ) (V E) := by
+ invFun_comp_eventuallyEq
+ isCovariantDerivativeOn_pushCovDer
+ isTorsionFreeOn_iff_christoffelSymbols
+ isTorsionFree_iff_christoffelSymbols'
+ is_good_localSection
+ linearMapAt_funToSec
+ localExtensionOn
+ localExtensionOn_apply_self
+ localExtensionOn_localFrameCoeff
+ localFrame
+ localFrame_coeff
+ local_section_at
+ map_add
+ map_of
+ map_of_loc_one_jet
+ map_of_loc_one_jet_spec
+ map_of_one_jet
+ map_of_one_jet_spec
+ map_of_spec
+ map_smul
+ map_zero
+ mdifferentiableAt
+ mdifferentiableAt_dependent_congr
+ mdifferentiableAt_funToSec
+ mdifferentiableAt_funToSec'
+ mdifferentiableAt_invFun
+ mdifferentiableAt_secToFun
+ mdifferentiableAt_secToFun_funToSec
+ mdifferentiableAt_total_funToSec_secToFun
+ mdifferentiableAt_total_secToFun
+ mdifferentiable_dependent_congr_iff
+ mem_horiz_iff_proj
+ mem_span_gramSchmidt
+ mfderiv_comp_section
+ mfderiv_proj_derivInv_apply
+ mfderiv_proj_fst_deriv
+ mfderiv_secToFun
+ mfderiv_secToFun_apply
+ mfderiv_total_funToSec
+ mkHom
+ mkHom_apply
+ mkHom_apply_eq_extend
+ mkHom₂
+ mkHom₂_apply
+ mkHom₂_apply_eq_extend
+ mk_funToSec_of_eq
+ mono
+ mynorm
+ of_le
+ one_form
+ orthonormalFrame
+ orthonormalFrame_apply_of_notMem
+ pointwise₂
+ preimage_baseSet_mem_nhds
+ proj
+ proj_acceleration
+ proj_invFun_eventuallyEq
+ proj_mderiv
+ proj_velocity
+ projection
+ projection_apply
+ pushCovDer
+ pushCovDer_funToSec
+ pushCovDer_isCovariantDerivativeOn
+ pushCovDer_secToFun
+ qux
+ secToFun
+ secToFun_apply_of_eq
+ secToFun_congr
+ secToFun_funToSec
+ secToFun_funToSec_eventuallyEq
+ secToFun_map_add
+ secToFun_map_smul
+ secToFun_map_zero
+ snd_apply_funToSec
+ snd_triv_proj
+ span_gramSchmidt
+ span_gramSchmidtNormed
+ span_gramSchmidtNormed_range
+ span_gramSchmidt_Iic
+ span_gramSchmidt_Iio
+ sum_section
+ surjective_mfderiv_of_eventually_rightInverse
+ surjective_symm
+ symm_map_add
+ symm_map_smul
+ symm_map_zero
+ totalSpace_mk_funToSec
+ total_funToSec_secToFun_eq
+ total_funToSec_secToFun_eventuallyEq
+ total_secToFun_funToSeq
+ total_secToFun_funToSeq_eventually_eq
+ traceCurvature
+ trivial_isSmooth
+ velocity
+ weakLocallyCompact_of_manifold
++ TensorialNear
++ horiz
++ horiz_vert_direct_sum
++ mem_horiz_iff_exists
++ mkHom₃
++ mkHom₃_apply
++ mkHom₃_apply_eq_extend
++ neg
++ of_endomorphism
++ pointwise
++ sub
++ sum
++ trivial
++ zero
++ «local»
-++ iUnion

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

Increase in strong tech debt: (relative, absolute) = (10.98, 0.03)

Current number	Change	Type (strong)
backward.isDefEq.respectTransparency	4865	9
backward.isDefEq.respectTransparency.types	2512	7
erw	509	12

Increase in weak tech debt: (relative, absolute) = (1.07, 0.04)

Current number	Change	Type (weak)
flexible linter exceptions	28	1
exposed public sections	5039	13

Current commit e1c5ca8741
Reference commit 4154674844

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: mfderiv_smul #34263
• feat(Manifold/VectorBundle): tensoriality construction #36277
• [Merged by Bors] - feat: covariant derivatives on vector bundles #36279
• [Merged by Bors] - feat: torsion of an affine connection #36285
• [Merged by Bors] - feat: metric connections #36299
• [Merged by Bors] - feat: continuousLinearMapAt_apply_of_mem #37537
• [Merged by Bors] - feat(Tactic/ToFun): allow configuring the name of the generated declaration #34257
• [Merged by Bors] - feat(fun_prop): allow fun_prop to call discharger on ModelWithCorners #39226
• [Merged by Bors] - feat: mfderivWithin_{add,neg,sub} #39451
• [Merged by Bors] - chore: rename extDerivFun to mvfderiv #39485
• [Merged by Bors] - feat: add and use custom (d)elaborators for mvfderiv, add basic API lemmas #39554
• [Merged by Bors] - feat: add mvfderivWithin with (d)elaborators and basic API #39513
• [Merged by Bors] - fix(Geometry/Manifold/Notation): typo in MDiffAt delaborator #39486
• [Merged by Bors] - feat: the Levi-Civita connection on a manifold #36845
• [Merged by Bors] - feat: sections of a fiber bundle with Subsingleton fiber are smooth and differentiable #41027
• [Merged by Bors] - chore(Geometry/Manifold/VectorBundle/Basic): consolidate open statements #42496
• [Merged by Bors] - feat: add contDiffWithinAt_clm_apply #42497
• feat: ContMDiff.clm_bundle_of_apply and friends #43042
  By Dependent Issues (🤖). Happy coding!

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.