Theorems · Theorem · probability

MeasureTheory.pdf.IsUniform.measure_preimage

∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  μ s ≠ 0 →
    μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → ∀ {A : Set E}, MeasurableSet A → ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s

Defined in

Mathlib.Probability.Distributions.Uniform

Cited by

1 results in Mathlib

Foundations

Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpace