Library discprob.prob.stochastic_order
From discprob.basic Require Import base order.
From discprob.prob Require Import prob countable finite.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
From mathcomp Require Import tuple finfun bigop prime binomial finset.
Require Import Reals Fourier FunctionalExtensionality Psatz.
Require Import Coq.omega.Omega.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.
Notation "x ≤ y" := (Rle x y) (at level 70, no associativity).
Notation "x ≥ y" := (Rge x y) (at level 70, no associativity).
Lemma Finite_inj x y: Finite x = Finite y → x = y.
Lemma big_cons_Rplus:
∀ (I : Type)
(i : I) (r : seq I) (P : pred I) (F : I → R)
(x:=\big[Rplus/0]_(j <- r | P j) F j),
\big[Rplus/0]_(j <- (i :: r) | P j) F j = (if P i then (F i) else 0) + x.
Lemma Rlt_not_eq': ∀ r1 r2, r1 < r2 → r2 ≠ r1.
Lemma if_sumbool_case_match {A: Type} P Q (b: {P} + {¬ P}) (b': {Q} + {¬ Q}) (x y: A):
(P ↔ Q) → (if b then x else y) = (if b' then x else y).
Lemma pr_sum_restrict {A: finType} (Ω: distrib A) (X: rrvar Ω) l P:
\big[Rplus/0]_(i <- l | P i) pr_eq X i =
\big[Rplus/0]_(i <- l | P i && (Rgt_dec (pr_eq X i) 0)) pr_eq X i.
Section pr_gt.
Definition pr_gt_indicator {A} {Ω: distrib A} (T: rrvar Ω) r :=
indicator T (λ n, Rgt_dec n r).
Lemma pr_gt_to_indicator {A} {Ω: distrib A} (T: rrvar Ω) r:
pr (rvar_dist T) (λ n, Rgt_dec (T n) r) = pr_eq (pr_gt_indicator T r) 1.
Variable A: finType.
Variable Ω: distrib A.
Variable T: rrvar Ω.
Lemma pr_gt_alt r: pr (rvar_dist T) (λ a, Rgt_dec (T a) r)
= \big[Rplus/0]_(v : imgT T) if (Rgt_dec (sval v) r) then pr_eq T (sval v) else 0.
Lemma pr_gt_alt3 r: pr (rvar_dist T) (λ n, Rgt_dec (T n) r) =
\big[Rplus/0]_(i <- filter (λ x, Rgt_dec (sval x) r)
(Finite.enum [finType of imgT T])) (pr_eq T (sval i)).
End pr_gt.
Lemma pr_gt_alt_comp {A: finType} {B: eqType} {Ω: distrib A} (T: rvar Ω B) (f: B → R) r:
pr (rvar_dist (rvar_comp T f)) (λ n, Rgt_dec ((rvar_comp T f) n) r)
= \big[Rplus/0]_(v : imgT T) if (Rgt_dec (f (sval v)) r) then pr_eq T (sval v) else 0.
Section pr_ge.
Definition pr_ge_indicator {A} {Ω: distrib A} (T: rrvar Ω) r :=
indicator T (λ n, Rge_dec n r).
Lemma pr_ge_to_indicator {A} {Ω: distrib A} (T: rrvar Ω) r:
pr (rvar_dist T) (λ n, Rge_dec (T n) r) = pr_eq (pr_ge_indicator T r) 1.
Variable A: finType.
Variable Ω: distrib A.
Variable T: rrvar Ω.
Lemma pr_ge_alt r: pr (rvar_dist T) (λ a, Rge_dec (T a) r)
= \big[Rplus/0]_(v : imgT T) if (Rge_dec (sval v) r) then pr_eq T (sval v) else 0.
Lemma pr_ge_alt3 r: pr (rvar_dist T) (λ n, Rge_dec (T n) r) =
\big[Rplus/0]_(i <- filter (λ x, Rge_dec (sval x) r)
(Finite.enum [finType of imgT T])) (pr_eq T (sval i)).
End pr_ge.
Lemma pr_ge_alt_comp {A: finType} {B: eqType} {Ω: distrib A} (T: rvar Ω B) (f: B → R) r:
pr (rvar_dist (rvar_comp T f)) (λ n, Rge_dec ((rvar_comp T f) n) r)
= \big[Rplus/0]_(v : imgT T) if (Rge_dec (f (sval v)) r) then pr_eq T (sval v) else 0.
Section pr_eq.
Definition pr_eq_indicator {A} {B: eqType} {Ω: distrib A} (T: rvar Ω B) r :=
indicator T (λ n, n == r).
Lemma pr_eq_to_indicator {A} {B} {Ω: distrib A} (T: rvar Ω B) r:
pr (rvar_dist T) (λ n, (T n) == r) = pr_eq (pr_eq_indicator T r) 1.
Variable A: finType.
Variable B: eqType.
Variable Ω: distrib A.
Variable T: rvar Ω B.
Lemma pr_eq_alt r: pr (rvar_dist T) (λ a, (T a) == r)
= \big[Rplus/0]_(v : imgT T) if (sval v == r) then pr_eq T (sval v) else 0.
End pr_eq.
Lemma pr_eq_alt_comp {A: finType} {B C: eqType} {Ω: distrib A} (T: rvar Ω B) (f: B → C) r:
pr (rvar_dist (rvar_comp T f)) (λ n, (rvar_comp T f) n == r)
= \big[Rplus/0]_(v : imgT T) if (f (sval v) == r) then pr_eq T (sval v) else 0.
Section convert.
Lemma pr_gt_to_geq_eps {A: finType} {Ω: distrib A} (X: rrvar Ω) (x eps: R):
(eps > 0 ∧ ∀ y, y \in img X → y ≠ x → Rabs (x - y) ≥ eps) →
pr_gt X x = pr_ge X (x + eps/2).
Lemma pr_ge_to_gt_eps {A: finType} {Ω: distrib A} (X: rrvar Ω) (x eps: R):
(eps > 0 ∧ ∀ y, y \in img X → y ≠ x → Rabs (x - y) ≥ eps) →
pr_ge X x = pr_gt X (x - eps/2).
Lemma pr_ge_split_eps {A: finType} {Ω: distrib A} (X: rrvar Ω) (x eps: R):
(eps > 0 ∧ ∀ y, y \in img X → y ≠ x → Rabs (x - y) ≥ eps) →
pr_eq X x = pr_ge X (x - eps/2) - pr_ge X (x + eps/2).
Lemma Rmin_dist_list (l: seq R) (x: R):
∃ eps, eps > 0 ∧ ∀ y, y \in l → y ≠ x → Rabs (x - y) ≥ eps.
Lemma pr_ge_split2 {A B: finType} {Ω: distrib A} {Ω': distrib B} (X: rrvar Ω) (Y: rrvar Ω')
(x: R): ∃ x1 x2,
pr_eq X x = pr_ge X x1 - pr_ge X x2 ∧
pr_eq Y x = pr_ge Y x1 - pr_ge Y x2.
Lemma pr_gt_to_geq2 {A B: finType} {Ω: distrib A} {Ω': distrib B} (X: rrvar Ω) (Y: rrvar Ω')
(x: R): ∃ x',
pr_gt X x = pr_ge X x' ∧
pr_gt Y x = pr_ge Y x'.
Lemma pr_ge_to_gt2 {A B: finType} {Ω: distrib A} {Ω': distrib B} (X: rrvar Ω) (Y: rrvar Ω')
(x: R): ∃ x',
pr_ge X x = pr_gt X x' ∧
pr_ge Y x = pr_gt Y x'.
End convert.
Definition eq_dist {A B: countType} {C: eqType} {Ω1: distrib A} {Ω2: distrib B}
(X: rvar Ω1 C) (Y: rvar Ω2 C) := ∀ x, pr_eq X x = pr_eq Y x.
Lemma eq_dist_ext {A: countType} {B: eqType} {Ω: distrib A} (X Y: rvar Ω B) :
(∀ x: A, X x = Y x) →
eq_dist X Y.
Lemma eq_dist_refl {A: countType} {C: eqType} {Ω: distrib A} (X: rvar Ω C) :
eq_dist X X.
Lemma eq_dist_sym {A B: countType} {C: eqType} {Ω: distrib A} {Ω': distrib B}
(X: rvar Ω C) (Y: rvar Ω' C) :
eq_dist X Y → eq_dist Y X.
Lemma eq_dist_trans {A B C: countType} (D: eqType) {ΩA: distrib A} {ΩB: distrib B} {ΩC: distrib C}
(X: rvar ΩA D) (Y: rvar ΩB D) (Z: rvar ΩC D) :
eq_dist X Y → eq_dist Y Z → eq_dist X Z.
Global Instance eq_dist_Reflexive {A} {B} {Ω}: Reflexive (@eq_dist A A B Ω Ω).
Lemma eq_dist_comp {A1 A2: finType} {B C: eqType} {Ω1: distrib A1} {Ω2: distrib A2}
(X1: rvar Ω1 B) (X2: rvar Ω2 B) (f: B → C) :
eq_dist X1 X2 → eq_dist (rvar_comp X1 f) (rvar_comp X2 f).
Lemma big_mkcond_sumbool
: ∀ (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) (r : seq I) (Q S: I → Prop)
(P : ∀ i, {Q i} + {S i}) (F : I → R),
\big[op/idx]_(i <- r | is_left (P i)) F i = \big[op/idx]_(i <- r) (if P i then F i else idx).
Lemma eq_dist_pr_ge {A B: finType} {Ω: distrib A} {Ω': distrib B} (X: rrvar Ω)
(Y: rrvar Ω'):
eq_dist X Y ↔ (∀ x, pr_ge X x = pr_ge Y x).
Lemma eq_dist_pr_gt {A B: finType} {Ω: distrib A} {Ω': distrib B}
(X: rrvar Ω) (Y: rrvar Ω'):
eq_dist X Y ↔ (∀ x, pr_gt X x = pr_gt Y x).
Module eq_dist_Ex.
Section eq_dist_Ex.
Variable (A1 A2: countType).
Variable (B: eqType).
Variable (Ω1: distrib A1).
Variable (Ω2: distrib A2).
Variable (X1: rvar Ω1 B).
Variable (X2: rvar Ω2 B).
Variable (f: B → R).
Variable (EQDIST: eq_dist X1 X2).
Variable (EX: ex_Ex (rvar_comp X1 f)).
Definition a := countable_sum (λ r: imgT X1, pr_eq X1 (sval r) × f (sval r)).
Definition a' :=
λ n, match n with
| O ⇒ 0
| S n' ⇒ countable_sum (λ r : imgT X1, pr_eq X1 (sval r) × f (sval r)) n'
end.
Definition σ := λ n,
match @pickle_inv [countType of imgT X2] n with
| None ⇒ O
| Some yb ⇒
match Rgt_dec (pr_eq X1 (sval yb)) 0 with
| left Hpf ⇒ S (@pickle [countType of imgT X1] (exist _ (sval yb) (pr_img _ _ Hpf)))
| _ ⇒ O
end
end.
Lemma σinj: ∀ n n', a' (σ n) ≠ 0 → σ n = σ n' → n = n'.
Lemma σcov: ∀ n, a' n ≠ 0 → ∃ m, σ m = n.
Lemma ex_Ex_alt:
ex_series (Rabs \o a').
Lemma rearrange:
ex_series (λ n, Rabs (a' (σ n))) ∧
is_series (λ n, a' (σ n)) (Series a').
Lemma a'_equal_ex_X1:
Ex (rvar_comp X1 f) = Series a'.
Lemma ex_Ex_eq_dist:
ex_Ex (rvar_comp X2 f).
Lemma Ex_eq_dist:
Ex (rvar_comp X1 f) = Ex (rvar_comp X2 f).
End eq_dist_Ex.
End eq_dist_Ex.
Definition ex_Ex_eq_dist := eq_dist_Ex.ex_Ex_eq_dist.
Definition Ex_eq_dist := eq_dist_Ex.Ex_eq_dist.
Lemma Ex_eq_dist_fin {A: finType} {B: countType}
{Ω: distrib A} {Ω': distrib B} (X: rrvar Ω) (Y: rrvar Ω'):
eq_dist X Y → Ex X = Ex Y.
From discprob.prob Require Import prob countable finite.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
From mathcomp Require Import tuple finfun bigop prime binomial finset.
Require Import Reals Fourier FunctionalExtensionality Psatz.
Require Import Coq.omega.Omega.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.
Notation "x ≤ y" := (Rle x y) (at level 70, no associativity).
Notation "x ≥ y" := (Rge x y) (at level 70, no associativity).
Lemma Finite_inj x y: Finite x = Finite y → x = y.
Lemma big_cons_Rplus:
∀ (I : Type)
(i : I) (r : seq I) (P : pred I) (F : I → R)
(x:=\big[Rplus/0]_(j <- r | P j) F j),
\big[Rplus/0]_(j <- (i :: r) | P j) F j = (if P i then (F i) else 0) + x.
Lemma Rlt_not_eq': ∀ r1 r2, r1 < r2 → r2 ≠ r1.
Lemma if_sumbool_case_match {A: Type} P Q (b: {P} + {¬ P}) (b': {Q} + {¬ Q}) (x y: A):
(P ↔ Q) → (if b then x else y) = (if b' then x else y).
Lemma pr_sum_restrict {A: finType} (Ω: distrib A) (X: rrvar Ω) l P:
\big[Rplus/0]_(i <- l | P i) pr_eq X i =
\big[Rplus/0]_(i <- l | P i && (Rgt_dec (pr_eq X i) 0)) pr_eq X i.
Section pr_gt.
Definition pr_gt_indicator {A} {Ω: distrib A} (T: rrvar Ω) r :=
indicator T (λ n, Rgt_dec n r).
Lemma pr_gt_to_indicator {A} {Ω: distrib A} (T: rrvar Ω) r:
pr (rvar_dist T) (λ n, Rgt_dec (T n) r) = pr_eq (pr_gt_indicator T r) 1.
Variable A: finType.
Variable Ω: distrib A.
Variable T: rrvar Ω.
Lemma pr_gt_alt r: pr (rvar_dist T) (λ a, Rgt_dec (T a) r)
= \big[Rplus/0]_(v : imgT T) if (Rgt_dec (sval v) r) then pr_eq T (sval v) else 0.
Lemma pr_gt_alt3 r: pr (rvar_dist T) (λ n, Rgt_dec (T n) r) =
\big[Rplus/0]_(i <- filter (λ x, Rgt_dec (sval x) r)
(Finite.enum [finType of imgT T])) (pr_eq T (sval i)).
End pr_gt.
Lemma pr_gt_alt_comp {A: finType} {B: eqType} {Ω: distrib A} (T: rvar Ω B) (f: B → R) r:
pr (rvar_dist (rvar_comp T f)) (λ n, Rgt_dec ((rvar_comp T f) n) r)
= \big[Rplus/0]_(v : imgT T) if (Rgt_dec (f (sval v)) r) then pr_eq T (sval v) else 0.
Section pr_ge.
Definition pr_ge_indicator {A} {Ω: distrib A} (T: rrvar Ω) r :=
indicator T (λ n, Rge_dec n r).
Lemma pr_ge_to_indicator {A} {Ω: distrib A} (T: rrvar Ω) r:
pr (rvar_dist T) (λ n, Rge_dec (T n) r) = pr_eq (pr_ge_indicator T r) 1.
Variable A: finType.
Variable Ω: distrib A.
Variable T: rrvar Ω.
Lemma pr_ge_alt r: pr (rvar_dist T) (λ a, Rge_dec (T a) r)
= \big[Rplus/0]_(v : imgT T) if (Rge_dec (sval v) r) then pr_eq T (sval v) else 0.
Lemma pr_ge_alt3 r: pr (rvar_dist T) (λ n, Rge_dec (T n) r) =
\big[Rplus/0]_(i <- filter (λ x, Rge_dec (sval x) r)
(Finite.enum [finType of imgT T])) (pr_eq T (sval i)).
End pr_ge.
Lemma pr_ge_alt_comp {A: finType} {B: eqType} {Ω: distrib A} (T: rvar Ω B) (f: B → R) r:
pr (rvar_dist (rvar_comp T f)) (λ n, Rge_dec ((rvar_comp T f) n) r)
= \big[Rplus/0]_(v : imgT T) if (Rge_dec (f (sval v)) r) then pr_eq T (sval v) else 0.
Section pr_eq.
Definition pr_eq_indicator {A} {B: eqType} {Ω: distrib A} (T: rvar Ω B) r :=
indicator T (λ n, n == r).
Lemma pr_eq_to_indicator {A} {B} {Ω: distrib A} (T: rvar Ω B) r:
pr (rvar_dist T) (λ n, (T n) == r) = pr_eq (pr_eq_indicator T r) 1.
Variable A: finType.
Variable B: eqType.
Variable Ω: distrib A.
Variable T: rvar Ω B.
Lemma pr_eq_alt r: pr (rvar_dist T) (λ a, (T a) == r)
= \big[Rplus/0]_(v : imgT T) if (sval v == r) then pr_eq T (sval v) else 0.
End pr_eq.
Lemma pr_eq_alt_comp {A: finType} {B C: eqType} {Ω: distrib A} (T: rvar Ω B) (f: B → C) r:
pr (rvar_dist (rvar_comp T f)) (λ n, (rvar_comp T f) n == r)
= \big[Rplus/0]_(v : imgT T) if (f (sval v) == r) then pr_eq T (sval v) else 0.
Section convert.
Lemma pr_gt_to_geq_eps {A: finType} {Ω: distrib A} (X: rrvar Ω) (x eps: R):
(eps > 0 ∧ ∀ y, y \in img X → y ≠ x → Rabs (x - y) ≥ eps) →
pr_gt X x = pr_ge X (x + eps/2).
Lemma pr_ge_to_gt_eps {A: finType} {Ω: distrib A} (X: rrvar Ω) (x eps: R):
(eps > 0 ∧ ∀ y, y \in img X → y ≠ x → Rabs (x - y) ≥ eps) →
pr_ge X x = pr_gt X (x - eps/2).
Lemma pr_ge_split_eps {A: finType} {Ω: distrib A} (X: rrvar Ω) (x eps: R):
(eps > 0 ∧ ∀ y, y \in img X → y ≠ x → Rabs (x - y) ≥ eps) →
pr_eq X x = pr_ge X (x - eps/2) - pr_ge X (x + eps/2).
Lemma Rmin_dist_list (l: seq R) (x: R):
∃ eps, eps > 0 ∧ ∀ y, y \in l → y ≠ x → Rabs (x - y) ≥ eps.
Lemma pr_ge_split2 {A B: finType} {Ω: distrib A} {Ω': distrib B} (X: rrvar Ω) (Y: rrvar Ω')
(x: R): ∃ x1 x2,
pr_eq X x = pr_ge X x1 - pr_ge X x2 ∧
pr_eq Y x = pr_ge Y x1 - pr_ge Y x2.
Lemma pr_gt_to_geq2 {A B: finType} {Ω: distrib A} {Ω': distrib B} (X: rrvar Ω) (Y: rrvar Ω')
(x: R): ∃ x',
pr_gt X x = pr_ge X x' ∧
pr_gt Y x = pr_ge Y x'.
Lemma pr_ge_to_gt2 {A B: finType} {Ω: distrib A} {Ω': distrib B} (X: rrvar Ω) (Y: rrvar Ω')
(x: R): ∃ x',
pr_ge X x = pr_gt X x' ∧
pr_ge Y x = pr_gt Y x'.
End convert.
Definition eq_dist {A B: countType} {C: eqType} {Ω1: distrib A} {Ω2: distrib B}
(X: rvar Ω1 C) (Y: rvar Ω2 C) := ∀ x, pr_eq X x = pr_eq Y x.
Lemma eq_dist_ext {A: countType} {B: eqType} {Ω: distrib A} (X Y: rvar Ω B) :
(∀ x: A, X x = Y x) →
eq_dist X Y.
Lemma eq_dist_refl {A: countType} {C: eqType} {Ω: distrib A} (X: rvar Ω C) :
eq_dist X X.
Lemma eq_dist_sym {A B: countType} {C: eqType} {Ω: distrib A} {Ω': distrib B}
(X: rvar Ω C) (Y: rvar Ω' C) :
eq_dist X Y → eq_dist Y X.
Lemma eq_dist_trans {A B C: countType} (D: eqType) {ΩA: distrib A} {ΩB: distrib B} {ΩC: distrib C}
(X: rvar ΩA D) (Y: rvar ΩB D) (Z: rvar ΩC D) :
eq_dist X Y → eq_dist Y Z → eq_dist X Z.
Global Instance eq_dist_Reflexive {A} {B} {Ω}: Reflexive (@eq_dist A A B Ω Ω).
Lemma eq_dist_comp {A1 A2: finType} {B C: eqType} {Ω1: distrib A1} {Ω2: distrib A2}
(X1: rvar Ω1 B) (X2: rvar Ω2 B) (f: B → C) :
eq_dist X1 X2 → eq_dist (rvar_comp X1 f) (rvar_comp X2 f).
Lemma big_mkcond_sumbool
: ∀ (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) (r : seq I) (Q S: I → Prop)
(P : ∀ i, {Q i} + {S i}) (F : I → R),
\big[op/idx]_(i <- r | is_left (P i)) F i = \big[op/idx]_(i <- r) (if P i then F i else idx).
Lemma eq_dist_pr_ge {A B: finType} {Ω: distrib A} {Ω': distrib B} (X: rrvar Ω)
(Y: rrvar Ω'):
eq_dist X Y ↔ (∀ x, pr_ge X x = pr_ge Y x).
Lemma eq_dist_pr_gt {A B: finType} {Ω: distrib A} {Ω': distrib B}
(X: rrvar Ω) (Y: rrvar Ω'):
eq_dist X Y ↔ (∀ x, pr_gt X x = pr_gt Y x).
Module eq_dist_Ex.
Section eq_dist_Ex.
Variable (A1 A2: countType).
Variable (B: eqType).
Variable (Ω1: distrib A1).
Variable (Ω2: distrib A2).
Variable (X1: rvar Ω1 B).
Variable (X2: rvar Ω2 B).
Variable (f: B → R).
Variable (EQDIST: eq_dist X1 X2).
Variable (EX: ex_Ex (rvar_comp X1 f)).
Definition a := countable_sum (λ r: imgT X1, pr_eq X1 (sval r) × f (sval r)).
Definition a' :=
λ n, match n with
| O ⇒ 0
| S n' ⇒ countable_sum (λ r : imgT X1, pr_eq X1 (sval r) × f (sval r)) n'
end.
Definition σ := λ n,
match @pickle_inv [countType of imgT X2] n with
| None ⇒ O
| Some yb ⇒
match Rgt_dec (pr_eq X1 (sval yb)) 0 with
| left Hpf ⇒ S (@pickle [countType of imgT X1] (exist _ (sval yb) (pr_img _ _ Hpf)))
| _ ⇒ O
end
end.
Lemma σinj: ∀ n n', a' (σ n) ≠ 0 → σ n = σ n' → n = n'.
Lemma σcov: ∀ n, a' n ≠ 0 → ∃ m, σ m = n.
Lemma ex_Ex_alt:
ex_series (Rabs \o a').
Lemma rearrange:
ex_series (λ n, Rabs (a' (σ n))) ∧
is_series (λ n, a' (σ n)) (Series a').
Lemma a'_equal_ex_X1:
Ex (rvar_comp X1 f) = Series a'.
Lemma ex_Ex_eq_dist:
ex_Ex (rvar_comp X2 f).
Lemma Ex_eq_dist:
Ex (rvar_comp X1 f) = Ex (rvar_comp X2 f).
End eq_dist_Ex.
End eq_dist_Ex.
Definition ex_Ex_eq_dist := eq_dist_Ex.ex_Ex_eq_dist.
Definition Ex_eq_dist := eq_dist_Ex.Ex_eq_dist.
Lemma Ex_eq_dist_fin {A: finType} {B: countType}
{Ω: distrib A} {Ω': distrib B} (X: rrvar Ω) (Y: rrvar Ω'):
eq_dist X Y → Ex X = Ex Y.