+ ContDiffVectorBundle.isContMDiffRiemannianBundle
+ IsBilinearMap
+ IsBilinearMap.pullback
+ IsBilinearMap.pullback_clm
+ IsBilinearMap.pullback_clm_apply
+ IsBilinearMap.toContinuousLinearMap
+ IsBilinearMap.toContinuousLinearMap_apply
+ IsBilinearMap.toLinearMap
+ LinearMap.BilinMap.isBilinearMap
+ LinearMap.BilinMap.pullback
+ LinearMap.BilinMap.pullback_apply_basis
+ LinearMap.BilinMap.toContinuousLinearMap
+ LinearMap.BilinMap.toContinuousLinearMap_apply
+ RMetric
+ RMetric_aux
+ RMetric_local
+ RMetric_local_pre
+ V
+ W
+ aux
+ aux_special
+ aux_tvs
+ bar
+ condition
+ contMDiffOn_localExtensionOn
+ contMDiff_localSection
+ convex_condition
+ convex_condition1
+ convex_condition2
+ convex_mapsMatchingInner
+ convex_mapsMatchingInner2
+ convex_mapsMatchingInner3
+ evalL
+ foo_aux
+ foo_aux_prop
+ hloc
+ hloc3
+ hloc_TODO
+ instance (x : B) : AddCommGroup (W E x) := by
+ instance (x : B) : IsTopologicalAddGroup (V E x) := by
+ instance (x : B) : Module ℝ (V E x) := by
+ instance (x : B) : NormedAddCommGroup (W E x) := by
+ instance (x : B) : NormedSpace ℝ (V E x) := by
+ instance : (x : B) → AddCommGroup (V E x) := by
+ instance : (x : B) → Module ℝ (V E x) := by
+ instance : (x : B) → NormedAddCommGroup (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 : ContMDiffVectorBundle n (ℝ →L[ℝ] ℝ) (V E) IB := by
+ instance : ContMDiffVectorBundle n (ℝ →L[ℝ] ℝ) (W E) IB := by
+ instance : FiberBundle (F →L[ℝ] F →L[ℝ] ℝ) (W E) := by
+ instance : FiberBundle (F →L[ℝ] ℝ) (V E) := by
+ instance : FiberBundle (ℝ →L[ℝ] ℝ) (V E) := by
+ instance : FiberBundle (ℝ →L[ℝ] ℝ) (W E) := by
+ instance : TopologicalSpace (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) (W E)) := by
+ instance : TopologicalSpace (TotalSpace (F →L[ℝ] ℝ) (V E)) := by
+ instance : TopologicalSpace (TotalSpace (ℝ →L[ℝ] ℝ) (V E)) := by
+ instance : TopologicalSpace (TotalSpace (ℝ →L[ℝ] ℝ) (W E)) := by
+ instance : VectorBundle ℝ (F →L[ℝ] F →L[ℝ] ℝ) (W E) := by
+ instance : VectorBundle ℝ (F →L[ℝ] ℝ) (V E) := by
+ instance : VectorBundle ℝ (ℝ →L[ℝ] ℝ) (V E) := by
+ instance : VectorBundle ℝ (ℝ →L[ℝ] ℝ) (W E) := by
+ isBilinearMap_eval
+ isBilinearMap_evalL
+ is_good_localSection
+ localExtensionOn
+ local_section_at
+ mapsMatchingInner
+ mapsMatchingInner2
+ mapsMatchingInner3
+ mynorm
+ pullback_aux
+ pullback_bifunction
+ pullback_clm
+ pullback_clm_apply
+ pullback_clm_apply_basis
+ qux
+ rMetric_contMDiff
+ rMetric_eq
++ foo
++ instance (x : B) : ContinuousAdd (V E x) := by
++ instance (x : B) : ContinuousSMul ℝ (V E x) := by
++ instance (x : B) : Module ℝ (W E x) := by
++ instance (x : B) : TopologicalSpace (W E x) := by
++ instance : (x : B) → TopologicalSpace (V E x) := by

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

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

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

Current commit 1f5636ec7c
Reference commit cefe7b7756

You can run this locally as

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