Library discprob.prob.rearrange

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

Lemma sum_n_m_filter (a: nat → R) (P: pred nat) n m:
  sum_n_m (λ n, if P n then (Rabs (a n)) else 0) n m ≤ sum_n_m (Rabs \o a) n m.

Lemma foldl_max l:
  ∀ x, foldl max x l ≥ x.

Lemma max_fun_range (σ: nat → nat) m:
  ∃ N, (∀ m', m' ≤ m → σ m' ≤ N) ∧ (∃ m0, m0 ≤ m ∧ σ m0 = N).

Section bijective.

Lemma bij_nat_cover (σ: nat → nat) (bij: bijective σ):
  ∀ n, ∃ m, ∀ m', m' ≥ m →
  ∃ N, (∀ n', n' ≤ n → ∃ m'', m'' ≤ m' ∧ σ m'' = n') ∧ N ≥ n ∧ (∀ m'', m'' ≤ m' → σ m'' ≤ N).

Lemma sum_n_bij_sandwich (a: nat → R) (σ: nat → nat) (bij: bijective σ):
  ∀ n, ∃ m, ∀ m', m' ≥ m →
  ∃ n', n' ≥ n ∧ sum_n (Rabs \o a) n ≤ sum_n ((Rabs \o a) \o σ) m' ≤ sum_n (Rabs \o a) n'.

Lemma sum_n_m_bij_diff_abs (a: nat → R) (σ: nat → nat) (bij: bijective σ):
  ∀ N, ∃ M, ∀ m, m ≥ M →
  ∃ n, n ≥ N ∧ Rabs (sum_n (Rabs \o a \o σ) m - sum_n (Rabs \o a) N) ≤ sum_n_m (Rabs \o a) (S N) n.

Lemma sum_n_m_bij_diff (a: nat → R) (σ: nat → nat) (bij: bijective σ):
  ∀ N, ∃ M, ∀ m, m ≥ M →
  ∃ n, n ≥ N ∧ Rabs (sum_n (a \o σ) m - sum_n a N) ≤ sum_n_m (Rabs \o a) (S N) n.

Lemma norm_dist_mid x y z: norm (x - y) ≤ norm (x - z) + norm (z - y).
Lemma series_rearrange (a: nat → R) (σ: nat → nat) (bij: bijective σ) (v: R):
  is_series (λ n, Rabs (a n)) v →
  is_series (λ n, Rabs (a (σ n))) v ∧
  is_series (λ n, a (σ n)) (Series a).

End bijective.

Section covering.

Variable (a: nat → R).
Variable (σ: nat → nat).
Variable (INJ: ∀ n n', a (σ n) ≠ 0 → σ n = σ n' → n = n').
Variable (COV: ∀ n, a n ≠ 0 → ∃ m, σ m = n).

Lemma inj_nat_cover:
  ∀ n, ∃ m, ∀ m', m' ≥ m →
  ∃ N, (∀ n', n' ≤ n → (∃ m'', m'' ≤ m' ∧ σ m'' = n') ∨ a n' = 0)
       ∧ N ≥ n ∧ (∀ m'', m'' ≤ m' → σ m'' ≤ N).

Lemma sum_n_m_cover_diff:
  ∀ N, ∃ M, ∀ m, m ≥ M →
  ∃ n, n ≥ N ∧ Rabs (sum_n (a \o σ) m - sum_n a N) ≤ sum_n_m (Rabs \o a) (S N) n.

End covering.

Lemma series_rearrange_covering (a: nat → R) (σ: nat → nat)
      (INJ: ∀ n n', a (σ n) ≠ 0 → σ n = σ n' → n = n')
      (COV: ∀ n, a n ≠ 0 → ∃ m, σ m = n)
      (v: R):
  is_series (λ n, Rabs (a n)) v →
  is_series (λ n, Rabs (a (σ n))) v ∧
  is_series (λ n, a (σ n)) (Series a).

Lemma series_rearrange_covering_pos (a: nat → R) (σ: nat → nat)
      (INJ: ∀ n n', a (σ n) ≠ 0 → σ n = σ n' → n = n')
      (COV: ∀ n, a n ≠ 0 → ∃ m, σ m = n)
      (POS: ∀ n, a n ≥ 0)
      (v: R):
  is_series a v →
  is_series (λ n, a (σ n)) v.
Lemma Series_rearrange_covering (a: nat → R) (σ: nat → nat)
      (INJ: ∀ n n', a (σ n) ≠ 0 → σ n = σ n' → n = n')
      (COV: ∀ n, a n ≠ 0 → ∃ m, σ m = n):
  ex_series (λ n, Rabs (a n)) →
  Series a = Series (a \o σ).

Lemma countable_series_rearrange_covering {Y X: countType}
      (a: X → R) (σ: Y → X)
      (INJ: ∀ n n', a (σ n) ≠ 0 → σ n = σ n' → n = n')
      (COV: ∀ n, a n ≠ 0 → ∃ m, σ m = n)
      (v: R):
  is_series (countable_sum (λ n, Rabs (a n))) v →
  is_series (countable_sum (λ n, Rabs (a (σ n)))) v ∧
  is_series (countable_sum (λ n, a (σ n))) (Series (countable_sum a)).

Lemma countable_series_oapp {X: countType}
      (a: X → R) (v: R):
  is_series (countable_sum (λ n, Rabs (oapp a R0 n))) v →
  is_series (countable_sum (λ n, Rabs (a n))) v ∧
  is_series (countable_sum (λ n, a n)) (Series (countable_sum (oapp a R0))).

Lemma countable_series_oapp' {X: countType}
      (a: X → R) (v: R):
  is_series (countable_sum (λ n, Rabs (a n))) v →
  is_series (countable_sum (λ n, Rabs (oapp a R0 n))) v ∧
  is_series (countable_sum (oapp a R0)) (Series (countable_sum a)).

Lemma countable_Series_oapp' {X: countType}
      (a: X → R):
  ex_series (countable_sum (λ n, Rabs (a n))) →
  Series (countable_sum a) = Series (countable_sum (oapp a R0)).

Remark gt_support_conv {X: countType} (b: X → R): ∀ x, b x > 0 → support b.

Lemma countable_series_rearrange_covering_match {X Y: countType}
      (a: X → R) (b: Y → R) (σ: support b → support a)
      (Hapos: ∀ x, a x ≥ 0)
      (Hbpos: ∀ x, b x ≥ 0)
      (INJ: ∀ n n', σ n = σ n' → n = n')
      (COV: ∀ n, ∃ m, σ m = n)
      (EQ: ∀ n, a (sval (σ n)) = b (sval n))
      (v: R):
  is_series (countable_sum (λ n, a n)) v →
  is_series (countable_sum (λ n, b n)) v.

Lemma countable_series_rearrange_covering_match_fun {X Y: countType}
      (a: X → R) (b: Y → R) (σ: {x : Y | b x ≠ 0} → { x : X | a x ≠ 0 })
   
      (INJ: ∀ n n', σ n = σ n' → n = n')
      (COV: ∀ n, ∃ m, σ m = n)
      (EQ: ∀ n, a (sval (σ n)) = b (sval n))
      (v: R):
  is_series (countable_sum (λ n, Rabs (a n))) v →
  is_series (countable_sum (λ n, Rabs (b n))) v ∧
  is_series (countable_sum b) (Series (countable_sum a)).