Module infotheo.probability.proba

Require realType_ext.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra fingroup lra.
From mathcomp Require boolp.
From mathcomp Require Import unstable mathcomp_extra functions reals exp.
Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln fdist.

# Probabilities over finite distributions This file provides a formalization of finite probabilities using distributions over a finite type (see fsdist.v for finitely-supported distributions). Selected lemmas: - expected value of a sum of RVs (`E_sum_2`), a.k.a., the ``First Fundamental Mystery of Probability'' - variance of a sum (`V_sum_2`) - variance of the average for independent RVs (`Var_average`) - union bound/Boole's inequality (`Pr_bigcup`) - Boole's equality (`Boole_eq`) - laws of total probability (`total_prob`, `total_prob_cond`) - Bayes' theorems (`Bayes`, `Bayes_extended`) - an algebraic proof (by Erik Martin-Dorel) of the formula of inclusion-exclusion (`Pr_bigcup_incl_excl`) - reasoning by cases (`reasoning_by_cases`, `creasoning_by_cases`) - Markov' inequality (`markov`) - Chebyshev's inequality (`chebyshev_inequality`) - weak law of large numbers (`wlln`) ``` E `*T == the set of pairs (x, y) with x in E T`* F == the set of pairs (x, y) with y in F Pr d E == probability of event E over the distribution d {RV P -> T} == the type of random variables over an ambient distribution P where T is an eqType; if T is a ring or a module, so is {RV P -> T} ambient_dist X == the P in X : {RV P -> T} `Pr[ X = a ] == the probability that the random variable X is a with a : A : eqType `Pr[ X >= r ] == the probability that the random variable X is greater or equal to r `Pr[ X <= r ] == the probability that the random variable X is less or equal to r `Pr[ X \in E ] == the probability that the random variable X is in E (expect finTypes) `p_X := fdistmap X P with X : {RV P -> A} const_RV k == constant RV `log == binary log as a RV ``` Operations on random variables: ``` f `o X == composition of a function and a RV f `*: X == non-uniform scaling by scalers specified by f X `+cst m, X `-cst m == translation of a RV [% X, Y, ..., Z] == successive pairings of RVs k `cst* X, X `*cst k := k *: X (parsing-only notations for compatibility) `+,`-,`^2,`-- := +, -, ^+ 2, -, resp. (parsing-only, compatibility) X `/ n := n%:R^-1 `cst* X (parsing-only, compatibility) RV_fctE == multi-rule for evaluating RVs sumrRVE, prodRVE == evaluation laws for sums and products of RVs ``` ``` `E X == expected value of the random variable X Ex_alt X == expected value of an RV (sum in fin_img X) `E_[ X | F ] == conditional expectation of X given an event F Ind s a == indicator function (s : {set A}, a : A) `V X == the variance of the random variable X inde_events E F == E and F are independent events kwise_inde E == k-wise independence of the family of events E pairwise_inde E == pairwise independence of the family of events E mutual_inde E == mutual independence of the family of events E `Pr_P [ A | B ] == conditional probability for events fdist_cond E0 == distribution P conditioned by E with E : Pr P E != 0 cinde_events E F G == E and F are conditionally independent events given an event G P |= X _|_ Y == X and Y are independent The corresponding identifier is inde_RV X _|_ Y | Z == X and Y are conditionally independent given Z The corresponding identifier is cinde_RV `Pr[ X = a | Y = b ] == conditional probability for random variables `Pr[ X \in E | Y \in F ] == conditional probability for random variables P |= X _|_ Y | Z, X _|_ Y | Z == the RVs X and Y are conditionally independent given a RV Z (in a distribution P) P |= X _|_ Y == unconditional independence Z \= X @+ Y == Z is the sum of two random variables X \=sum Xs == X is the sum of the n>=1 independent and identically distributed random variables Xs ```

Reserved Notation "E `*T" (at level 1).
Reserved Notation "T`* F" (at level 40).
Reserved Notation "{ 'RV' d -> T }" (at level 0, d, T at level 1,
  format "{ 'RV' d -> T }").
Reserved Notation "`p_ X" (at level 5).
Reserved Notation "`Pr[ X = a ]" (at level 0, X, a at next level,
  format "`Pr[ X = a ]").
