Library probsa.probability.law_of_total_prob
(* -------------------------------- Coq-Proba ------------------------------- *)
From discprob.prob Require Export prob countable stochastic_order indep.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export indicator.
From probsa.probability Require Export conditional.
(* ---------------------------------- Main ---------------------------------- *)
From discprob.prob Require Export prob countable stochastic_order indep.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export indicator.
From probsa.probability Require Export conditional.
(* ---------------------------------- Main ---------------------------------- *)
Law of Total Probability
Section SumOfDisjointEventsExists.
Variable (Ω : countType).
Variable (μ : measure Ω).
Variables (I : countType) (B : I → pred Ω).
Hypothesis H_Bi_disjoint : ∀ ω, ∀ i j : I, B i ω → B j ω → i = j.
Definition is_in_cover : pred Ω :=
λ (ω : Ω), exC (λ i, B i ω).
Definition get_cover_index (ω : Ω) : option I :=
match LPO_countb (fun i ⇒ B i ω) with
| inleft i ⇒ Some (sval i)
| inright _ ⇒ None
end.
Definition pickle_cover_of ω : nat :=
match get_cover_index ω with
| None ⇒ O
| Some i ⇒ (pickle i).+1
end.
Remark get_cover_index_valid :
∀ v a, B v a → get_cover_index a = Some v.
Definition apt :=
λ mn, match mn with
| (S m, S n) ⇒
match (@pickle_inv I m), (@pickle_inv Ω n) with
| Some i, Some a ⇒ if B i a then μ a else 0
| _, _ ⇒ 0
end
| _ ⇒ 0
end.
Definition σpt : nat → nat × nat :=
λ n, match @pickle_inv [countType of Ω] n with
| Some a ⇒ (pickle_cover_of a , S(pickle a))
| None ⇒ (O, O)
end.
Remark σpt_inj :
∀ n n', apt (σpt n) ≠ 0 → σpt n = σpt n' → n = n'.
Remark σpt_cov :
∀ n, apt n ≠ 0 → ∃ m, σpt m = n.
Remark apt_row_rewrite :
∀ j, Series (λ k : nat, apt (S j, S k)) = countable_sum (λ i : I, ℙ<μ>{[ B i ]}) j.
Remark apt_double_summable_by_column :
double_summable apt.
Variable (Ω : countType).
Variable (μ : measure Ω).
Variables (I : countType) (B : I → pred Ω).
Hypothesis H_Bi_disjoint : ∀ ω, ∀ i j : I, B i ω → B j ω → i = j.
Definition is_in_cover : pred Ω :=
λ (ω : Ω), exC (λ i, B i ω).
Definition get_cover_index (ω : Ω) : option I :=
match LPO_countb (fun i ⇒ B i ω) with
| inleft i ⇒ Some (sval i)
| inright _ ⇒ None
end.
Definition pickle_cover_of ω : nat :=
match get_cover_index ω with
| None ⇒ O
| Some i ⇒ (pickle i).+1
end.
Remark get_cover_index_valid :
∀ v a, B v a → get_cover_index a = Some v.
Definition apt :=
λ mn, match mn with
| (S m, S n) ⇒
match (@pickle_inv I m), (@pickle_inv Ω n) with
| Some i, Some a ⇒ if B i a then μ a else 0
| _, _ ⇒ 0
end
| _ ⇒ 0
end.
Definition σpt : nat → nat × nat :=
λ n, match @pickle_inv [countType of Ω] n with
| Some a ⇒ (pickle_cover_of a , S(pickle a))
| None ⇒ (O, O)
end.
Remark σpt_inj :
∀ n n', apt (σpt n) ≠ 0 → σpt n = σpt n' → n = n'.
Remark σpt_cov :
∀ n, apt n ≠ 0 → ∃ m, σpt m = n.
Remark apt_row_rewrite :
∀ j, Series (λ k : nat, apt (S j, S k)) = countable_sum (λ i : I, ℙ<μ>{[ B i ]}) j.
Remark apt_double_summable_by_column :
double_summable apt.
Next we prove that if we have a partition of our measure space
Ω into sets B i, then the probabilities of each set B i
can be summed up and that sum is equal to the sum of the measure
of all ω ∈ Ω, where ω is only included in the sum if ω is
covered by some set in the partition.
Remark pr_eq_over_partition_is_series :
is_series
(countable_sum (λ (i : I), ℙ<μ>{[ B i ]}))
(Series (countable_sum (λ (ω : Ω), if is_in_cover ω then μ ω else 0))).
is_series
(countable_sum (λ (i : I), ℙ<μ>{[ B i ]}))
(Series (countable_sum (λ (ω : Ω), if is_in_cover ω then μ ω else 0))).
Finally, we show that if we have a countable partition of a
probability space (Ω, μ) into (disjoint) sets B i, then the
series of probabilities of those sets converges. In other words,
if we sum the probability measures of each set in the partition,
the resulting series converges.
Lemma ex_series_pr_eq_over_disjoint :
ex_series (countable_sum (λ i : I, ℙ<μ>{[ B i ]})).
End SumOfDisjointEventsExists.
Section SumOfPartitionEventsExists.
Lemma ex_series_pr_eq_over_partition :
∀ {Ω} (μ : measure Ω), ∀ (P : @Ω_partition Ω μ),
ex_series (countable_sum (λ i : I P, ℙ<μ>{[ p P i]})).
End SumOfPartitionEventsExists.
ex_series (countable_sum (λ i : I, ℙ<μ>{[ B i ]})).
End SumOfDisjointEventsExists.
Section SumOfPartitionEventsExists.
Lemma ex_series_pr_eq_over_partition :
∀ {Ω} (μ : measure Ω), ∀ (P : @Ω_partition Ω μ),
ex_series (countable_sum (λ i : I P, ℙ<μ>{[ p P i]})).
End SumOfPartitionEventsExists.
In the following section we prove the law of total probability.
The law states that, given an event P and a countable set of
pairwise disjoint events B i, the probability of P is equal to
the sum of the probabilities of the intersection P ∩ B i for all
i.
The proof of this result is highly technical; therefore, it is
recommended to skip over any "Definitions" and "Remarks".
Consider any predicate P : Ω → bool. Notice that any predicate
trivially defines a subset of Ω as {ω ∈ Ω | P ω }. Also
recall that subsets of Ω are also events.
Consider a countable type I (this can be either finite or
countably infinite set) and a family of predicates B : I → pred
Ω.
Next, let us assume that B covers all positive-probability
elements of Ω. That is, for any element ω : Ω with positive
probability, there exists an element i : I such that ω
satisfies/belongs to B i.
Second, let us assume that B is a set of disjoint sets. That
is, for any element ω : Ω and for any distinct i, j : I, if
both B i ω and B j ω are true, then i must equal j. This
enforces the requirement that the sets defined by the predicates
in B must be disjoint.
Hypothesis H_Bi_covers : ∀ ω, μ ω > 0 → ∃ i : I, B i ω.
Hypothesis H_Bi_disjoint : ∀ ω, ∀ i j : I, B i ω → B j ω → i = j.
Definition atotal : nat × nat → R :=
fun mn ⇒
match mn with
| (m, n) ⇒
match (@pickle_inv I m), (@pickle_inv Ω n) with
| Some i, Some a ⇒ (if (B i a) && P a then μ a else 0)
| _, _ ⇒ 0
end
end.
Remark ex_total_column_abs i :
ex_series
(λ k : nat,
Rabs
match @pickle_inv Ω k with
| Some a ⇒ if (B i a) && P a then μ a else 0
| None ⇒ 0
end).
Remark atotal_double_summable_by_column:
double_summable atotal.
Remark atotal_row_rewrite j :
Series (λ k : nat, atotal (j, k))
= countable_sum (λ i : I, pr μ (λ a, (B i a) && P a)) j.
Remark atotal_column_rewrite k :
Series (λ j : nat, atotal (j, k))
= countable_sum (λ a, if P a then μ a else 0) k.
Hypothesis H_Bi_disjoint : ∀ ω, ∀ i j : I, B i ω → B j ω → i = j.
Definition atotal : nat × nat → R :=
fun mn ⇒
match mn with
| (m, n) ⇒
match (@pickle_inv I m), (@pickle_inv Ω n) with
| Some i, Some a ⇒ (if (B i a) && P a then μ a else 0)
| _, _ ⇒ 0
end
end.
Remark ex_total_column_abs i :
ex_series
(λ k : nat,
Rabs
match @pickle_inv Ω k with
| Some a ⇒ if (B i a) && P a then μ a else 0
| None ⇒ 0
end).
Remark atotal_double_summable_by_column:
double_summable atotal.
Remark atotal_row_rewrite j :
Series (λ k : nat, atotal (j, k))
= countable_sum (λ i : I, pr μ (λ a, (B i a) && P a)) j.
Remark atotal_column_rewrite k :
Series (λ j : nat, atotal (j, k))
= countable_sum (λ a, if P a then μ a else 0) k.
With this, we prove that the probability of an event defined by
P is equal to the (possibly infinite) sum of events defined by
B i ∩ P, where i ∈ I.
Lemma law_of_total_probability :
ℙ<μ>{[ P ]} = ∑[∞]_{i <- I} ℙ<μ>{[ B i ∩ P ]}.
End LawOfTotalProbability.
Section LawOfTotalProbabilityProd.
Context {Ω} (μ : measure Ω).
Variable (A : pred Ω).
Variable (S : @Ω_partition Ω μ).
Lemma law_of_total_probability_prod :
ℙ<μ>{[ A ]} = ∑[∞]_{ i <- I S } ℙ<μ>{[ A ∩ p S i ]}.
End LawOfTotalProbabilityProd.
(* ------------------------------ Corollaries ------------------------------- *)
Corollary bigop_inf_cdf_le :
∀ {Ω} {μ : measure Ω} (X : nrvar μ) (n0 : nat),
∑[∞]_{n<-nat} (I[n ≤ n0] × ℙ<μ>{[ λ ω, X ω == n ]})%R = ℙ<μ>{[ X ⟨<=⟩ n0 ]}.
Corollary bigop_inf_option_cdf_lt :
∀ {Ω} {μ : measure Ω} (X : Ω → option nat) (n0 : option nat),
∑[∞]_{n<-option nat} (I[n0 ⟨<⟩ n] × ℙ<μ>{[ λ ω, X ω == n ]})%R = ℙ<μ>{[ λ ω, n0 ⟨<⟩ X ω ]}.
ℙ<μ>{[ P ]} = ∑[∞]_{i <- I} ℙ<μ>{[ B i ∩ P ]}.
End LawOfTotalProbability.
Section LawOfTotalProbabilityProd.
Context {Ω} (μ : measure Ω).
Variable (A : pred Ω).
Variable (S : @Ω_partition Ω μ).
Lemma law_of_total_probability_prod :
ℙ<μ>{[ A ]} = ∑[∞]_{ i <- I S } ℙ<μ>{[ A ∩ p S i ]}.
End LawOfTotalProbabilityProd.
(* ------------------------------ Corollaries ------------------------------- *)
Corollary bigop_inf_cdf_le :
∀ {Ω} {μ : measure Ω} (X : nrvar μ) (n0 : nat),
∑[∞]_{n<-nat} (I[n ≤ n0] × ℙ<μ>{[ λ ω, X ω == n ]})%R = ℙ<μ>{[ X ⟨<=⟩ n0 ]}.
Corollary bigop_inf_option_cdf_lt :
∀ {Ω} {μ : measure Ω} (X : Ω → option nat) (n0 : option nat),
∑[∞]_{n<-option nat} (I[n0 ⟨<⟩ n] × ℙ<μ>{[ λ ω, X ω == n ]})%R = ℙ<μ>{[ λ ω, n0 ⟨<⟩ X ω ]}.