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

23 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)

Imported by 2 files

structure ProbabilityTheory.IsUniform The assertion that the law of $X$ is the uniform probability measure on a finite set $H$ line 24 source
Source documentation
The assertion that the law of $X$ is the uniform probability measure on a finite set $H$. While in applications $H$ will be non-empty finite set, $X$ measurable, and and $μ$ a probability measure, it could be technically convenient to have a definition that works even without these hypotheses. (For instance, isUniform would be well-defined, but false, for infinite H).
This should probably be refactored, requiring instead that μ.map X = uniformOn H.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Set, autoParam, MeasureTheory.Measure
1 instances, coercions and auxiliary constants left out.
```
structure IsUniform (H : Set S) (X : Ω → S) (μ : Measure Ω := by volume_tac) : Prop where
…
```
lemma ProbabilityTheory.isUniform_uniformOn line 28 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, ProbabilityTheory.IsUniform, id, ProbabilityTheory.uniformOn
Proof uses: ProbabilityTheory.IsUniform.mk, Membership.mem, Eq, Inter.inter, Singleton.singleton, Set.ext, of_eq_true, Iff, Eq.trans, True, congr, congrArg, congrFun', Set.inter_eq_left', LE.le, eq_true, iff_self, ENNReal, autoParam, MeasureTheory.Measure and 15 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.exists_isUniform Uniform distributions exist line 38 source
Source documentation
Uniform distributions exist.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Finset, Finset.Nonempty, Exists, MeasureTheory.Measure, And, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IsUniform, Membership.mem, FiniteRange
Proof uses: Exists.intro, Subtype, HSMul.hSMul, ENNReal, Inv.inv, Finset.card, Finset.sum, Finset.univ, MeasureTheory.Measure.dirac, And.intro, MeasureTheory.IsProbabilityMeasure.mk, Eq.mpr, Eq, Set, Set.univ, OfNat.ofNat, HMul.hMul, id, congrFun', congrArg and 48 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma exists_isUniform [MeasurableSpace S] [MeasurableSingletonClass S]
    (H : Finset S) (h : H.Nonempty) :
    ∃ (Ω : Type uS) (_ : MeasurableSpace Ω) (X : Ω → S) (μ : Measure Ω),
      IsProbabilityMeasure μ ∧ Measurable X ∧ IsUniform H X μ ∧ (∀ ω, X ω ∈ H) ∧ FiniteRange X := by