Reserved Notation "`Pr[ X '\in' E ]" (at level 0, X, E at next level,
  format "`Pr[ X '\in' E ]").
Reserved Notation "`Pr[ X >= r ]" (at level 0, X, r at next level,
  format "`Pr[ X >= r ]").
Reserved Notation "`Pr[ X <= r ]" (at level 0, X, r at next level,
  format "`Pr[ X <= r ]").
Reserved Notation "k `cst* X" (at level 49).
Reserved Notation "X `*cst k" (at level 49).
Reserved Notation "k `*: X" (at level 49).
Reserved Notation "f `o X" (at level 50, format "f `o '/ ' X").
Reserved Notation "X '`/' n" (at level 49, format "X '`/' n").
Reserved Notation "X `+ Y" (at level 50).
Reserved Notation "X `- Y" (at level 50).
Reserved Notation "X '`+cst' m" (at level 50).
Reserved Notation "X '`-cst' m" (at level 50).
Reserved Notation "X '`^2' " (at level 1).
Reserved Notation "'`--' P" (at level 5).
Reserved Notation "'`log' P" (at level 5).
Reserved Notation "'[%' x , y , .. , z ']'" (at level 0,
  format "[% x , y , .. , z ]").
Reserved Notation "X '\=sum' Xs" (at level 50).
Reserved Notation "'`E'" (at level 0).
Reserved Notation "'`V'" (at level 0).
Reserved Notation "`Pr_ P [ A | B ]" (at level 0, P, A, B at next level,
  format "`Pr_ P [ A | B ]").
Reserved Notation "`Pr_[ A | B ]" (at level 0, A, B at next level,
  format "`Pr_[ A | B ]").
Reserved Notation "`E_[ X | B ]" (at level 0, X, B at next level,
  format "`E_[ X | B ]").
Reserved Notation "`Pr[ X = a | Y = b ]" (at level 0, X, Y, a, b at next level,
  format "`Pr[ X = a | Y = b ]").
Reserved Notation "`Pr[ X '\in' E | Y '\in' F ]" (at level 0, X, Y, E, F at next level,
  format "`Pr[ X '\in' E | Y '\in' F ]").
Reserved Notation "`Pr[ X '\in' E | Y = F ]" (at level 0, X, Y, E, F at next level,
  format "`Pr[ X '\in' E | Y = F ]").
Reserved Notation "`Pr[ X = E | Y '\in' F ]" (at level 0, X, Y, E, F at next level,
  format "`Pr[ X = E | Y '\in' F ]").
Reserved Notation "X _|_ Y | Z" (at level 50, Y, Z at next level).
Reserved Notation "P |= X _|_ Y | Z" (at level 50, X, Y, Z at next level).
Reserved Notation "P |= X _|_ Y" (at level 50, X, Y at next level,
  format "P |= X _|_ Y").
Reserved Notation "Z \= X '@+' Y" (at level 50).

Set Implicit Arguments.
Set SsrOldRewriteGoalsOrder.
Unset Strict Implicit.
Import Prenex Implicits.

Local Open Scope ring_scope.
Local Open Scope reals_ext_scope.
Local Open Scope fdist_scope.
Local Open Scope proba_scope.

Delimit Scope set_scope with set.
Delimit Scope proba_scope with proba.

Import Order.POrderTheory GRing.Theory Num.Theory.

From mathcomp Require Import normedtype.
Import numFieldNormedType.Exports.

Lemma m1powD {R : pzRingType} k :
  k <> 0%nat -> (-1) ^+ (k-1) = - (-1) ^+ k :> R.

Proof.

by case: k => [//|k _]; rewrite subn1 /= exprS mulN1r opprK. Qed.

Notation "E `*T" := ([set x | x.1 \in E]) : proba_scope.
Notation "T`* F" := ([set x | x.2 \in F]) : proba_scope.

Section TsetT.
Context {R : realType}.

Variables (A B : finType) (P : R.-fdist (A * B)).
Implicit Types (E : {set A}) (F : {set B}).

Lemma TsetT : T`* setT = setT :> {set A * B}.

Proof.