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: 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

[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 2347eb48f3

Import changes exceeding 2%

%	File
+73.39%	Mathlib.MeasureTheory.VectorMeasure.AddContent
+71.76%	Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.VectorMeasure.AddContent	1548	2684	+1136 (+73.39%)
Mathlib.MeasureTheory.VectorMeasure.BoundedVariation	1565	2688	+1123 (+71.76%)

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.VectorMeasure.BoundedVariation	1123
Mathlib.MeasureTheory.VectorMeasure.AddContent	1136
Mathlib.MeasureTheory.VectorMeasure.WithDensityVec (new file)	2341
Mathlib.MeasureTheory.VectorMeasure.Prod (new file)	2374

---

Declarations diff (regex)

+ HasProd
+ HasProd.flip
+ Integrable.tendsto_setIntegral_nhds_zero
+ LpToLpOfMeasureLeSMul
+ LpToLpOfMeasureLeSMulₗ
+ StronglyMeasurable.hasProd
+ _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_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'
+ _root_.Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure
+ bar
+ baz
+ bloub
+ bloub2
+ coeFn_LpToLpOfMeasureLeSMul
+ coeFn_LpToLpOfMeasureLeSMulₗ
+ continuousLinearMap_apply_integral
+ 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'
+ enorm_LpToLpOfMeasureLeSMulₗ_apply_le
+ 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
+ ext_of_generateFrom
+ foo
+ glouk
+ hasProd_flip
+ hasProd_flip_iff
+ hasSum_setIntegral_iUnion
+ hasSum_setIntegral_iUnion_nat
+ instance (hf : BoundedVariationOn f univ) : IsFiniteMeasure hf.variationAux := 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_continuousLinearMap_comp
+ integral_iUnion
+ integral_indicator_const
+ 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
+ lintegral_fn_integral_sub
+ norm_LpToLpOfMeasureLeSMul
+ norm_LpToLpOfMeasureLeSMulₗ_apply_le
+ 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
+ setIntegral_const
+ 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_map
+ setIntegral_map_equiv
+ setIntegral_toSignedMeasure
+ setIntegral_union_eq_left_of_ae
+ setIntegral_union_eq_left_of_forall
+ stronglyMeasurable_vectorMeasure_prodMk_left
+ tendsto_iff_enorm_div_tendsto_zero
+ tendsto_setIntegral_of_L1
+ tendsto_setIntegral_of_L1'
+ variationAux
+ variation_WithDensity_le
+ variation_apply_singleton
+ variation_prod_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)
4955	1	exposed public sections

Current commit 2347eb48f3
Reference commit 9fbe5e0065

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
• 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
  By Dependent Issues (🤖). Happy coding!