Library probsa.probability.pmf
From probsa.util Require Export bigop_inf.
From probsa.probability Require Export pred stochastic_order independence.
Section ProbMassFunction.
Program Definition pmf_zero : distrib [countType of nat] :=
{|
pmf := fun (n : nat) ⇒ if (n == 0%nat) then 1 else 0
|}.
Program Definition pmf_sum (x1 x2 : distrib [countType of nat]) : distrib [countType of nat] :=
{|
pmf := fun (n : nat) ⇒ ∑_{0 ≤ i ≤ n} pmf x1 i × pmf x2 (n - i)%nat
|}.
End ProbMassFunction.
Infix "⊕" := pmf_sum (at level 50, left associativity).
Notation "⨁_{ i <- xs | P } F" :=
(\big[pmf_sum/pmf_zero]_(i <- xs | P) F%R)
(at level 41, F at level 41, i, xs at level 50,
format "'[' ⨁_{ i <- xs | P } '/ ' F ']'") : probability_scope.
Notation "⨁_{ m <= i < n } F" :=
(\big[pmf_sum/pmf_zero]_(i <- index_iota m n) F%R)
(at level 41, F at level 41, i, m, n at level 50,
format "'[' ⨁_{ m <= i < n } '/ ' F ']'") : probability_scope.
Notation "⨁_{ i < n } F" :=
(\big[pmf_sum/pmf_zero]_(i <- iota 0 n) F%R)
(at level 41, F at level 41, i, n at level 50,
format "'[' ⨁_{ i < n } '/ ' F ']'") : probability_scope.
From probsa.probability Require Export pred stochastic_order independence.
Section ProbMassFunction.
Program Definition pmf_zero : distrib [countType of nat] :=
{|
pmf := fun (n : nat) ⇒ if (n == 0%nat) then 1 else 0
|}.
Program Definition pmf_sum (x1 x2 : distrib [countType of nat]) : distrib [countType of nat] :=
{|
pmf := fun (n : nat) ⇒ ∑_{0 ≤ i ≤ n} pmf x1 i × pmf x2 (n - i)%nat
|}.
End ProbMassFunction.
Infix "⊕" := pmf_sum (at level 50, left associativity).
Notation "⨁_{ i <- xs | P } F" :=
(\big[pmf_sum/pmf_zero]_(i <- xs | P) F%R)
(at level 41, F at level 41, i, xs at level 50,
format "'[' ⨁_{ i <- xs | P } '/ ' F ']'") : probability_scope.
Notation "⨁_{ m <= i < n } F" :=
(\big[pmf_sum/pmf_zero]_(i <- index_iota m n) F%R)
(at level 41, F at level 41, i, m, n at level 50,
format "'[' ⨁_{ m <= i < n } '/ ' F ']'") : probability_scope.
Notation "⨁_{ i < n } F" :=
(\big[pmf_sum/pmf_zero]_(i <- iota 0 n) F%R)
(at level 41, F at level 41, i, n at level 50,
format "'[' ⨁_{ i < n } '/ ' F ']'") : probability_scope.
We say a random variable X is stochastically dominated by distribution p
(written X ⪯ p) if the CDF of X is pointwise greater than or equal to
the CDF of p. Formally, ℙ<μ>{X ≤ h} ≥ ℙ<p>{ω | ω ≤ h}, where on the RHS,
ω ranges over natural numbers sampled from p, so ω ≤ h is simply a
comparison of natural numbers. Note that a distribution p over natural
numbers can be viewed as a probability measure where p(n) gives the
probability of observing n.
Definition le_nrvar_ndistrib {Ω} {μ : measure Ω} (X : nrvar μ) (p : distrib [countType of nat]) :=
∀ h, ℙ<μ>{[ X ⟨<=⟩ h ]} ≥ ℙ<p>{[ leq^~ h ]}.
Instance dominance_nrvar_ndistrib :
∀ {Ω} {μ : measure Ω}, DominanceRelation (nrvar μ) (distrib [countType of nat]) :=
{ dominates := le_nrvar_ndistrib }.
Definition le_ndistrib_nrvar {Ω} {μ : measure Ω} (p : distrib [countType of nat]) (X : nrvar μ) :=
∀ h, ℙ<p>{[ leq^~ h ]} ≥ ℙ<μ>{[ X ⟨<=⟩ h ]}.
Instance dominance_ndistrib_nrvar :
∀ {Ω} {μ : measure Ω}, DominanceRelation (distrib [countType of nat]) (nrvar μ) :=
{ dominates := le_ndistrib_nrvar }.
Section StochasticOrder.
Context {Ω} {μ : measure Ω}.
Variable X1 X2 : nrvar μ.
Hypothesis H_independent : indep2 X1 X2.
Variable p1 p2 : distrib [countType of nat].
Hypothesis H_X1_bounded_by_p1 : X1 ⪯ p1.
Hypothesis H_X2_bounded_by_p2 : X2 ⪯ p2.
∀ h, ℙ<μ>{[ X ⟨<=⟩ h ]} ≥ ℙ<p>{[ leq^~ h ]}.
Instance dominance_nrvar_ndistrib :
∀ {Ω} {μ : measure Ω}, DominanceRelation (nrvar μ) (distrib [countType of nat]) :=
{ dominates := le_nrvar_ndistrib }.
Definition le_ndistrib_nrvar {Ω} {μ : measure Ω} (p : distrib [countType of nat]) (X : nrvar μ) :=
∀ h, ℙ<p>{[ leq^~ h ]} ≥ ℙ<μ>{[ X ⟨<=⟩ h ]}.
Instance dominance_ndistrib_nrvar :
∀ {Ω} {μ : measure Ω}, DominanceRelation (distrib [countType of nat]) (nrvar μ) :=
{ dominates := le_ndistrib_nrvar }.
Section StochasticOrder.
Context {Ω} {μ : measure Ω}.
Variable X1 X2 : nrvar μ.
Hypothesis H_independent : indep2 X1 X2.
Variable p1 p2 : distrib [countType of nat].
Hypothesis H_X1_bounded_by_p1 : X1 ⪯ p1.
Hypothesis H_X2_bounded_by_p2 : X2 ⪯ p2.
If X1 ⪯ p1, X2 ⪯ p2, and X1, X2 are independent, then their sum is
stochastically dominated by the convolution of p1 and p2.
Complement of the previous lemma: the probability that the sum of two
independent random variables exceeds a threshold t is bounded by the
probability that a sample from the convolution of their bounding
distributions exceeds t.
Corollary addrv_addmpf_respect_ltn :
∀ t,
ℙ<μ>{[ λ ω, (t < X1 ω + X2 ω)%nat ]} ≤ ℙ<p1 ⊕ p2>{[ ltn t ]}.
End StochasticOrder.
Section StochasticOrderSum.
Context {Ω} {μ : measure Ω}.
Context {X : eqType}.
Variable (F : X → nrvar μ) (P : pred X).
Variable (xs : seq X).
Hypothesis H_independent : independent [seq F x | x <- xs].
Variable p : X → distrib [countType of nat].
Hypothesis H_bound : ∀ x, x \in xs → P x → F x ⪯ p x.
Lemma sumrv_sumpmf_respect_stochastic_order :
∑[rv]_{ x <- xs | P x } F x ⪯ ⨁_{x <- xs | P x} p x.
End StochasticOrderSum.
∀ t,
ℙ<μ>{[ λ ω, (t < X1 ω + X2 ω)%nat ]} ≤ ℙ<p1 ⊕ p2>{[ ltn t ]}.
End StochasticOrder.
Section StochasticOrderSum.
Context {Ω} {μ : measure Ω}.
Context {X : eqType}.
Variable (F : X → nrvar μ) (P : pred X).
Variable (xs : seq X).
Hypothesis H_independent : independent [seq F x | x <- xs].
Variable p : X → distrib [countType of nat].
Hypothesis H_bound : ∀ x, x \in xs → P x → F x ⪯ p x.
Lemma sumrv_sumpmf_respect_stochastic_order :
∑[rv]_{ x <- xs | P x } F x ⪯ ⨁_{x <- xs | P x} p x.
End StochasticOrderSum.