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: [Merged by Bors] - feat: set integral for vector measures #40330
• depends on: [Merged by Bors] - feat: the semivariation of a vector measure #40384
• depends on: [Merged by Bors] - chore: move strong measurability proof to setToFun #40602
• depends on: [Merged by Bors] - chore: refactor the vector measure integral by changing the reference measure #40603
• depends on: [Merged by Bors] - feat: more API for set integrals wrt vector measures #40808
• depends on: feat: linear map from L^p (mu) to L^p (nu) when nu is bounded by a multiple of mu #40811
• depends on: [Merged by Bors] - chore: use NeBot in left and right limits #41079
• depends on: feat: vector measures with density wrt vector measures #41080

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

Import changes exceeding 2%

%	File
+73.57%	Mathlib.MeasureTheory.VectorMeasure.AddContent
+71.94%	Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.VectorMeasure.AddContent	1551	2692	+1141 (+73.57%)
Mathlib.MeasureTheory.VectorMeasure.BoundedVariation	1568	2696	+1128 (+71.94%)

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.VectorMeasure.BoundedVariation	1128
Mathlib.MeasureTheory.VectorMeasure.AddContent	1141
Mathlib.MeasureTheory.VectorMeasure.WithDensityVec (new file)	2348
Mathlib.MeasureTheory.VectorMeasure.Prod (new file)	2381

---

Declarations diff (regex)

+ HasProd
+ HasProd.flip
+ LpToLpOfMeasureLeSMul
+ LpToLpOfMeasureLeSMulₗ
+ MonotoneOn.boundedVariationOn
+ StronglyMeasurable.hasProd
+ _root_.BoundedVariationOn.eVariationOn_Ici_eq_Ioi_add_edist
+ _root_.BoundedVariationOn.eVariationOn_Iic_eq_Iio_add_edist
+ _root_.BoundedVariationOn.tendsto_eVariationOn_Icc_left
+ _root_.BoundedVariationOn.tendsto_eVariationOn_Icc_right
+ _root_.LocallyBoundedVariationOn.ofDual
+ _root_.LocallyBoundedVariationOn.tendsto_eVariationOn_Icc_left
+ _root_.LocallyBoundedVariationOn.tendsto_eVariationOn_Icc_right
+ _root_.MeasureTheory.AEStronglyMeasurable.integral_vectorMeasure_prod_right'
+ _root_.MeasureTheory.Integrable.integral_vectorMeasure_prod_left
+ _root_.MeasureTheory.Integrable.prod_vectorMeasure
+ _root_.MeasureTheory.Measure.variation_withDensityᵥ
+ _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'
+ coeFn_LpToLpOfMeasureLeSMul
+ coeFn_LpToLpOfMeasureLeSMulₗ
+ continuous_integral_integral
+ eLpNorm_le_of_measure_le_smul
+ eLpNorm_smul_measure_le
+ eVariationOn_Ico_eq_Icc_of_continuousWithinAt
+ eVariationOn_Ico_eq_Icc_of_continuousWithinAt'
+ eVariationOn_Ioc_eq_Icc_of_continuousWithinAt
+ eVariationOn_Ioc_eq_Icc_of_continuousWithinAt'
+ eVariationOn_Ioc_le_variation
+ eVariationOn_on_inter_Ici_eq_Ioi_add_edist
+ eVariationOn_on_inter_Iic_eq_Iio_add_edist
+ enorm_LpToLpOfMeasureLeSMulₗ_apply_le
+ eq_biSup_inter_Icc
+ exists_extension_of_isSetSemiring_of_le_measure
+ ext_of_generateFrom
+ hasProd_flip
+ hasProd_flip_iff
+ instance (hf : BoundedVariationOn f univ) : IsFiniteMeasure hf.variationAux := by
+ instance (hf : BoundedVariationOn f univ) : IsFiniteMeasure hf.vectorMeasure.variation := by
+ 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) :
+ integrable_vectorMeasure_prodMk_left
+ integral_integral
+ integral_integral_smul
+ integral_integral_smul_swap
+ integral_integral_smul_symm
+ integral_integral_swap
+ integral_integral_symm
+ integral_prod
+ integral_prod_smul
+ integral_prod_smul_symm
+ integral_prod_swap
+ integral_prod_symm
+ leftLim_eq
+ lintegral_fn_integral_sub
+ locallyBoundedVariation_ofDual
+ norm_LpToLpOfMeasureLeSMul
+ norm_LpToLpOfMeasureLeSMulₗ_apply_le
+ 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
+ rightLim_eq
+ stronglyMeasurable_vectorMeasure_prodMk_left
+ sub_left
+ sub_right
+ tendsto_iff_enorm_div_tendsto_zero
+ tendsto_left
+ tendsto_right
+ variationAux
+ variationAux_Ioc
+ variationAux_Ioc_le
+ variationAux_eq_variation_vectorMeasure
+ variationAux_singleton
+ variation_WithDensity_le
+ variation_apply_singleton
+ variation_prod_le
+ variation_vectorMeasure_Icc_le
+ variation_vectorMeasure_Ici_le
+ variation_vectorMeasure_Ico
+ variation_vectorMeasure_Ico_le
+ variation_vectorMeasure_Iic_le
+ variation_vectorMeasure_Iio
+ variation_vectorMeasure_Iio_le
+ variation_vectorMeasure_Ioc
+ variation_vectorMeasure_Ioc_le
+ variation_vectorMeasure_Ioi
+ variation_vectorMeasure_Ioi_le
+ variation_vectorMeasure_Ioo_le
+ variation_vectorMeasure_Ioo_left
+ variation_vectorMeasure_Ioo_right
+ variation_vectorMeasure_le_variationAux
+ variation_vectorMeasure_singleton
+ variation_vectorMeasure_univ_le
+ variation_withDensity
+ variation_withDensity'
+ withDensity
+ withDensity_apply
+ withDensity_apply_univ
+ withDensity_congr
+ withDensity_zero
+ withDensity_zero_vectorMeasure
- instance [SFinite μ] (c : ℝ≥0∞) : SFinite (c • μ) := by

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

Computed after the build finishes.

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
4974	1	exposed public sections

Current commit e9f44eb459
Reference commit 571b8a8e54

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
• [Merged by Bors] - feat: conditional expectation of an infinite sum #40187
• [Merged by Bors] - feat: more API for the variation of vector measures #40188
• [Merged by Bors] - feat: more API for integrals wrt vector measures #40198
• [Merged by Bors] - feat: more API for the integral wrt vector measures #40285
• [Merged by Bors] - feat: set integral for vector measures #40330
• [Merged by Bors] - feat: the semivariation of a vector measure #40384
• [Merged by Bors] - chore: move strong measurability proof to setToFun #40602
• [Merged by Bors] - chore: refactor the vector measure integral by changing the reference measure #40603
• [Merged by Bors] - feat: more API for set integrals wrt vector measures #40808
• feat: linear map from L^p (mu) to L^p (nu) when nu is bounded by a multiple of mu #40811
• [Merged by Bors] - chore: use NeBot in left and right limits #41079
• feat: vector measures with density wrt vector measures #41080
  By Dependent Issues (🤖). Happy coding!