Library Stdlib.Reals.PSeries_reg

From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import SeqSeries.
From Stdlib Require Import Ranalysis1.
From Stdlib Require Import MVT.
From Stdlib Require Import Lra.
Local Open Scope R_scope.

Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.

Lemma Boule_convex : forall c d x y z,
  Boule c d x -> Boule c d y -> x <= z <= y -> Boule c d z.

Definition boule_of_interval x y (h : x < y) :
  {c :R & {r : posreal | c - r = x /\ c + r = y }}.

Definition boule_in_interval x y z (h : x < z < y) :
  {c : R & {r | Boule c r z /\ x < c - r /\ c + r < y }}.

Lemma Ball_in_inter : forall c1 c2 r1 r2 x,
  Boule c1 r1 x -> Boule c2 r2 x ->
  {r3 : posreal | forall y, Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y }.

Lemma Boule_center : forall x r, Boule x r x.

Uniform convergence

Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R)
  (r:posreal) : Prop :=
  forall eps:R,
    0 < eps ->
    exists N : nat ,
      (forall (n:nat) (y:R),
        (N <= n)%nat -> Boule x r y -> Rabs (f y - fn n y) < eps ).

Normal convergence

Definition CVN_r (fn:nat -> R -> R) (r:posreal) : Type :=
  { An :nat -> R &
    { l :R |
      Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n) l /\
      (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n ) } }.

Definition CVN_R (fn:nat -> R -> R) : Type := forall r:posreal, CVN_r fn r.

Definition SFL (fn:nat -> R -> R)
  (cv:forall x:R, { l :R | Un_cv (fun N:nat => SP fn N x) l })
  (y:R) : R := let (a,_) := cv y in a.

In a complete space, normal convergence implies uniform convergence

Lemma CVN_CVU :
  forall (fn:nat -> R -> R)
    (cv:forall x:R, {l :R | Un_cv (fun N:nat => SP fn N x) l })
    (r:posreal), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL fn cv) 0 r.

Each limit of a sequence of functions which converges uniformly is continue

Lemma CVU_continuity :
  forall (fn:nat -> R -> R) (f:R -> R) (x:R) (r:posreal),
    CVU fn f x r ->
    (forall (n:nat) (y:R), Boule x r y -> continuity_pt (fn n) y ) ->
    forall y:R, Boule x r y -> continuity_pt f y.

Lemma continuity_pt_finite_SF :
  forall (fn:nat -> R -> R) (N:nat) (x:R),
    (forall n:nat, (n <= N)%nat -> continuity_pt (fn n) x ) ->
    continuity_pt (fun y:R => sum_f_R0 (fun k:nat => fn k y) N) x.

Continuity and normal convergence

Lemma SFL_continuity_pt :
  forall (fn:nat -> R -> R)
    (cv:forall x:R, { l :R | Un_cv (fun N:nat => SP fn N x) l })
    (r:posreal),
    CVN_r fn r ->
    (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y ) ->
    forall y:R, Boule 0 r y -> continuity_pt (SFL fn cv) y.

Lemma SFL_continuity :
  forall (fn:nat -> R -> R)
    (cv:forall x:R, { l :R | Un_cv (fun N:nat => SP fn N x) l }),
    CVN_R fn -> (forall n:nat, continuity (fn n)) -> continuity (SFL fn cv).

As R is complete, normal convergence implies that (fn) is simply-uniformly convergent

Lemma CVN_R_CVS :
  forall fn:nat -> R -> R,
    CVN_R fn -> forall x:R, { l :R | Un_cv (fun N:nat => SP fn N x) l }.

Lemma CVU_cv : forall f g c d, CVU f g c d ->
   forall x, Boule c d x -> Un_cv (fun n => f n x) (g x).

Lemma CVU_ext_lim :
  forall f g1 g2 c d, CVU f g1 c d -> (forall x, Boule c d x -> g1 x = g2 x ) ->
    CVU f g2 c d.

Lemma CVU_derivable :
  forall f f' g g' c d,
   CVU f' g' c d ->
   (forall x, Boule c d x -> Un_cv (fun n => f n x) (g x)) ->
   (forall n x, Boule c d x -> derivable_pt_lim (f n) x (f' n x)) ->
   forall x, Boule c d x -> derivable_pt_lim g x (g' x).