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.

From Coq Require Import Reals Psatz ssreflect.
Require Import Rcomplements Rbar Lim_seq Continuity Derive Series Lub Hierarchy.

Local Tactic Notation "intuition" := (intuition auto with arith zarith real).

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

Open Scope R_scope.

Sequence of functions


Definition CVS_dom (fn : nat R R) (D : R Prop) :=
   x : R, D x ex_finite_lim_seq (fun nfn n x).

Definition CVU_dom (fn : nat R R) (D : R Prop) :=
   eps : posreal, eventually (fun n x : R,
    D x Rabs ((fn n x) - real (Lim_seq (fun nfn n x))) < eps).
Definition CVU_cauchy (fn : nat R R) (D : R Prop) :=
   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 : nat R R) (f : R R) (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 : nat R R) (D : R Prop) :
  CVU_dom fn D CVS_dom fn D.
Lemma CVU_dom_cauchy (fn : nat R R) (D : R Prop) :
  CVU_dom fn D CVU_cauchy fn D.

Lemma CVU_dom_include (fn : nat R R) (D1 D2 : R Prop) :
  ( y, D2 y D1 y) CVU_dom fn D1 CVU_dom fn D2.

Limits, integrals and differentiability

Definition is_connected (D : R Prop) :=
   a b x, D a D b a x b D x.

Lemma CVU_limits_open (fn : nat R R) (D : R Prop) :
  open D
   CVU_dom fn D
   ( x n, D x ex_finite_lim (fn n) x)
   x, D x ex_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 : nat R R) (D : R Prop) :
  open D
  CVU_dom fn D
  ( n, x, D x continuity_pt (fn n) x)
     x, D x continuity_pt (fun yreal (Lim_seq (fun nfn n y))) x.

Lemma CVU_Derive (fn : nat R R) (D : R Prop) :
  open D is_connected D
   CVU_dom fn D
   ( n x, D x ex_derive (fn n) x)
   ( n x, D x continuity_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 : nat R R) (a b : R) :
  a < b CVS_dom fn (fun xa x b)
   ( (n : nat) (x : R), a x b continuity_pt (fn n) x)
   ( (x : R), a x b continuity_pt (fun yLim_seq (fun nfn n y)) x)
   ( (n : nat) (x y : R), a x x y y b fn n x fn n y)
   CVU_dom fn (fun xa x b).

Series of functions

Lemma CVN_CVU_r (fn : nat R R) (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.