Library Waterproof.Libs.Analysis.Series

Require Import Coq.Reals.Reals.
Require Import Lra.
Require Import Classical.
Require Import Classical_Pred_Type.
Require Import ClassicalChoice.

Require Import Automation.
Require Import Libs.Analysis.Sequences.
Require Import Notations.
Require Import Tactics.

Waterproof Enable Automation RealsAndIntegers.

#[export] Hint Resolve Rabs_Rabsolu : wp_reals.
#[export] Hint Resolve Rabs_minus_sym : wp_reals.
#[export] Hint Resolve Rmult_lt_0_compat : wp_reals.
#[export] Hint Resolve Rinv_lt_contravar : wp_reals.

Open Scope R_scope.

Lemma sigma_split_v2 :
  ∀ (a : ℕ → ℝ) (k l M : ℕ),
    (k < l)%nat ⇒ (l ≤ M)%nat
      ⇒ sigma a k M = sigma a k (l - 1)%nat + sigma a l M.
Proof.
    Take a : (ℕ → ℝ) and k, l, M : ℕ; such that
      (k < l)%nat and (l ≤ M)%nat.
    It holds that (l = S (l - 1)%nat) (i).
    rewrite (i) at 2.
    By sigma_split it suffices to show that (k <= l - 1 < M)%nat.
    We show both (k <= l - 1)%nat and (l - 1 < M)%nat.
    - We conclude that (k ≤ l - 1)%nat.
    - We conclude that (l - 1 < M)%nat.
Qed.

Notation partial_sums := sum_f_R0.

Lemma partial_sums_pos_incr :
  ∀ (a : ℕ → ℝ), (∀ n : ℕ, a n ≥ 0)⇒
    Un_growing (partial_sums a).
Proof.
    Take a : (ℕ → ℝ); such that (∀ n : ℕ, a n ≥ 0).
    We need to show that (for all n : ℕ, partial_sums a n ≤ partial_sums a (S n)).
    Take n : ℕ.
    It holds that (a (S n) ≥ 0).
    It holds that ((partial_sums a n) + a (S n) = partial_sums a (S n)).
    We conclude that (& partial_sums a n <= (partial_sums a n) + a (S n)
                                         = partial_sums a (S n)).
Qed.

Definition series_cv_to (a : ℕ → ℝ) (l : ℝ) :=
  Un_cv (partial_sums a) l.
Definition series_cv (a : ℕ → ℝ) :=
  ∃ l : ℝ, series_cv_to a l.
Definition series_cv_abs (a : ℕ → ℝ) :=
  series_cv (fun n ↦ Rabs( a n )).
Definition series_cv_abs_to (a : ℕ → ℝ) (l : ℝ) :=
  series_cv_to (fun n ↦ Rabs(a n)) l.

Theorem mouse_tail :
  ∀ (a : ℕ → ℝ) (k l : ℕ) (L : ℝ),
    (k < l)%nat ⇒
      ((Un_cv (fun Nn ↦ sigma a l Nn) L)
        ⇔
      (Un_cv (fun Nn ↦ sigma a k Nn) ((sigma a k (l-1)) + L))).
Proof.
    Take a : (ℕ → ℝ) and k, l : ℕ and L : ℝ.
    Assume that (k < l)%nat (i).
    We show both directions.
    - We need to show that (Un_cv(fun Nn ↦ (sigma a l Nn), L)
        ⇨ Un_cv (fun Nn ↦ (sigma a k Nn), sigma a k (l - 1) + L)).
      Assume that (Un_cv (fun Nn ↦ (sigma a l Nn), L)).
      We claim that (Un_cv (fun N ↦ sigma a k (l-1)) (sigma a k (l-1))) (xi).
      { We need to show that ((constant_sequence (sigma a k (l-1))) ⟶ (sigma a k (l-1))).
        By lim_const_seq we conclude that (constant_sequence (sigma a k (l-1)) ⟶ sigma a k (l-1)).
      }
      By CV_plus it holds that (Un_cv (fun Nn ↦ sigma a k (l-1)%nat + sigma a l Nn) (sigma a k (l-1)%nat + L)).
      We claim that (evt_eq_sequences (fun Nn ↦ (sigma a k (l - 1) + sigma a l Nn)) (fun Nn ↦ (sigma a k Nn))) (x).
      { We need to show that (∃ M : ℕ, ∀ n : ℕ, (n ≥ M)%nat ⇒ sigma a k (l - 1)%nat + sigma a l n = sigma a k n).
        Choose M := l%nat.
        Take n : ℕ; such that (n ≥ M)%nat.
        By sigma_split_v2 it suffices to show that (k < l <= n)%nat.
        We conclude that (k < l <= n)%nat.
      }
      
      apply conv_evt_eq_seq with (a := fun Nn ↦ sigma a k (l-1) + sigma a l Nn).
      + By (x) we conclude that (evt_eq_sequences (fun Nn ↦ (sigma a k (l - 1) + sigma a l Nn), fun Nn ↦ (sigma a k Nn))).
      +
        We need to show that (Un_cv (fun Nn ↦ (sigma a k (l - 1) + sigma a l Nn), sigma a k (l - 1) + L)).
        By (xi) we conclude that (Un_cv (fun Nn ↦ (sigma a k (l - 1) + sigma a l Nn), sigma a k (l - 1) + L)).
    - We need to show that (Un_cv (fun Nn ↦ (sigma a k Nn), (sigma a k (l - 1) + L)) ⇨ Un_cv (fun Nn ↦ (sigma a l Nn), L)).
      Assume that (Un_cv (fun Nn ↦ (sigma a k Nn), sigma a k (l - 1) + L)) (ii).
      We claim that (Un_cv (fun N ↦ (sigma a k (l-1)), (sigma a k (l-1)))).
      { We need to show that ((constant_sequence (sigma a k (l-1))) ⟶ (sigma a k (l-1))).
        By lim_const_seq we conclude that (constant_sequence (sigma a k (l-1)) ⟶ sigma a k (l-1)).
      }
      By CV_minus it holds that (Un_cv (fun N ↦ sigma a k N - (sigma a k (l-1))) (sigma a k (l-1) + L - (sigma a k (l-1)))).
      We claim that (evt_eq_sequences (fun Nn ↦ (sigma a k Nn - sigma a k (l-1))) (fun Nn ↦ (sigma a l Nn))) (iii).
      { We need to show that (∃ M : ℕ, ∀ n : ℕ, (n ≥ M)%nat ⇒ sigma a k n - sigma a k (l-1) = sigma a l n).
        Choose M := l%nat.
        Take n : ℕ; such that (n ≥ M)%nat.
        It suffices to show that (sigma a k n = sigma a k (l - 1) + sigma a l n).
        By sigma_split_v2 it suffices to show that (k < l <= n)%nat.
        We conclude that (k < l <= n)%nat.
      }
      apply conv_evt_eq_seq with (a := fun n ↦ sigma a k n - sigma a k (l-1)) (b := fun n ↦ sigma a l n).
      + By (iii) we conclude that (evt_eq_sequences (fun n ↦ (sigma a k n - sigma a k (l - 1)), fun n ↦ (sigma a l n))).
      + We need to show that (Un_cv (fun N ↦ (sigma a k N - sigma a k (l - 1)), L)).
        It holds that ((sigma a k (l - 1) + L - sigma a k (l - 1)) = L) (iv).
        rewrite <- (iv).         By (ii) we conclude that (Un_cv (fun N ↦ (sigma a k N - sigma a k (l - 1)), sigma a k (l - 1) + L - sigma a k (l - 1))).
Qed.

Close Scope R_scope.