Library discprob.prob.countable
From discprob.basic Require Import base Series_Ext.
Require Import Reals Fourier Omega Psatz.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.
Definition support {X} (v: X → R) := { x : X | is_true (Rgt_dec (v x) 0) }.
Definition countable_sum {A: countType} (f: A → R) :=
λ n: nat, oapp f R0 (@pickle_inv A n).
Lemma countable_sum_ext {A: countType} (f f': A → R) n :
(∀ n, f n = f' n) → countable_sum f n = countable_sum f' n.
Lemma countable_sum_le {A: countType} (f f': A → R) n :
(∀ n, f n ≤ f' n) → countable_sum f n ≤ countable_sum f' n.
Lemma LPO_count {A: countType} (P: A → Prop):
(∀ a, P a ∨ ¬ P a) → {a : A | P a} + {(∀ a, ¬ P a)}.
Lemma LPO_countb {A: countType} (P: A → bool):
{a : A | P a} + {(∀ a, ¬ P a)}.
Definition exC {A: countType} (B: pred A) : bool := LPO_countb B.
Lemma exCP {A: countType} (B: pred A) : reflect (∃ x, B x) (exC B).
Lemma pickle_inv_some_inv {A: countType} n a':
@pickle_inv A n = Some a' →
pickle a' = n.
Lemma pickle_inv_some_inj {A: countType} n n' a':
@pickle_inv A n = Some a' →
@pickle_inv A n = @pickle_inv A n' →
n = n'.
Lemma pickle_inj {A: countType} (a a': A):
pickle a = pickle a' → a = a'.
Definition img {A: countType} {B: eqType} (f: A → B ) : pred B := λ y, exC (λ x, f x == y).
Definition imgT {A: countType} {B: eqType} (f: A → B) := {y | y \in img f}.
Definition img_pickle {A: countType} {B: eqType} (f: A → B) : { y | exC (λ x, f x == y) } → nat.
Definition img_unpickle {A: countType} {B: eqType} (f: A → B) (n: nat)
: option { y | exC (λ x, f x == y) } :=
(match unpickle n with
| Some a ⇒
Some (exist (λ y : B, exC (λ x : A, f x == y)) (f a)
(introT (exCP (λ x : A, f x == f a)) (ex_intro (λ x : A, f x == f a) a (eqxx (T:=B) (f a)))))
| None ⇒ None
end).
Lemma pickle_imgK {A: countType} {B: eqType} (f: A → B):
pcancel (img_pickle f) (img_unpickle f).
Definition img_choiceMixin {A: countType} {B: eqType} (f: A → B) :=
PcanChoiceMixin (pickle_imgK f).
Canonical img_choiceType {A: countType} {B: eqType} {f: A → B} :=
Eval hnf in ChoiceType (imgT f) (@img_choiceMixin A B f).
Definition img_countMixin {A: countType} {B: eqType} (f: A → B) :=
PcanCountMixin (pickle_imgK f).
Canonical img_countType {A: countType} {B: eqType} (f: A → B) :=
Eval hnf in CountType (imgT f) (@img_countMixin A B f).
Section countable_series_facts.
Variable (A: countType).
Implicit Types (a b: A → R).
Lemma countable_sum_scal c a:
∀ n, countable_sum (λ x, scal c (a x)) n = (λ n, scal c (countable_sum a n)) n.
Lemma is_seriesC_0 a: (∀ n, a n = 0) → is_series (countable_sum a) 0.
Lemma is_seriesC_ext a b l:
(∀ n, a n = b n) → is_series (countable_sum a) l → is_series (countable_sum b) l.
Lemma ex_seriesC_ext a b:
(∀ n, a n = b n) → ex_series (countable_sum a) → ex_series (countable_sum b).
Global Instance is_series_Proper:
Proper (pointwise_relation nat (@eq R) ==> @eq R ==> iff) is_series.
Global Instance ex_series_Proper:
Proper (pointwise_relation nat (@eq R) ==> iff) ex_series.
Global Instance Series_Proper:
Proper (pointwise_relation nat (@eq R) ==> eq) Series.
Global Instance countable_sum_Proper:
Proper (pointwise_relation A (@eq R) ==> pointwise_relation nat (@eq R)) countable_sum.
Global Instance countable_sum_Proper' {B: countType}:
Proper (pointwise_relation B (@eq R) ==> eq ==> eq) countable_sum.
Lemma is_seriesC_filter_pos a (P: pred A) (v: R):
(∀ n, a n ≥ 0) →
is_series (countable_sum a) v → ex_series (countable_sum (λ n, if P n then a n else 0)).
Lemma is_seriesC_filter_PQ a (P Q: pred A) (v: R):
(∀ n, a n ≥ 0) →
is_series (countable_sum (λ n, if P n then a n else 0)) v →
(∀ n, Q n → P n) →
ex_series (countable_sum (λ n, if Q n then a n else 0)).
Lemma ex_seriesC_filter_PQ a (P Q: pred A):
(∀ n, a n ≥ 0) →
ex_series (countable_sum (λ n, if P n then a n else 0)) →
(∀ n, Q n → P n) →
ex_series (countable_sum (λ n, if Q n then a n else 0)).
Lemma ex_seriesC_filter_P a (Q: pred A):
(∀ n, a n ≥ 0) →
ex_series (countable_sum a) →
ex_series (countable_sum (λ n, if Q n then a n else 0)).
Lemma is_seriesC_filter_split a (P: pred A) (v: R):
(∀ n, a n ≥ 0) →
is_series (countable_sum a) v →
Series (countable_sum (λ n, if P n then a n else 0)) +
Series (countable_sum (λ n, if ~~ P n then a n else 0)) = v.
Lemma is_seriesC_filter_union a (P Q: pred A) (v: R):
(∀ n, a n ≥ 0) →
is_series (countable_sum (λ n, if P n || Q n then a n else 0)) v →
Series (countable_sum (λ n, if P n then a n else 0)) +
Series (countable_sum (λ n, if Q n then a n else 0))
- Series (countable_sum (λ n, if P n && Q n then a n else 0)) = v.
Lemma SeriesC_ext a b:
(∀ n, a n = b n) →
Series (countable_sum a) = Series (countable_sum b).
Lemma SeriesC_le a b:
(∀ n, 0 ≤ a n ≤ b n) → ex_series (countable_sum b) →
Series (countable_sum a) ≤ Series (countable_sum b).
Lemma SeriesC_le' a b:
(∀ n, a n ≤ b n) →
ex_series (countable_sum a) → ex_series (countable_sum b) →
Series (countable_sum a) ≤ Series (countable_sum b).
Lemma countable_sum_plus a b:
∀ n, (countable_sum (λ x, a x + b x) n = (λ n, countable_sum a n + countable_sum b n) n).
Lemma countable_sum_Rabs a:
∀ n, (countable_sum (λ x, Rabs (a x)) n) = (λ n, Rabs (countable_sum a n)) n.
Lemma ex_seriesC_le a b:
(∀ n, 0 ≤ a n ≤ b n) → ex_series (countable_sum b) →
ex_series (countable_sum a).
Lemma countable_sum_scal_l c a:
∀ n, (countable_sum (λ x, c × a x) n = (λ n, c × (countable_sum a n)) n).
Lemma countable_sum_scal_r c a:
∀ n, (countable_sum (λ x, a x × c) n = (λ n, (countable_sum a n) × c) n).
Lemma SeriesC_scal_l (c : R) a:
Series (λ n, countable_sum (λ x, c × a x) n) = c × Series (countable_sum a).
Lemma SeriesC_scal_r (c : R) a:
Series (λ n, countable_sum (λ x, a x × c) n) = Series (countable_sum a) × c.
Lemma ex_seriesC_scal_l (c : R) a:
ex_series (countable_sum a) →
ex_series (countable_sum (λ x, c × a x)).
Lemma ex_seriesC_scal_r (c : R) a:
ex_series (countable_sum a) →
ex_series (countable_sum (λ x, a x × c)).
Lemma ex_seriesC_plus a b:
ex_series (countable_sum a) →
ex_series (countable_sum b) →
ex_series (countable_sum (λ x, a x + b x)).
Lemma is_seriesC_scal_l (c : R) a v:
is_series (countable_sum a) v →
is_series (countable_sum (λ x, c × a x)) (c × v).
Lemma is_seriesC_scal_r (c : R) a v:
is_series (countable_sum a) v →
is_series (countable_sum (λ x, a x × c)) (v × c).
Lemma is_seriesC_plus a b v1 v2:
is_series (countable_sum a) v1 →
is_series (countable_sum b) v2 →
is_series (countable_sum (λ x, a x + b x)) (v1 + v2).
Lemma is_seriesC_bump (x' : A) v:
is_series (countable_sum (λ x, if x == x' then v else 0)) v.
Lemma ex_seriesC_Rabs a:
ex_series (countable_sum (λ x, Rabs (a x))) →
ex_series (countable_sum a).
Lemma SeriesC_bump (x' : A) v:
Series (countable_sum (λ x, if x == x' then v else 0)) = v.
Lemma SeriesC_0 a:
(∀ x, a x = 0) →
Series (countable_sum a) = 0.
End countable_series_facts.
Require Import Reals Fourier Omega Psatz.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.
Definition support {X} (v: X → R) := { x : X | is_true (Rgt_dec (v x) 0) }.
Definition countable_sum {A: countType} (f: A → R) :=
λ n: nat, oapp f R0 (@pickle_inv A n).
Lemma countable_sum_ext {A: countType} (f f': A → R) n :
(∀ n, f n = f' n) → countable_sum f n = countable_sum f' n.
Lemma countable_sum_le {A: countType} (f f': A → R) n :
(∀ n, f n ≤ f' n) → countable_sum f n ≤ countable_sum f' n.
Lemma LPO_count {A: countType} (P: A → Prop):
(∀ a, P a ∨ ¬ P a) → {a : A | P a} + {(∀ a, ¬ P a)}.
Lemma LPO_countb {A: countType} (P: A → bool):
{a : A | P a} + {(∀ a, ¬ P a)}.
Definition exC {A: countType} (B: pred A) : bool := LPO_countb B.
Lemma exCP {A: countType} (B: pred A) : reflect (∃ x, B x) (exC B).
Lemma pickle_inv_some_inv {A: countType} n a':
@pickle_inv A n = Some a' →
pickle a' = n.
Lemma pickle_inv_some_inj {A: countType} n n' a':
@pickle_inv A n = Some a' →
@pickle_inv A n = @pickle_inv A n' →
n = n'.
Lemma pickle_inj {A: countType} (a a': A):
pickle a = pickle a' → a = a'.
Definition img {A: countType} {B: eqType} (f: A → B ) : pred B := λ y, exC (λ x, f x == y).
Definition imgT {A: countType} {B: eqType} (f: A → B) := {y | y \in img f}.
Definition img_pickle {A: countType} {B: eqType} (f: A → B) : { y | exC (λ x, f x == y) } → nat.
Definition img_unpickle {A: countType} {B: eqType} (f: A → B) (n: nat)
: option { y | exC (λ x, f x == y) } :=
(match unpickle n with
| Some a ⇒
Some (exist (λ y : B, exC (λ x : A, f x == y)) (f a)
(introT (exCP (λ x : A, f x == f a)) (ex_intro (λ x : A, f x == f a) a (eqxx (T:=B) (f a)))))
| None ⇒ None
end).
Lemma pickle_imgK {A: countType} {B: eqType} (f: A → B):
pcancel (img_pickle f) (img_unpickle f).
Definition img_choiceMixin {A: countType} {B: eqType} (f: A → B) :=
PcanChoiceMixin (pickle_imgK f).
Canonical img_choiceType {A: countType} {B: eqType} {f: A → B} :=
Eval hnf in ChoiceType (imgT f) (@img_choiceMixin A B f).
Definition img_countMixin {A: countType} {B: eqType} (f: A → B) :=
PcanCountMixin (pickle_imgK f).
Canonical img_countType {A: countType} {B: eqType} (f: A → B) :=
Eval hnf in CountType (imgT f) (@img_countMixin A B f).
Section countable_series_facts.
Variable (A: countType).
Implicit Types (a b: A → R).
Lemma countable_sum_scal c a:
∀ n, countable_sum (λ x, scal c (a x)) n = (λ n, scal c (countable_sum a n)) n.
Lemma is_seriesC_0 a: (∀ n, a n = 0) → is_series (countable_sum a) 0.
Lemma is_seriesC_ext a b l:
(∀ n, a n = b n) → is_series (countable_sum a) l → is_series (countable_sum b) l.
Lemma ex_seriesC_ext a b:
(∀ n, a n = b n) → ex_series (countable_sum a) → ex_series (countable_sum b).
Global Instance is_series_Proper:
Proper (pointwise_relation nat (@eq R) ==> @eq R ==> iff) is_series.
Global Instance ex_series_Proper:
Proper (pointwise_relation nat (@eq R) ==> iff) ex_series.
Global Instance Series_Proper:
Proper (pointwise_relation nat (@eq R) ==> eq) Series.
Global Instance countable_sum_Proper:
Proper (pointwise_relation A (@eq R) ==> pointwise_relation nat (@eq R)) countable_sum.
Global Instance countable_sum_Proper' {B: countType}:
Proper (pointwise_relation B (@eq R) ==> eq ==> eq) countable_sum.
Lemma is_seriesC_filter_pos a (P: pred A) (v: R):
(∀ n, a n ≥ 0) →
is_series (countable_sum a) v → ex_series (countable_sum (λ n, if P n then a n else 0)).
Lemma is_seriesC_filter_PQ a (P Q: pred A) (v: R):
(∀ n, a n ≥ 0) →
is_series (countable_sum (λ n, if P n then a n else 0)) v →
(∀ n, Q n → P n) →
ex_series (countable_sum (λ n, if Q n then a n else 0)).
Lemma ex_seriesC_filter_PQ a (P Q: pred A):
(∀ n, a n ≥ 0) →
ex_series (countable_sum (λ n, if P n then a n else 0)) →
(∀ n, Q n → P n) →
ex_series (countable_sum (λ n, if Q n then a n else 0)).
Lemma ex_seriesC_filter_P a (Q: pred A):
(∀ n, a n ≥ 0) →
ex_series (countable_sum a) →
ex_series (countable_sum (λ n, if Q n then a n else 0)).
Lemma is_seriesC_filter_split a (P: pred A) (v: R):
(∀ n, a n ≥ 0) →
is_series (countable_sum a) v →
Series (countable_sum (λ n, if P n then a n else 0)) +
Series (countable_sum (λ n, if ~~ P n then a n else 0)) = v.
Lemma is_seriesC_filter_union a (P Q: pred A) (v: R):
(∀ n, a n ≥ 0) →
is_series (countable_sum (λ n, if P n || Q n then a n else 0)) v →
Series (countable_sum (λ n, if P n then a n else 0)) +
Series (countable_sum (λ n, if Q n then a n else 0))
- Series (countable_sum (λ n, if P n && Q n then a n else 0)) = v.
Lemma SeriesC_ext a b:
(∀ n, a n = b n) →
Series (countable_sum a) = Series (countable_sum b).
Lemma SeriesC_le a b:
(∀ n, 0 ≤ a n ≤ b n) → ex_series (countable_sum b) →
Series (countable_sum a) ≤ Series (countable_sum b).
Lemma SeriesC_le' a b:
(∀ n, a n ≤ b n) →
ex_series (countable_sum a) → ex_series (countable_sum b) →
Series (countable_sum a) ≤ Series (countable_sum b).
Lemma countable_sum_plus a b:
∀ n, (countable_sum (λ x, a x + b x) n = (λ n, countable_sum a n + countable_sum b n) n).
Lemma countable_sum_Rabs a:
∀ n, (countable_sum (λ x, Rabs (a x)) n) = (λ n, Rabs (countable_sum a n)) n.
Lemma ex_seriesC_le a b:
(∀ n, 0 ≤ a n ≤ b n) → ex_series (countable_sum b) →
ex_series (countable_sum a).
Lemma countable_sum_scal_l c a:
∀ n, (countable_sum (λ x, c × a x) n = (λ n, c × (countable_sum a n)) n).
Lemma countable_sum_scal_r c a:
∀ n, (countable_sum (λ x, a x × c) n = (λ n, (countable_sum a n) × c) n).
Lemma SeriesC_scal_l (c : R) a:
Series (λ n, countable_sum (λ x, c × a x) n) = c × Series (countable_sum a).
Lemma SeriesC_scal_r (c : R) a:
Series (λ n, countable_sum (λ x, a x × c) n) = Series (countable_sum a) × c.
Lemma ex_seriesC_scal_l (c : R) a:
ex_series (countable_sum a) →
ex_series (countable_sum (λ x, c × a x)).
Lemma ex_seriesC_scal_r (c : R) a:
ex_series (countable_sum a) →
ex_series (countable_sum (λ x, a x × c)).
Lemma ex_seriesC_plus a b:
ex_series (countable_sum a) →
ex_series (countable_sum b) →
ex_series (countable_sum (λ x, a x + b x)).
Lemma is_seriesC_scal_l (c : R) a v:
is_series (countable_sum a) v →
is_series (countable_sum (λ x, c × a x)) (c × v).
Lemma is_seriesC_scal_r (c : R) a v:
is_series (countable_sum a) v →
is_series (countable_sum (λ x, a x × c)) (v × c).
Lemma is_seriesC_plus a b v1 v2:
is_series (countable_sum a) v1 →
is_series (countable_sum b) v2 →
is_series (countable_sum (λ x, a x + b x)) (v1 + v2).
Lemma is_seriesC_bump (x' : A) v:
is_series (countable_sum (λ x, if x == x' then v else 0)) v.
Lemma ex_seriesC_Rabs a:
ex_series (countable_sum (λ x, Rabs (a x))) →
ex_series (countable_sum a).
Lemma SeriesC_bump (x' : A) v:
Series (countable_sum (λ x, if x == x' then v else 0)) = v.
Lemma SeriesC_0 a:
(∀ x, a x = 0) →
Series (countable_sum a) = 0.
End countable_series_facts.