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: 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: feat: more API for integrals wrt vector measures #40198

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

Import changes exceeding 2%

%	File
+72.40%	Mathlib.MeasureTheory.VectorMeasure.AddContent

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.VectorMeasure.AddContent	1551	2674	+1123 (+72.40%)

Import changes for all files

Files	Import difference
83 files Mathlib.InformationTheory.KullbackLeibler.ChainRule Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalLExpectation Mathlib.MeasureTheory.Function.ConvergenceInDistribution Mathlib.MeasureTheory.Function.FactorsThrough Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion Mathlib.MeasureTheory.Measure.LevyConvergence Mathlib.Probability.BorelCantelli Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily Mathlib.Probability.CentralLimitTheorem Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Distributions.Binomial Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Poisson.Basic Mathlib.Probability.Distributions.Poisson.PoissonLimitThm Mathlib.Probability.Distributions.SetBernoulli Mathlib.Probability.Distributions.TwoValued Mathlib.Probability.HasLawExists Mathlib.Probability.HasLaw Mathlib.Probability.IdentDistribIndep Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.BoundedContinuousFunction Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.InfinitePi Mathlib.Probability.Independence.Integration Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Kernel.CompProdEqIff Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.IonescuTulcea.Traj Mathlib.Probability.Kernel.Posterior Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Moments.Basic Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.CovarianceBilinDual Mathlib.Probability.Moments.CovarianceBilin Mathlib.Probability.Moments.Covariance Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted Mathlib.Probability.Moments.Variance Mathlib.Probability.Notation Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.FiniteDimensionalLaws Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.LocalProperty Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Predictable Mathlib.Probability.Process.Stopping Mathlib.Probability.ProductMeasure Mathlib.Probability.StrongLaw	1
Mathlib.MeasureTheory.VectorMeasure.Integral	3
Mathlib.MeasureTheory.VectorMeasure.BoundedVariation	1110
Mathlib.MeasureTheory.VectorMeasure.AddContent	1123
Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum (new file)	2267
Mathlib.MeasureTheory.VectorMeasure.SetIntegral (new file)	2280
Mathlib.MeasureTheory.VectorMeasure.WithDensityVec (new file)	2335

---

Declarations diff

