Library Stdlib.Reals.Alembert
From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import Rseries.
From Stdlib Require Import SeqProp.
From Stdlib Require Import PartSum.
From Stdlib Require Import Lra.
From Stdlib Require Import Compare_dec.
Local Open Scope R_scope.
Lemma Alembert_C1 :
forall An:
nat -> R,
(forall n:
nat, 0
< An n) ->
Un_cv (
fun n:
nat =>
Rabs (
An (
S n)
/ An n)) 0
->
{ l:R | Un_cv (
fun N:
nat =>
sum_f_R0 An N)
l }.
Lemma Alembert_C2_aux_positivity :
forall Xn :
nat -> R,
let Yn i :=
(2
* Rabs (
Xn i)
+ Xn i) / 2
in
(forall n,
Xn n <> 0
) ->
forall n, 0
< Yn n.
Lemma Alembert_C2_aux_Un_cv :
forall Xn :
nat -> R,
let Yn i :=
(2
* Rabs (
Xn i)
+ Xn i) / 2
in
(forall n,
Xn n <> 0
) ->
Un_cv (
fun n:
nat =>
Rabs (
Xn (
S n)
/ Xn n)) 0
->
Un_cv (
fun n =>
Rabs (
Yn (
S n)
/ Yn n)) 0.
Lemma Alembert_C2 :
forall An:
nat -> R,
(forall n:
nat,
An n <> 0
) ->
Un_cv (
fun n:
nat =>
Rabs (
An (
S n)
/ An n)) 0
->
{ l:R | Un_cv (
fun N:
nat =>
sum_f_R0 An N)
l }.
Lemma AlembertC3_step1 :
forall (
An:
nat -> R) (
x:
R),
x <> 0
->
(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 AlembertC3_step2 :
forall (
An:
nat -> R) (
x:
R),
x = 0
-> { l:R | Pser An x l }.
A useful criterion of convergence for power series
Convergence of power series in D(O,1/k)
k=0 is described in Alembert_C3