Theorems · Inductive type · probability

MeasureTheory.HasPDF

{Ω : Type u_1} →
  {E : Type u_2} →
    [inst : MeasurableSpace E] →
      {m : MeasurableSpace Ω} →
        (Ω → E) → MeasureTheory.Measure Ω → autoParam (MeasureTheory.Measure E) MeasureTheory.HasPDF._auto_1 → Prop

A random variable X : Ω → E is said to have a probability density function (HasPDF) with respect to the measure ℙ on Ω and μ on E if the push-forward measure of ℙ along X is absolutely continuous with respect to μ and they have a Lebesgue decomposition (HaveLebesgueDecomposition).

Defined in

Mathlib.Probability.Density

Cited by

37 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

MeasurableSpace