Probability density function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the probability density function of random variables, by which we mean
measurable functions taking values in a Borel space. 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 #
measure_theory.has_pdf: A random variableX : Ω → Eis said tohas_pdfwith respect to the measureℙonΩandμonEif there exists a measurable functionfsuch that the push-forward measure ofℙalongXequalsμ.with_density f.measure_theory.pdf: IfXis a random variable thathas_pdf X ℙ μ, thenpdf Xis the measurable functionfsuch that the push-forward measure ofℙalongXequalsμ.with_density f.measure_theory.pdf.uniform: A random variableXis said to follow the uniform distribution if it has a constant probability density function with a compact, non-null support.
Main results #
measure_theory.pdf.integral_fun_mul_eq_integral: Law of the unconscious statistician, i.e. if a random variableX : Ω → Ehas pdff, then𝔼(g(X)) = ∫ x, g x * f x dxfor all measurableg : E → ℝ.measure_theory.pdf.integral_mul_eq_integral: A real-valued random variableXwith pdffhas expectation∫ x, x * f x dx.measure_theory.pdf.uniform.integral_eq: IfXfollows the uniform distribution with its pdf having supports, thenXhas expectation(λ s)⁻¹ * ∫ x in s, x dxwhereλis the Lebesgue measure.
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]
structure
measure_theory.has_pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
(X : Ω → E)
(ℙ : measure_theory.measure Ω)
(μ : measure_theory.measure E . "volume_tac") :
Prop
- pdf' : measurable X ∧ ∃ (f : E → ennreal), measurable f ∧ measure_theory.measure.map X «ℙ» = measure_theory.measure.with_density μ f
A random variable X : Ω → E is said to has_pdf with respect to the measure ℙ on Ω and
μ on E if there exists a measurable function f such that the push-forward measure of ℙ
along X equals μ.with_density f.
@[measurability]
theorem
measure_theory.has_pdf.measurable
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
(X : Ω → E)
(ℙ : measure_theory.measure Ω)
(μ : measure_theory.measure E . "volume_tac")
[hX : measure_theory.has_pdf X «ℙ» μ] :
noncomputable
def
measure_theory.pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
(X : Ω → E)
(ℙ : measure_theory.measure Ω)
(μ : measure_theory.measure E . "volume_tac") :
If X is a random variable that has_pdf X ℙ μ, then pdf X is the measurable function f
such that the push-forward measure of ℙ along X equals μ.with_density f.
Equations
- measure_theory.pdf X «ℙ» μ = dite (measure_theory.has_pdf X «ℙ» μ) (λ (hX : measure_theory.has_pdf X «ℙ» μ), classical.some _) (λ (hX : ¬measure_theory.has_pdf X «ℙ» μ), 0)
theorem
measure_theory.pdf_undef
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E}
(h : ¬measure_theory.has_pdf X «ℙ» μ) :
measure_theory.pdf X «ℙ» μ = 0
theorem
measure_theory.has_pdf_of_pdf_ne_zero
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E}
(h : measure_theory.pdf X «ℙ» μ ≠ 0) :
measure_theory.has_pdf X «ℙ» μ
theorem
measure_theory.pdf_eq_zero_of_not_measurable
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E}
(hX : ¬measurable X) :
measure_theory.pdf X «ℙ» μ = 0
theorem
measure_theory.measurable_of_pdf_ne_zero
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
(X : Ω → E)
(h : measure_theory.pdf X «ℙ» μ ≠ 0) :
@[measurability]
theorem
measure_theory.measurable_pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
(X : Ω → E)
(ℙ : measure_theory.measure Ω)
(μ : measure_theory.measure E . "volume_tac") :
measurable (measure_theory.pdf X «ℙ» μ)
theorem
measure_theory.map_eq_with_density_pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
(X : Ω → E)
(ℙ : measure_theory.measure Ω)
(μ : measure_theory.measure E . "volume_tac")
[hX : measure_theory.has_pdf X «ℙ» μ] :
measure_theory.measure.map X «ℙ» = measure_theory.measure.with_density μ (measure_theory.pdf X «ℙ» μ)
theorem
measure_theory.map_eq_set_lintegral_pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
(X : Ω → E)
(ℙ : measure_theory.measure Ω)
(μ : measure_theory.measure E . "volume_tac")
[hX : measure_theory.has_pdf X «ℙ» μ]
{s : set E}
(hs : measurable_set s) :
⇑(measure_theory.measure.map X «ℙ») s = ∫⁻ (x : E) in s, measure_theory.pdf X «ℙ» μ x ∂μ
theorem
measure_theory.pdf.lintegral_eq_measure_univ
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E}
[measure_theory.has_pdf X «ℙ» μ] :
theorem
measure_theory.pdf.ae_lt_top
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
[measure_theory.is_finite_measure «ℙ»]
{μ : measure_theory.measure E}
{X : Ω → E} :
theorem
measure_theory.pdf.of_real_to_real_ae_eq
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
[measure_theory.is_finite_measure «ℙ»]
{X : Ω → E} :
(λ (x : E), ennreal.of_real (measure_theory.pdf X «ℙ» μ x).to_real) =ᵐ[μ] measure_theory.pdf X «ℙ» μ
theorem
measure_theory.pdf.integrable_iff_integrable_mul_pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
[measure_theory.is_finite_measure «ℙ»]
{X : Ω → E}
[measure_theory.has_pdf X «ℙ» μ]
{f : E → ℝ}
(hf : measurable f) :
measure_theory.integrable (λ (x : Ω), f (X x)) «ℙ» ↔ measure_theory.integrable (λ (x : E), f x * (measure_theory.pdf X «ℙ» μ x).to_real) μ
theorem
measure_theory.pdf.integral_fun_mul_eq_integral
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
[measure_theory.is_finite_measure «ℙ»]
{X : Ω → E}
[measure_theory.has_pdf X «ℙ» μ]
{f : E → ℝ}
(hf : measurable f) :
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, f x * pdf X ∂μ
where μ is a measure on the codomain of X.
theorem
measure_theory.pdf.map_absolutely_continuous
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E}
[measure_theory.has_pdf X «ℙ» μ] :
theorem
measure_theory.pdf.to_quasi_measure_preserving
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E}
[measure_theory.has_pdf X «ℙ» μ] :
A random variable that has_pdf is quasi-measure preserving.
theorem
measure_theory.pdf.have_lebesgue_decomposition_of_has_pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E}
[hX' : measure_theory.has_pdf X «ℙ» μ] :
theorem
measure_theory.pdf.has_pdf_iff
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E} :
measure_theory.has_pdf X «ℙ» μ ↔ measurable X ∧ (measure_theory.measure.map X «ℙ»).have_lebesgue_decomposition μ ∧ (measure_theory.measure.map X «ℙ»).absolutely_continuous μ
theorem
measure_theory.pdf.has_pdf_iff_of_measurable
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{X : Ω → E}
(hX : measurable X) :
measure_theory.has_pdf X «ℙ» μ ↔ (measure_theory.measure.map X «ℙ»).have_lebesgue_decomposition μ ∧ (measure_theory.measure.map X «ℙ»).absolutely_continuous μ
theorem
measure_theory.pdf.quasi_measure_preserving_has_pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{F : Type u_3}
[measurable_space F]
{ν : measure_theory.measure F}
{X : Ω → E}
[measure_theory.has_pdf X «ℙ» μ]
{g : E → F}
(hg : measure_theory.measure.quasi_measure_preserving g μ ν)
(hmap : (measure_theory.measure.map g (measure_theory.measure.map X «ℙ»)).have_lebesgue_decomposition ν) :
measure_theory.has_pdf (g ∘ X) «ℙ» ν
A random variable that has_pdf transformed under a quasi_measure_preserving
map also has_pdf if (map g (map X ℙ)).have_lebesgue_decomposition μ.
quasi_measure_preserving_has_pdf' is more useful in the case we are working with a
probability measure and a real-valued random variable.
theorem
measure_theory.pdf.quasi_measure_preserving_has_pdf'
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{F : Type u_3}
[measurable_space F]
{ν : measure_theory.measure F}
[measure_theory.is_finite_measure «ℙ»]
[measure_theory.sigma_finite ν]
{X : Ω → E}
[measure_theory.has_pdf X «ℙ» μ]
{g : E → F}
(hg : measure_theory.measure.quasi_measure_preserving g μ ν) :
measure_theory.has_pdf (g ∘ X) «ℙ» ν
theorem
measure_theory.pdf.real.has_pdf_iff_of_measurable
{Ω : Type u_1}
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
[measure_theory.is_finite_measure «ℙ»]
{X : Ω → ℝ}
(hX : measurable X) :
A real-valued random variable X has_pdf X ℙ λ (where λ is the Lebesgue measure) if and
only if the push-forward measure of ℙ along X is absolutely continuous with respect to λ.
theorem
measure_theory.pdf.real.has_pdf_iff
{Ω : Type u_1}
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
[measure_theory.is_finite_measure «ℙ»]
{X : Ω → ℝ} :
theorem
measure_theory.pdf.integral_mul_eq_integral
{Ω : Type u_1}
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
[measure_theory.is_finite_measure «ℙ»]
{X : Ω → ℝ}
[measure_theory.has_pdf X «ℙ» measure_theory.measure_space.volume] :
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
measure_theory.pdf.has_finite_integral_mul
{Ω : Type u_1}
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
[measure_theory.is_finite_measure «ℙ»]
{X : Ω → ℝ}
{f : ℝ → ℝ}
{g : ℝ → ennreal}
(hg : measure_theory.pdf X «ℙ» measure_theory.measure_space.volume =ᵐ[measure_theory.measure_space.volume] g)
(hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤) :
Uniform Distribution
def
measure_theory.pdf.is_uniform
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
(X : Ω → E)
(support : set E)
(ℙ : measure_theory.measure Ω)
(μ : measure_theory.measure E . "volume_tac") :
Prop
A random variable X has uniform distribution if it has a probability density function f
with support s such that f = (μ s)⁻¹ 1ₛ a.e. where 1ₛ is the indicator function for s.
Equations
- measure_theory.pdf.is_uniform X support «ℙ» μ = (measure_theory.pdf X «ℙ» μ =ᵐ[μ] support.indicator ((⇑μ support)⁻¹ • 1))
theorem
measure_theory.pdf.is_uniform.has_pdf
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{X : Ω → E}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{s : set E}
(hns : ⇑μ s ≠ 0)
(hnt : ⇑μ s ≠ ⊤)
(hu : measure_theory.pdf.is_uniform X s «ℙ» μ) :
measure_theory.has_pdf X «ℙ» μ
theorem
measure_theory.pdf.is_uniform.pdf_to_real_ae_eq
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{X : Ω → E}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{s : set E}
(hX : measure_theory.pdf.is_uniform X s «ℙ» μ) :
theorem
measure_theory.pdf.is_uniform.measure_preimage
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{X : Ω → E}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{s : set E}
(hns : ⇑μ s ≠ 0)
(hnt : ⇑μ s ≠ ⊤)
(hms : measurable_set s)
(hu : measure_theory.pdf.is_uniform X s «ℙ» μ)
{A : set E}
(hA : measurable_set A) :
theorem
measure_theory.pdf.is_uniform.is_probability_measure
{Ω : Type u_1}
{E : Type u_2}
[measurable_space E]
{m : measurable_space Ω}
{X : Ω → E}
{ℙ : measure_theory.measure Ω}
{μ : measure_theory.measure E}
{s : set E}
(hns : ⇑μ s ≠ 0)
(hnt : ⇑μ s ≠ ⊤)
(hms : measurable_set s)
(hu : measure_theory.pdf.is_uniform X s «ℙ» μ) :
theorem
measure_theory.pdf.is_uniform.mul_pdf_integrable
{Ω : Type u_1}
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{X : Ω → ℝ}
{s : set ℝ}
(hms : measurable_set s)
(hns : ⇑measure_theory.measure_space.volume s ≠ 0)
[measure_theory.is_finite_measure «ℙ»]
(hcs : is_compact s)
(huX : measure_theory.pdf.is_uniform X s «ℙ» measure_theory.measure_space.volume) :
theorem
measure_theory.pdf.is_uniform.integral_eq
{Ω : Type u_1}
{m : measurable_space Ω}
{ℙ : measure_theory.measure Ω}
{X : Ω → ℝ}
{s : set ℝ}
(hms : measurable_set s)
(hns : ⇑measure_theory.measure_space.volume s ≠ 0)
(hnt : ⇑measure_theory.measure_space.volume s ≠ ⊤)
(huX : measure_theory.pdf.is_uniform X s «ℙ» measure_theory.measure_space.volume) :
A real uniform random variable X with support s has expectation
(λ s)⁻¹ * ∫ x in s, x ∂λ where λ is the Lebesgue measure.