Library Waterproof.Libs.Analysis.Series

From Stdlib Require Import Reals.Reals.
From Stdlib Require Import Lra.
From Stdlib Require Import Classical.
From Stdlib Require Import Classical_Pred_Type.
From Stdlib 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 as (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 as (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)) as (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)) as (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) as (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)) as (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 as (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.