Library discprob.basic.bigop_ext
From discprob.basic Require Import base nify order seq_ext.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop seq.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.
Require Import Reals Psatz Omega.
Section RAddLaw.
Import Monoid.
Lemma Rplus_associative: associative Rplus.
Lemma Rplus_left_id: left_id R0 Rplus.
Lemma Rplus_right_id: right_id R0 Rplus.
Lemma Rplus_commutative: commutative Rplus.
Lemma Rplus_left_distributive: left_distributive Rmult Rplus.
Lemma Rplus_right_distributive: right_distributive Rmult Rplus.
Lemma Rmult_left_zero: left_zero 0 Rmult.
Lemma Rmult_right_zero: right_zero 0 Rmult.
Canonical Rplus_monoid := Law Rplus_associative Rplus_left_id Rplus_right_id.
Canonical Rplus_comoid := ComLaw Rplus_commutative.
Canonical Rplus_addoid := AddLaw Rplus_left_distributive Rplus_right_distributive.
Canonical Rmult_muloid := MulLaw Rmult_left_zero Rmult_right_zero.
End RAddLaw.
Section sum_reidx.
Local Open Scope R_scope.
Lemma inj_neq {X Y: eqType} (h: X → Y) a b: injective h → a != b → h a != h b.
Lemma sum_reidx_map {A B: eqType} (p: seq A) (q: seq B) P Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a = F' (h a)) →
(∀ a, a \in p → P a = true → (h a) \in q ∧ Q (h a) = true ) →
(∀ b, b \in q → Q b → ¬ (∃ a, a \in p ∧ P a = true ∧ h a = b) → F' b = 0) →
uniq p → uniq q → (∀ x x', P x → h x = h x' → x = x') →
\big[Rplus/0]_(i <- p | P i) (F i) =
\big[Rplus/0]_(i <- q | Q i) (F' i).
Lemma sum_reidx_map_le {A B: eqType} (p: seq A) (q: seq B) P Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a ≤ F' (h a)) →
(∀ a, a \in p → P a = true → (h a) \in q ∧ Q (h a) = true ) →
(∀ b, b \in q → Q b → ¬ (∃ a, a \in p ∧ P a = true ∧ h a = b) → F' b ≥ 0) →
uniq p → uniq q → (∀ x x', P x → h x = h x' → x = x') →
\big[Rplus/0]_(i <- p | P i) (F i) ≤
\big[Rplus/0]_(i <- q | Q i) (F' i).
Variable A B : eqType.
Lemma sum_reidx_map_sym (p: seq A) (q: seq B) (P: A → bool) Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a = F' (h a)) →
(∀ a, a \in p → P a → (¬ (h a \in q ∧ Q (h a) = true)) → F a = 0) →
(∀ b, b \in q → Q b → ¬ (∃ a, a \in p ∧ P a = true ∧ h a = b) → F' b = 0) →
uniq p → uniq q → injective h →
\big[Rplus/0]_(i <- p | P i) (F i) =
\big[Rplus/0]_(i <- q | Q i) (F' i).
Lemma sum_reidx_surj1 (p: seq A) (q: seq B) P Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a = F' (h a)) →
(∀ a, a \in p → P a = true → (h a) \in q ∧ Q (h a) = true ) →
(∀ b, b \in q → Q b → ∃ a, a \in p ∧ P a = true ∧ h a = b) →
uniq p → uniq q → injective h →
\big[Rplus/0]_(i <- p | P i) (F i) =
\big[Rplus/0]_(i <- q | Q i) (F' i).
Lemma sum_reidx_surj2 (p: seq A) (q: seq B) P Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a = F' (h a)) →
(∀ a, a \in p → P a = true → (h a) \in q ∧ Q (h a) = true ) →
(∀ b, b \in q → Q b → has (fun a ⇒ P a && (h a == b)) p) →
uniq p → uniq q → injective h →
\big[Rplus/0]_(i <- p | P i) (F i) =
\big[Rplus/0]_(i <- q | Q i) (F' i).
End sum_reidx.
Lemma Rabs_bigop_triang {A} (f: A → R) (p: seq A) (P: pred A):
Rabs (\big[Rplus/0]_(i <- p | P i) (f i)) ≤ \big[Rplus/0]_(i <- p | P i) (Rabs (f i)).
Lemma bigop_cond_non0 {A} (f: A → R) (p: seq A) P:
\big[Rplus/0]_(i <- p | P i) (f i) =
\big[Rplus/0]_(i <- p | P i && (f i != 0)) (f i).
Lemma Rabs_bigop_filter {A} (f: A → R) (p: seq A) (P Q: pred A):
(∀ a, P a → Q a) →
\big[Rplus/0]_(i <- p | P i) (Rabs (f i)) ≤ \big[Rplus/0]_(i <- p | Q i) (Rabs (f i)).
Lemma sum_n_bigop (f: nat → R) n:
sum_n f n = \big[Rplus/0]_(i < S n) (f i).
Lemma sum_n_m_bigop (f: nat → R) n m:
sum_n_m f n m = \big[Rplus/0]_(n ≤ i < S m) (f i).
Lemma Rle_bigr {A} (f1 f2: A → R) (p: seq A) (P: pred A):
(∀ i, P i → f1 i ≤ f2 i) →
(\big[Rplus/0]_(i <- p | P i) (f1 i)) ≤ \big[Rplus/0]_(i <- p | P i) f2 i.
Lemma Rle_bigr' {A} (f1 f2: A → R) (p: seq A) (P Q: pred A):
(∀ i, P i → (Q i) ∧ f1 i ≤ f2 i) →
(∀ i, ¬ P i → Q i → 0 ≤ f2 i) →
(\big[Rplus/0]_(i <- p | P i) (f1 i)) ≤ \big[Rplus/0]_(i <- p | Q i) f2 i.
Lemma Rle_big0 {A} (f: A → R) (p: seq A) (P: pred A):
(∀ i, P i → 0 ≤ f i) →
0 ≤ \big[Rplus/0]_(i <- p | P i) f i.
Lemma Rle_big0_In {A} (f: A → R) (p: seq A) (P: pred A):
(∀ i, P i → List.In i p → 0 ≤ f i) →
0 ≤ \big[Rplus/0]_(i <- p | P i) f i.
Lemma Rlt_big_inv {A: eqType} (f g: A → R) (p: seq A) (P: pred A):
\big[Rplus/0]_(i <- p | P i) f i < \big[Rplus/0]_(i <- p | P i) g i →
∃ i, (i \in p) ∧ P i ∧ f i < g i.
Lemma Rlt_bigr {A: eqType} (f1 f2: A → R) (p: seq A) (P: pred A):
(∀ i, P i → f1 i ≤ f2 i) →
(∃ i, (i \in p) ∧ P i ∧ f1 i < f2 i) →
(\big[Rplus/0]_(i <- p | P i) (f1 i)) < \big[Rplus/0]_(i <- p | P i) f2 i.
Lemma Rlt_0_bigr {A: eqType} (f: A → R) (p: seq A) (P: pred A):
(∀ i, P i → 0 ≤ f i) →
(∃ i, (i \in p) ∧ P i ∧ 0 < f i) →
0 < \big[Rplus/0]_(i <- p | P i) f i.
Lemma Rlt_0_big_inv {A: eqType} (f: A → R) (p: seq A) (P: pred A):
0 < \big[Rplus/0]_(i <- p | P i) f i →
(∃ i, (i \in p) ∧ P i ∧ 0 < f i).
Lemma big_INR {A: finType} F:
(\big[Rplus/0]_(i : A) INR (F i) = INR (\sum_(i : A) (F i))).
Lemma Rmax_INR a b: Rmax (INR a) (INR b) = INR (max a b).
From mathcomp Require Import ssrnat.
Lemma sum_index_ordinal_P_aux {A} (f: A → R) (l: seq A) r P P':
(∀ i, (i < size l)%nat → P i = P' (nth r l i)) →
\big[Rplus/0%R]_(a in 'I_(size l) | P a) nth 0 [seq (f i) | i <- l] a =
\big[Rplus/0%R]_(a<-l | P' a) (f a).
Lemma sum_index_ordinal_P {A} (f: A → R) (l: seq (A)) r (P: 'I_(size l) → bool) P':
(∀ i, P i = P' (nth r l i)) →
\big[Rplus/0%R]_(a in 'I_(size l) | P a) nth 0 [seq (f i) | i <- l] a =
\big[Rplus/0%R]_(a<-l | P' a) (f a).
Lemma sum_index_ordinal {A: eqType} f (l: seq A):
\big[Rplus/0]_(a in 'I_(size l)) nth 0 [seq (f i) | i <- l] a =
\big[Rplus/0]_(a<-[seq (f i) | i <- l]) a.
Lemma sum_index_ordinal_F {A: eqType} (l: seq (R × A)) F:
\big[Rplus/0]_(a in 'I_(size l)) F (nth 0 [seq i.1 | i <- l] a) =
\big[Rplus/0]_(a<-[seq i.1 | i <- l]) F a.
Lemma big_Rplus_allpair {A B: Type} (l1: seq A) (l2: seq B) F:
\big[Rplus/0]_(i <- [seq (x1, x2) | x1 <- l1, x2 <- l2]) F i =
\big[Rplus/0]_(i1 <- l1) \big[Rplus/0]_(i2 <- l2) F (i1, i2).
Lemma big_Rplus_allpair' {A B: eqType} P Q (l1: seq {x: A | P x}) (l2: seq {x: B | Q x}) F:
\big[Rplus/0]_(i <- [seq (sval x1, sval x2) | x1 <- l1, x2 <- l2]) F i =
\big[Rplus/0]_(i1 <- l1) \big[Rplus/0]_(i2 <- l2) F (sval i1, sval i2).
Lemma big1_In: ∀ (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) (l : list I)
(P : pred I) (F : I → R) (Heq0: ∀ i : I, P i → List.In i l → F i = idx),
\big[op/idx]_(i <- l | P i) F i = idx.
Lemma eq_bigr_In: ∀ (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) (l : list I)
(P : pred I) (F F': I → R) (Heq: ∀ i : I, P i → List.In i l → F i = F' i),
\big[op/idx]_(i <- l | P i) F i =
\big[op/idx]_(i <- l | P i) F' i.
Lemma sum_nS {G: AbelianGroup} :
∀ (a : nat → G) (n : nat),
sum_n a n.+1 = plus (a O) (sum_n (λ n, a (S n)) n).
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop seq.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.
Require Import Reals Psatz Omega.
Section RAddLaw.
Import Monoid.
Lemma Rplus_associative: associative Rplus.
Lemma Rplus_left_id: left_id R0 Rplus.
Lemma Rplus_right_id: right_id R0 Rplus.
Lemma Rplus_commutative: commutative Rplus.
Lemma Rplus_left_distributive: left_distributive Rmult Rplus.
Lemma Rplus_right_distributive: right_distributive Rmult Rplus.
Lemma Rmult_left_zero: left_zero 0 Rmult.
Lemma Rmult_right_zero: right_zero 0 Rmult.
Canonical Rplus_monoid := Law Rplus_associative Rplus_left_id Rplus_right_id.
Canonical Rplus_comoid := ComLaw Rplus_commutative.
Canonical Rplus_addoid := AddLaw Rplus_left_distributive Rplus_right_distributive.
Canonical Rmult_muloid := MulLaw Rmult_left_zero Rmult_right_zero.
End RAddLaw.
Section sum_reidx.
Local Open Scope R_scope.
Lemma inj_neq {X Y: eqType} (h: X → Y) a b: injective h → a != b → h a != h b.
Lemma sum_reidx_map {A B: eqType} (p: seq A) (q: seq B) P Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a = F' (h a)) →
(∀ a, a \in p → P a = true → (h a) \in q ∧ Q (h a) = true ) →
(∀ b, b \in q → Q b → ¬ (∃ a, a \in p ∧ P a = true ∧ h a = b) → F' b = 0) →
uniq p → uniq q → (∀ x x', P x → h x = h x' → x = x') →
\big[Rplus/0]_(i <- p | P i) (F i) =
\big[Rplus/0]_(i <- q | Q i) (F' i).
Lemma sum_reidx_map_le {A B: eqType} (p: seq A) (q: seq B) P Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a ≤ F' (h a)) →
(∀ a, a \in p → P a = true → (h a) \in q ∧ Q (h a) = true ) →
(∀ b, b \in q → Q b → ¬ (∃ a, a \in p ∧ P a = true ∧ h a = b) → F' b ≥ 0) →
uniq p → uniq q → (∀ x x', P x → h x = h x' → x = x') →
\big[Rplus/0]_(i <- p | P i) (F i) ≤
\big[Rplus/0]_(i <- q | Q i) (F' i).
Variable A B : eqType.
Lemma sum_reidx_map_sym (p: seq A) (q: seq B) (P: A → bool) Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a = F' (h a)) →
(∀ a, a \in p → P a → (¬ (h a \in q ∧ Q (h a) = true)) → F a = 0) →
(∀ b, b \in q → Q b → ¬ (∃ a, a \in p ∧ P a = true ∧ h a = b) → F' b = 0) →
uniq p → uniq q → injective h →
\big[Rplus/0]_(i <- p | P i) (F i) =
\big[Rplus/0]_(i <- q | Q i) (F' i).
Lemma sum_reidx_surj1 (p: seq A) (q: seq B) P Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a = F' (h a)) →
(∀ a, a \in p → P a = true → (h a) \in q ∧ Q (h a) = true ) →
(∀ b, b \in q → Q b → ∃ a, a \in p ∧ P a = true ∧ h a = b) →
uniq p → uniq q → injective h →
\big[Rplus/0]_(i <- p | P i) (F i) =
\big[Rplus/0]_(i <- q | Q i) (F' i).
Lemma sum_reidx_surj2 (p: seq A) (q: seq B) P Q (h : A → B) (F: A → R) (F': B → R) :
(∀ a, a \in p → F a = F' (h a)) →
(∀ a, a \in p → P a = true → (h a) \in q ∧ Q (h a) = true ) →
(∀ b, b \in q → Q b → has (fun a ⇒ P a && (h a == b)) p) →
uniq p → uniq q → injective h →
\big[Rplus/0]_(i <- p | P i) (F i) =
\big[Rplus/0]_(i <- q | Q i) (F' i).
End sum_reidx.
Lemma Rabs_bigop_triang {A} (f: A → R) (p: seq A) (P: pred A):
Rabs (\big[Rplus/0]_(i <- p | P i) (f i)) ≤ \big[Rplus/0]_(i <- p | P i) (Rabs (f i)).
Lemma bigop_cond_non0 {A} (f: A → R) (p: seq A) P:
\big[Rplus/0]_(i <- p | P i) (f i) =
\big[Rplus/0]_(i <- p | P i && (f i != 0)) (f i).
Lemma Rabs_bigop_filter {A} (f: A → R) (p: seq A) (P Q: pred A):
(∀ a, P a → Q a) →
\big[Rplus/0]_(i <- p | P i) (Rabs (f i)) ≤ \big[Rplus/0]_(i <- p | Q i) (Rabs (f i)).
Lemma sum_n_bigop (f: nat → R) n:
sum_n f n = \big[Rplus/0]_(i < S n) (f i).
Lemma sum_n_m_bigop (f: nat → R) n m:
sum_n_m f n m = \big[Rplus/0]_(n ≤ i < S m) (f i).
Lemma Rle_bigr {A} (f1 f2: A → R) (p: seq A) (P: pred A):
(∀ i, P i → f1 i ≤ f2 i) →
(\big[Rplus/0]_(i <- p | P i) (f1 i)) ≤ \big[Rplus/0]_(i <- p | P i) f2 i.
Lemma Rle_bigr' {A} (f1 f2: A → R) (p: seq A) (P Q: pred A):
(∀ i, P i → (Q i) ∧ f1 i ≤ f2 i) →
(∀ i, ¬ P i → Q i → 0 ≤ f2 i) →
(\big[Rplus/0]_(i <- p | P i) (f1 i)) ≤ \big[Rplus/0]_(i <- p | Q i) f2 i.
Lemma Rle_big0 {A} (f: A → R) (p: seq A) (P: pred A):
(∀ i, P i → 0 ≤ f i) →
0 ≤ \big[Rplus/0]_(i <- p | P i) f i.
Lemma Rle_big0_In {A} (f: A → R) (p: seq A) (P: pred A):
(∀ i, P i → List.In i p → 0 ≤ f i) →
0 ≤ \big[Rplus/0]_(i <- p | P i) f i.
Lemma Rlt_big_inv {A: eqType} (f g: A → R) (p: seq A) (P: pred A):
\big[Rplus/0]_(i <- p | P i) f i < \big[Rplus/0]_(i <- p | P i) g i →
∃ i, (i \in p) ∧ P i ∧ f i < g i.
Lemma Rlt_bigr {A: eqType} (f1 f2: A → R) (p: seq A) (P: pred A):
(∀ i, P i → f1 i ≤ f2 i) →
(∃ i, (i \in p) ∧ P i ∧ f1 i < f2 i) →
(\big[Rplus/0]_(i <- p | P i) (f1 i)) < \big[Rplus/0]_(i <- p | P i) f2 i.
Lemma Rlt_0_bigr {A: eqType} (f: A → R) (p: seq A) (P: pred A):
(∀ i, P i → 0 ≤ f i) →
(∃ i, (i \in p) ∧ P i ∧ 0 < f i) →
0 < \big[Rplus/0]_(i <- p | P i) f i.
Lemma Rlt_0_big_inv {A: eqType} (f: A → R) (p: seq A) (P: pred A):
0 < \big[Rplus/0]_(i <- p | P i) f i →
(∃ i, (i \in p) ∧ P i ∧ 0 < f i).
Lemma big_INR {A: finType} F:
(\big[Rplus/0]_(i : A) INR (F i) = INR (\sum_(i : A) (F i))).
Lemma Rmax_INR a b: Rmax (INR a) (INR b) = INR (max a b).
From mathcomp Require Import ssrnat.
Lemma sum_index_ordinal_P_aux {A} (f: A → R) (l: seq A) r P P':
(∀ i, (i < size l)%nat → P i = P' (nth r l i)) →
\big[Rplus/0%R]_(a in 'I_(size l) | P a) nth 0 [seq (f i) | i <- l] a =
\big[Rplus/0%R]_(a<-l | P' a) (f a).
Lemma sum_index_ordinal_P {A} (f: A → R) (l: seq (A)) r (P: 'I_(size l) → bool) P':
(∀ i, P i = P' (nth r l i)) →
\big[Rplus/0%R]_(a in 'I_(size l) | P a) nth 0 [seq (f i) | i <- l] a =
\big[Rplus/0%R]_(a<-l | P' a) (f a).
Lemma sum_index_ordinal {A: eqType} f (l: seq A):
\big[Rplus/0]_(a in 'I_(size l)) nth 0 [seq (f i) | i <- l] a =
\big[Rplus/0]_(a<-[seq (f i) | i <- l]) a.
Lemma sum_index_ordinal_F {A: eqType} (l: seq (R × A)) F:
\big[Rplus/0]_(a in 'I_(size l)) F (nth 0 [seq i.1 | i <- l] a) =
\big[Rplus/0]_(a<-[seq i.1 | i <- l]) F a.
Lemma big_Rplus_allpair {A B: Type} (l1: seq A) (l2: seq B) F:
\big[Rplus/0]_(i <- [seq (x1, x2) | x1 <- l1, x2 <- l2]) F i =
\big[Rplus/0]_(i1 <- l1) \big[Rplus/0]_(i2 <- l2) F (i1, i2).
Lemma big_Rplus_allpair' {A B: eqType} P Q (l1: seq {x: A | P x}) (l2: seq {x: B | Q x}) F:
\big[Rplus/0]_(i <- [seq (sval x1, sval x2) | x1 <- l1, x2 <- l2]) F i =
\big[Rplus/0]_(i1 <- l1) \big[Rplus/0]_(i2 <- l2) F (sval i1, sval i2).
Lemma big1_In: ∀ (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) (l : list I)
(P : pred I) (F : I → R) (Heq0: ∀ i : I, P i → List.In i l → F i = idx),
\big[op/idx]_(i <- l | P i) F i = idx.
Lemma eq_bigr_In: ∀ (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) (l : list I)
(P : pred I) (F F': I → R) (Heq: ∀ i : I, P i → List.In i l → F i = F' i),
\big[op/idx]_(i <- l | P i) F i =
\big[op/idx]_(i <- l | P i) F' i.
Lemma sum_nS {G: AbelianGroup} :
∀ (a : nat → G) (n : nat),
sum_n a n.+1 = plus (a O) (sum_n (λ n, a (S n)) n).