No significant changes to the import graph

+ Bundle.Trivial.mdifferentiableAt_iff
+ Bundle.pullback_diag
+ Bundle.torsion
+ ChristoffelSymbol
+ ChristoffelSymbol.sum_eq
+ ContMDiff.smul_section_of_tsupport'
+ ContMDiffCovariantDerivative
+ ContMDiffCovariantDerivative.affineCombination
+ ContMDiffCovariantDerivative.affineCombination'
+ ContMDiffCovariantDerivativeOn
+ ContMDiffWithinAt.orthogonalProjection
+ CovariantDerivative
+ 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_horiz
+ CovariantDerivative.mfderiv_proj_lift_vec
+ CovariantDerivative.orbit_geodVF
+ CovariantDerivative.proj_geodVF
+ CovariantDerivative.proj_lift_vec
+ FiberBundle.trivializationAt.baseSet_mem_nhds
+ IsBilinearMap
+ IsBilinearMap.toContinuousLinearMap
+ IsBilinearMap.toLinearMap
+ IsCompatible
+ IsCovariantDerivativeOn
+ IsCovariantDerivativeOn.fst_comp_lift_vec
+ IsCovariantDerivativeOn.lift_vec
+ IsCovariantDerivativeOn.lift_vec_apply
+ IsCovariantDerivativeOn.lift_vec_eq_iff
+ IsCovariantDerivativeOn.projection_lift_vec
+ IsLeviCivitaConnection
+ IsLeviCivitaConnection.eq_leviCivitaRhs
+ IsLeviCivitaConnection.uniqueness
+ IsLocalFrameOn.gramSchmidtNormed
+ IsMIntegralCurveAt.acceleration
+ IsMIntegralCurveAt.eventually_acceleration
+ IsMIntegralCurveAt.eventually_isMIntegralCurveAt
+ IsMIntegralCurveAt.mdifferentiableAt
+ IsMIntegralCurveAt.mfderiv
+ IsMIntegralCurveAt.proj_acceleration
+ IsMIntegralCurveAt.velocity_eventuallyEq
+ IsMIntegralCurveAt_iff_mfderiv
+ IsOrthonormalFrameOn
+ IsOrthonormalFrameOn.gramSchmidtNormed
+ IsOrthonormalFrameOn.mono
+ IsTorsionFree
+ IsTorsionFreeOn
+ LeviCivitaConnection
+ LeviCivitaConnection.christoffelSymbol_symm
+ LeviCivitaConnection_aux
+ LinearEquiv.comap_isCompl
+ LinearMap.comap_isCompl
+ MDifferentiable.inner_bundle'
+ MDifferentiableAt.inner_bundle'
+ V
+ W
+ _root_.Bundle.vert
+ _root_.ContMDiffCovariantDerivativeOn.affineCombination
+ _root_.ContMDiffCovariantDerivativeOn.affineCombination'
+ _root_.CovariantDerivative.exists_one_form
+ _root_.IsCovariantDerivativeOn.congr_iff_christoffelSymbol_eq
+ _root_.IsCovariantDerivativeOn.congr_of_christoffelSymbol_eq
+ _root_.IsCovariantDerivativeOn.isTorsionFreeOn_iff_localFrame
+ _root_.contMDiffAt_orthonormalFrame_of_mem
+ _root_.mdifferentiableAt_orthonormalFrame_of_mem
+ _root_.mdifferentiableAt_section_trivial_iff
+ add_one_form
+ apply_section_eventuallyEq
+ apply_symm_eventuallyEq
+ aux1
+ aux2
+ aux_computation
+ aux_computation2
+ aux_computation2'
+ aux_special
+ aux_tvs
+ bar
+ baseSet_mem_nhds
+ baseSet_prod_univ_mem_nhds
+ baz
+ bijective_deriv
+ bijective_symm
+ christoffelSymbol_zero
+ christoffelSymbol_zero_apply
+ coe_gramSchmidtBasis
+ coe_gramSchmidtNormedBasis
+ coeff_eq_inner'
+ comap_trivializationAt_horiz
+ comap_vert
+ comp_invFun_eventuallyEq
+ condition
+ condition1
+ condition2
+ congr_X_at
+ congr_of_forall_product
+ congr_σ_of_eqOn
+ congr_σ_smoothBumpFunction
+ contDiff_extend
+ contMDiffAt_aux
+ contMDiffAt_coeff
+ contMDiffAt_iff_coeff
+ contMDiffAt_iff_coeff'
+ contMDiffCovariantDerivativeOn_univ_iff
+ contMDiffOn_coeff
+ contMDiffOn_iff_coeff
+ contMDiffOn_iff_coeff'
+ contMDiffOn_localExtensionOn
+ contMDiffOn_orthonormalFrame_baseSet
+ contMDiffWithinAt_aux
+ contMDiffWithinAt_coeff
+ contMDiffWithinAt_inner
+ contMDiff_extend
+ contMDiff_localSection
+ convex_condition
+ convex_condition1
+ convex_condition2
+ coordChangeL_coordChangeL
+ coordChangeL_mem_horiz
+ coordChangeL_mem_horiz_iff
+ coordChangeL_pushCovDer
+ cov_eq_proj
+ deriv
+ derivInv
+ derivInv_deriv
+ derivInv_deriv_apply
+ deriv_derivInv
+ deriv_derivInv_apply
+ difference
+ differenceAux
+ differenceAux_apply
+ differenceAux_smul_eq
+ differenceAux_smul_eq'
+ differenceAux_tensorial
+ difference_apply
+ difference_def
+ eq_of
+ eq_one_form
+ eq_product_apply
+ evalL
+ exists_map_of
+ exists_one_form
+ extend
+ extend_add
+ extend_apply_self
+ extend_smul
+ extend_zero
+ foo
+ foo_aux
+ foo_aux_prop
+ foobar
+ fst_comp_eventuallyEq
+ 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 (cov : CovariantDerivative I F V) {s : Set M} :
+ 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 : CoeFun (CovariantDerivative I F V)
+ 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
+ isBilinearMap_differenceAux
+ isBilinearMap_eval
+ isBilinearMap_evalL
+ isCovariantDerivativeOn_lcCandidate
+ isCovariantDerivativeOn_lcCandidateAux
+ isCovariantDerivativeOn_lcCandidateAux_of_nonempty
+ isCovariantDerivativeOn_pushCovDer
+ isTorsionFreeOn_iff_christoffelSymbols
+ isTorsionFreeOn_univ
+ isTorsionFree_def
+ isTorsionFree_iff
+ isTorsionFree_iff_christoffelSymbols'
+ is_good_localSection
+ isolate_aux
+ lcCandidate
+ lcCandidateAux
+ lcCandidate_eq_lcCandidateAux
+ 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
+ localExtensionOn
+ localExtensionOn_apply_self
+ localExtensionOn_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
+ mdifferentiableAt
+ mdifferentiableAt_dependent_congr
+ mdifferentiableAt_invFun
+ mdifferentiableAt_section_of_function
+ mdifferentiable_dependent_congr_iff
+ mdifferentiable_extend
+ mem_horiz_iff_exists
+ mem_horiz_iff_proj
+ mem_span_gramSchmidt
+ mfderiv_comp_section
+ mfderiv_const_smul
+ mfderiv_proj_derivInv_apply
+ mfderiv_proj_fst_deriv
+ mfderiv_smul
+ mlieBracketWithin_smul_left
+ mlieBracketWithin_smul_right
+ mlieBracket_smul_left
+ mlieBracket_smul_right
+ mpullbackWithin_const_smul
+ mpullbackWithin_const_smul_apply
+ mpullback_const_smul
+ mpullback_const_smul_apply
+ mynorm
+ of_isCovariantDerivativeOn_of_open_cover
+ of_isCovariantDerivativeOn_of_open_cover_coe
+ of_isTorsionFreeOn_of_open_cover
+ of_subsingleton
+ one_form
+ orthonormalFrame
+ orthonormalFrame_apply_of_notMem
+ orthonormalFrame_isOrthonormalFrameOn
+ preimage_baseSet_mem_nhds
+ 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
+ proj
+ proj_acceleration
+ proj_invFun_eventuallyEq
+ proj_mderiv
+ proj_velocity
+ projection
+ projection_apply
+ pushCovDer
+ pushCovDer_isCovariantDerivativeOn
+ pushCovDer_ofSect
+ qux
+ 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
+ smul_const_X
+ snd_triv_proj
+ span_gramSchmidt
+ span_gramSchmidtNormed
+ span_gramSchmidtNormed_range
+ span_gramSchmidt_Iic
+ span_gramSchmidt_Iio
+ surjective_mfderiv_of_eventually_rightInverse
+ surjective_symm
+ symm_apply_apply_mk_eventuallyEq
+ symm_map_add
+ symm_map_smul
+ symm_map_zero
+ tensoriality_criterion
+ tensoriality_criterion'
+ tensoriality_criterion''
+ tensoriality_criterion₂
+ tensoriality_criterion₂'
+ torsion_add_left
+ torsion_add_left_apply
+ torsion_add_right
+ torsion_add_right_apply
+ torsion_antisymm
+ torsion_self
+ torsion_smul_left
+ torsion_smul_left_apply
+ torsion_smul_right
+ torsion_smul_right_apply
+ torsion_tensorial
+ torsion_zero
+ torsion_zero'
+ trivial_isSmooth
+ velocity
++ affineCombination
++ affineCombination'
++ aux
++ congr
++ horiz
++ horiz_vert_direct_sum
++ iUnion
++ mono
++ of_endomorphism
++ sum_X
++ trivial
++ zeroX
++ zeroσ

## 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.

Current commit c487a9a1d2
Reference commit 7c0aa26a8b

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).