Library Coquelicot.Seq_fct
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/
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.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
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.
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.
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))))).
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).