Library probsa.util.indicator

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export notation.
Local Open Scope nat_scope.

(* ---------------------------------- Main ---------------------------------- *)
Definition indicatorR (b : bool) : R := if b then 1%R else 0%R.
Notation "'I[' b ']'" := (indicatorR b%N)
  (at level 10, format "I[ b ]") : probability_scope.

Lemma indicator_andb_mult :
  ∀ A B, (I[A && B] = I[A] × I[B])%R.

Lemma indicator_pred_eq :
  ∀ A B, A = B → I[A] = I[B].

Lemma indicator_pred_impl :
  ∀ A B, (B ==> A) → (I[A] ≥ I[B])%R.

Lemma bigsum_upper_bound_to_indicator :
  ∀ (t u : nat) (f : nat → R),
    t ≤ u →
    ∑_{0 ≤ i ≤ t} f i = ∑_{0 ≤ i ≤ u} I[i ≤ t] × f i.