Library mathcomp.analysis.probability
(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality.
From HB Require Import structures.
Require Import reals ereal signed topology normedtype sequences esum measure.
Require Import exp numfun lebesgue_measure lebesgue_integral.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality.
From HB Require Import structures.
Require Import reals ereal signed topology normedtype sequences esum measure.
Require Import exp numfun lebesgue_measure lebesgue_integral.
Probability (experimental)
This file provides basic notions of probability theory. See measure.v for
the type probability T R (a measure that sums to 1).
{RV P >-> R} == real random variable: a measurable function from
the measurableType of the probability P to R
distribution X == measure image of P by X : {RV P -> R}, declared
as an instance of probability measure
'E_P[X] == expectation of the real measurable function X
covariance X Y == covariance between real random variable X and Y
'V_P[X] == variance of the real random variable X
{dmfun T >-> R} == type of discrete real-valued measurable functions
{dRV P >-> R} == real-valued discrete random variable
dRV_dom X == domain of the discrete random variable X
dRV_eunm X == bijection between the domain and the range of X
pmf X r := fine (P (X @^-1` [set r]))
enum_prob X k == probability of the kth value in the range of X
Reserved Notation "'{' 'RV' P >-> R '}'"
(at level 0, format "'{' 'RV' P '>->' R '}'").
Reserved Notation "''E_' P [ X ]" (format "''E_' P [ X ]", at level 5).
Reserved Notation "''V_' P [ X ]" (format "''V_' P [ X ]", at level 5).
Reserved Notation "{ 'dmfun' aT >-> T }"
(at level 0, format "{ 'dmfun' aT >-> T }").
Reserved Notation "'{' 'dRV' P >-> R '}'"
(at level 0, format "'{' 'dRV' P '>->' R '}'").
Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Definition random_variable (d : _) (T : measurableType d) (R : realType)
(P : probability T R) := {mfun T >-> R}.
Notation "{ 'RV' P >-> R }" := (@random_variable _ _ R P) : form_scope.
Lemma notin_range_measure d (T : measurableType d) (R : realType)
(P : {measure set T → \bar R}) (X : T → R) r :
r \notin range X → P (X @^-1` [set r]) = 0%E.
Lemma probability_range d (T : measurableType d) (R : realType)
(P : probability T R) (X : {RV P >-> R}) : P (X @^-1` range X) = 1%E.
Definition distribution (d : _) (T : measurableType d) (R : realType)
(P : probability T R) (X : {mfun T >-> R}) :=
pushforward P (@measurable_funP _ _ _ X).
Section distribution_is_probability.
Context d (T : measurableType d) (R : realType) (P : probability T R)
(X : {mfun T >-> R}).
Let distribution0 : distribution P X set0 = 0%E.
Let distribution_ge0 A : (0 ≤ distribution P X A)%E.
Let distribution_sigma_additive : semi_sigma_additive (distribution P X).
Let distribution_is_probability : distribution P X [set: _] = 1%:E.
End distribution_is_probability.
Section transfer_probability.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Lemma probability_distribution (X : {RV P >-> R}) r :
P [set x | X x = r] = distribution P X [set r].
Lemma integral_distribution (X : {RV P >-> R}) (f : R → \bar R) :
measurable_fun [set: R] f → (∀ y, 0 ≤ f y) →
\int[distribution P X]_y f y = \int[P]_x (f \o X) x.
End transfer_probability.
Canonical expectation_unlockable := Unlockable expectation.unlock.
Arguments expectation {d T R} P _%R.
Notation "''E_' P [ X ]" := (@expectation _ _ _ P X) : ereal_scope.
Section expectation_lemmas.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Lemma expectation_fin_num (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) →
'E_P[X] \is a fin_num.
Lemma expectation_cst r : 'E_P[cst r] = r%:E.
Lemma expectation_indic (A : set T) (mA : measurable A) : 'E_P[\1_A] = P A.
Lemma integrable_expectation (X : {RV P >-> R})
(iX : P.-integrable [set: T] (EFin \o X)) : `| 'E_P[X] | < +oo.
Lemma expectationM (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X))
(k : R) : 'E_P[k \o× X] = k%:E × 'E_P [X].
Lemma expectation_ge0 (X : {RV P >-> R}) :
(∀ x, 0 ≤ X x)%R → 0 ≤ 'E_P[X].
Lemma expectation_le (X Y : T → R) :
measurable_fun [set: T] X → measurable_fun [set: T] Y →
(∀ x, 0 ≤ X x)%R → (∀ x, 0 ≤ Y x)%R →
{ae P, (∀ x, X x ≤ Y x)%R} → 'E_P[X] ≤ 'E_P[Y].
Lemma expectationD (X Y : {RV P >-> R}) :
P.-integrable [set: T] (EFin \o X) → P.-integrable [set: T] (EFin \o Y) →
'E_P[X \+ Y] = 'E_P[X] + 'E_P[Y].
Lemma expectationB (X Y : {RV P >-> R}) :
P.-integrable [set: T] (EFin \o X) → P.-integrable [set: T] (EFin \o Y) →
'E_P[X \- Y] = 'E_P[X] - 'E_P[Y].
Lemma expectation_sum (X : seq {RV P >-> R}) :
(∀ Xi, Xi \in X → P.-integrable [set: T] (EFin \o Xi)) →
'E_P[\sum_(Xi <- X) Xi] = \sum_(Xi <- X) 'E_P[Xi].
End expectation_lemmas.
Canonical covariance_unlockable := Unlockable covariance.unlock.
Arguments covariance {d T R} P _%R _%R.
Section covariance_lemmas.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Lemma covarianceE (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) →
P.-integrable setT (EFin \o Y) →
P.-integrable setT (EFin \o (X × Y)%R) →
covariance P X Y = 'E_P[X × Y] - 'E_P[X] × 'E_P[Y].
Lemma covarianceC (X Y : T → R) : covariance P X Y = covariance P Y X.
Lemma covariance_fin_num (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) →
P.-integrable setT (EFin \o Y) →
P.-integrable setT (EFin \o (X × Y)%R) →
covariance P X Y \is a fin_num.
Lemma covariance_cst_l c (X : {RV P >-> R}) : covariance P (cst c) X = 0.
Lemma covariance_cst_r (X : {RV P >-> R}) c : covariance P X (cst c) = 0.
Lemma covarianceZl a (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) →
P.-integrable setT (EFin \o Y) →
P.-integrable setT (EFin \o (X × Y)%R) →
covariance P (a \o× X)%R Y = a%:E × covariance P X Y.
Lemma covarianceZr a (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) →
P.-integrable setT (EFin \o Y) →
P.-integrable setT (EFin \o (X × Y)%R) →
covariance P X (a \o× Y)%R = a%:E × covariance P X Y.
Lemma covarianceNl (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) →
P.-integrable setT (EFin \o Y) →
P.-integrable setT (EFin \o (X × Y)%R) →
covariance P (\- X)%R Y = - covariance P X Y.
Lemma covarianceNr (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) →
P.-integrable setT (EFin \o Y) →
P.-integrable setT (EFin \o (X × Y)%R) →
covariance P X (\- Y)%R = - covariance P X Y.
Lemma covarianceNN (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) →
P.-integrable setT (EFin \o Y) →
P.-integrable setT (EFin \o (X × Y)%R) →
covariance P (\- X)%R (\- Y)%R = covariance P X Y.
Lemma covarianceDl (X Y Z : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
P.-integrable setT (EFin \o Y) → P.-integrable setT (EFin \o (Y ^+ 2)%R) →
P.-integrable setT (EFin \o Z) → P.-integrable setT (EFin \o (Z ^+ 2)%R) →
P.-integrable setT (EFin \o (X × Z)%R) →
P.-integrable setT (EFin \o (Y × Z)%R) →
covariance P (X \+ Y)%R Z = covariance P X Z + covariance P Y Z.
Lemma covarianceDr (X Y Z : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
P.-integrable setT (EFin \o Y) → P.-integrable setT (EFin \o (Y ^+ 2)%R) →
P.-integrable setT (EFin \o Z) → P.-integrable setT (EFin \o (Z ^+ 2)%R) →
P.-integrable setT (EFin \o (X × Y)%R) →
P.-integrable setT (EFin \o (X × Z)%R) →
covariance P X (Y \+ Z)%R = covariance P X Y + covariance P X Z.
Lemma covarianceBl (X Y Z : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
P.-integrable setT (EFin \o Y) → P.-integrable setT (EFin \o (Y ^+ 2)%R) →
P.-integrable setT (EFin \o Z) → P.-integrable setT (EFin \o (Z ^+ 2)%R) →
P.-integrable setT (EFin \o (X × Z)%R) →
P.-integrable setT (EFin \o (Y × Z)%R) →
covariance P (X \- Y)%R Z = covariance P X Z - covariance P Y Z.
Lemma covarianceBr (X Y Z : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
P.-integrable setT (EFin \o Y) → P.-integrable setT (EFin \o (Y ^+ 2)%R) →
P.-integrable setT (EFin \o Z) → P.-integrable setT (EFin \o (Z ^+ 2)%R) →
P.-integrable setT (EFin \o (X × Y)%R) →
P.-integrable setT (EFin \o (X × Z)%R) →
covariance P X (Y \- Z)%R = covariance P X Y - covariance P X Z.
End covariance_lemmas.
Section variance.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Definition variance (X : T → R) := covariance P X X.
Lemma varianceE (X : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
'V_P[X] = 'E_P[X ^+ 2] - ('E_P[X]) ^+ 2.
Lemma variance_fin_num (X : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o X ^+ 2)%R →
'V_P[X] \is a fin_num.
Lemma variance_ge0 (X : {RV P >-> R}) : (0 ≤ 'V_P[X])%E.
Lemma variance_cst r : 'V_P[cst r] = 0%E.
Lemma varianceZ a (X : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
'V_P[(a \o× X)%R] = (a ^+ 2)%:E × 'V_P[X].
Lemma varianceN (X : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
'V_P[(\- X)%R] = 'V_P[X].
Lemma varianceD (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
P.-integrable setT (EFin \o Y) → P.-integrable setT (EFin \o (Y ^+ 2)%R) →
P.-integrable setT (EFin \o (X × Y)%R) →
'V_P[X \+ Y]%R = 'V_P[X] + 'V_P[Y] + 2%:E × covariance P X Y.
Lemma varianceB (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
P.-integrable setT (EFin \o Y) → P.-integrable setT (EFin \o (Y ^+ 2)%R) →
P.-integrable setT (EFin \o (X × Y)%R) →
'V_P[(X \- Y)%R] = 'V_P[X] + 'V_P[Y] - 2%:E × covariance P X Y.
Lemma varianceD_cst_l c (X : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
'V_P[(cst c \+ X)%R] = 'V_P[X].
Lemma varianceD_cst_r (X : {RV P >-> R}) c :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
'V_P[(X \+ cst c)%R] = 'V_P[X].
Lemma varianceB_cst_l c (X : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
'V_P[(cst c \- X)%R] = 'V_P[X].
Lemma varianceB_cst_r (X : {RV P >-> R}) c :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
'V_P[(X \- cst c)%R] = 'V_P[X].
Lemma covariance_le (X Y : {RV P >-> R}) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
P.-integrable setT (EFin \o Y) → P.-integrable setT (EFin \o (Y ^+ 2)%R) →
P.-integrable setT (EFin \o (X × Y)%R) →
covariance P X Y ≤ sqrte 'V_P[X] × sqrte 'V_P[Y].
End variance.
Notation "'V_ P [ X ]" := (variance P X).
Section markov_chebyshev_cantelli.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Lemma markov (X : {RV P >-> R}) (f : R → R) (eps : R) :
(0 < eps)%R →
measurable_fun [set: R] f → (∀ r, 0 ≤ f r)%R →
{in `[0, +oo[%classic &, {homo f : x y / x ≤ y}}%R →
(f eps)%:E × P [set x | eps%:E ≤ `| (X x)%:E | ] ≤
'E_P[f \o (fun x ⇒ `| x |%R) \o X].
Lemma chebyshev (X : {RV P >-> R}) (eps : R) : (0 < eps)%R →
P [set x | (eps ≤ `| X x - fine ('E_P[X])|)%R ] ≤ (eps ^- 2)%:E × 'V_P[X].
Lemma cantelli (X : {RV P >-> R}) (lambda : R) :
P.-integrable setT (EFin \o X) → P.-integrable setT (EFin \o (X ^+ 2)%R) →
(0 < lambda)%R →
P [set x | lambda%:E ≤ (X x)%:E - 'E_P[X]]
≤ (fine 'V_P[X] / (fine 'V_P[X] + lambda^2))%:E.
End markov_chebyshev_cantelli.
Notation "{ 'dmfun' aT >-> T }" :=
(@discreteMeasurableFun.type _ aT T) : form_scope.
Definition discrete_random_variable (d : _) (T : measurableType d)
(R : realType) (P : probability T R) := {dmfun T >-> R}.
Notation "{ 'dRV' P >-> R }" :=
(@discrete_random_variable _ _ R P) : form_scope.
Section dRV_definitions.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Definition dRV_dom_enum (X : {dRV P >-> R}) :
{ B : set nat & {splitbij B >-> range X}}.
Qed.
Definition dRV_dom (X : {dRV P >-> R}) : set nat := projT1 (dRV_dom_enum X).
Definition dRV_enum (X : {dRV P >-> R}) : {splitbij (dRV_dom X) >-> range X} :=
projT2 (dRV_dom_enum X).
Definition enum_prob (X : {dRV P >-> R}) :=
(fun k ⇒ P (X @^-1` [set dRV_enum X k])) \_ (dRV_dom X).
End dRV_definitions.
Section distribution_dRV.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Variable X : {dRV P >-> R}.
Lemma distribution_dRV_enum (n : nat) : n \in dRV_dom X →
distribution P X [set dRV_enum X n] = enum_prob X n.
Lemma distribution_dRV A : measurable A →
distribution P X A = \sum_(k <oo) enum_prob X k × \d_ (dRV_enum X k) A.
Lemma sum_enum_prob : \sum_(n <oo) (enum_prob X) n = 1.
End distribution_dRV.
Section discrete_distribution.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Lemma dRV_expectation (X : {dRV P >-> R}) :
P.-integrable [set: T] (EFin \o X) →
'E_P[X] = \sum_(n <oo) enum_prob X n × (dRV_enum X n)%:E.
Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])).
Lemma expectation_pmf (X : {dRV P >-> R}) :
P.-integrable [set: T] (EFin \o X) → 'E_P[X] =
\sum_(n <oo | n \in dRV_dom X) (pmf X (dRV_enum X n))%:E × (dRV_enum X n)%:E.
End discrete_distribution.