# Library Coq.Reals.PartSum

Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import Rcomplete.
Require Import Max.
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.