Library discprob.prob.finite

From discprob.basic Require Import base Series_Ext seq_ext nify.
From discprob.prob Require Import countable rearrange prob.
Require Import Reals Fourier Omega Psatz.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop seq.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.

Definition finite_sum {A: finType} (f: A → R) :=
  λ n: nat, oapp f R0 (nth_error (Finite.enum A) n).

Section finite_sum_facts.

Variable (A: finType).
Implicit Types (a: A → R).

Lemma ex_series_eventually0 (a: nat → R):
  (∃ N, ∀ n, n ≥ N → a n = 0) → ex_series a.

Lemma ex_series_list_Rabs {B: eqType} (l: list B) (f: B → R):
  ex_series (λ n, Rabs (oapp f R0 (nth_error l n))).

Lemma ex_seriesF_Rabs a:
  ex_series (λ n, Rabs (finite_sum a n)).

Lemma ex_seriesF a:
  ex_series (finite_sum a).

Lemma SeriesF_big_op a:
  Series (finite_sum a) = \big[Rplus/0]_(i in A) (a i).

Lemma SeriesF_is_seriesC a:
  is_series (countable_sum a) (Series (finite_sum a)).

Lemma SeriesC_SeriesF a:
  Series (countable_sum a) = Series (finite_sum a).

Lemma SeriesC_fin_big a:
  Series (countable_sum a) = \big[Rplus/0]_(i in A) (a i).

Lemma SeriesF_is_seriesC' a v:
    \big[Rplus/0]_(i in A) a i = v →
    is_series (countable_sum a) v.

End finite_sum_facts.

Section img_fin.
Variable (A: finType) (B: eqType).
Definition img_fin_enum (f: A → B) : seq (imgT f).
Defined.

Lemma img_fin_enum_sval (f: A → B):
  map sval (img_fin_enum f) = undup [seq (f i) | i <- Finite.enum A].

Lemma img_fin_uniq (f: A → B) : uniq (img_fin_enum f).

Lemma img_fin_mem f x : x \in img_fin_enum f.

Definition img_finMixin (f: A → B) :=
  Eval hnf in @UniqFinMixin [countType of imgT f] (img_fin_enum f) (img_fin_uniq f) (img_fin_mem f).
Canonical img_finType (f: A → B) :=
  Eval hnf in FinType (imgT f) (img_finMixin f).
End img_fin.

Lemma img_fin_enum_sval_comp {A: finType} {B C: eqType} (f: A → B) (g: B → C):
  map sval (img_fin_enum _ _ (g \o f)) = undup [seq (g (f i)) | i <- Finite.enum A].

Lemma img_fin_big {A: finType} {B: eqType} (f: A → B) (F: B → R) P:
  \big[Rplus/0]_(i in img_finType A B f | P (sval i)) (F (sval i)) =
  \big[Rplus/0]_(i <- undup [seq (f i) | i <- Finite.enum A] | P i) (F i).

Lemma img_fin_big' {A: finType} {B: eqType} (f: A → B) (F: B → R) P:
  \big[Rplus/0]_(i <- img_fin_enum A B f | P (sval i)) (F (sval i)) =
  \big[Rplus/0]_(i <- undup [seq (f i) | i <- Finite.enum A] | P i) (F i).

  Lemma ex_Ex_fin {A: finType} {Ω: distrib A} (X: rrvar Ω):
    ex_Ex X.

  Hint Resolve ex_Ex_fin.

Section Ex_fin_prop.
  Variable (A: finType).
  Variable (Ω: distrib A).

Lemma Ex_fin_pt (X: rrvar Ω):
  Ex X = \big[Rplus/0]_(a in A) (X a × (rvar_dist X) a).

Lemma Ex_fin_comp {B: eqType} (X: rvar Ω B) (f: B → R):
  Ex (rvar_comp X f) = \big[Rplus/0]_(a : imgT X) (pr_eq X (sval a) × f (sval a)).

Lemma Ex_fin_comp_mono {B: eqType} (X: rvar Ω B) (f: B → R) (g: B → R):
    (∀ x, f x ≤ g x) →
    Ex (rvar_comp X f) ≤ Ex (rvar_comp X g).

Lemma pr_sum_all {B: eqType} (X: rvar Ω B):
  \big[Rplus/0]_(i : imgT X) pr_eq X (sval i) = 1.

Lemma Ex_comp_ext {B: eqType} (X: rvar Ω B) (f f': B → R):
  (∀ x, f x = f' x) →
  Ex (rvar_comp X f) = Ex (rvar_comp X f').

Lemma Ex_fin_plus_l (X: rrvar Ω) (x: R):
  Ex (rvar_comp X (Rplus x)) = x + Ex X.

Lemma Ex_fin_plus_r (X: rrvar Ω) (x: R):
  Ex (rvar_comp X (λ y, y + x)) = Ex X + x.

Lemma Ex_fin_scal_r (X: rrvar Ω) (c: R):
  Ex (rvar_comp X (λ x, x × c)) = Ex X × c.

Lemma Ex_fin_scal_l (X: rrvar Ω) (c: R):
  Ex (rvar_comp X (λ x, c × x)) = c × Ex X.

Lemma Ex_fin_sum (X Y: rrvar Ω):
  Ex (mkRvar Ω (λ x, X x + Y x)) =
  Ex X + Ex Y.

Lemma img_rvar_comp {B B': eqType} (r: rvar Ω B) (f: B → B'):
  map sval (Finite.enum [finType of (imgT (rvar_comp r f))])
  = undup ([ seq (f (sval x)) | x <- Finite.enum [finType of (imgT r)]]).
End Ex_fin_prop.


Lemma img_pair_rv {A A': finType} {B B': eqType} (Ω: distrib A) (Ω' : distrib A')
      (r: rvar Ω B) (r': rvar Ω' B'):
  perm_eq (map sval (Finite.enum [finType of imgT (rvar_pair r r')]))
          [seq (sval x1, sval x2) | x1 <- Finite.enum [finType of (imgT r)],
                          x2 <- Finite.enum [finType of (imgT r')]].

Lemma Rmult_if_distrib (P : bool) v a b:
  (if P then a else b) × v =
  (if P then a × v else b × v).

Lemma pr_eq_rvar_pair {A A': finType} {B B': eqType} {Ω: distrib A} {Ω': distrib A'}
      (r: rvar Ω B) (r': rvar Ω' B') bb:
  pr_eq (rvar_pair r r') bb = pr_eq r (fst bb) × pr_eq r' (snd bb).

Lemma rvar_pair_comp {A1 B1 A2 B2} {C1 C2: eqType} (Ω1: distrib A1) (Ω2: distrib A2)
      (r1: rvar Ω1 B1) (r2: rvar Ω2 B2) (f1: B1 → C1) (f2: B2 → C2):
  rvar_pair (rvar_comp r1 f1) (rvar_comp r2 f2) =
  rvar_comp (rvar_pair r1 r2) (λ xy, (f1 (fst xy), f2 (snd xy))).