+ AddContent.extendUnion
+ AddContent.extendUnionFun
+ AddContent.extendUnionFun_eq
+ AddContent.extendUnionFun_eq_of_mem
+ AddContent.extendUnion_eq
+ AddContent.extendUnion_eq_of_mem
+ AddContent.onIoc
+ AddContent.onIocAux
+ AddContent.onIocAux_apply
+ AddContent.onIocAux_empty
+ AddContent.onIoc_apply
+ BoundedVariationOn.addContent
+ Dense.lipschitzWith_extend
+ Ioc
+ Ioc_mem_Ioc_le
+ IsSetSemiring.diff_mem_finiteUnions
+ IsSetSemiring.isSetRing_finiteUnions
+ MeasuredSets
+ MeasuredSets.continuous_measure
+ MeasuredSets.edist_def
+ VectorMeasure.exists_extension_of_isSetRing_of_le_measure_of_dense
+ VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_dense
+ VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom
+ VectorMeasure.of_additive_of_le_measure
+ _root_.BoundedVariationOn.measure
+ _root_.Set.finiteUnions
+ _root_.Set.self_subset_finiteUnions
+ addContent_biUnion
+ enorm_mul_le_of_le'
+ enorm_mul₃_le'
+ enorm_mul₄_le'
+ exists_measure_symmDiff_lt_of_generateFrom
+ foo
+ instance (hf : BoundedVariationOn f univ) (x₀ : α) : IsFiniteMeasure (hf.measure x₀) := sorry
+ instance : FunLike (AddContent G C) (Set α) G
+ instance : Inhabited (AddContent G C)
+ instance : PseudoEMetricSpace (MeasuredSets μ)
+ instance : SetLike (MeasuredSets μ) α
+ norm_mul₄_le'
+ prod_biUnion_of_pairwise_eq_one
+ sum_addContent_eq_of_sUnion_eq
+ symmDiff_union_subset
+ union_symmDiff_subset
+ union_symmDiff_union_subset
- instance : FunLike (AddContent C) (Set α) ℝ≥0∞
- instance : Inhabited (AddContent C)

## 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 4a91171b40
Reference commit 721b21cf2b

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