IdentDistrib.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 9 curated AI-written annotations and 485 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2

25 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)

Imported by 3 files

lemma ProbabilityTheory.identDistrib_id_left line 26 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AEMeasurable, ProbabilityTheory.IdentDistrib, id, MeasureTheory.Measure.map
Proof uses: ProbabilityTheory.IdentDistrib.mk, aemeasurable_id, of_eq_true, Eq, Eq.trans, True, congrFun', congrArg, MeasureTheory.Measure.map_id, eq_self

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.identDistrib_id_right line 31 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AEMeasurable, ProbabilityTheory.IdentDistrib, id, MeasureTheory.Measure.map
Proof uses: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.identDistrib_id_left
lemma ProbabilityTheory.identDistrib_id line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Iff, ProbabilityTheory.IdentDistrib, id, Eq
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, And, AEMeasurable, MeasureTheory.Measure.map, propext, ProbabilityTheory.identDistrib_iff, congr, MeasureTheory.Measure.map_id, true_and, iff_self
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IdentDistrib.fst_id The first projection in a product space with measure μ.prod ν is distributed like μ line 38 source
Source documentation
The first projection in a product space with measure μ.prod ν is distributed like μ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IdentDistrib, Prod, Prod.fst, id, MeasureTheory.Measure.prod
Proof uses: Eq, MeasureTheory.Measure.map, of_eq_true, Eq.trans, True, congrArg, HSMul.hSMul, ENNReal, Set, Set.univ, MeasureTheory.Measure.map_fst_prod, OfNat.ofNat, congrFun', MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, eq_self, Eq.mpr, ProbabilityTheory.identDistrib_id_right, Measurable.aemeasurable, measurable_fst
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma IdentDistrib.fst_id
    {μ : Measure α} {ν : Measure β} [IsProbabilityMeasure ν] :
    IdentDistrib Prod.fst id (μ.prod ν) μ := by
…
```
lemma ProbabilityTheory.IdentDistrib.snd_id The second projection in a product space with measure μ.prod ν is distributed like ν line 46 source
Source documentation
The second projection in a product space with measure μ.prod ν is distributed like ν.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IdentDistrib, Prod, Prod.snd, id, MeasureTheory.Measure.prod
Proof uses: Eq, MeasureTheory.Measure.map, of_eq_true, Eq.trans, True, congrArg, HSMul.hSMul, ENNReal, Set, Set.univ, MeasureTheory.Measure.map_snd_prod, OfNat.ofNat, congrFun', MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, eq_self, Eq.mpr, ProbabilityTheory.identDistrib_id_right, Measurable.aemeasurable, measurable_snd
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma IdentDistrib.snd_id
    {μ : Measure α} {ν : Measure β} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
    IdentDistrib Prod.snd id (μ.prod ν) ν := by
…
```
lemma ProbabilityTheory.IdentDistrib.cond line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, MeasurableSet, Measurable, ProbabilityTheory.IdentDistrib, Prod, Prod.mk, ProbabilityTheory.cond, Set.preimage
Proof uses: ProbabilityTheory.IdentDistrib.mk, AEMeasurable.mono_ac, Function.comp, Prod.fst, AEMeasurable.comp_aemeasurable, Measurable.aemeasurable, MeasureTheory.Measure.map, measurable_fst, ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.cond_absolutelyContinuous, ProbabilityTheory.IdentDistrib.aemeasurable_snd, MeasureTheory.Measure.ext, Eq.mpr, Eq, ENNReal, id, congrArg, MeasureTheory.Measure.map_apply₀, ProbabilityTheory.IdentDistrib.comp, MeasurableSet.nullMeasurableSet and 18 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.identDistrib_comp_left A function is identically distributed to itself composed with a measurable embedding of conull range line 78 source
Source documentation
A function is identically distributed to itself composed with a measurable embedding of conull range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableEmbedding, Filter.Eventually, Membership.mem, Set, Set.range, MeasureTheory.ae, Measurable, ProbabilityTheory.IdentDistrib, Function.comp, MeasureTheory.Measure.comap
Proof uses: ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Measurable.comp, MeasurableEmbedding.measurable, Eq.mpr, Eq, MeasureTheory.Measure.map, id, congrArg, Eq.symm, MeasureTheory.Measure.map_map, MeasureTheory.Measure.restrict, MeasurableEmbedding.map_comap, MeasureTheory.Measure.restrict_eq_self_of_ae_mem, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma identDistrib_comp_left {i : δ → α} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂μ, a ∈ range i)
    (hf : Measurable f) : IdentDistrib (f ∘ i) f (μ.comap i) μ where
