feat: the Levi-Civita connection on a manifold

[grunweg]

---

• depends on: feat: metric connections #36299

[github-actions]

PR summary 2badb0c337

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric (new file)	2184
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita (new file)	2269

---

Declarations diff

+ IsCompatible
+ IsLeviCivitaConnection
+ IsLeviCivitaConnection.eq_leviCivitaRhs
+ IsLeviCivitaConnection.uniqueness
+ LeviCivitaConnection
+ _root_.MDifferentiable.inner_bundle'
+ _root_.MDifferentiableAt.inner_bundle'
+ aux
+ compatibilityTensor
+ compatibilityTensorAux
+ compatibilityTensorAux_apply
+ compatibilityTensorAux_tensorial₁
+ compatibilityTensorAux_tensorial₂
+ compatibilityTensor_apply
+ compatibilityTensor_apply_eq_extend
+ congr_of_forall_product
+ congr_of_forall_product_apply
+ fromTangentSpace_mfderiv_add
+ fromTangentSpace_mfderiv_add_apply
+ isCompatible_iff
+ isCovariantDerivativeOn_lcAux
+ lcAux
+ lcAux_apply
+ lcAux₀
+ lcAux₀'
+ lcAux₀_apply
+ lcAux₁
+ lcAux₁_apply
+ leviCivitaConnection_apply
+ leviCivitaConnection_isCompatible
+ leviCivitaConnection_isCompatible_aux
+ leviCivitaConnection_isLeviCivitaConnection
+ leviCivitaConnection_torsion_eq_zero
+ leviCivitaRhs
+ leviCivitaRhs'
+ leviCivitaRhs'_addX
+ leviCivitaRhs'_addX_apply
+ leviCivitaRhs'_addY_apply
+ leviCivitaRhs'_addZ
+ leviCivitaRhs'_addZ_apply
+ leviCivitaRhs'_smulX_apply
+ leviCivitaRhs'_smulY_apply
+ leviCivitaRhs'_smulY_const_apply
+ leviCivitaRhs'_smulZ
+ leviCivitaRhs'_smulZ_apply
+ leviCivitaRhs_addX
+ leviCivitaRhs_addX_apply
+ leviCivitaRhs_addY
+ leviCivitaRhs_addY_apply
+ leviCivitaRhs_addZ
+ leviCivitaRhs_addZ_apply
+ leviCivitaRhs_apply
+ leviCivitaRhs_smulX
+ leviCivitaRhs_smulX_apply
+ leviCivitaRhs_smulY_apply
+ leviCivitaRhs_smulY_const
+ leviCivitaRhs_smulY_const_apply
+ leviCivitaRhs_smulZ
+ leviCivitaRhs_smulZ_apply
+ leviCivitaRhs_tensorial₁
+ leviCivitaRhs_tensorial₂
+ product
+ product_add_left
+ product_add_left_apply
+ product_add_right
+ product_add_right_apply
+ product_apply
+ product_congr_left
+ product_congr_left₂
+ product_congr_right
+ product_congr_right₂
+ product_neg_left
+ product_neg_right
+ product_smul_const_left
+ product_smul_const_right
+ product_smul_left
+ product_smul_right
+ product_sub_left
+ product_sub_right
+ product_swap
+ product_zero_left
+ product_zero_right
+ rhs_aux
+ rhs_aux_addX
+ rhs_aux_addY
+ rhs_aux_addY_apply
+ rhs_aux_addZ
+ rhs_aux_addZ_apply
+ rhs_aux_smulX
+ rhs_aux_smulX_apply
+ rhs_aux_smulY
+ rhs_aux_smulY_apply
+ rhs_aux_smulY_const
+ rhs_aux_smulY_const_apply
+ rhs_aux_smulZ
+ rhs_aux_smulZ_apply
+ rhs_aux_smulZ_const
+ rhs_aux_smulZ_const_apply
+ rhs_aux_swap

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
635	1	erw
7373	1	backward.isDefEq

Current commit b7b1ec0d9c
Reference commit 2badb0c337

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh 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-dependent-issues]

This PR/issue depends on:

• feat: metric connections #36299
  By Dependent Issues (🤖). Happy coding!