Library probsa.probability.cdf

Require Export prosa.util.ssrlia.

From probsa.util Require Export indicator.
From probsa.probability Require Export nrvar.
Local Open Scope nat_scope.

Definition cdf {Ω} {μ : measure Ω} (X : nrvar μ) (x : nat) := ℙ <μ >{[ X ⟨<=⟩ x ]}.
Notation "'𝔽<' μ '>{[' X ']}(' x ')'" := (@cdf _ μ X x)
  (at level 10, format "𝔽< μ >{[ X ]}( x )") : probability_scope.
Notation "'𝔽<' μ '>{[' X ']}'" := (@cdf _ μ X )
  (at level 10, format "𝔽< μ >{[ X ]}") : probability_scope.

Lemma cdf_nonnegative :
  ∀ {Ω} {μ : measure Ω} (X : nrvar μ),
  ∀ x, 0 ≤ 𝔽<μ >{[ X ]}(x ).
Proof. by intros; apply Rge_le, ge_pr_0. Qed.

Lemma cdf_nondecreasing :
  ∀ {Ω} {μ : measure Ω} (X : nrvar μ),
  ∀ x1 x2, x1 ≤ x2 → 𝔽<μ >{[ X ]}(x1 ) ≤ 𝔽<μ >{[ X ]}(x2 ).
Proof.
  intros × LE.
  apply pr_mono_pred ⇒ ω LE2.
  by eapply leq_trans; first apply LE2.
Qed.

We show that the CDF of a random variable X at x.+1 (which is the successor of x, i.e., x + 1) is equal to the CDF of X at x plus the probability of X being equal to x.+1.

Lemma cdf_succ_to_cdf_preq :
  ∀ {Ω} {μ : measure Ω} (X : nrvar μ) (x : nat),
    ( 𝔽<μ >{[ X ]}(x.+1) = 𝔽<μ >{[ X ]}(x ) + ℙ <μ >{[ X ⟨=⟩ x.+1 ]} )%R.
Proof.
  intros; rewrite /pr_eq /pr -Series_plus //=.
  - apply Series_ext ⇒ n.
    rewrite -countable_sum_plus.
    apply countable_sum_ext ⇒ ω.
    unfold "⟨<=⟩", "⟨=⟩", nrvar_nat_pred_eqop, rvar_nat_pred_leqop ⇒ //=.
    rewrite leq_eqVlt ltnS; destruct (X ω == x.+1) eqn:EQ, (X ω ≤ x) eqn:LE;
      try rewrite EQ; try rewrite LE //=.
    + by exfalso; ssrlia.
    + by rewrite Rplus_0_l.
    + by rewrite Rplus_0_r.
    + by rewrite Rplus_0_r.
  - by apply pr_ex_series.
  - by apply pr_ex_series.
Qed.

Next, we show that the probability of a random variable X being less than or equal to a certain x is the total probability of X being exactly i for all i from 0 to x.

Lemma cdf_to_sum_of_preq :
  ∀ {Ω} {μ : measure Ω} (X : nrvar μ) x,
    𝔽<μ >{[ X ]}(x ) = ∑_{0 ≤ i ≤ x } ℙ <μ >{[ X ⟨=⟩ i ]}.
Proof.
  intros *; induction x.
  - cbv[iota]; rewrite big_seq1.
    by apply pr_eq_pred' ⇒ ω; split; unfold "⟨<=⟩", rvar_nat_pred_leqop; [rewrite leqn0 | move ⇒ /eqP ->].
  - rewrite big_nat_recr //= -IHx; clear IHx.
    by rewrite cdf_succ_to_cdf_preq.
Qed.

We extend the previous lemma to a sum over an arbitrary range from 0 to u for u ≥ t. The condition u ≥ t ensures that probabilities of X (ℙ<μ>{[ X ⟨=⟩ i ]}) where i is greater than t are filtered out.

Corollary cdf_to_sum_of_indicators :
  ∀ {Ω} {μ : measure Ω} (X : nrvar μ),
  ∀ (t u : nat),
    t ≤ u →
    𝔽<μ >{[ X ]}(t ) = ∑_{0 ≤ i ≤ u } I [i ≤ t ] × ℙ <μ >{[ X ⟨=⟩ i ]}.
Proof.
  intros × LE; rewrite -bigsum_upper_bound_to_indicator //.
  by apply cdf_to_sum_of_preq.
Qed.