…
```
lemma ProbabilityTheory.identDistrib_comp_right A function is identically distributed to itself composed with a measurable embedding of conull range line 86 source
Source documentation
A function is identically distributed to itself composed with a measurable embedding of conull range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableEmbedding, Filter.Eventually, Membership.mem, Set, Set.range, MeasureTheory.ae, Measurable, ProbabilityTheory.IdentDistrib, Function.comp, MeasureTheory.Measure.comap
Proof uses: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.identDistrib_comp_left
6 instances, coercions and auxiliary constants left out.
```
lemma identDistrib_comp_right {i : δ → α} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂μ, a ∈ range i)
    (hf : Measurable f) : IdentDistrib f (f ∘ i) μ (μ.comap i) :=
…
```
lemma ProbabilityTheory.IdentDistrib.comp_left Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions line 94 source
Source documentation
Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableEmbedding, Filter.Eventually, Membership.mem, Set, Set.range, MeasureTheory.ae, Measurable, ProbabilityTheory.IdentDistrib, Function.comp, MeasureTheory.Measure.comap
Proof uses: ProbabilityTheory.IdentDistrib.trans, ProbabilityTheory.identDistrib_comp_left
6 instances, coercions and auxiliary constants left out.
```
lemma IdentDistrib.comp_left {i : δ → α} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂μ, a ∈ range i)
    (hf : Measurable f) (hfg : IdentDistrib f g μ ν) : IdentDistrib (f ∘ i) g (μ.comap i) ν :=
…
```
lemma ProbabilityTheory.IdentDistrib.comp_right Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions line 100 source
Source documentation
Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableEmbedding, Filter.Eventually, Membership.mem, Set, Set.range, MeasureTheory.ae, Measurable, ProbabilityTheory.IdentDistrib, Function.comp, MeasureTheory.Measure.comap
Proof uses: ProbabilityTheory.IdentDistrib.trans, ProbabilityTheory.identDistrib_comp_right
6 instances, coercions and auxiliary constants left out.
```
lemma IdentDistrib.comp_right {i : δ → β} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂ν, a ∈ range i)
    (hg : Measurable g) (hfg : IdentDistrib f g μ ν) : IdentDistrib f (g ∘ i) μ (ν.comap i) :=
