Library Coquelicot.Seq_fct

This file is part of the Coquelicot formalization of real analysis in Coq:
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Import Reals Ssreflect.ssreflect Rbar.
Require Import Rcomplements.
Require Import Lim_seq Continuity Derive Series.
Require Import Lub Hierarchy.

This file describes sequences of functions and results about their convergence.

Open Scope R_scope.

Sequence of functions


Definition CVS_dom (fn : natRR) (D : RProp) :=
   x : R, D xex_finite_lim_seq (fun nfn n x).

Definition CVU_dom (fn : natRR) (D : RProp) :=
   eps : posreal, eventually (fun n x : R,
    D xRabs ((fn n x) - real (Lim_seq (fun nfn n x))) < eps).
Definition CVU_cauchy (fn : natRR) (D : RProp) :=
   eps : posreal, N : nat,
   (n m : nat) (x : R), D x → (N n)%nat → (N m)%nat
    → Rabs (fn n x - fn m x) < eps.

Equivalence with standard library

Lemma CVU_dom_Reals (fn : natRR) (f : RR) (x : R) (r : posreal) :
  ( y, (Boule x r y) → (Finite (f y)) = Lim_seq (fun nfn n y)) →
  (CVU fn f x r CVU_dom fn (Boule x r)).

Various inclusions and equivalences between definitions

Lemma CVU_CVS_dom (fn : natRR) (D : RProp) :
  CVU_dom fn DCVS_dom fn D.
Lemma CVU_dom_cauchy (fn : natRR) (D : RProp) :
  CVU_dom fn D CVU_cauchy fn D.

Lemma CVU_dom_include (fn : natRR) (D1 D2 : RProp) :
  ( y, D2 yD1 y) → CVU_dom fn D1CVU_dom fn D2.

Limits, integrals and differentiability

Definition is_connected (D : RProp) :=
   a b x, D aD ba x bD x.

Lemma CVU_limits_open (fn : natRR) (D : RProp) :
  open D
  → CVU_dom fn D
  → ( x n, D xex_finite_lim (fn n) x)
  → x, D xex_finite_lim_seq (fun nreal (Lim (fn n) x))
     ex_finite_lim (fun yreal (Lim_seq (fun nfn n y))) x
     real (Lim_seq (fun nreal (Lim (fn n) x)))
      = real (Lim (fun yreal (Lim_seq (fun nfn n y))) x).
Lemma CVU_cont_open (fn : natRR) (D : RProp) :
  open D
  CVU_dom fn D
  ( n, x, D xcontinuity_pt (fn n) x)
    → x, D xcontinuity_pt (fun yreal (Lim_seq (fun nfn n y))) x.

Lemma CVU_Derive (fn : natRR) (D : RProp) :
  open Dis_connected D
  → CVU_dom fn D
  → ( n x, D xex_derive (fn n) x)
  → ( n x, D xcontinuity_pt (Derive (fn n)) x)
  → CVU_dom (fun n xDerive (fn n) x) D
  → ( x , D x
       (is_derive (fun yreal (Lim_seq (fun nfn n y))) x
         (real (Lim_seq (fun nDerive (fn n) x))))).

Dini's theorem

Lemma Dini (fn : natRR) (a b : R) :
  a < bCVS_dom fn (fun xa x b)
  → ( (n : nat) (x : R), a x bcontinuity_pt (fn n) x)
  → ( (x : R), a x bcontinuity_pt (fun yLim_seq (fun nfn n y)) x)
  → ( (n : nat) (x y : R), a xx yy bfn n x fn n y)
  → CVU_dom fn (fun xa x b).

Series of functions

Lemma CVN_CVU_r (fn : natRR) (r : posreal) :
  CVN_r fn r x, (Rabs x < r) → e : posreal,
    CVU (fun nSP fn n) (fun xSeries (fun nfn n x)) x e.