Library discprob.prob.double

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

Definition double_summable a :=
  ∃ (r: R), ∀ n, sum_n (λ j, sum_n (λ k, Rabs (a (j, k))) n) n ≤ r.

Lemma double_summable_mono_cond a:
  (∃ (r: R), ∃ N, ∀ n, n ≥ N → sum_n (λ j, sum_n (λ k, Rabs (a (j, k))) n) n ≤ r) →
  double_summable a.

Lemma double_summable_ext a a':
  (∀ j k, Rabs (a (j, k)) = Rabs (a' (j, k))) →
  double_summable a → double_summable a'.

Lemma double_summable_abs a :
  double_summable a → double_summable (Rabs \o a).

Lemma double_summable_by_flip a:
  double_summable a →
  double_summable (λ xy, a (snd xy, fst xy)).

Lemma double_summable_flip a:
  double_summable (λ xy, a (snd xy, fst xy)) → double_summable a.

Lemma ex_series_rows_ds a:
  (∀ j, ex_series (λ k, Rabs (a (j, k)))) →
  ex_series (λ j, Series (λ k, Rabs (a (j, k)))) →
  double_summable a.

Lemma ex_series_columns_ds a:
  (∀ k, ex_series (λ j, Rabs (a (j, k)))) →
  ex_series (λ k, Series (λ j, Rabs (a (j, k)))) →
  double_summable a.

Lemma ex_series_row a (DS: double_summable a) j:
  ex_series (λ k, Rabs (a (j, k))).

Lemma ex_series_column a (DS: double_summable a) k:
  ex_series (λ j, Rabs (a (j, k))).

Module pre_converge.

Section covering1.

Variable (a: nat × nat → R).
Variable (σ: nat → 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_cover1:
  ∀ N, ∃ K, ∀ n, n ≤ N → (fst (σ n) ≤ K ∧ snd (σ n) ≤ K).

Lemma inj_nat_cover2:
  ∀ K1 K2, ∃ N, ∀ l m, l ≤ K1 → m ≤ K2 →
 ( ∃ n, n ≤ N ∧ σ n = (l, m)) ∨ a (l, m) = 0.

Lemma sum_n_m_cover_diff_double:
  ∀ N, ∃ K, ∀ l m, l ≥ K → m ≥ K →
  ∃ n, n ≥ N ∧ Rabs (sum_n (λ j, sum_n (λ k, a (j, k)) m) l - sum_n (a \o σ) N)
               ≤ sum_n_m (Rabs \o a \o σ) (S N) n.

Lemma is_lim_seq_sum_n (f: nat × nat → R) (h: nat → R) l:
  (∀ j, j ≤ l → is_lim_seq (λ m, sum_n (λ k, f (j, k)) m) (h j)) →
  is_lim_seq (λ m, sum_n (λ j, sum_n (λ k, f (j, k)) m) l) (sum_n h l).

Lemma is_lim_seq_fin_abs:
  ∀ (u : nat → R) (l : R), is_lim_seq u l → is_lim_seq (λ n : nat, Rabs (u n)) (Rabs l).

End covering1.

Section covering2.
Variable (a: nat × nat → R).
Variable (σ: nat → nat × nat).

Variable (INJ: ∀ n n', a (σ n) ≠ 0 → σ n = σ n' → n = n').
Variable (COV: ∀ n, a n ≠ 0 → ∃ m, σ m = n).
Variable (EXS: ex_series (Rabs \o a \o σ)).

Lemma abs_inj: ∀ n n', Rabs (a (σ n)) ≠ 0 → σ n = σ n' → n = n'.

Lemma abs_cov: ∀ n, Rabs (a n) ≠ 0 → ∃ m, σ m = n.

Lemma summable_implies_ds:
  double_summable a.

Lemma series_double_covering:
  is_series (λ j, Series (λ k, a (j, k))) (Series (a \o σ)).

Lemma series_double_covering':
  is_series (a \o σ) (Series (λ j, Series (λ k, a (j, k)))).

End covering2.
End pre_converge.

Section summable.

Variable (a: nat × nat → R).
Variable (σ: nat → nat × nat).

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

Variable (DS: double_summable a).

Lemma ex_series_ordering:
  ex_series (Rabs \o a \o σ).

Lemma series_double_covering:
  is_series (λ j, Series (λ k, a (j, k))) (Series (a \o σ)).

Lemma series_double_covering':
  is_series (a \o σ) (Series (λ j, Series (λ k, a (j, k)))).

End summable.

Lemma series_double_covering_Rabs a σ
      (INJ: ∀ n n', a (σ n) ≠ 0 → σ n = σ n' → n = n')
      (COV: ∀ n, a n ≠ 0 → ∃ m, σ m = n)

      (DS: double_summable a):
  is_series (λ j, Series (λ k, Rabs (a (j, k)))) (Series (Rabs \o a \o σ)).

Lemma series_double_covering_Rabs' a σ
      (INJ: ∀ n n', a (σ n) ≠ 0 → σ n = σ n' → n = n')
      (COV: ∀ n, a n ≠ 0 → ∃ m, σ m = n)

      (DS: double_summable a):

  is_series (Rabs \o a \o σ) (Series (λ j, Series (λ k, Rabs (a (j, k))))).

Lemma sum_n_m_ext_const_zero: ∀ (G : AbelianGroup) (a : nat → G) (n m : nat),
    (∀ n, a n = zero) →
    sum_n_m a n m = zero.

Module double_swap.
Section double_swap.

Variable (a : nat × nat → R).
Variable (DS: double_summable a).

Definition σ := λ x, match @pickle_inv [countType of nat × nat] x with
            | Some (m, n) ⇒ (S m, S n)
            | None ⇒ (O, O)
            end.

Definition a' := λ mn, match mn with
                   | (S m', S n') ⇒ a (m', n')
                   | (_, _) ⇒ 0
                   end.

Lemma a_a'_Series_ext j: (λ j, Series (λ k, a (j, k))) j = (λ j, Series (λ k, a' (S j, S k))) j.

Lemma a_a'_Series_ext_swap j:
  (λ k, Series (λ j, a (j, k))) j = (λ k, Series (λ j, a' (S j, S k))) j.

Lemma a_a'_finite_sum n m:
  sum_n (λ j, sum_n (λ k, a (j, k)) m) n =
  sum_n (λ j, sum_n (λ k, a' (j, k)) (S m)) (S n).

Lemma a_a'_finite_sum_abs n m:
  sum_n (λ j, sum_n (λ k, Rabs (a (j, k))) m) n =
  sum_n (λ j, sum_n (λ k, Rabs (a' (j, k))) (S m)) (S n).

Lemma ds_a': double_summable a'.

Lemma σ_inj:
  ∀ n n' : nat, a' (σ n) ≠ 0 → σ n = σ n' → n = n'.

Lemma is_series_a'_σ_rows:
  is_series (λ j : nat, Series (λ k : nat, a' (j, k))) (Series (a' \o σ)).

Lemma is_series_a'_σ_columns:
  is_series (λ k : nat, Series (λ j : nat, a' (j, k))) (Series (a' \o σ)).

Lemma Series_a'_shift:
  (Series (λ n : nat, Series (λ j : nat, a' (j.+1, n.+1)))) =
  (Series (λ n : nat, Series (λ j : nat, a' (j, n)))).

Lemma is_series_a'_shift v:
  is_series (λ j : nat, Series (λ n : nat, a' (j, n))) v →
  is_series (λ j : nat, Series (λ n : nat, a' (j.+1, n.+1))) v.

Lemma ex_series_a'_shift:
  ex_series (λ j : nat, Series (λ n : nat, a' (j, n))) →
  ex_series (λ j : nat, Series (λ n : nat, a' (j.+1, n.+1))).

Lemma series_double_swap:
  is_series (λ j, Series (λ k, a (j, k))) (Series (λ k, Series (λ j, a (j, k)))).

End double_swap.
End double_swap.

Lemma series_double_swap a (DS: double_summable a):
  is_series (λ j, Series (λ k, a (j, k))) (Series (λ k, Series (λ j, a (j, k)))).

Lemma Series_double_swap a (DS: double_summable a):
  Series (λ j, Series (λ k, a (j, k))) = (Series (λ k, Series (λ j, a (j, k)))).