Library probsa.probability.law_of_total_prob

From discprob.prob Require Export prob countable stochastic_order indep.

From probsa.util Require Export indicator.
From probsa.probability Require Export conditional.

Law of Total Probability

In the following section, we show that if we have a countable set of pairwise disjoint sets, then the sum of probabilities of those sets converges to a finite value. The proof of this result is highly technical; therefore, it is recommended to skip over any "Definitions" and "Remarks".

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.

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))).

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.

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".

Section LawOfTotalProbability.

Consider a probability space (Ω, μ), ...

Context {Ω} {μ : measure Ω}.

Consider any predicate P : Ω → bool. Notice that any predicate trivially defines a subset of Ω as {ω ∈ Ω | P ω }. Also recall that subsets of Ω are also events.

Variable (P : pred Ω).

Consider a countable type I (this can be either finite or countably infinite set) and a family of predicates B : I → pred Ω.

Variables (I : countType) (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.

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.

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 ω ]}.