Documentation

Mathlib.Probability.Density

Probability density function #

This file defines the probability density function of random variables, by which we mean measurable functions taking values in a Borel space. The probability density function is defined as the Radon–Nikodym derivative of the law of X. In particular, a measurable function f is said to the probability density function of a random variable X if for all measurable sets S, ℙ(X ∈ S) = ∫ x in S, f x dx. Probability density functions are one way of describing the distribution of a random variable, and are useful for calculating probabilities and finding moments (although the latter is better achieved with moment generating functions).

This file also defines the continuous uniform distribution and proves some properties about random variables with this distribution.

Main definitions #

Main results #

TODOs #

Ultimately, we would also like to define characteristic functions to describe distributions as it exists for all random variables. However, to define this, we will need Fourier transforms which we currently do not have.

class MeasureTheory.HasPDF {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : ΩE) (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) _auto✝) :

A random variable X : Ω → E is said to 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 HaveLebesgueDecomposition.

Instances
    theorem MeasureTheory.HasPDF.pdf' {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {X : ΩE} {ℙ : MeasureTheory.Measure Ω} {μ : autoParam (MeasureTheory.Measure E) _auto✝} [self : MeasureTheory.HasPDF X μ] :
    AEMeasurable X (MeasureTheory.Measure.map X ).HaveLebesgueDecomposition μ (MeasureTheory.Measure.map X ).AbsolutelyContinuous μ
    theorem MeasureTheory.hasPDF_iff {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    ∀ {x : MeasurableSpace Ω} {X : ΩE} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, MeasureTheory.HasPDF X μ AEMeasurable X (MeasureTheory.Measure.map X ).HaveLebesgueDecomposition μ (MeasureTheory.Measure.map X ).AbsolutelyContinuous μ
    theorem MeasureTheory.hasPDF_iff_of_aemeasurable {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    ∀ {x : MeasurableSpace Ω} {X : ΩE} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, AEMeasurable X (MeasureTheory.HasPDF X μ (MeasureTheory.Measure.map X ).HaveLebesgueDecomposition μ (MeasureTheory.Measure.map X ).AbsolutelyContinuous μ)
    theorem MeasureTheory.HasPDF.aemeasurable {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    ∀ {x : MeasurableSpace Ω} (X : ΩE) ( : MeasureTheory.Measure Ω) (μ : MeasureTheory.Measure E) [hX : MeasureTheory.HasPDF X μ], AEMeasurable X
    instance MeasureTheory.HasPDF.haveLebesgueDecomposition {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    ∀ {x : MeasurableSpace Ω} {X : ΩE} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [hX : MeasureTheory.HasPDF X μ], (MeasureTheory.Measure.map X ).HaveLebesgueDecomposition μ
    Equations
    • =
    theorem MeasureTheory.HasPDF.absolutelyContinuous {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    ∀ {x : MeasurableSpace Ω} {X : ΩE} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [hX : MeasureTheory.HasPDF X μ], (MeasureTheory.Measure.map X ).AbsolutelyContinuous μ

    A random variable that HasPDF is quasi-measure preserving.

    theorem MeasureTheory.HasPDF.congr {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    ∀ {x : MeasurableSpace Ω} {X Y : ΩE} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, X =ᵐ[] Y∀ [hX : MeasureTheory.HasPDF X μ], MeasureTheory.HasPDF Y μ
    theorem MeasureTheory.HasPDF.congr' {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    ∀ {x : MeasurableSpace Ω} {X Y : ΩE} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, X =ᵐ[] Y(MeasureTheory.HasPDF X μ MeasureTheory.HasPDF Y μ)
    theorem MeasureTheory.hasPDF_of_map_eq_withDensity {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    ∀ {x : MeasurableSpace Ω} {X : ΩE} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, AEMeasurable X ∀ (f : EENNReal), AEMeasurable f μMeasureTheory.Measure.map X = μ.withDensity fMeasureTheory.HasPDF X μ

    X HasPDF if there is a pdf f such that map X ℙ = μ.withDensity f.

    def MeasureTheory.pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
    {x : MeasurableSpace Ω} → (ΩE)MeasureTheory.Measure ΩautoParam (MeasureTheory.Measure E) _auto✝EENNReal

    If X is a random variable, then pdf X is the Radon–Nikodym derivative of the push-forward measure of along X with respect to μ.

    Equations
    Instances For
      theorem MeasureTheory.pdf_def {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
      ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : ΩE}, MeasureTheory.pdf X μ = (MeasureTheory.Measure.map X ).rnDeriv μ
      theorem MeasureTheory.pdf_of_not_aemeasurable {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
      ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : ΩE}, ¬AEMeasurable X MeasureTheory.pdf X μ =ᵐ[μ] 0
      theorem MeasureTheory.pdf_of_not_haveLebesgueDecomposition {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] :
      ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : ΩE}, ¬(MeasureTheory.Measure.map X ).HaveLebesgueDecomposition μMeasureTheory.pdf X μ = 0
      theorem MeasureTheory.aemeasurable_of_pdf_ne_zero {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} (X : ΩE) (h : ¬MeasureTheory.pdf X μ =ᵐ[μ] 0) :
      theorem MeasureTheory.hasPDF_of_pdf_ne_zero {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : ΩE} (hac : (MeasureTheory.Measure.map X ).AbsolutelyContinuous μ) (hpdf : ¬MeasureTheory.pdf X μ =ᵐ[μ] 0) :
      theorem MeasureTheory.setLIntegral_pdf_le_map {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : ΩE) (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) _auto✝) (s : Set E) :
      ∫⁻ (x : E) in s, MeasureTheory.pdf X μ xμ (MeasureTheory.Measure.map X ) s
      @[deprecated MeasureTheory.setLIntegral_pdf_le_map]
      theorem MeasureTheory.set_lintegral_pdf_le_map {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : ΩE) (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) _auto✝) (s : Set E) :
      ∫⁻ (x : E) in s, MeasureTheory.pdf X μ xμ (MeasureTheory.Measure.map X ) s

      Alias of MeasureTheory.setLIntegral_pdf_le_map.

      theorem MeasureTheory.map_eq_setLIntegral_pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : ΩE) (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) _auto✝) [hX : MeasureTheory.HasPDF X μ] {s : Set E} (hs : MeasurableSet s) :
      (MeasureTheory.Measure.map X ) s = ∫⁻ (x : E) in s, MeasureTheory.pdf X μ xμ
      @[deprecated MeasureTheory.map_eq_setLIntegral_pdf]
      theorem MeasureTheory.map_eq_set_lintegral_pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : ΩE) (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) _auto✝) [hX : MeasureTheory.HasPDF X μ] {s : Set E} (hs : MeasurableSet s) :
      (MeasureTheory.Measure.map X ) s = ∫⁻ (x : E) in s, MeasureTheory.pdf X μ xμ

      Alias of MeasureTheory.map_eq_setLIntegral_pdf.

      theorem MeasureTheory.pdf.congr {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : ΩE} {Y : ΩE} (hXY : X =ᵐ[] Y) :
      theorem MeasureTheory.pdf.lintegral_eq_measure_univ {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : ΩE} [MeasureTheory.HasPDF X μ] :
      ∫⁻ (x : E), MeasureTheory.pdf X μ xμ = Set.univ
      theorem MeasureTheory.pdf.eq_of_map_eq_withDensity {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure ] {X : ΩE} [MeasureTheory.HasPDF X μ] (f : EENNReal) (hmf : AEMeasurable f μ) :
      MeasureTheory.Measure.map X = μ.withDensity f MeasureTheory.pdf X μ =ᵐ[μ] f
      theorem MeasureTheory.pdf.eq_of_map_eq_withDensity' {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite μ] {X : ΩE} [MeasureTheory.HasPDF X μ] (f : EENNReal) (hmf : AEMeasurable f μ) :
      MeasureTheory.Measure.map X = μ.withDensity f MeasureTheory.pdf X μ =ᵐ[μ] f
      theorem MeasureTheory.pdf.ae_lt_top {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure ] {μ : MeasureTheory.Measure E} {X : ΩE} :
      ∀ᵐ (x : E) ∂μ, MeasureTheory.pdf X μ x <
      theorem MeasureTheory.pdf.ofReal_toReal_ae_eq {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure ] {X : ΩE} :
      (fun (x : E) => ENNReal.ofReal (MeasureTheory.pdf X μ x).toReal) =ᵐ[μ] MeasureTheory.pdf X μ
      theorem MeasureTheory.pdf.lintegral_pdf_mul {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : ΩE} [MeasureTheory.HasPDF X μ] {f : EENNReal} (hf : AEMeasurable f μ) :
      ∫⁻ (x : E), MeasureTheory.pdf X μ x * f xμ = ∫⁻ (x : Ω), f (X x)

      The Law of the Unconscious Statistician for nonnegative random variables.

      theorem MeasureTheory.pdf.integrable_pdf_smul_iff {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] [MeasureTheory.IsFiniteMeasure ] {X : ΩE} [MeasureTheory.HasPDF X μ] {f : EF} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
      MeasureTheory.Integrable (fun (x : E) => (MeasureTheory.pdf X μ x).toReal f x) μ MeasureTheory.Integrable (fun (x : Ω) => f (X x))
      theorem MeasureTheory.pdf.integral_pdf_smul {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] [MeasureTheory.IsFiniteMeasure ] {X : ΩE} [MeasureTheory.HasPDF X μ] {f : EF} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
      ∫ (x : E), (MeasureTheory.pdf X μ x).toReal f xμ = ∫ (x : Ω), f (X x)

      The Law of the Unconscious Statistician: Given a random variable X and a measurable function f, f ∘ X is a random variable with expectation ∫ x, pdf X x • f x ∂μ where μ is a measure on the codomain of X.

      theorem MeasureTheory.pdf.quasiMeasurePreserving_hasPDF {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {F : Type u_3} [MeasurableSpace F] {ν : MeasureTheory.Measure F} {X : ΩE} [MeasureTheory.HasPDF X μ] (hX : AEMeasurable X ) {g : EF} (hg : MeasureTheory.Measure.QuasiMeasurePreserving g μ ν) (hmap : (MeasureTheory.Measure.map g (MeasureTheory.Measure.map X )).HaveLebesgueDecomposition ν) :

      A random variable that HasPDF transformed under a QuasiMeasurePreserving map also HasPDF if (map g (map X ℙ)).HaveLebesgueDecomposition μ.

      quasiMeasurePreserving_hasPDF is more useful in the case we are working with a probability measure and a real-valued random variable.

      theorem Real.hasPDF_iff_of_aemeasurable {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure ] {X : Ω} (hX : AEMeasurable X ) :
      MeasureTheory.HasPDF X MeasureTheory.volume (MeasureTheory.Measure.map X ).AbsolutelyContinuous MeasureTheory.volume

      A real-valued random variable X HasPDF X ℙ λ (where λ is the Lebesgue measure) if and only if the push-forward measure of along X is absolutely continuous with respect to λ.

      theorem Real.hasPDF_iff {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure ] {X : Ω} :
      MeasureTheory.HasPDF X MeasureTheory.volume AEMeasurable X (MeasureTheory.Measure.map X ).AbsolutelyContinuous MeasureTheory.volume
      theorem MeasureTheory.pdf.integral_mul_eq_integral {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure ] {X : Ω} [MeasureTheory.HasPDF X MeasureTheory.volume] :
      ∫ (x : ), x * (MeasureTheory.pdf X MeasureTheory.volume x).toReal = ∫ (x : Ω), X x

      If X is a real-valued random variable that has pdf f, then the expectation of X equals ∫ x, x * f x ∂λ where λ is the Lebesgue measure.

      theorem MeasureTheory.pdf.hasFiniteIntegral_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure ] {X : Ω} {f : } {g : ENNReal} (hg : MeasureTheory.pdf X MeasureTheory.volume =ᵐ[MeasureTheory.volume] g) (hgi : ∫⁻ (x : ), f x‖₊ * g x ) :
      MeasureTheory.HasFiniteIntegral (fun (x : ) => f x * (MeasureTheory.pdf X MeasureTheory.volume x).toReal) MeasureTheory.volume
      theorem MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {F : Type u_3} [MeasurableSpace F] {ν : MeasureTheory.Measure F} {X : ΩE} {Y : ΩF} [MeasureTheory.IsFiniteMeasure ] [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.HasPDF (fun (ω : Ω) => (X ω, Y ω)) (μ.prod ν)] :
      ProbabilityTheory.IndepFun X Y MeasureTheory.pdf (fun (ω : Ω) => (X ω, Y ω)) (μ.prod ν) =ᵐ[μ.prod ν] fun (z : E × F) => MeasureTheory.pdf X μ z.1 * MeasureTheory.pdf Y ν z.2

      Random variables are independent iff their joint density is a product of marginal densities.