[Merged by Bors] - feat: more API for the variation of vector measures

[sgouezel]

Prompted by the extension of the API around integrals wrt vector measures in #39113

---

[github-actions]

PR summary 06cfdd5534

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.VectorMeasure.Variation.Basic	1549	1572	+23 (+1.48%)

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.VectorMeasure.Variation.Basic	23

---

Declarations diff

+ _root_.MeasurableEmbedding.variation_map
+ dirac_zero
+ instance : CovariantClass ℝ≥0 ℝ≥0∞ (· • ·) (· ≤ ·)
+ instance : CovariantClass ℝ≥0∞ ℝ≥0∞ (· • ·) (· ≤ ·)
+ instance [Finite X] : IsFiniteMeasure μ.variation
+ instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.map φ).variation
+ instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation
+ instance [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [CovariantClass R ℝ≥0∞ (· • ·) (· ≤ ·)] :
+ instance {x : X} {v : V} : IsFiniteMeasure (VectorMeasure.dirac x v).variation := by
+ instance {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} [IsFiniteMeasure μ.variation] :
+ mapRange_smul
+ restrict_dirac
+ restrict_dirac_of_mem
+ restrict_dirac_of_notMem
+ restrict_inter_add_diff
+ restrict_restrict
+ restrict_singleton
+ restrict_union
+ restrict_union_add_inter
+ variation_apply_eq_zero
+ variation_apply_le_of_forall_enorm_le
+ variation_dirac
+ variation_eq_zero
+ variation_map_le
+ variation_restrict
+ variation_restrict_le
+ variation_smul
+ variation_smul_le

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 06cfdd5534
Reference commit 06f1f222bb

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

[EtienneC30]

Thanks!
maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

[RemyDegenne]

bors d+

[mathlib-bors]

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[sgouezel]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Post-Build Step