[Merged by Bors] - feat(Probability/Independence/InfinitePi): rearrangement of infinite product measures

[jvanwinden]

This PR introduces a lemma for coordinate transformations of infinitePi measures.

• MeasureTheory.Measure.map_infinitePi_infinitePi_of_inj: if f : α → ι is injective, then the pushforward of the coordinates rearranged according to f (i.e., the law of fun ω i ↦ ω (f i) is the same as the infinite product of the rearranged laws.

This lemma bears some resemblance to infinitePi_map_piCongrLeft, but does not require f to be a bijection and probably is easier to work with in practice.

---

[github-actions]

PR summary 6bc2dbd211

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.MeasureTheory.Measure.map_infinitePi_infinitePi_of_inj

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.

[CoolRmal]

I think you should move the first lemmas into other places. No theorems in Mathlib start with ProbabilityTheory.Measure (so maybe you should also change your description of this PR).

Maybe you can move map_infinitePi_infinitePi_of_inj into Mathlib.Probability.ProductMeasure, and use it to golf (or prove analogues of) infinitePi_map_piCongrLeft

[EtienneC30]

Maybe you can move map_infinitePi_infinitePi_of_inj into Mathlib.Probability.ProductMeasure, and use it to golf (or prove analogues of) infinitePi_map_piCongrLeft

I agree it's not ideal to use independence to prove map_infinitePi_infinitePi_of_inj which a priori is more fundamental, but I also think that this gives a nicer proof and that it is in some sense a special case of the independence result, so I'd say we can keep it there.

[jvanwinden]

-awaiting-author

[EtienneC30]

Thanks! Can you just update the PR title and description please?
maintainer delegate

[github-actions]

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

[jvanwinden]

-awaiting-author

[RemyDegenne]

Thanks!
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