Theorems · Definition · probability

MeasureTheory.pdf.IsUniform

{E : Type u_1} →
  [inst : MeasurableSpace E] →
    {Ω : Type u_2} →
      {x : MeasurableSpace Ω} →
        (Ω → E) →
          Set E →
            MeasureTheory.Measure Ω → autoParam (MeasureTheory.Measure E) MeasureTheory.pdf.IsUniform._auto_1 → Prop

A random variable X has uniform distribution on s if its push-forward measure is (μ s)⁻¹ • μ.restrict s.

Defined in: Mathlib.Probability.Distributions.Uniform
Cited by: 14 results in Mathlib
Foundations: Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
MeasureTheory.Measure.mapproof · cited by 858
ProbabilityTheory.condproof · cited by 43

Cited by14

Results whose statement or proof uses this declaration.

MeasureTheory.pdf.IsUniform.pdf_eqstatement and proof · cited by 3
MeasureTheory.pdf.IsUniform.aemeasurablestatement and proof · cited by 2
MeasureTheory.pdf.IsUniform.isProbabilityMeasurestatement and proof · cited by 2
MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_topstatement and proof · cited by 2
MeasureTheory.pdf.IsUniform.hasPDFstatement and proof · cited by 1
MeasureTheory.pdf.IsUniform.measure_preimagestatement and proof · cited by 1
MeasureTheory.pdf.IsUniform.toMeasurable_iffstatement · cited by 1
MeasureTheory.pdf.IsUniform.absolutelyContinuousstatement and proof · cited by 0
MeasureTheory.pdf.IsUniform.condstatement · cited by 0
MeasureTheory.pdf.IsUniform.integral_eqstatement and proof · cited by 0
MeasureTheory.pdf.IsUniform.mul_pdf_integrablestatement and proof · cited by 0
MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eqstatement and proof · cited by 0