Library discprob.basic.Series_Ext

From discprob.basic Require Import base order bigop_ext.
Require Import Reals Fourier Psatz.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import ClassicalEpsilon.

Lemma Rbar_le_fin x y: 0 ≤ y → Rbar_le x (Finite y) → Rle (real x) y.

Lemma Rbar_le_fin' x y: 0 ≤ y → Rbar_le x y → Rle x (real y).

Lemma Rbar_eq_fin x y: x = (Finite y) → (real x) = y.

Lemma is_series_0 a: (∀ n, a n = 0) → is_series a 0.

Lemma Series_0 a: (∀ n, a n = 0) → Series a = 0.

Lemma is_lim_seq_pos a (v: R):
  (∀ n, a n ≥ 0) →
  is_lim_seq a v →
  0 ≤ v.

Lemma Lim_seq_pos a:
  (∀ n, a n ≥ 0) →
  0 ≤ Lim_seq a.

Lemma Series_pos a:
  (∀ n, a n ≥ 0) →
  0 ≤ Series a.

Lemma Series_strict_pos_inv a:
  (∀ n, a n ≥ 0) →
  0 < Series a →
  ∃ n, a n > 0.

Lemma is_lim_seq_unique_series a v:
  is_series a v → Lim_seq (sum_n a) = v.

Lemma is_series_partial_pos a n v:
  (∀ n, a n ≥ 0) →
  is_series a v →
  sum_n a n ≤ v.

Lemma sum_n_partial_pos a :
  (∀ n, a n ≥ 0) →
   ∀ n : nat, sum_n a n ≥ 0.

Lemma sum_n_pos a (n: nat):
  (∀ n, a n ≥ 0) →
  0 ≤ sum_n a n.

Lemma sum_n_strict_pos a (n: nat):
  (∀ n, a n ≥ 0) →
  a n > 0 →
  0 < sum_n a n.

Lemma Series_partial_pos a (n: nat):
  (∀ n, a n ≥ 0) →
  ex_finite_lim_seq (sum_n a) →
  sum_n a n ≤ Series a.

Lemma Series_strict_pos a (n: nat):
  (∀ n, a n ≥ 0) →
  a n > 0 →
  ex_finite_lim_seq (sum_n a) →
  0 < Series a.

Lemma is_series_filter_pos a (P: pred nat) (v: R):
  (∀ n, a n ≥ 0) →
  is_series a v → ex_series (λ n, if P n then a n else 0).

Lemma is_series_filter_PQ a (P Q: pred nat) (v: R):
  (∀ n, a n ≥ 0) →
  is_series (λ n, if P n then a n else 0) v →
  (∀ n, Q n → P n) →
  ex_series (λ n, if Q n then a n else 0).

Lemma is_series_filter_split a (P: pred nat) (v: R):
  (∀ n, a n ≥ 0) →
  is_series a v →
  Series (λ n, if P n then a n else 0) + Series (λ n, if ~~ P n then a n else 0) = v.

Lemma is_series_filter_union a (P Q: pred nat) (v: R):
  (∀ n, a n ≥ 0) →
  is_series (λ n, if P n || Q n then a n else 0) v →
  Series (λ n, if P n then a n else 0) + Series (λ n, if Q n then a n else 0)
    - Series (λ n, if P n && Q n then a n else 0) = v.

Lemma is_series_bump_hd v:
  is_series (λ x, if eq_nat_dec x 0 then v else 0) v.

Lemma is_series_bump n v:
  is_series (λ x, if eq_nat_dec x n then v else 0) v.

Lemma Series_bump n v:
  Series (λ x, if eq_nat_dec x n then v else 0) = v.

Lemma Series_le':
  ∀ a b : nat → R, (∀ n : nat, a n ≤ b n) → ex_series a → ex_series b → Series a ≤ Series b.

Lemma is_lub_seq_eps_below a x:
  is_lub (λ r : R, ∃ n : nat, a n = r) x →
  ∀ eps : posreal , ∃ n, x - eps < a n ≤ x.

Lemma is_lub_seq_eps_ball a x:
  is_lub (λ r : R, ∃ n : nat, a n = r) x →
  ∀ eps : posreal , ∃ n, ball x eps (a n).

Lemma sum_n_nonneg_terms_increasing a n n':
  n ≤ n' → (∀ n, a n ≥ 0) → sum_n a n ≤ sum_n a n'.

Lemma Lim_seq_le_loc_const u v:
  0 ≤ v →
  eventually (λ n : nat, u n ≤ v) → Lim_seq u ≤ v.

Lemma ex_series_non_neg_le_const a v:
  (∀ n : nat, 0 ≤ a n) → (∀ n, sum_n a n ≤ v) → ex_series a ∧ Series a ≤ v.

Lemma ex_series_is_lim_seq (f: nat → R):
  ex_series f → is_lim_seq (sum_n f) (Series f).

Lemma is_lim_seq_is_series (f: nat → R) (v: R):
  is_lim_seq (sum_n f) v → is_series f v.

Lemma is_series_single_non_zero (f: nat → R) i:
  (∀ j, f j ≠ 0 → i = j) →
  is_series f (f i).

Lemma Series_single_non_zero (f: nat → R) i:
  (∀ j, f j ≠ 0 → i = j) →
  Series f = (f i).

Lemma ex_series_single_non_zero (f: nat → R):
  (∀ i j, f i ≠ 0 → f j ≠ 0 → i = j) →
  ex_series f.