…
```
lemma ProbabilityTheory._root_.MeasureTheory.MeasurePreserving.identDistrib line 104 source
theorem ProbabilityTheory.IdentDistrib.prodMk line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.IdentDistrib, ProbabilityTheory.IndepFun, Prod, Prod.mk
Proof uses: ProbabilityTheory.IdentDistrib.mk, AEMeasurable.prodMk, ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.IdentDistrib.aemeasurable_snd, Eq.mpr, Eq, MeasureTheory.Measure.map, MeasureTheory.Measure.prod, id, congrArg, Eq.mp, propext, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map, ProbabilityTheory.IdentDistrib.map_eq, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.AEMeasurable.piMk Move to a different section? line 136 source
Source documentation
Move to a different section?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Countable, AEMeasurable
Proof uses: Exists.intro, And, Measurable, Filter.EventuallyEq, MeasureTheory.ae, AEMeasurable.mk, And.intro, Measurable.of_eval, AEMeasurable.measurable_mk, Filter.mp_mem, Set.ofPred, Eq, Iff.mpr, Filter.Eventually, eventually_countable_forall, AEMeasurable.ae_eq_mk, Filter.univ_mem', Membership.mem, Set, id and 1 more
6 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma AEMeasurable.piMk {I : Type*} [Countable I] {F : I → Ω → β} (hF : ∀ i, AEMeasurable (F i) μ) :
    AEMeasurable (fun x i => F i x) μ := by
…
```
theorem ProbabilityTheory.IdentDistrib.iprodMk line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, ProbabilityTheory.IdentDistrib, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.iIndepFun
Proof uses: ProbabilityTheory.IdentDistrib.mk, ProbabilityTheory.AEMeasurable.piMk, ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.IdentDistrib.aemeasurable_snd, Fintype, Nonempty, Eq, nonempty_fintype, MeasureTheory.Measure.map, Nonempty.intro, Eq.mpr, MeasureTheory.Measure.pi, id, congrArg, Eq.mp, propext, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map, Eq.rec, Eq.refl, funext and 1 more
4 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
theorem ProbabilityTheory.IdentDistrib.mul line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Mul, MeasurableMul₂, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.IdentDistrib, ProbabilityTheory.IndepFun, HMul.hMul
Proof uses: ProbabilityTheory.IdentDistrib.comp_of_aemeasurable, Prod, Prod.mk, Prod.fst, Prod.snd, ProbabilityTheory.IdentDistrib.prodMk, Measurable.aemeasurable, MeasureTheory.Measure.map, MeasurableMul₂.measurable_mul
4 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.identDistrib_map A random variable is identically distributed to its pullbacks line 173 source
Source documentation
A random variable is identically distributed to its pullbacks.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Measurable, MeasureTheory.Measure, ProbabilityTheory.IdentDistrib, Function.comp, MeasureTheory.Measure.map
Proof uses: ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Measurable.comp, MeasureTheory.Measure.map_map
```
lemma identDistrib_map {X : Ω → α} (hX : Measurable X) {f : α → β} (hf : Measurable f)
    (μ : Measure Ω) : IdentDistrib f (f ∘ X) (μ.map X) μ where
…
```
lemma ProbabilityTheory.identDistrib_ulift_self line 179 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Measurable, ProbabilityTheory.IdentDistrib, ULift, Function.comp, ULift.down, MeasureTheory.Measure.comap
Proof uses: Measurable.comp, measurable_down, ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, MeasureTheory.Measure.ext, MeasureTheory.Measure.map, Set, MeasurableSet, Eq.mpr, Eq, ENNReal, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, Set.image, MeasureTheory.Measure.comap_apply, ULift.down_injective, Set.preimage_image_eq, Set.preimage_comp and 3 more
4 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.identDistrib_of_sum To show identical distribution of two random variables on a mixture of probability measures, it suffices to do so on each non-trivial component line 194 source
Source documentation
To show identical distribution of two random variables on a mixture of probability measures, it suffices to do so on each non-trivial component.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Finset, Measurable, Ne, OfNat.ofNat, ProbabilityTheory.IdentDistrib, Finset.sum, HSMul.hSMul
Proof uses: ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Eq.mpr, Eq, MeasureTheory.Measure.map, LinearMap, RingHom.id, MeasureTheory.Measure.mapₗ, id, congrArg, Eq.symm, MeasureTheory.Measure.mapₗ_apply_of_measurable, congr, Eq.trans, map_sum, RingHom, Finset.sum_congr, Eq.refl, Membership.mem, map_smul and 16 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma identDistrib_of_sum {X : Ω → α} {Y : Ω' → α} {μ : T → Measure Ω}
    {μ' : T → Measure Ω'} {w : T → ENNReal} (s : Finset T) (hX : Measurable X) (hY : Measurable Y)
    (h_ident : ∀ y, w y ≠ 0 → IdentDistrib X Y (μ y) (μ' y)) :
    IdentDistrib X Y (∑ y ∈ s, (w y) • (μ y)) (∑ y ∈ s, (w y) • (μ' y)) where
…
```
lemma ProbabilityTheory.identDistrib_comp_fst A random variable is identically distributed to its lift to a product space (in the first factor) line 212 source
Source documentation
A random variable is identically distributed to its lift to a product space (in the first factor).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IdentDistrib, Prod, Function.comp, Prod.fst, MeasureTheory.Measure.prod
Proof uses: ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Measurable.comp, measurable_fst, Eq.mpr, Eq, MeasureTheory.Measure.map, id, congrArg, Eq.symm, MeasureTheory.Measure.map_map, HSMul.hSMul, ENNReal, Set, Set.univ, MeasureTheory.Measure.map_fst_prod, Eq.rec, Eq.refl, of_eq_true, Eq.trans and 6 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma identDistrib_comp_fst {X : Ω → α} (hX : Measurable X) (μ : Measure Ω) (μ' : Measure Ω')
    [IsProbabilityMeasure μ'] : IdentDistrib (X ∘ Prod.fst) X (μ.prod μ') μ where
…
```
lemma ProbabilityTheory.identDistrib_comp_snd A random variable is identically distributed to its lift to a product space (in the second factor) line 223 source
Source documentation
A random variable is identically distributed to its lift to a product space (in the second factor).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Measurable, MeasureTheory.Measure, MeasureTheory.SigmaFinite, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IdentDistrib, Prod, Function.comp, Prod.snd, MeasureTheory.Measure.prod
Proof uses: ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Measurable.comp, measurable_snd, Eq.mpr, Eq, MeasureTheory.Measure.map, id, congrArg, Eq.symm, MeasureTheory.Measure.map_map, HSMul.hSMul, ENNReal, Set, Set.univ, MeasureTheory.Measure.map_snd_prod, Eq.rec, Eq.refl, of_eq_true, Eq.trans and 6 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma identDistrib_comp_snd {X : Ω → α} (hX : Measurable X) (μ : Measure Ω) (μ' : Measure Ω')
  [SigmaFinite μ] [IsProbabilityMeasure μ'] : IdentDistrib (X ∘ Prod.snd) X (μ'.prod μ) μ where
…
```
lemma ProbabilityTheory.independent_copies For X, Y random variables, one can find independent copies X', Y' of X, Y line 233 source
Source documentation
For X, Y random variables, one can find independent copies X', Y' of X, Y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Exists, Prod, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib
Proof uses: Exists.intro, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, Prod.fst, Prod.snd, And.intro, inferInstance, measurable_fst, measurable_snd, ProbabilityTheory.indepFun_fst_snd, ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, of_eq_true, Eq, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, ENNReal and 8 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma independent_copies {X : Ω → α} {Y : Ω' → β} (hX : Measurable X) (hY : Measurable Y)
    (μ : Measure Ω) (μ' : Measure Ω') [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
    ∃ ν : Measure (α × β), ∃ X' : α × β → α, ∃ Y' : α × β → β, IsProbabilityMeasure ν
      ∧ Measurable X' ∧ Measurable Y' ∧ IndepFun X' Y' ν
      ∧ IdentDistrib X' X ν μ ∧ IdentDistrib Y' Y ν μ' := by
…
```
lemma ProbabilityTheory.independent_copies_two For X, Y random variables, one can find independent copies X', Y' of X, Y line 244 source
Source documentation
For X, Y random variables, one can find independent copies X', Y' of X, Y. Version formulated in spaces with a canonical measures.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Exists, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib
Proof uses: Exists.intro, Prod, inferInstance, Function.comp, Prod.fst, Prod.snd, And.intro, Measurable.comp, measurable_fst, measurable_snd, ProbabilityTheory.IndepFun.comp, MeasureTheory.Measure.prod, ProbabilityTheory.indepFun_fst_snd, ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Eq, MeasureTheory.Measure, rfl, of_eq_true, MeasureTheory.Measure.map and 16 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma independent_copies_two {Ω : Type u} {Ω' : Type v} [MeasureSpace Ω] [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')]
    {X : Ω → α} {Y : Ω' → β} (hX : Measurable X) (hY : Measurable Y) :
    ∃ (Ω'' : Type (max u v)) (m'' : MeasureSpace Ω'') (X' : Ω'' → α) (Y' : Ω'' → β),
    IsProbabilityMeasure (ℙ : Measure Ω'') ∧ Measurable X' ∧ Measurable Y' ∧
      IndepFun X' Y' ∧ IdentDistrib X' X ∧ IdentDistrib Y' Y := by
…
```
lemma ProbabilityTheory.independent_copies' Let Xᵢ : Ωᵢ → Sᵢ be random variables for i = 1,...,k line 263 source
Source documentation
Let Xᵢ : Ωᵢ → Sᵢ be random variables for i = 1,...,k. Then there exist jointly independent random variables Xᵢ' : Ω' → Sᵢ for i=1,...,k such that each Xᵢ' is a copy of Xᵢ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, MeasurableSpace, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Exists, And, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Exists.intro, inferInstance, MeasureTheory.Measure.pi, Function.comp, Function.eval, And.intro, Eq.mpr, Finset, Set, Membership.mem, MeasurableSet, MeasurableSpace.comap, ENNReal, Set.iInter, Finset.prod and 32 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma independent_copies' {I : Type u} [Finite I] {α : I → Type u'}
    [mS : ∀ i : I, MeasurableSpace (α i)] {Ω : I → Type v}
    [mΩ : ∀ i : I, MeasurableSpace (Ω i)] (X : ∀ i : I, Ω i → α i) (hX : ∀ i : I, Measurable (X i))
    (μ : ∀ i : I, Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] :
    ∃ (A : Type (max u v)) (_ : MeasurableSpace A) (μA : Measure A) (X' : ∀ i, A → α i),
    IsProbabilityMeasure μA ∧ iIndepFun X' μA ∧
    ∀ i : I, Measurable (X' i) ∧ IdentDistrib (X' i) (X i) μA (μ i) := by
…
```
lemma ProbabilityTheory.independent_copies3_nondep A version with exactly 3 random variables that have the same codomain line 283 source
Source documentation
A version with exactly 3 random variables that have the same codomain. It's unfortunately incredibly painful to prove this from the general case.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Exists, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib
Proof uses: ULift, HAdd.hAdd, Fin.cases, inferInstance, Fin.succ, Fin.rec0, Function.comp, ULift.down, Measurable.comp, measurable_down, MeasureTheory.Measure.comap, ProbabilityTheory.independent_copies', Exists.intro, And.intro, Eq.mpr, eq_of_heq, Eq, autoParam, HEq, Eq.refl and 25 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma independent_copies3_nondep {α : Type u}
    [mS : MeasurableSpace α]
    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3}
    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃]
    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃)
    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃)
    [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [IsProbabilityMeasure μ₃] :
    ∃ (A : Type (max u_1 u_2 u_3)) (_ : MeasurableSpace A) (μA : Measure A) (X₁' X₂' X₃' : A → α),
      IsProbabilityMeasure μA ∧ iIndepFun ![X₁', X₂', X₃'] μA ∧
      Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧
      IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃ := by
…
```
lemma ProbabilityTheory.independent_copies4_nondep A version with exactly 4 random variables that have the same codomain line 327 source
Source documentation
A version with exactly 4 random variables that have the same codomain. It's unfortunately incredibly painful to prove this from the general case.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Exists, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib
Proof uses: ULift, HAdd.hAdd, Fin.cases, inferInstance, Fin.succ, Fin.rec0, Function.comp, ULift.down, Measurable.comp, measurable_down, MeasureTheory.Measure.comap, ProbabilityTheory.independent_copies', Exists.intro, And.intro, Eq.mpr, eq_of_heq, Eq, autoParam, HEq, Eq.refl and 25 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma independent_copies4_nondep {α : Type u}
    [mS : MeasurableSpace α]
    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3} {Ω₄ : Type u_4}
    [mΩ₁ : MeasurableSpace Ω₁] [mΩ₂ : MeasurableSpace Ω₂]
    [mΩ₃ : MeasurableSpace Ω₃] [mΩ₄ : MeasurableSpace Ω₄]
    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α} {X₄ : Ω₄ → α}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃) (hX₄ : Measurable X₄)
    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃) (μ₄ : Measure Ω₄)
    [hμ₁ : IsProbabilityMeasure μ₁] [hμ₂ : IsProbabilityMeasure μ₂]
    [hμ₃ : IsProbabilityMeasure μ₃] [hμ₄ : IsProbabilityMeasure μ₄] :
    ∃ (A : Type (max u_1 u_2 u_3 u_4)) (_ : MeasurableSpace A) (μA : Measure A)
      (X₁' X₂' X₃' X₄' : A → α),
…
```