feat: integration by parts for stieltjes vector measures

[sgouezel]

---

• depends on: [Merged by Bors] - feat: if an L^p space is complete, so is its target space unless the measure is zero #39614
• depends on: [Merged by Bors] - feat: drop completeness assumption in the definition of setToFun, expand API #39615
• depends on: [Merged by Bors] - feat: more API for the variation of vector measures #39616
• depends on: [Merged by Bors] - chore: cleanup Integral file #39652
• depends on: [Merged by Bors] - chore: drop completeness from the definition of conditional expectation #39862
• depends on: [Merged by Bors] - feat: more basic lemmas on norms and sums #40100
• depends on: [Merged by Bors] - feat: the smul on measures is ordered #40101
• depends on: [Merged by Bors] - chore: improve docstrings in Besicovitch file #40102
• depends on: [Merged by Bors] - feat: the integral of the enorm of the conditional expectation of an indicator is the measure of the set #40103
• depends on: [Merged by Bors] - chore: move dominated convergence to general versions for setToFun #40104
• depends on: [Merged by Bors] - feat: missing small lemmas in measure theory, cleanup #40106
• depends on: [Merged by Bors] - feat: conditional expectation of an infinite sum #40187
• depends on: [Merged by Bors] - feat: more API for the variation of vector measures #40188
• depends on: [Merged by Bors] - feat: more API for integrals wrt vector measures #40198
• depends on: [Merged by Bors] - feat: more API for the integral wrt vector measures #40285
• depends on: feat: set integral for vector measures #40330
• depends on: feat: the semivariation of a vector measure #40384
• depends on: chore: move strong measurability proof to setToFun #40602
• depends on: chore: refactor the vector measure integral by changing the reference measure #40603

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

[github-actions]

PR summary fbd3d8ed4a

Import changes exceeding 2%

%	File
+6.95%	Mathlib.Analysis.Normed.Group.Continuity
+73.23%	Mathlib.MeasureTheory.VectorMeasure.AddContent
+4.45%	Mathlib.Topology.UniformSpace.Dini

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.VectorMeasure.AddContent	1550	2685	+1135 (+73.23%)
Mathlib.Analysis.Normed.Group.Continuity	1238	1324	+86 (+6.95%)
Mathlib.Topology.UniformSpace.Dini	1393	1455	+62 (+4.45%)

Import changes for all files

Files	Import difference
35 files Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.IntegerCompl Mathlib.Analysis.Complex.ReImTopology Mathlib.Analysis.Complex.Spectrum Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Convex.Strong Mathlib.Analysis.InnerProductSpace.Affine Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.LocallyConvex.PointwiseConvergence Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Normed.Module.Normalize Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.RCLike.Extend Mathlib.Analysis.RCLike.TangentCone Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.NumberTheory.ModularForms.Cusps Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.Identities Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.NumberTheory.Padics.HeightOneSpectrum Mathlib.NumberTheory.Padics.WithVal Mathlib.RingTheory.HahnSeries.HahnEmbedding Mathlib.RingTheory.PowerSeries.Restricted Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Compactness.DeltaGeneratedSpace	6
Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli	8
Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups Mathlib.NumberTheory.ModularForms.CongruenceSubgroups	15
Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.Topology.ContinuousMap.Polynomial	16
Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Field.Ultra	18
7 files Mathlib.NumberTheory.ArithmeticFunction.Carmichael Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.RingHoms Mathlib.RingTheory.DividedPowers.Padic Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.ZMod.UnitsCyclic	20
Mathlib.Topology.Algebra.Polynomial	23
Mathlib.Analysis.Asymptotics.Completion	25
Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Ring.Ultra	30
Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Padics.PadicNumbers	43
Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.Unitary.Maps	46
Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Multilinear.Topology	53
Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli Mathlib.Topology.ContinuousMap.Bounded.Basic	56
8 files Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.Normed.Operator.Compact.Basic Mathlib.Analysis.Normed.Operator.Compact Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM Mathlib.Topology.Algebra.Module.StrongTopology	57
18 files Mathlib.Analysis.Calculus.TangentCone.ProperSpace Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.MetricSpace Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.Normed.Affine.Ceva Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Operator.Conformal Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Seminorm Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.UniformConvergence	58
3 files Mathlib.Analysis.Normed.Module.Extr Mathlib.Analysis.Normed.Module.Ray Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt	59
Mathlib.Topology.Bornology.BoundedOperation	60
6 files Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Topology.CWComplex.Classical.Basic Mathlib.Topology.CWComplex.Classical.Finite Mathlib.Topology.CWComplex.Classical.Graph Mathlib.Topology.CWComplex.Classical.Subcomplex	61
23 files Mathlib.Analysis.Calculus.TangentCone.DimOne Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Field.Instances Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.SeparationQuotient Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Module.Ball.Action Mathlib.Analysis.Normed.Module.Ball.RadialEquiv Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.RCLike.Real Mathlib.Analysis.Normed.Module.Shrink Mathlib.Analysis.Normed.Module.TransferInstance Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Ring.Int Mathlib.Analysis.Normed.Ring.Lemmas Mathlib.Analysis.NormedSpace.Real Mathlib.Topology.UniformSpace.Dini	62
Mathlib.Analysis.Normed.Group.NullSubmodule	66
Mathlib.Topology.Algebra.InfiniteSum.Field	71
Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.Continuity	86
Mathlib.MeasureTheory.VectorMeasure.BoundedVariation	1122
Mathlib.MeasureTheory.VectorMeasure.AddContent	1135
Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation (new file)	2126
Mathlib.MeasureTheory.VectorMeasure.SetIntegral (new file)	2282
Mathlib.MeasureTheory.VectorMeasure.WithDensityVec (new file)	2342
Mathlib.MeasureTheory.VectorMeasure.Prod (new file)	2375

