Library Stdlib.Reals.PartSum

Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import Rcomplete.
Local Open Scope R_scope.

Lemma tech1 :
  forall (An:nat -> R) (N:nat),
    (forall n:nat, (n <= N)%nat -> 0 < An n) -> 0 < sum_f_R0 An N.

Lemma tech2 :
  forall (An:nat -> R) (m n:nat),
    (m < n)%nat ->
    sum_f_R0 An n =
    sum_f_R0 An m + sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m).

Lemma tech3 :
  forall (k:R) (N:nat),
    k <> 1 -> sum_f_R0 (fun i:nat => k ^ i) N = (1 - k ^ S N) / (1 - k).

Lemma tech4 :
  forall (An:nat -> R) (k:R) (N:nat),
    0 <= k -> (forall i:nat, An (S i) < k * An i) -> An N <= An 0%nat * k ^ N.

Lemma tech5 :
  forall (An:nat -> R) (N:nat), sum_f_R0 An (S N) = sum_f_R0 An N + An (S N).

Lemma tech6 :
  forall (An:nat -> R) (k:R) (N:nat),
    0 <= k ->
    (forall i:nat, An (S i) < k * An i) ->
    sum_f_R0 An N <= An 0%nat * sum_f_R0 (fun i:nat => k ^ i) N.

Lemma tech7 : forall r1 r2:R, r1 <> 0 -> r2 <> 0 -> r1 <> r2 -> / r1 <> / r2.

Lemma tech11 :
  forall (An Bn Cn:nat -> R) (N:nat),
    (forall i:nat, An i = Bn i - Cn i) ->
    sum_f_R0 An N = sum_f_R0 Bn N - sum_f_R0 Cn N.

Lemma tech12 :
  forall (An:nat -> R) (x l:R),
    Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l ->
    Pser An x l.

Lemma scal_sum :
  forall (An:nat -> R) (N:nat) (x:R),
    x * sum_f_R0 An N = sum_f_R0 (fun i:nat => An i * x) N.

Lemma decomp_sum :
  forall (An:nat -> R) (N:nat),
    (0 < N)%nat ->
    sum_f_R0 An N = An 0%nat + sum_f_R0 (fun i:nat => An (S i)) (pred N).

Lemma plus_sum :
  forall (An Bn:nat -> R) (N:nat),
    sum_f_R0 (fun i:nat => An i + Bn i) N = sum_f_R0 An N + sum_f_R0 Bn N.

Lemma sum_eq :
  forall (An Bn:nat -> R) (N:nat),
    (forall i:nat, (i <= N)%nat -> An i = Bn i) ->
    sum_f_R0 An N = sum_f_R0 Bn N.

Lemma uniqueness_sum :
  forall (An:nat -> R) (l1 l2:R),
    infinite_sum An l1 -> infinite_sum An l2 -> l1 = l2.

Lemma minus_sum :
  forall (An Bn:nat -> R) (N:nat),
    sum_f_R0 (fun i:nat => An i - Bn i) N = sum_f_R0 An N - sum_f_R0 Bn N.

Lemma sum_decomposition :
  forall (An:nat -> R) (N:nat),
    sum_f_R0 (fun l:nat => An (2 * l)%nat) (S N) +
    sum_f_R0 (fun l:nat => An (S (2 * l))) N = sum_f_R0 An (2 * S N).

Lemma sum_Rle :
  forall (An Bn:nat -> R) (N:nat),
    (forall n:nat, (n <= N)%nat -> An n <= Bn n) ->
    sum_f_R0 An N <= sum_f_R0 Bn N.

Lemma Rsum_abs :
  forall (An:nat -> R) (N:nat),
    Rabs (sum_f_R0 An N) <= sum_f_R0 (fun l:nat => Rabs (An l)) N.

Lemma sum_cte :
  forall (x:R) (N:nat), sum_f_R0 (fun _:nat => x) N = x * INR (S N).

Lemma sum_growing :
  forall (An Bn:nat -> R) (N:nat),
    (forall n:nat, An n <= Bn n) -> sum_f_R0 An N <= sum_f_R0 Bn N.

Lemma Rabs_triang_gen :
  forall (An:nat -> R) (N:nat),
    Rabs (sum_f_R0 An N) <= sum_f_R0 (fun i:nat => Rabs (An i)) N.

Lemma cond_pos_sum :
  forall (An:nat -> R) (N:nat),
    (forall n:nat, 0 <= An n) -> 0 <= sum_f_R0 An N.

Definition Cauchy_crit_series (An:nat -> R) : Prop :=
  Cauchy_crit (fun N:nat => sum_f_R0 An N).

Lemma cauchy_abs :
  forall An:nat -> R,
    Cauchy_crit_series (fun i:nat => Rabs (An i)) -> Cauchy_crit_series An.

Lemma cv_cauchy_1 :
  forall An:nat -> R,
    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } ->
    Cauchy_crit_series An.

Lemma cv_cauchy_2 :
  forall An:nat -> R,
    Cauchy_crit_series An ->
    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.

Lemma sum_eq_R0 :
  forall (An:nat -> R) (N:nat),
    (forall n:nat, (n <= N)%nat -> An n = 0) -> sum_f_R0 An N = 0.

Definition SP (fn:nat -> R -> R) (N:nat) (x:R) : R :=
  sum_f_R0 (fun k:nat => fn k x) N.

Lemma sum_incr :
  forall (An:nat -> R) (N:nat) (l:R),
    Un_cv (fun n:nat => sum_f_R0 An n) l ->
    (forall n:nat, 0 <= An n) -> sum_f_R0 An N <= l.

Lemma sum_cv_maj :
  forall (An:nat -> R) (fn:nat -> R -> R) (x l1 l2:R),
    Un_cv (fun n:nat => SP fn n x) l1 ->
    Un_cv (fun n:nat => sum_f_R0 An n) l2 ->
    (forall n:nat, Rabs (fn n x) <= An n) -> Rabs l1 <= l2.