Library Coq.Reals.Alembert
A useful criterion of convergence for power series
Theorem Alembert_C3 :
forall (
An:nat ->
R) (
x:R),
(
forall n:nat,
An n <> 0) ->
Un_cv (
fun n:nat =>
Rabs (
An (
S n) /
An n)) 0 ->
{
l:R |
Pser An x l }.
Lemma Alembert_C4 :
forall (
An:nat ->
R) (
k:R),
0 <=
k < 1 ->
(
forall n:nat, 0 <
An n) ->
Un_cv (
fun n:nat =>
Rabs (
An (
S n) /
An n))
k ->
{
l:R |
Un_cv (
fun N:nat =>
sum_f_R0 An N)
l }.
Lemma Alembert_C5 :
forall (
An:nat ->
R) (
k:R),
0 <=
k < 1 ->
(
forall n:nat,
An n <> 0) ->
Un_cv (
fun n:nat =>
Rabs (
An (
S n) /
An n))
k ->
{
l:R |
Un_cv (
fun N:nat =>
sum_f_R0 An N)
l }.
Convergence of power series in D(O,1/k)
k=0 is described in Alembert_C3
Lemma Alembert_C6 :
forall (
An:nat ->
R) (
x k:R),
0 <
k ->
(
forall n:nat,
An n <> 0) ->
Un_cv (
fun n:nat =>
Rabs (
An (
S n) /
An n))
k ->
Rabs x < /
k -> {
l:R |
Pser An x l }.