Library probsa.probability.prob

(* ---------------------------------- Prosa --------------------------------- *)
Require Export prosa.util.all.

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Import iota indicator.
From probsa.probability Require Import pred.

(* --------------------------------- Lemmas --------------------------------- *)

Additional Lemmas

In this file, we prove several useful lemmas about the probability function.

Lemma pr_pos :
  ∀ {Ω} (μ : measure Ω) (P : pred Ω) (ω : Ω ),
    P ω →
    μ ω > 0 →
    ℙ <μ >{[ P ]} > 0.

Lemma pr_pos_inv :
  ∀ {Ω} {μ : measure Ω} (P : pred Ω),
    ℙ <μ >{[ P ]} > 0 →
    ∃ ω , P ω ∧ μ ω > 0.

Lemma pr_pos_or_zero :
  ∀ {Ω} (μ : measure Ω) (P : pred Ω),
    ℙ <μ >{[ P ]} = 0 ∨ ℙ <μ >{[ P ]} > 0.

Lemma pr_leq_intersectionr :
  ∀ {Ω} (μ : measure Ω) (A B : pred Ω),
    ℙ <μ >{[ A ∩ B ]} ≤ ℙ <μ >{[ B ]}.

Given two events A and B, the probability that A or B occurs is equal to the sum of the probabilities of A and B minus the probability of their intersection.

In other words, if we want to calculate the probability of an event that can be expressed as the union of two events A and B, we can find the probabilities of A and B separately, and then subtract the probability of their intersection to avoid double-counting.

Lemma pr_of_union :
  ∀ {Ω} {μ : measure Ω} (A B : pred Ω),
    ℙ <μ >{[ A ∪ B ]} = ℙ <μ >{[ A ]} + ℙ <μ >{[ B ]} - ℙ <μ >{[ A ∩ B ]}.

Lemma pr_bool_move :
  ∀ {Ω} {μ : measure Ω} (P : pred Ω) (B : bool ),
    ℙ <μ >{[ λ ω : Ω , B && P ω ]} = I [B ] × ℙ <μ >{[ P ]}.

Lemma pr_eq_measure :
  ∀ {Ω} {μ1 μ2 : measure Ω} (P : pred Ω ),
    (∀ ω, μ1 ω = μ2 ω ) →
    ℙ <μ1 >{[ P ]} = ℙ <μ2 >{[ P ]}.

Lemma pr_eq_pred_pos :
  ∀ {Ω} {μ : measure Ω} (P Q : pred Ω),
    (∀ ω, μ ω > 0 → P ω = Q ω ) →
    ℙ <μ >{[ P ]} = ℙ <μ >{[ Q ]}.

Lemma pr_pred_compl :
  ∀ {Ω} {μ : measure Ω} (P : pred Ω),
    ℙ <μ >{[ P ]} = 1 - ℙ <μ >{[ !P ]}.

Lemma pr_ineq_compl :
  ∀ {ΩX ΩY} {μX : measure ΩX} {μY : measure ΩY} (X : ΩX → nat) (Y : ΩY → nat) (c : nat),
    ℙ <μX >{[ λ ω , (c ≥ X ω)%N ]} ≥ ℙ <μY >{[ λ ω , (c ≥ Y ω)%N ]} →
    ℙ <μX >{[ λ ω , (c < X ω)%N ]} ≤ ℙ <μY >{[ λ ω , (c < Y ω)%N ]}.

The following lemma states that the measure of the union of a disjoint sequence of events (represented as λ ω, has (fun i ⇒ p i ω) (index_iota t1 t2)) is equal to the sum of the measures of the individual events. Note that the predicate λ ω, has (fun i ⇒ p i ω) (index_iota t1 t2) has a simple intuitive interpretation -- the predicate is true for a given ω : Ω if and only if p i ω is true for at least one of the indices i from the range t1 to t2-1.

More specifically, given a probability space (Ω,μ) and a sequence of predicates p i : Ω → Prop for i ranging from t1 to t2-1, the lemma asserts that if the predicates are pairwise disjoint (i.e., p i and p j have no common points for distinct i and j), then the probability of the union of these events is equal to the sum of the probabilities of each individual event.

The proof of the lemma relies on the fact that the sequence of events we consider is pairwise disjoint. This allows us to apply the additivity property of measures, which states that the measure of the union of a sequence of pairwise disjoint events is equal to the sum of the measures of the individual events.

The condition that the predicates p i are pairwise disjoint is essential for the proof of the lemma to hold. Without this condition, the events we consider may have overlapping points, and the additivity property of measures would not apply. In fact, the sum of the probabilities of the individual events can be greater than the probability of the union of events with overlapping points.

Lemma union_disj_eq_sum_prob :
  ∀ {Ω} {μ : measure Ω} (t1 t2 : nat) (p : nat → pred Ω),
    (∀ (ω : Ω) (i1 i2 : nat), p i1 ω → p i2 ω → i1 = i2 ) →
    ℙ <μ >{[ λ ω , has (fun i ⇒ p i ω) (index_iota t1 t2) ]} = ∑_{t1 ≤ i < t2 } ℙ <μ >{[ p i ]}.