Library Coq.Reals.PartSum
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import Rcomplete.
Require Import Max.
Open Local 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.