---

Declarations diff (regex)

+ HasProd
+ HasProd.flip
+ Integrable.integrableOn
+ Integrable.tendsto_setIntegral_nhds_zero
+ IntegrableOn.biUnion_finite
+ IntegrableOn.biUnion_finset
+ IntegrableOn.empty
+ IntegrableOn.iUnion_finite
+ IntegrableOn.integrable_indicator
+ IntegrableOn.mono
+ IntegrableOn.union
+ LpToLpOfMeasureLeSMul
+ LpToLpOfMeasureLeSMulₗ
+ StronglyMeasurable.hasProd
+ StronglyMeasurable.setToFun_prod_right
+ _root_.MeasurableEmbedding.setIntegral_map_vectorMeasure
+ _root_.MeasureTheory.AEStronglyMeasurable.integral_vectorMeasure_prod_right'
+ _root_.MeasureTheory.Integrable.integral_vectorMeasure_prod_left
+ _root_.MeasureTheory.Integrable.prod_vectorMeasure
+ _root_.MeasureTheory.Measure.variation_toSignedMeasure
+ _root_.MeasureTheory.Measure.variation_withDensityᵥ
+ _root_.MeasureTheory.SignedMeasure.exists_subset_lt_enorm_apply_of_lt_variation
+ _root_.MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_left
+ _root_.MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_left'
+ _root_.MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_right
+ _root_.MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_right'
+ _root_.Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure
+ _root_.measurableSet_integrable
+ bound
+ coeFn_LpToLpOfMeasureLeSMul
+ coeFn_LpToLpOfMeasureLeSMulₗ
+ continuousLinearMap_apply_integral
+ continuous_integral
+ continuous_integral_integral
+ dominatedFinMeasAdditive_transpose_cbmApplyMeasure
+ eLpNorm_le_of_measure_le_smul
+ eLpNorm_smul_measure_le
+ enorm_LpToLpOfMeasureLeSMulₗ_apply_le
+ enorm_apply_le_bound
+ enorm_apply_le_semivariation
+ enorm_apply_le_semivariation_of_subset
+ enorm_integral_le_lintegral_enorm_transpose
+ enorm_setIntegral_le_lintegral_enorm
+ enorm_setIntegral_le_lintegral_enorm_transpose
+ enorm_setIntegral_le_of_enorm_le_const
+ enorm_setIntegral_le_of_enorm_le_const_ae
+ exists_extension_of_isSetSemiring_of_le_measure
+ exists_lt_sum_of_lt_variation
+ exists_ne_zero_of_setIntegral_ne_zero
+ exists_one_le_enorm_apply_of_semivariation_eq_top
+ exists_subset_lt_enorm_apply_of_lt_semivariation
+ ext_of_generateFrom
+ frequently_ae_ne_zero_of_setIntegral_ne_zero
+ hasProd_flip
+ hasProd_flip_iff
+ hasSum_setIntegral_iUnion
+ hasSum_setIntegral_iUnion_nat
+ instance [CompleteSpace G] [IsFiniteMeasure μ.variation] : HasProd μ ν B
+ instance [CompleteSpace G] [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] :
+ instance [CompleteSpace G] [h : IsFiniteMeasure ν.variation] : HasProd μ ν B := by
+ instance [SFinite μ] {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (c : R) :
+ integrableOn_univ
+ integrable_indicator_iff
+ integrable_vectorMeasure_prodMk_left
+ integral_continuousLinearMap_comp
+ integral_eq_setToFun_transpose
+ integral_iUnion
+ integral_indicator
+ integral_indicator_const
+ integral_integral
+ integral_integral_smul
+ integral_integral_smul_swap
+ integral_integral_smul_symm
+ integral_integral_swap
+ integral_integral_symm
+ integral_piecewise
+ integral_prod
+ integral_prod_smul
+ integral_prod_smul_symm
+ integral_prod_swap
+ integral_prod_symm
+ integral_singleton
+ integral_singleton'
+ lintegral_fn_integral_sub
+ mk_coe
+ nnnorm_apply_le_bound
+ norm_LpToLpOfMeasureLeSMul
+ norm_LpToLpOfMeasureLeSMulₗ_apply_le
+ norm_apply_le_bound
+ norm_integral_le_integral_norm
+ norm_setIntegral_le_of_norm_le_const
+ norm_setIntegral_le_of_norm_le_const_ae
+ of_biUnion
+ of_if
+ opENorm_flip
+ opENorm_lsmul
+ opENorm_lsmul_apply
+ opENorm_lsmul_le
+ opENorm_mul
+ opNNNorm_flip
+ prod
+ prodOfIsFiniteMeasureLeft
+ prod_apply
+ prod_apply_eq_integral
+ prod_eq_of_forall_apply_prod
+ prod_eq_zero_of_not_hasProd
+ prod_flip_apply_eq_integral
+ prod_mono
+ restrict_withDensity
+ semivariation
+ semivariation_apply_le_bound
+ semivariation_le_variation
+ semivariation_mono
+ semivariation_union_le
+ semivariation_univ_lt_top
+ setIntegral_add_compl
+ setIntegral_biUnion_finset
+ setIntegral_compl
+ setIntegral_congr_ae
+ setIntegral_congr_fun
+ setIntegral_congr_set
+ setIntegral_const
+ setIntegral_dirac
+ setIntegral_dirac'
+ setIntegral_empty
+ setIntegral_eq_integral_of_ae_compl_eq_zero
+ setIntegral_eq_integral_of_forall_compl_eq_zero
+ setIntegral_eq_of_subset_of_ae_sdiff_eq_zero
+ setIntegral_eq_of_subset_of_forall_sdiff_eq_zero
+ setIntegral_eq_zero_of_ae_eq_zero
+ setIntegral_eq_zero_of_forall_eq_zero
+ setIntegral_eq_zero_of_not_measurableSet
+ setIntegral_iUnion_fintype
+ setIntegral_indicator
+ setIntegral_inter_add_sdiff
+ setIntegral_map
+ setIntegral_map_equiv
+ setIntegral_of_variation_apply_eq_zero
+ setIntegral_sdiff
+ setIntegral_toSignedMeasure
+ setIntegral_union
+ setIntegral_union_eq_left_of_ae
+ setIntegral_union_eq_left_of_forall
+ setIntegral_univ
+ setToFun_simpleFunc_eq_setToSimpleFunc
+ setToSimpleFunc_eq_sum_of_subset
+ stronglyMeasurable_vectorMeasure_prodMk_left
+ tendsto_iff_enorm_div_tendsto_zero
+ tendsto_iff_enorm_inv_mul_tendsto_zero
+ tendsto_one_iff_enorm_tendsto_zero
+ tendsto_setIntegral_of_L1
+ tendsto_setIntegral_of_L1'
+ variation_WithDensity_le
+ variation_prod_le
+ variation_withDensity
+ variation_withDensity'
+ withDensity
+ withDensity_apply
+ withDensity_apply_univ
+ withDensity_congr
+ withDensity_zero
+ withDensity_zero_vectorMeasure
- Integrable.add_cbm
- Integrable.finsetSum_cbm
- Integrable.neg_cbm
- Integrable.sub_cbm
- Integrable.zero_cbm
- instance [SFinite μ] (c : ℝ≥0∞) : SFinite (c • μ) := by
- measurableSet_integrable
- variation_toSignedMeasure

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)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit fbd3d8e).

