Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.IsUniform.comp

PFR.ForMathlib.Uniform · PFR/ForMathlib/Uniform.lean:68 to 77

Source documentation

The image of a uniform random variable under an injective map is uniform on the image.

Exact Lean statement

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
  eq_of_mem

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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  eq_of_mem := by    intro x hx y hy    simp only [Finset.coe_image, mem_image, Finset.mem_coe] at hx hy    rcases hx with ⟨x, hx, rfl⟩    rcases hy with ⟨y, hy, rfl⟩    have A z : f ⁻¹' {f z} = {z} := by ext; simp [hf.eq_iff]    simp [preimage_comp, A, h.eq_of_mem hx hy]  measure_preimage_compl := by simpa [preimage_comp, hf] using h.measure_preimage_compl