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

Lemma cdf_nondecreasing :
  ∀ {Ω} {μ : measure Ω} (X : nrvar μ),
  ∀ x1 x2, x1 ≤ x2 → 𝔽<μ >{[ X ]}(x1 ) ≤ 𝔽<μ >{[ X ]}(x2 ).

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.

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

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