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.Common.
Require Import Notations.Reals.
Require Import Notations.Sets.
Require Import Chains.
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.
  Assume 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.
  Assume 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 : ℝ) :=
  converges_to (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 ⇒
      ((converges_to (fun Nn ↦ sigma a l Nn) L)
        ⇔
      (converges_to (fun Nn ↦ sigma a k Nn) ((sigma a k (l-1)) + L))).
Proof.
    Assume that (k < l)%nat (i).
    We show both directions.
    - We need to show that (converges_to (fun Nn ↦ (sigma a l Nn), L)
        ⇨ converges_to (fun Nn ↦ (sigma a k Nn), sigma a k (l - 1) + L)).
      Assume that (converges_to (fun Nn ↦ (sigma a l Nn), L)).
      We claim that (converges_to (fun N ↦ sigma a k (l-1)) (sigma a k (l-1))) (xi).
      { We need to show that (converges_to (constant_sequence (sigma a k (l-1))) (sigma a k (l-1))).
        By lim_const_seq we conclude that (converges_to (constant_sequence (sigma a k (l-1))) (sigma a k (l-1))).
      }
      By convergence_plus it holds that (converges_to (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.
        * Indeed, (M ∈ ℕ).
        * We need to show that
            (∀ n ≥ M,
              sigma(a, k, (M - 1)%nat) + sigma(a, M, n) = sigma(a, k, n)).
          Take n ≥ M.
          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 (converges_to (fun Nn ↦ (sigma a k (l - 1) + sigma a l Nn), sigma a k (l - 1) + L)).
        By (xi) we conclude that (converges_to (fun Nn ↦ (sigma a k (l - 1) + sigma a l Nn), sigma a k (l - 1) + L)).
    - We need to show that (converges_to (fun Nn ↦ (sigma a k Nn), (sigma a k (l - 1) + L)) ⇨ converges_to (fun Nn ↦ (sigma a l Nn), L)).
      Assume that (converges_to (fun Nn ↦ (sigma a k Nn), sigma a k (l - 1) + L)) (ii).
      We claim that (converges_to (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 convergence_minus it holds that (converges_to (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.
        * Indeed, (M ∈ ℕ).
        * We need to show that (for all n, (n ≥ M)%nat
            ⇨ sigma(a, k, n) - sigma(a, k, (M - 1)%nat) = sigma(a, M, n)).
          Take n : ℕ; such that (n ≥ M)%nat.
          It suffices to show that
            (sigma a k n = sigma a k (M - 1)%nat + sigma a l n).
          apply sigma_split_v2.
          - We conclude that (k < l)%nat.
          - We conclude that (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 (converges_to (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 (converges_to (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.