+ Integrable.integrableOn
+ Integrable.map
+ Integrable.of_integral_ne_zero
+ Integrable.restrict
+ Integrable.tendsto_setIntegral_nhds_zero
+ IntegrableOn
+ IntegrableOn.empty
+ IntegrableOn.integrable_indicator
+ IntegrableOn.mono
+ IntegrableOn.union
+ _root_.MeasurableEmbedding.integrable_map_vectorMeasure
+ _root_.MeasurableEmbedding.integral_map_vectorMeasure
+ _root_.MeasurableEmbedding.setIntegral_map_vectorMeasure
+ _root_.MeasurableEmbedding.variation_transpose_map
+ _root_.Topology.IsClosedEmbedding.integral_map_vectorMeasure
+ _root_.Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure
+ absolutelyContinuous_variation_transpose
+ coeFn_tsum
+ condExp_tsum
+ continuousAt_of_dominated
+ continuousOn_of_dominated
+ continuousWithinAt_of_dominated
+ continuous_of_dominated
+ dist_integral_le_lintegral_edist
+ edist_integral_le_lintegral_edist
+ enorm_integral_le_lintegral_enorm
+ enorm_integral_le_of_enorm_le_const
+ enorm_setIntegral_le_lintegral_enorm
+ enorm_setIntegral_le_of_enorm_le_const
+ enorm_setIntegral_le_of_enorm_le_const_ae
+ exists_extension_of_isSetSemiring_of_le_measure
+ exists_ne_zero_of_integral_ne_zero
+ exists_ne_zero_of_setIntegral_ne_zero
+ frequently_ae_ne_zero_of_integral_ne_zero
+ frequently_ae_ne_zero_of_setIntegral_ne_zero
+ hasSum_coeFn_tsum
+ hasSum_coeFn_tsum_nat
+ hasSum_integral_of_dominated_convergence
+ hasSum_setIntegral_iUnion
+ hasSum_setIntegral_iUnion_nat
+ instance [IsFiniteMeasure μ.variation] :
+ integrableOn_biUnion_finite
+ integrableOn_biUnion_finset
+ integrableOn_iUnion_finite
+ integrableOn_univ
+ integrable_add_cbm
+ integrable_add_vectorMeasure
+ integrable_finsetSum_cbm
+ integrable_finsetSum_vectorMeasure
+ integrable_indicator_iff
+ integrable_zero_cbm
+ integrable_zero_vectorMeasure
+ integral_const
+ integral_dirac
+ integral_dirac'
+ integral_eq_setToFun
+ integral_iUnion
+ integral_indicator
+ integral_indicator_const
+ integral_indicator₂
+ integral_map
+ integral_map_equiv
+ integral_non_aestronglyMeasurable
+ integral_of_not_completeSpace
+ integral_piecewise
+ integral_singleton
+ integral_singleton'
+ integral_smul_nnreal_vectorMeasure
+ integral_smul_vectorMeasure
+ integral_toSignedMeasure
+ integral_tsum
+ integral_union_eq_left_of_ae
+ integral_union_eq_left_of_forall
+ integral_unique
+ nndist_integral_add_vectorMeasure_le_lintegral
+ norm_integral_le_lintegral_norm
+ norm_integral_le_of_norm_le_const
+ norm_setIntegral_le_of_norm_le_const
+ norm_setIntegral_le_of_norm_le_const_ae
+ restrict_withDensity
+ setIntegral_add_compl
+ setIntegral_biUnion_finset
+ setIntegral_compl
+ setIntegral_congr_ae
+ setIntegral_congr_fun
+ setIntegral_congr_set
+ setIntegral_const
+ setIntegral_diff
+ 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_diff_eq_zero
+ setIntegral_eq_of_subset_of_forall_diff_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_diff
+ setIntegral_map
+ setIntegral_map_equiv
+ setIntegral_toSignedMeasure
+ setIntegral_union
+ setIntegral_univ
+ setIntegral_vectorMeasure_zero
+ summable_norm_of_tsum_eLpNorm_ne_top
+ tendsto_integral_filter_of_dominated_convergence
+ tendsto_integral_filter_of_norm_le_const
+ tendsto_integral_of_L1
+ tendsto_integral_of_L1'
+ tendsto_integral_of_dominated_convergence
+ tendsto_setIntegral_of_L1
+ tendsto_setIntegral_of_L1'
+ transpose_add
+ transpose_dirac
+ transpose_map
+ transpose_restrict
+ transpose_smul
+ transpose_zero
+ variation_WithDensity_le
+ variation_transpose_eq
+ variation_transpose_eq_smul
+ variation_transpose_le
+ variation_transpose_lsmul
+ variation_transpose_lsmul_flip
+ variation_transpose_map_le
+ variation_withDensity
+ variation_withDensity'
+ variation_withDensityᵥ
+ withDensity
+ withDensity_apply
+ withDensity_apply_univ
+ withDensity_congr
+ withDensity_zero
+ withDensity_zero_vectorMeasure
- transpose_zero_vectorMeasure

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 7e091d0a5f
Reference commit 8ec10e9bfb

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: if an L^p space is complete, so is its target space unless the measure is zero #39614
• [Merged by Bors] - feat: drop completeness assumption in the definition of setToFun, expand API #39615
• [Merged by Bors] - feat: more API for the variation of vector measures #39616
• [Merged by Bors] - chore: cleanup Integral file #39652
• [Merged by Bors] - chore: drop completeness from the definition of conditional expectation #39862
• [Merged by Bors] - feat: more basic lemmas on norms and sums #40100
• [Merged by Bors] - feat: the smul on measures is ordered #40101
• [Merged by Bors] - chore: improve docstrings in Besicovitch file #40102
• [Merged by Bors] - feat: the integral of the enorm of the conditional expectation of an indicator is the measure of the set #40103
• [Merged by Bors] - chore: move dominated convergence to general versions for setToFun #40104
• [Merged by Bors] - feat: missing small lemmas in measure theory, cleanup #40106
• feat: conditional expectation of an infinite sum #40187
• [Merged by Bors] - feat: more API for the variation of vector measures #40188
• feat: more API for integrals wrt vector measures #40198
  By Dependent Issues (🤖). Happy coding!