Library probsa.util.indicator

From probsa.util Require Export notation.
Local Open Scope nat_scope.

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.
Proof.
  by move ⇒ [] [] //=; nra.
Qed.

Lemma indicator_pred_eq :
  ∀ A B, A = B → I[A] = I[B].
Proof. by move ⇒ A B →. Qed.

Lemma indicator_pred_impl :
  ∀ A B, (B ==> A) → (I[A] ≥ I[B])%R.
Proof. by move ⇒ [] [] //=; nra. Qed.

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.
Proof.
  intros; rewrite (@big_cat_nat _ _ _ t.+1 0 u.+1) //=.
  have ->: ∑_{t.+1 ≤ i ≤ u} I[i ≤ t] × f i = 0%R.
  { apply big1_seq ⇒ i; rewrite mem_iota ⇒ /andP [_ /andP [LE _]].
    by rewrite leqNgt LE //= Rmult_0_l.
  }
  rewrite Rplus_0_r; apply eq_big_seq ⇒ i; rewrite mem_iota add0n ltnS ⇒ /andP [_ LE].
  by rewrite LE // Rmult_1_l.
Qed.