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.