Library Coquelicot.Continuity

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.

Require Import Reals.
Require Import Ssreflect.ssreflect.
Require Import Rcomplements Rbar Hierarchy.
Require Import Compactness Lim_seq.

This file describes defineitions and properties of continuity on R and on uniform spaces. It also contains many results about the limit of a real function (predicates is_lim and ex_lim and total function Lim). This limit may be either a real or an extended real.

Limit of fonctions

Definition


Definition is_lim (f : RR) (x l : Rbar) :=
  filterlim f (Rbar_locally' x) (Rbar_locally l).

Definition is_lim' (f : RR) (x l : Rbar) :=
  match l with
    | Finite l
       eps : posreal, Rbar_locally' x (fun yRabs (f y - l) < eps)
    | p_infty M : R, Rbar_locally' x (fun yM < f y)
    | m_infty M : R, Rbar_locally' x (fun yf y < M)
  end.
Definition ex_lim (f : RR) (x : Rbar) := l : Rbar, is_lim f x l.
Definition ex_finite_lim (f : RR) (x : Rbar) := l : R, is_lim f x l.
Definition Lim (f : RR) (x : Rbar) := Lim_seq (fun nf (Rbar_loc_seq x n)).

Lemma is_lim_spec :
   f x l,
  is_lim' f x l is_lim f x l.

Equivalence with standard library Reals

Lemma is_lim_Reals_0 (f : RR) (x l : R) :
  is_lim f x llimit1_in f (fun yy x) l x.
Lemma is_lim_Reals_1 (f : RR) (x l : R) :
  limit1_in f (fun yy x) l xis_lim f x l.
Lemma is_lim_Reals (f : RR) (x l : R) :
  is_lim f x l limit1_in f (fun yy x) l x.

Composition

Lemma is_lim_comp' :
   {T} {F} {FF : @Filter T F} (f : TR) (g : RR) (x l : Rbar),
  filterlim f F (Rbar_locally x) → is_lim g x l
  F (fun yFinite (f y) x) →
  filterlim (fun yg (f y)) F (Rbar_locally l).

Lemma is_lim_comp_seq (f : RR) (u : natR) (x l : Rbar) :
  is_lim f x l
  eventually (fun nFinite (u n) x) →
  is_lim_seq u xis_lim_seq (fun nf (u n)) l.

Uniqueness

Lemma is_lim_unique (f : RR) (x l : Rbar) :
  is_lim f x lLim f x = l.
Lemma Lim_correct (f : RR) (x : Rbar) :
  ex_lim f xis_lim f x (Lim f x).

Lemma ex_finite_lim_correct (f : RR) (x : Rbar) :
  ex_finite_lim f x ex_lim f x is_finite (Lim f x).
Lemma Lim_correct' (f : RR) (x : Rbar) :
  ex_finite_lim f xis_lim f x (real (Lim f x)).

Operations and order

Extensionality

Lemma is_lim_ext_loc (f g : RR) (x l : Rbar) :
  Rbar_locally' x (fun yf y = g y)
  → is_lim f x lis_lim g x l.
Lemma ex_lim_ext_loc (f g : RR) (x : Rbar) :
  Rbar_locally' x (fun yf y = g y)
  → ex_lim f xex_lim g x.
Lemma Lim_ext_loc (f g : RR) (x : Rbar) :
  Rbar_locally' x (fun yf y = g y)
  → Lim g x = Lim f x.

Lemma is_lim_ext (f g : RR) (x l : Rbar) :
  ( y, f y = g y)
  → is_lim f x lis_lim g x l.
Lemma ex_lim_ext (f g : RR) (x : Rbar) :
  ( y, f y = g y)
  → ex_lim f xex_lim g x.
Lemma Lim_ext (f g : RR) (x : Rbar) :
  ( y, f y = g y)
  → Lim g x = Lim f x.

Composition

Lemma is_lim_comp (f g : RR) (x k l : Rbar) :
  is_lim f l kis_lim g x lRbar_locally' x (fun yFinite (g y) l)
    → is_lim (fun xf (g x)) x k.
Lemma ex_lim_comp (f g : RR) (x : Rbar) :
  ex_lim f (Lim g x) → ex_lim g xRbar_locally' x (fun yFinite (g y) Lim g x)
    → ex_lim (fun xf (g x)) x.
Lemma Lim_comp (f g : RR) (x : Rbar) :
  ex_lim f (Lim g x) → ex_lim g xRbar_locally' x (fun yFinite (g y) Lim g x)
    → Lim (fun xf (g x)) x = Lim f (Lim g x).

Identity

Lemma is_lim_id (x : Rbar) :
  is_lim (fun yy) x x.
Lemma ex_lim_id (x : Rbar) :
  ex_lim (fun yy) x.
Lemma Lim_id (x : Rbar) :
  Lim (fun yy) x = x.

Constant

Lemma is_lim_const (a : R) (x : Rbar) :
  is_lim (fun _a) x a.
Lemma ex_lim_const (a : R) (x : Rbar) :
  ex_lim (fun _a) x.
Lemma Lim_const (a : R) (x : Rbar) :
  Lim (fun _a) x = a.

Additive operators

Opposite

Lemma is_lim_opp (f : RR) (x l : Rbar) :
  is_lim f x lis_lim (fun y- f y) x (Rbar_opp l).
Lemma ex_lim_opp (f : RR) (x : Rbar) :
  ex_lim f xex_lim (fun y- f y) x.
Lemma Lim_opp (f : RR) (x : Rbar) :
  Lim (fun y- f y) x = Rbar_opp (Lim f x).

Addition

Lemma is_lim_plus (f g : RR) (x lf lg l : Rbar) :
  is_lim f x lfis_lim g x lg
  is_Rbar_plus lf lg l
  is_lim (fun yf y + g y) x l.
Lemma is_lim_plus' (f g : RR) (x : Rbar) (lf lg : R) :
  is_lim f x lfis_lim g x lg
  is_lim (fun yf y + g y) x (lf + lg).
Lemma ex_lim_plus (f g : RR) (x : Rbar) :
  ex_lim f xex_lim g x
  ex_Rbar_plus (Lim f x) (Lim g x) →
  ex_lim (fun yf y + g y) x.
Lemma Lim_plus (f g : RR) (x : Rbar) :
  ex_lim f xex_lim g x
  ex_Rbar_plus (Lim f x) (Lim g x) →
  Lim (fun yf y + g y) x = Rbar_plus (Lim f x) (Lim g x).

Subtraction

Lemma is_lim_minus (f g : RR) (x lf lg l : Rbar) :
  is_lim f x lfis_lim g x lg
  is_Rbar_minus lf lg l
  is_lim (fun yf y - g y) x l.
Lemma is_lim_minus' (f g : RR) (x : Rbar) (lf lg : R) :
  is_lim f x lfis_lim g x lg
  is_lim (fun yf y - g y) x (lf - lg).
Lemma ex_lim_minus (f g : RR) (x : Rbar) :
  ex_lim f xex_lim g x
  ex_Rbar_minus (Lim f x) (Lim g x) →
  ex_lim (fun yf y - g y) x.
Lemma Lim_minus (f g : RR) (x : Rbar) :
  ex_lim f xex_lim g x
  ex_Rbar_minus (Lim f x) (Lim g x) →
  Lim (fun yf y - g y) x = Rbar_minus (Lim f x) (Lim g x).

Multiplicative operators

Multiplicative inverse

Lemma is_lim_inv (f : RR) (x l : Rbar) :
  is_lim f x ll 0 → is_lim (fun y/ f y) x (Rbar_inv l).
Lemma ex_lim_inv (f : RR) (x : Rbar) :
  ex_lim f xLim f x 0 → ex_lim (fun y/ f y) x.
Lemma Lim_inv (f : RR) (x : Rbar) :
  ex_lim f xLim f x 0 → Lim (fun y/ f y) x = Rbar_inv (Lim f x).

Multiplication

Lemma is_lim_mult (f g : RR) (x lf lg : Rbar) :
  is_lim f x lfis_lim g x lg
  ex_Rbar_mult lf lg
  is_lim (fun yf y × g y) x (Rbar_mult lf lg).
Lemma ex_lim_mult (f g : RR) (x : Rbar) :
  ex_lim f xex_lim g x
  ex_Rbar_mult (Lim f x) (Lim g x) →
  ex_lim (fun yf y × g y) x.
Lemma Lim_mult (f g : RR) (x : Rbar) :
  ex_lim f xex_lim g x
  ex_Rbar_mult (Lim f x) (Lim g x) →
  Lim (fun yf y × g y) x = Rbar_mult (Lim f x) (Lim g x).

Scalar multiplication

Lemma is_lim_scal_l (f : RR) (a : R) (x l : Rbar) :
  is_lim f x lis_lim (fun ya × f y) x (Rbar_mult a l).
Lemma ex_lim_scal_l (f : RR) (a : R) (x : Rbar) :
  ex_lim f xex_lim (fun ya × f y) x.
Lemma Lim_scal_l (f : RR) (a : R) (x : Rbar) :
  Lim (fun ya × f y) x = Rbar_mult a (Lim f x).

Lemma is_lim_scal_r (f : RR) (a : R) (x l : Rbar) :
  is_lim f x lis_lim (fun yf y × a) x (Rbar_mult l a).
Lemma ex_lim_scal_r (f : RR) (a : R) (x : Rbar) :
  ex_lim f xex_lim (fun yf y × a) x.
Lemma Lim_scal_r (f : RR) (a : R) (x : Rbar) :
  Lim (fun yf y × a) x = Rbar_mult (Lim f x) a.

Division

Lemma is_lim_div (f g : RR) (x lf lg : Rbar) :
  is_lim f x lfis_lim g x lglg 0 →
  ex_Rbar_div lf lg
  is_lim (fun yf y / g y) x (Rbar_div lf lg).
Lemma ex_lim_div (f g : RR) (x : Rbar) :
  ex_lim f xex_lim g xLim g x 0 →
  ex_Rbar_div (Lim f x) (Lim g x) →
  ex_lim (fun yf y / g y) x.
Lemma Lim_div (f g : RR) (x : Rbar) :
  ex_lim f xex_lim g xLim g x 0 →
  ex_Rbar_div (Lim f x) (Lim g x) →
  Lim (fun yf y / g y) x = Rbar_div (Lim f x) (Lim g x).

Composition by linear functions

Lemma is_lim_comp_lin (f : RR) (a b : R) (x l : Rbar) :
  is_lim f (Rbar_plus (Rbar_mult a x) b) la 0
  → is_lim (fun yf (a × y + b)) x l.
Lemma ex_lim_comp_lin (f : RR) (a b : R) (x : Rbar) :
  ex_lim f (Rbar_plus (Rbar_mult a x) b)
  → ex_lim (fun yf (a × y + b)) x.
Lemma Lim_comp_lin (f : RR) (a b : R) (x : Rbar) :
  ex_lim f (Rbar_plus (Rbar_mult a x) b) → a 0 →
  Lim (fun yf (a × y + b)) x = Lim f (Rbar_plus (Rbar_mult a x) b).

Continuity and limit

Lemma is_lim_continuity (f : RR) (x : R) :
  continuity_pt f xis_lim f x (f x).
Lemma ex_lim_continuity (f : RR) (x : R) :
  continuity_pt f xex_finite_lim f x.
Lemma Lim_continuity (f : RR) (x : R) :
  continuity_pt f xLim f x = f x.

Lemma C0_extension_right {T : UniformSpace} (f : RT) lb (a b : R) :
   a < b
   ( c : R, a < c < bfilterlim f (locally c) (locally (f c))) →
   (filterlim f (at_left b) (locally lb)) →
   {g : RT | ( c, a < cfilterlim g (locally c) (locally (g c)))
      ( c : R, c < bg c = f c) g b = lb}.
Lemma filterlim_Ropp_left (x : R) :
  filterlim Ropp (at_left x) (at_right (- x)).
Lemma filterlim_Ropp_right (x : R) :
  filterlim Ropp (at_right x) (at_left (- x)).

Lemma C0_extension_left {T : UniformSpace} (f : RT) la (a b : R) :
   a < b
   ( c : R, a < c < bfilterlim f (locally c) (locally (f c))) →
   (filterlim f (at_right a) (locally la)) →
   {g : RT | ( c, c < bfilterlim g (locally c) (locally (g c)))
      ( c : R, a < cg c = f c) g a = la}.

Lemma C0_extension_lt {T : UniformSpace} (f : RT) la lb (a b : R) :
  a < b
   ( c : R, a < c < bfilterlim f (locally c) (locally (f c))) →
   (filterlim f (at_right a) (locally la)) →
   (filterlim f (at_left b) (locally lb)) →
   {g : RT | ( c, filterlim g (locally c) (locally (g c)))
      ( c : R, a < c < bg c = f c) g a = la g b = lb}.

Lemma C0_extension_le {T : UniformSpace} (f : RT) (a b : R) :
   ( c : R, a c bfilterlim f (locally c) (locally (f c))) →
   {g : RT | ( c, filterlim g (locally c) (locally (g c)))
      ( c : R, a c bg c = f c)}.

Lemma bounded_continuity {K : AbsRing} {V : NormedModule K}
  (f : RV) a b :
  ( x, a x bfilterlim f (locally x) (locally (f x)))
  → {M : R | x, a x bnorm (f x) < M}.

Order


Lemma is_lim_le_loc (f g : RR) (x lf lg : Rbar) :
  Rbar_locally' x (fun yf y g y) →
  is_lim f x lfis_lim g x lg
  Rbar_le lf lg.

Lemma is_lim_le_p_loc (f g : RR) (x : Rbar) :
  Rbar_locally' x (fun yf y g y) →
  is_lim f x p_infty
  is_lim g x p_infty.

Lemma is_lim_le_m_loc (f g : RR) (x : Rbar) :
  Rbar_locally' x (fun yg y f y) →
  is_lim f x m_infty
  is_lim g x m_infty.

Lemma is_lim_le_le_loc (f g h : RR) (x : Rbar) (l : Rbar) :
  Rbar_locally' x (fun yf y h y g y) →
  is_lim f x lis_lim g x l
  is_lim h x l.

Generalized intermediate value theorem


Lemma IVT_gen (f : RR) (a b y : R) :
  Ranalysis1.continuity f
  → Rmin (f a) (f b) y Rmax (f a) (f b)
  → { x : R | Rmin a b x Rmax a b f x = y }.

Lemma IVT_Rbar_incr (f : RR) (a b la lb : Rbar) (y : R) :
  is_lim f a lais_lim f b lb
  → ( (x : R), Rbar_lt a xRbar_lt x bcontinuity_pt f x)
  → Rbar_lt a b
  → Rbar_lt la y Rbar_lt y lb
  → {x : R | Rbar_lt a x Rbar_lt x b f x = y}.

Lemma IVT_Rbar_decr (f : RR) (a b la lb : Rbar) (y : R) :
  is_lim f a lais_lim f b lb
  → ( (x : R), Rbar_lt a xRbar_lt x bcontinuity_pt f x)
  → Rbar_lt a b
  → Rbar_lt lb y Rbar_lt y la
  → {x : R | Rbar_lt a x Rbar_lt x b f x = y}.

2D-continuity

Definitions


Definition continuity_2d_pt f x y :=
   eps : posreal, locally_2d (fun u vRabs (f u v - f x y) < eps) x y.

Lemma continuity_2d_pt_filterlim :
   f x y,
  continuity_2d_pt f x y
  filterlim (fun z : R × Rf (fst z) (snd z)) (locally (x,y)) (locally (f x y)).

Lemma uniform_continuity_2d :
   f a b c d,
  ( x y, a x bc y dcontinuity_2d_pt f x y) →
   eps : posreal, delta : posreal,
   x y u v,
  a x bc y d
  a u bc v d
  Rabs (u - x) < deltaRabs (v - y) < delta
  Rabs (f u v - f x y) < eps.

Lemma uniform_continuity_2d_1d :
   f a b c,
  ( x, a x bcontinuity_2d_pt f x c) →
   eps : posreal, delta : posreal,
   x y u v,
  a x bc - delta y c + delta
  a u bc - delta v c + delta
  Rabs (u - x) < delta
  Rabs (f u v - f x y) < eps.

Lemma uniform_continuity_2d_1d' :
   f a b c,
  ( x, a x bcontinuity_2d_pt f c x) →
   eps : posreal, delta : posreal,
   x y u v,
  a x bc - delta y c + delta
  a u bc - delta v c + delta
  Rabs (u - x) < delta
  Rabs (f v u - f y x) < eps.

Lemma continuity_2d_pt_neq_0 :
   f x y,
  continuity_2d_pt f x yf x y 0 →
  locally_2d (fun u vf u v 0) x y.

Operations

Identity

Lemma continuity_pt_id :
   x, continuity_pt (fun xx) x.

Lemma continuity_2d_pt_id1 :
   x y, continuity_2d_pt (fun u vu) x y.

Lemma continuity_2d_pt_id2 :
   x y, continuity_2d_pt (fun u vv) x y.

Constant functions

Lemma continuity_2d_pt_const :
   x y c, continuity_2d_pt (fun u vc) x y.

Extensionality


Lemma continuity_pt_ext_loc :
   f g x,
  locally x (fun xf x = g x) →
  continuity_pt f xcontinuity_pt g x.

Lemma continuity_pt_ext :
   f g x,
  ( x, f x = g x) →
  continuity_pt f xcontinuity_pt g x.

Lemma continuity_2d_pt_ext_loc :
   f g x y,
  locally_2d (fun u vf u v = g u v) x y
  continuity_2d_pt f x ycontinuity_2d_pt g x y.

Lemma continuity_2d_pt_ext :
   f g x y,
  ( x y, f x y = g x y) →
  continuity_2d_pt f x ycontinuity_2d_pt g x y.

Composition


Lemma continuity_1d_2d_pt_comp :
   f g x y,
  continuity_pt f (g x y) →
  continuity_2d_pt g x y
  continuity_2d_pt (fun x yf (g x y)) x y.

Additive operators


Lemma continuity_2d_pt_opp (f : RRR) (x y : R) :
  continuity_2d_pt f x y
  continuity_2d_pt (fun u v- f u v) x y.

Lemma continuity_2d_pt_plus (f g : RRR) (x y : R) :
  continuity_2d_pt f x y
  continuity_2d_pt g x y
  continuity_2d_pt (fun u vf u v + g u v) x y.

Lemma continuity_2d_pt_minus (f g : RRR) (x y : R) :
  continuity_2d_pt f x y
  continuity_2d_pt g x y
  continuity_2d_pt (fun u vf u v - g u v) x y.

Multiplicative operators


Lemma continuity_2d_pt_inv (f : RRR) (x y : R) :
  continuity_2d_pt f x y
  f x y 0 →
  continuity_2d_pt (fun u v/ f u v) x y.

Lemma continuity_2d_pt_mult (f g : RRR) (x y : R) :
  continuity_2d_pt f x y
  continuity_2d_pt g x y
  continuity_2d_pt (fun u vf u v × g u v) x y.

Continuity in Uniform Spaces

Continuity


Section Continuity.

Context {T U : UniformSpace}.

Definition continuous_on (D : TProp) (f : TU) :=
   x, D xfilterlim f (within D (locally x)) (locally (f x)).

Definition continuous (f : TU) (x : T) :=
  filterlim f (locally x) (locally (f x)).

Lemma continuous_continuous_on :
   (D : TProp) (f : TU) (x : T),
  locally x D
  continuous_on D f
  continuous f x.

Lemma continuous_on_subset :
   (D E : TProp) (f : TU),
  ( x, E xD x) →
  continuous_on D f
  continuous_on E f.

Lemma continuous_on_forall :
   (D : TProp) (f : TU),
  ( x, D xcontinuous f x) →
  continuous_on D f.

Lemma continuous_ext_loc (f g : TU) (x : T) :
  locally x (fun y : Tg y = f y)
  → continuous g xcontinuous f x.
Lemma continuous_ext :
   (f g : TU) (x : T),
  ( x, f x = g x) →
  continuous f x
  continuous g x.

Lemma continuous_on_ext :
   (D : TProp) (f g : TU),
  ( x, D xf x = g x) →
  continuous_on D f
  continuous_on D g.

End Continuity.

Lemma continuous_comp {U V W : UniformSpace} (f : UV) (g : VW) (x : U) :
  continuous f xcontinuous g (f x)
  → continuous (fun xg (f x)) x.
Lemma continuous_comp_2 {U V W X : UniformSpace}
  (f : UV) (g : UW) (h : VWX) (x : U) :
  continuous f xcontinuous g x
  → continuous (fun (x : V × W) ⇒ h (fst x) (snd x)) (f x,g x)
  → continuous (fun xh (f x) (g x)) x.

Lemma is_lim_comp_continuous (f g : RR) (x : Rbar) (l : R) :
  is_lim f x lcontinuous g l
    → is_lim (fun xg (f x)) x (g l).

Lemma continuous_fst {U V : UniformSpace} (x : U) (y : V) :
  continuous (fst (B:=V)) (x, y).
Lemma continuous_snd {U V : UniformSpace} (x : U) (y : V) :
  continuous (snd (B:=V)) (x, y).

Lemma continuous_const {U V : UniformSpace} (c : V) (x : U) :
  continuous (fun _c) x.

Lemma continuous_id {U : UniformSpace} (x : U) :
  continuous (fun yy) x.

Section Continuity_op.

Context {U : UniformSpace} {K : AbsRing} {V : NormedModule K}.

Lemma continuous_opp (f : UV) (x : U) :
  continuous f x
  continuous (fun x : Uopp (f x)) x.

Lemma continuous_plus (f g : UV) (x : U) :
  continuous f xcontinuous g x
  continuous (fun x : Uplus (f x) (g x)) x.

Lemma continuous_minus (f g : UV) (x : U) :
  continuous f xcontinuous g x
  continuous (fun x : Uminus (f x) (g x)) x.

Lemma continuous_scal (k : UK) (f : UV) (x : U) :
  continuous k xcontinuous f xcontinuous (fun yscal (k y) (f y)) x.
Lemma continuous_scal_r (k : K) (f : UV) (x : U) :
  continuous f xcontinuous (fun yscal k (f y)) x.
Lemma continuous_scal_l (f : UK) (k : V) (x : U) :
  continuous f xcontinuous (fun yscal (f y) k) x.

End Continuity_op.

Lemma continuous_mult {U : UniformSpace} {K : AbsRing}
  (f g : UK) (x : U) :
  continuous f xcontinuous g x
  → continuous (fun ymult (f y) (g y)) x.

Section UnifCont.

Context {V : UniformSpace}.

Lemma unifcont_1d (f : RV) a b :
  ( x, a x bcontinuous f x) →
   eps : posreal, {delta : posreal | x y,
    a x ba y bball x delta y~~ ball (f x) eps (f y)}.

End UnifCont.

Section UnifCont_N.

Context {K : AbsRing} {V : NormedModule K}.

Lemma unifcont_normed_1d (f : RV) a b :
  ( x, a x bcontinuous f x) →
   eps : posreal, {delta : posreal | x y,
    a x ba y bball x delta yball_norm (f x) eps (f y)}.

End UnifCont_N.