Library Coquelicot.Seq_fct

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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 Psatz.
Require Import mathcomp.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

Definitions

Definition CVS_dom (fn : nat → R → R) (D : R → Prop) :=
  ∀ x : R, D x → ex_finite_lim_seq (fun n ⇒ fn 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 n ⇒ fn 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 n ⇒ fn 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 n ⇒ real (Lim (fn n) x))
    ∧ ex_finite_lim (fun y ⇒ real (Lim_seq (fun n ⇒ fn n y))) x
    ∧ real (Lim_seq (fun n ⇒ real (Lim (fn n) x)))
      = real (Lim (fun y ⇒ real (Lim_seq (fun n ⇒ fn 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 y ⇒ real (Lim_seq (fun n ⇒ fn 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 x ⇒ Derive (fn n) x) D
  → (∀ x , D x →
       (is_derive (fun y ⇒ real (Lim_seq (fun n ⇒ fn n y))) x
         (real (Lim_seq (fun n ⇒ Derive (fn n) x))))).

Dini's theorem

Lemma Dini (fn : nat → R → R) (a b : R) :
  a < b → CVS_dom fn (fun x ⇒ a ≤ x ≤ b)
  → (∀ (n : nat) (x : R), a ≤ x ≤ b → continuity_pt (fn n) x )
  → (∀ (x : R), a ≤ x ≤ b → continuity_pt (fun y ⇒ Lim_seq (fun n ⇒ fn n y)) x )
  → (∀ (n : nat) (x y : R), a ≤ x → x ≤ y → y ≤ b → fn n x ≤ fn n y )
  → CVU_dom fn (fun x ⇒ a ≤ 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 n ⇒ SP fn n) (fun x ⇒ Series (fun n ⇒ fn n x)) x e.