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

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 }.