• +169 new declarations
• −7 removed declarations

+ContinuousLinearMap.opENorm_flip
+ContinuousLinearMap.opENorm_lsmul
+ContinuousLinearMap.opENorm_lsmul_apply
+ContinuousLinearMap.opENorm_lsmul_le
+ContinuousLinearMap.opENorm_mul
+ContinuousLinearMap.opNNNorm_flip
+MeasurableEmbedding.setIntegral_map_vectorMeasure
+MeasureTheory.AEStronglyMeasurable.integral_vectorMeasure_prod_right'
+MeasureTheory.Integrable.integral_vectorMeasure_prod_left
+MeasureTheory.Integrable.prod_vectorMeasure
+MeasureTheory.Lp.LpToLpOfMeasureLeSMul
+MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ
+MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ.congr_simp
+MeasureTheory.Lp.coeFn_LpToLpOfMeasureLeSMul
+MeasureTheory.Lp.coeFn_LpToLpOfMeasureLeSMulₗ
+MeasureTheory.Lp.enorm_LpToLpOfMeasureLeSMulₗ_apply_le
+MeasureTheory.Lp.norm_LpToLpOfMeasureLeSMul
+MeasureTheory.Lp.norm_LpToLpOfMeasureLeSMulₗ_apply_le
+MeasureTheory.Measure.prod_mono
+MeasureTheory.Measure.variation_toSignedMeasure
+MeasureTheory.Measure.variation_withDensityᵥ
+MeasureTheory.SignedMeasure.exists_subset_lt_enorm_apply_of_lt_variation
+MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_of_subset
+MeasureTheory.StronglyMeasurable.hasProd
+MeasureTheory.StronglyMeasurable.hasSum
+MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_left
+MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_left'
+MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_right
+MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_right'
+MeasureTheory.StronglyMeasurable.setToFun_prod_right
+MeasureTheory.VectorMeasure.HasProd
+MeasureTheory.VectorMeasure.HasProd.casesOn
+MeasureTheory.VectorMeasure.HasProd.exists_prod
+MeasureTheory.VectorMeasure.HasProd.flip
+MeasureTheory.VectorMeasure.HasProd.mk
+MeasureTheory.VectorMeasure.HasProd.rec
+MeasureTheory.VectorMeasure.HasProd.recOn
-MeasureTheory.VectorMeasure.Integrable.add_cbm
-MeasureTheory.VectorMeasure.Integrable.finsetSum_cbm
+MeasureTheory.VectorMeasure.Integrable.integrableOn
-MeasureTheory.VectorMeasure.Integrable.neg_cbm
-MeasureTheory.VectorMeasure.Integrable.sub_cbm
+MeasureTheory.VectorMeasure.Integrable.tendsto_setIntegral_nhds_zero
-MeasureTheory.VectorMeasure.Integrable.zero_cbm
+MeasureTheory.VectorMeasure.IntegrableOn.biUnion_finite
+MeasureTheory.VectorMeasure.IntegrableOn.biUnion_finset
+MeasureTheory.VectorMeasure.IntegrableOn.empty
+MeasureTheory.VectorMeasure.IntegrableOn.iUnion_finite
+MeasureTheory.VectorMeasure.IntegrableOn.integrable_indicator
+MeasureTheory.VectorMeasure.IntegrableOn.mono
+MeasureTheory.VectorMeasure.IntegrableOn.union
+MeasureTheory.VectorMeasure.bound
+MeasureTheory.VectorMeasure.continuousLinearMap_apply_integral
+MeasureTheory.VectorMeasure.continuous_integral
+MeasureTheory.VectorMeasure.continuous_integral_integral
+MeasureTheory.VectorMeasure.enorm_apply_le_bound
+MeasureTheory.VectorMeasure.enorm_apply_le_semivariation
+MeasureTheory.VectorMeasure.enorm_apply_le_semivariation_of_subset
+MeasureTheory.VectorMeasure.enorm_integral_le_lintegral_enorm_transpose
+MeasureTheory.VectorMeasure.enorm_setIntegral_le_lintegral_enorm
+MeasureTheory.VectorMeasure.enorm_setIntegral_le_lintegral_enorm_transpose
+MeasureTheory.VectorMeasure.enorm_setIntegral_le_of_enorm_le_const
+MeasureTheory.VectorMeasure.enorm_setIntegral_le_of_enorm_le_const_ae
+MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure
+MeasureTheory.VectorMeasure.exists_lt_sum_of_lt_variation
+MeasureTheory.VectorMeasure.exists_ne_zero_of_setIntegral_ne_zero
+MeasureTheory.VectorMeasure.exists_subset_lt_enorm_apply_of_lt_semivariation
+MeasureTheory.VectorMeasure.ext_of_generateFrom
+MeasureTheory.VectorMeasure.frequently_ae_ne_zero_of_setIntegral_ne_zero
+MeasureTheory.VectorMeasure.hasProd_flip
+MeasureTheory.VectorMeasure.hasProd_flip_iff
+MeasureTheory.VectorMeasure.hasSum_setIntegral_iUnion
+MeasureTheory.VectorMeasure.instHasProdOfCompleteSpaceOfIsFiniteMeasureVariation
+MeasureTheory.VectorMeasure.instHasProdOfCompleteSpaceOfIsFiniteMeasureVariation_1
+MeasureTheory.VectorMeasure.instIsFiniteMeasureProdVariationProdOfCompleteSpace
+MeasureTheory.VectorMeasure.integrableOn_univ
+MeasureTheory.VectorMeasure.integrable_indicator_iff
+MeasureTheory.VectorMeasure.integrable_vectorMeasure_prodMk_left
+MeasureTheory.VectorMeasure.integral_continuousLinearMap_comp
+MeasureTheory.VectorMeasure.integral_eq_setToFun_transpose
+MeasureTheory.VectorMeasure.integral_iUnion
+MeasureTheory.VectorMeasure.integral_indicator
+MeasureTheory.VectorMeasure.integral_indicator_const
+MeasureTheory.VectorMeasure.integral_integral
+MeasureTheory.VectorMeasure.integral_integral_smul
+MeasureTheory.VectorMeasure.integral_integral_smul_swap
+MeasureTheory.VectorMeasure.integral_integral_smul_symm
+MeasureTheory.VectorMeasure.integral_integral_swap
+MeasureTheory.VectorMeasure.integral_integral_symm
+MeasureTheory.VectorMeasure.integral_piecewise
+MeasureTheory.VectorMeasure.integral_prod
+MeasureTheory.VectorMeasure.integral_prod_smul
+MeasureTheory.VectorMeasure.integral_prod_smul_symm
+MeasureTheory.VectorMeasure.integral_prod_swap
+MeasureTheory.VectorMeasure.integral_prod_symm
+MeasureTheory.VectorMeasure.integral_singleton
+MeasureTheory.VectorMeasure.integral_singleton'
+MeasureTheory.VectorMeasure.lintegral_fn_integral_sub
+MeasureTheory.VectorMeasure.nnnorm_apply_le_bound
+MeasureTheory.VectorMeasure.norm_apply_le_bound
+MeasureTheory.VectorMeasure.norm_integral_le_integral_norm
+MeasureTheory.VectorMeasure.norm_setIntegral_le_of_norm_le_const
+MeasureTheory.VectorMeasure.norm_setIntegral_le_of_norm_le_const_ae
+MeasureTheory.VectorMeasure.of_biUnion
+MeasureTheory.VectorMeasure.of_if
+MeasureTheory.VectorMeasure.prod
+MeasureTheory.VectorMeasure.prodOfIsFiniteMeasureLeft
+MeasureTheory.VectorMeasure.prod_apply
+MeasureTheory.VectorMeasure.prod_apply_eq_integral
+MeasureTheory.VectorMeasure.prod_eq_of_forall_apply_prod
+MeasureTheory.VectorMeasure.prod_eq_zero_of_not_hasProd
+MeasureTheory.VectorMeasure.prod_flip_apply_eq_integral
+MeasureTheory.VectorMeasure.restrict_withDensity
+MeasureTheory.VectorMeasure.semivariation
+MeasureTheory.VectorMeasure.semivariation_apply_le_bound
+MeasureTheory.VectorMeasure.semivariation_le_variation
+MeasureTheory.VectorMeasure.semivariation_mono
+MeasureTheory.VectorMeasure.semivariation_union_le
+MeasureTheory.VectorMeasure.setIntegral_add_compl
+MeasureTheory.VectorMeasure.setIntegral_biUnion_finset
+MeasureTheory.VectorMeasure.setIntegral_compl
+MeasureTheory.VectorMeasure.setIntegral_congr_ae
+MeasureTheory.VectorMeasure.setIntegral_congr_fun
+MeasureTheory.VectorMeasure.setIntegral_congr_set
+MeasureTheory.VectorMeasure.setIntegral_const
+MeasureTheory.VectorMeasure.setIntegral_dirac
+MeasureTheory.VectorMeasure.setIntegral_dirac'
+MeasureTheory.VectorMeasure.setIntegral_empty
+MeasureTheory.VectorMeasure.setIntegral_eq_integral_of_ae_compl_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_integral_of_forall_compl_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_of_subset_of_ae_sdiff_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_of_subset_of_forall_sdiff_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_ae_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_forall_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_not_measurableSet
+MeasureTheory.VectorMeasure.setIntegral_iUnion_fintype
+MeasureTheory.VectorMeasure.setIntegral_indicator
+MeasureTheory.VectorMeasure.setIntegral_inter_add_sdiff
+MeasureTheory.VectorMeasure.setIntegral_map
+MeasureTheory.VectorMeasure.setIntegral_map_equiv
+MeasureTheory.VectorMeasure.setIntegral_of_variation_apply_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_sdiff
+MeasureTheory.VectorMeasure.setIntegral_toSignedMeasure
+MeasureTheory.VectorMeasure.setIntegral_union
+MeasureTheory.VectorMeasure.setIntegral_union_eq_left_of_ae
+MeasureTheory.VectorMeasure.setIntegral_union_eq_left_of_forall
+MeasureTheory.VectorMeasure.setIntegral_univ
+MeasureTheory.VectorMeasure.stronglyMeasurable_vectorMeasure_prodMk_left
+MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1
+MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1'
+MeasureTheory.VectorMeasure.variation_WithDensity_le
+MeasureTheory.VectorMeasure.variation_prod_le
-MeasureTheory.VectorMeasure.variation_toSignedMeasure
+MeasureTheory.VectorMeasure.variation_withDensity
+MeasureTheory.VectorMeasure.variation_withDensity'
+MeasureTheory.VectorMeasure.withDensity
+MeasureTheory.VectorMeasure.withDensity_apply
+MeasureTheory.VectorMeasure.withDensity_apply_univ
+MeasureTheory.VectorMeasure.withDensity_congr
+MeasureTheory.VectorMeasure.withDensity_fun_zero
+MeasureTheory.VectorMeasure.withDensity_zero
+MeasureTheory.VectorMeasure.withDensity_zero_vectorMeasure
+MeasureTheory.dominatedFinMeasAdditive_transpose_cbmApplyMeasure
+MeasureTheory.eLpNorm_le_of_measure_le_smul
+MeasureTheory.eLpNorm_smul_measure_le
-MeasureTheory.instSFiniteHSMulENNRealMeasure
+MeasureTheory.instSFiniteHSMulMeasure
+MeasureTheory.setToFun_simpleFunc_eq_setToSimpleFunc
+NNReal.mk_coe
+Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure
+tendsto_iff_enorm_div_tendsto_zero
+tendsto_iff_enorm_inv_mul_tendsto_zero
+tendsto_iff_enorm_neg_add_tendsto_zero
+tendsto_iff_enorm_sub_tendsto_zero
+tendsto_one_iff_enorm_tendsto_zero
+tendsto_zero_iff_enorm_tendsto_zero

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
4943	2	exposed public sections

Current commit fbd3d8ed4a
Reference commit 271d273e99

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