…
```
Mentions: ProbabilityTheory.IsUniform, FiniteRange
lemma ProbabilityTheory.IsUniform.comp The image of a uniform random variable under an injective map is uniform on the image line 68 source
Source documentation
The image of a uniform random variable under an injective map is uniform on the image.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DecidableEq, Finset, ProbabilityTheory.IsUniform, Function.Injective, Finset.image, Function.comp
Proof uses: ProbabilityTheory.IsUniform.mk, Membership.mem, Set, And, Eq, Exists, ENNReal, autoParam, Set.preimage, Singleton.singleton, Eq.mp, Eq.trans, Set.image, congrFun', congrArg, Finset.coe_image, funext, Set.ext, of_eq_true, Iff and 13 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.comp [DecidableEq T] {H : Finset S} (h : IsUniform H X μ) {f : S → T}
    (hf : Injective f) : IsUniform (Finset.image f H) (f ∘ X) μ where
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.exists_isUniform_measureSpace Uniform distributions exist, version giving a measure space line 80 source
Source documentation
Uniform distributions exist, version giving a measure space

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Finset, Finset.Nonempty, Exists, MeasureTheory.MeasureSpace, And, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IsUniform, Membership.mem, FiniteRange
Proof uses: MeasureTheory.Measure, ProbabilityTheory.exists_isUniform, Exists.intro, MeasureTheory.MeasureSpace.mk, And.intro
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma exists_isUniform_measureSpace {S : Type uS} [MeasurableSpace S]
    [MeasurableSingletonClass S] (H : Finset S) (h : H.Nonempty) :
    ∃ (Ω : Type uS) (mΩ : MeasureSpace Ω) (U : Ω → S),
    IsProbabilityMeasure (ℙ : Measure Ω) ∧ Measurable U ∧ IsUniform H U ∧ (∀ ω : Ω, U ω ∈ H) ∧
      FiniteRange U := by
…
```
Mentions: ProbabilityTheory.IsUniform, FiniteRange
lemma ProbabilityTheory.exists_isUniform_measureSpace' Uniform distributions exist, version with a Finite set rather than a Finset and giving a measure space line 90 source
Source documentation
Uniform distributions exist, version with a Finite set rather than a Finset and giving a measure space

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Set.Finite, Set.Nonempty, Exists, MeasureTheory.MeasureSpace, And, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IsUniform, Membership.mem, FiniteRange
Proof uses: Finset, Set.Finite.toFinset, Finset.Nonempty, Eq.mpr, id, Eq, ProbabilityTheory.exists_isUniform_measureSpace, Exists.intro, And.intro, Eq.mp, congrFun', MeasureTheory.Measure, autoParam, congrArg, Set.Finite.coe_toFinset, forall_congr
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma exists_isUniform_measureSpace' {S : Type uS} [MeasurableSpace S]
    [MeasurableSingletonClass S] (H : Set S) (hH : H.Finite) (h'H : H.Nonempty) :
    ∃ (Ω : Type uS) (mΩ : MeasureSpace Ω) (U : Ω → S),
    IsProbabilityMeasure (ℙ : Measure Ω) ∧ Measurable U ∧ IsUniform H U
      ∧ (∀ ω, U ω ∈ H) ∧ FiniteRange U := by
…
```
Mentions: ProbabilityTheory.IsUniform, FiniteRange
lemma ProbabilityTheory.IsUniform.ae_mem A uniform random variable on H almost surely takes values in H line 102 source
Source documentation
A uniform random variable on H almost surely takes values in H.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, ProbabilityTheory.IsUniform, Filter.Eventually, Membership.mem, MeasureTheory.ae
Proof uses: ProbabilityTheory.IsUniform.measure_preimage_compl
3 instances, coercions and auxiliary constants left out.
```
lemma IsUniform.ae_mem (h : IsUniform H X μ) : ∀ᵐ ω ∂μ, X ω ∈ H := h.measure_preimage_compl
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.nonempty Uniform random variables only exist for non-empty sets H line 105 source
Source documentation
Uniform random variables only exist for non-empty sets H.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finset, ProbabilityTheory.IsUniform, NeZero, Finset.Nonempty
Proof uses: Eq, EmptyCollection.emptyCollection, Or, Finset.eq_empty_or_nonempty, Eq.mpr, False, id, False.elim, Eq.mp, ENNReal, autoParam, Set, Set.preimage, Compl.compl, OfNat.ofNat, Eq.trans, Set.univ, congrFun', congrArg, Finset.coe_empty and 5 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.nonempty {H : Finset S} (h : IsUniform H X μ) [hμ : NeZero μ] : H.Nonempty := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.measure_preimage_of_nmem A "unit test" for the definition of uniform distribution line 111 source
Source documentation
A "unit test" for the definition of uniform distribution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, ProbabilityTheory.IsUniform, Not, Membership.mem, Eq, ENNReal, Set.preimage, Singleton.singleton, OfNat.ofNat
Proof uses: le_antisymm, autoParam, LE.le.trans, Compl.compl, MeasureTheory.measure_mono, Set.preimage_mono, Eq.mpr, LE.le, id, Eq.trans, Eq.le, ProbabilityTheory.IsUniform.measure_preimage_compl, zero_le
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measure_preimage_of_nmem (h : IsUniform H X μ) {s : S} (hs : s ∉ H) :
    μ (X ⁻¹' {s}) = 0 := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.measureReal_preimage_of_nmem Another "unit test" for the definition of uniform distribution line 118 source
Source documentation
Another "unit test" for the definition of uniform distribution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, ProbabilityTheory.IsUniform, Not, Membership.mem, Eq, Real, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, OfNat.ofNat
Proof uses: Eq.mpr, ENNReal.toReal, ENNReal, id, congrArg, MeasureTheory.measureReal_def, ProbabilityTheory.IsUniform.measure_preimage_of_nmem, ENNReal.toReal_zero, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measureReal_preimage_of_nmem (h : IsUniform H X μ) {s : S} (hs : s ∉ H) :
    μ.real (X ⁻¹' {s}) = 0 := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.measure_preimage_of_mem A "unit test" for the definition of uniform distribution line 125 source
Source documentation
A "unit test" for the definition of uniform distribution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, Finset, ProbabilityTheory.IsUniform, Measurable, Membership.mem, Eq, ENNReal, Set, Set.preimage, Singleton.singleton, HDiv.hDiv, Set.univ, Nat.card, Subtype
Proof uses: HMul.hMul, Trans.trans, Finset.card, Finset.sum, HAdd.hAdd, Compl.compl, Eq.mpr, Union.union, id, congrArg, Eq.symm, MeasureTheory.measure_union, Disjoint.preimage, disjoint_compl_left, MeasurableSet.of_discrete, of_eq_true, Eq.trans, True, Set.compl_union_self, eq_self and 44 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measure_preimage_of_mem
    {H : Finset S} (h : IsUniform H X μ) (hX : Measurable X)
    {s : S} (hs : s ∈ H) :
    μ (X ⁻¹' {s}) = μ univ / Nat.card H := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.measureReal_preimage_of_mem A "unit test" for the definition of uniform distribution line 155 source
Source documentation
A "unit test" for the definition of uniform distribution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, Finset, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IsUniform, Measurable, Membership.mem, Eq, Real, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, HDiv.hDiv, OfNat.ofNat, Finset.card
Proof uses: of_eq_true, Eq.trans, Inv.inv, True, congr, congrArg, ENNReal.toReal, ENNReal, Set.univ, Nat.card, Subtype, ProbabilityTheory.IsUniform.measure_preimage_of_mem, MeasureTheory.IsProbabilityMeasure.measure_univ, Nat, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_coe, one_div, ENNReal.toReal_inv, ENNReal.toReal_natCast and 1 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measureReal_preimage_of_mem {A : Finset S} [IsProbabilityMeasure μ]
    (h : IsUniform A X μ) (hX : Measurable X) {s : S} (hs : s ∈ A) :
    μ.real (X ⁻¹' {s}) = 1 / A.card := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.measureReal_preimage_of_mem' line 160 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, Finset, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IsUniform, Measurable, Membership.mem, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, HDiv.hDiv, OfNat.ofNat, Finset.card
Proof uses: Eq.mpr, Set.preimage, id, congrArg, MeasureTheory.map_measureReal_apply, MeasurableSet.singleton, ProbabilityTheory.IsUniform.measureReal_preimage_of_mem, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IsUniform.measure_preimage $\mathbb{P}(U_H \in H') = \dfrac{|H' \cap H|}{|H|}$ line 166 source
Source documentation
$\mathbb{P}(U_H \in H') = \dfrac{|H' \cap H|}{|H|}$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, Finset, ProbabilityTheory.IsUniform, Measurable, Set, Eq, ENNReal, Set.preimage, HDiv.hDiv, HMul.hMul, Set.univ, Nat.card, Inter.inter, Subtype, Membership.mem
Proof uses: Trans.trans, Finset.sum, Set.Finite.toFinset, Set.toFinite, OfNat.ofNat, HAdd.hAdd, SDiff.sdiff, Union.union, of_eq_true, Eq.trans, True, congrArg, Set.inter_union_sdiff, eq_self, MeasureTheory.measure_union, Disjoint.preimage, disjoint_inf_sdiff, id, MeasurableSet, MeasurableSet.diff and 34 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measure_preimage {H : Finset S} (h : IsUniform H X μ) (hX : Measurable X)
    (H' : Set S) : μ (X ⁻¹' H') = (μ univ) * (Nat.card (H' ∩ H : Set S)) / Nat.card H := calc
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.measureReal_preimage $\mathbb{P}(U_H \in H') = \dfrac{|H' \cap H|}{|H|}$ line 182 source
Source documentation
$\mathbb{P}(U_H \in H') = \dfrac{|H' \cap H|}{|H|}$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, Finset, ProbabilityTheory.IsUniform, Measurable, Set, Eq, Real, MeasureTheory.Measure.real, Set.preimage, HDiv.hDiv, HMul.hMul, Set.univ, Nat.card, Inter.inter, Subtype, Membership.mem
Proof uses: of_eq_true, Eq.trans, ENNReal.toReal, ENNReal, Set.ncard, Finset.card, True, congr, congrArg, ProbabilityTheory.IsUniform.measure_preimage, Nat, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_coe, ENNReal.toReal_div, ENNReal.toReal_mul, ENNReal.toReal_natCast, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measureReal_preimage {H : Finset S} (h : IsUniform H X μ) (hX : Measurable X)
    (H' : Set S) :
    μ.real (X ⁻¹' H') = (μ.real univ) * (Nat.card (H' ∩ H).Elem) / Nat.card H := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.nonempty_preimage_of_mem line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, NeZero, Finset, ProbabilityTheory.IsUniform, Measurable, Membership.mem, Set.Nonempty, Set.preimage, Singleton.singleton, Set
Proof uses: MeasureTheory.nonempty_of_measure_ne_zero, Eq.mpr, Ne, ENNReal, OfNat.ofNat, HDiv.hDiv, Set.univ, Nat.card, Subtype, id, Eq, congrArg, ProbabilityTheory.IsUniform.measure_preimage_of_mem, of_eq_true, Eq.trans, Finset.card, True, congrFun', Nat, Fintype.card and 9 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IsUniform.full_measure line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, DiscreteMeasurableSpace, ProbabilityTheory.IsUniform, Measurable, Eq, ENNReal, MeasureTheory.Measure.map, Set.univ
Proof uses: Eq.mpr, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, MeasurableSet.of_discrete, MeasureTheory.measure_eq_measure_of_null_sdiff, Set.subset_univ, SDiff.sdiff, OfNat.ofNat, autoParam, Compl.compl, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike, Set.ext and 11 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IsUniform.of_identDistrib A copy of a uniform random variable is also uniform line 201 source
Source documentation
A copy of a uniform random variable is also uniform.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, DiscreteMeasurableSpace, ProbabilityTheory.IsUniform, ProbabilityTheory.IdentDistrib, MeasurableSet
Proof uses: ProbabilityTheory.IsUniform.mk, Membership.mem, Eq.mpr, Eq, ENNReal, autoParam, Set.preimage, Singleton.singleton, id, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.measure_mem_eq, MeasurableSet.singleton, ProbabilityTheory.IsUniform.eq_of_mem, Compl.compl, OfNat.ofNat, MeasurableSet.compl, ProbabilityTheory.IsUniform.measure_preimage_compl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.of_identDistrib {Ω' : Type*} [MeasurableSpace Ω'] (h : IsUniform H X μ)
    {X' : Ω' → S} {μ' : Measure Ω'} (h' : IdentDistrib X X' μ μ') (hH : MeasurableSet (H : Set S)) :
    IsUniform H X' μ' := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.measure_preimage_ne_zero $\mathbb{P}(U_H \in H') \neq 0$ if $H'$ intersects $H$ and the measure is non-zero line 213 source
Source documentation
$\mathbb{P}(U_H \in H') \neq 0$ if $H'$ intersects $H$ and the measure is non-zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, Finset, NeZero, ProbabilityTheory.IsUniform, Measurable, Set, Set.Nonempty, Inter.inter, Ne, ENNReal, Set.preimage, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, Eq.trans, HDiv.hDiv, HMul.hMul, Set.univ, Set.ncard, Finset.card, congrFun', congrArg, Nat.card, Subtype, Membership.mem, ProbabilityTheory.IsUniform.measure_preimage, Nat, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_coe, Not and 11 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measure_preimage_ne_zero {H : Finset S} [NeZero μ] (h : IsUniform H X μ)
    (hX : Measurable X) {H' : Set S} (h' : (H' ∩ H).Nonempty) : μ (X ⁻¹' H') ≠ 0 := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.restrict If $X$ is uniform w.r.t line 219 source
Source documentation
If $X$ is uniform w.r.t. $\mu$ on $H$, then $X$ is uniform w.r.t. $\mu$ conditioned by $H'$ on $H' \cap H$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, Set, ProbabilityTheory.IsUniform, Measurable, Inter.inter, ProbabilityTheory.cond, Set.preimage
Proof uses: ProbabilityTheory.IsUniform.mk, Membership.mem, id, Eq, ENNReal, autoParam, Singleton.singleton, Eq.mpr, HMul.hMul, Inv.inv, MeasureTheory.Measure.restrict, congrArg, MeasureTheory.Measure.restrict_eq_self, Set.preimage_mono, Iff.mpr, LE.le, Set.singleton_subset_iff, And.left, ProbabilityTheory.IsUniform.eq_of_mem, And.right and 30 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.restrict {H : Set S} (h : IsUniform H X μ) (hX : Measurable X) (H' : Set S) :
    IsUniform (H' ∩ H) X (μ[|X ⁻¹' H']) where
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IdentDistrib.of_isUniform line 239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, DiscreteMeasurableSpace, MeasureTheory.IsProbabilityMeasure, Finite, Countable, Measurable, ProbabilityTheory.IsUniform, ProbabilityTheory.IdentDistrib
Proof uses: ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, MeasureTheory.Measure.ext, MeasureTheory.Measure.map, MeasurableSet, Eq.mpr, Eq, ENNReal, tsum, Set.indicator, Singleton.singleton, SummationFilter.unconditional, id, congrArg, Eq.symm, MeasureTheory.Measure.tsum_indicator_apply_singleton, eq_of_heq, AddCommMonoid, TopologicalSpace, optParam and 39 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IsUniform.map_eq_uniformOn line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, Countable, MeasureTheory.IsProbabilityMeasure, Set, ProbabilityTheory.IsUniform, Measurable, Set.Finite, Set.Nonempty, Eq, MeasureTheory.Measure.map, ProbabilityTheory.uniformOn
Proof uses: Finite, ProbabilityTheory.isProbabilityMeasure_uniformOn, ProbabilityTheory.IdentDistrib, id, ProbabilityTheory.IdentDistrib.of_isUniform, measurable_id, ProbabilityTheory.isUniform_uniformOn, Eq.mp, congrArg, MeasureTheory.Measure.map_id, ProbabilityTheory.IdentDistrib.map_eq
4 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.isUniform_iff_map_eq_uniformOn A random variable is uniform iff its distribution is line 270 source
Source documentation
A random variable is uniform iff its distribution is.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, MeasurableSpace, DiscreteMeasurableSpace, Finite, MeasureTheory.Measure, Countable, MeasureTheory.IsProbabilityMeasure, Measurable, Iff, ProbabilityTheory.IsUniform, Eq, MeasureTheory.Measure.map, ProbabilityTheory.uniformOn
Proof uses: Iff.intro, MeasureTheory.Measure.ext, MeasurableSet, Finset, Set.Finite.toFinset, Set.toFinite, Eq.rec, Eq.symm, Set.Finite.coe_toFinset, Inter.inter, Eq.mpr, ENNReal, HDiv.hDiv, Nat.card, id, congrArg, ProbabilityTheory.uniformOn_apply, tsum, Set.indicator, Singleton.singleton and 75 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma isUniform_iff_map_eq_uniformOn [Finite H] {Ω : Type*} [mΩ : MeasurableSpace Ω] (μ : Measure Ω)
    [Countable S] [IsProbabilityMeasure μ] {U : Ω → S} (hU : Measurable U) :
    IsUniform H U μ ↔ μ.map U = uniformOn H := by
…
```
Mentions: hU, ProbabilityTheory.IsUniform