feat(Probability): add API for infinite product measures

[jvanwinden]

This PR introduces two lemmas which serve as API for infinite product measures:

• ProbabilityTheory.Measure.hasLaw_infinitePi_eval: the i-th coordinate on an infinite product measure has law μ i
• ProbabilityTheory.Measure.map_infinitePi_infinitePi_of_inj: when 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.

The second 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 2b6e69e442

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Probability.ProductMeasure	2441	2453	+12 (+0.49%)

Import changes for all files

Files	Import difference
Mathlib.Probability.ProductMeasure	12

---

Declarations diff

+ Measure.map_infinitePi_infinitePi_of_inj
+ hasLaw_infinitePi_eval

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

[CoolRmal]

Suggested change

	{P : (i : ι) → Measure (Ω i)} [∀ i, IsProbabilityMeasure (P i)] {f : ι → ι}
	{P : (i : ι) → Measure (Ω i)} [∀ i, IsProbabilityMeasure (P i)] {f : α → ι}

This domain of f can be an arbitrary type.