Library Coquelicot.RInt_analysis

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
Copyright (C) 2016-2017 Thomas Sibut-Pinote
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 ssrbool.
From mathcomp Require Import eqtype seq.

Require Import Markov Rcomplements Rbar Lub Lim_seq Derive SF_seq.
Require Import Continuity Hierarchy Seq_fct RInt PSeries.

This file contains results about the integral as a function: continuity, differentiability, and composition. Theorems on parametric integrals are also provided.

Continuity


Section Continuity.

Context {V : NormedModule R_AbsRing}.

Lemma continuous_RInt_0 :
   (f : R V) (a : R) If,
    locally a (fun xis_RInt f a x (If x))
     continuous If a.

Lemma continuous_RInt_1 (f : R V) (a b : R) (If : R V) :
  locally b (fun z : Ris_RInt f a z (If z))
   continuous If b.
Lemma continuous_RInt_2 (f : R V) (a b : R) (If : R V) :
  locally a (fun z : Ris_RInt f z b (If z))
   continuous If a.
Lemma continuous_RInt (f : R V) (a b : R) (If : R R V) :
  locally (a,b) (fun z : R × Ris_RInt f (fst z) (snd z) (If (fst z) (snd z)))
   continuous (fun z : R × RIf (fst z) (snd z)) (a,b).

End Continuity.

Lemma ex_RInt_locally {V : CompleteNormedModule R_AbsRing} (f : R V) (a b : R) :
  ex_RInt f a b
   ( eps : posreal, ex_RInt f (a - eps) (a + eps))
   ( eps : posreal, ex_RInt f (b - eps) (b + eps))
   locally (a,b) (fun z : R × Rex_RInt f (fst z) (snd z)).

Riemann integral and differentiability


Section Derive.

Context {V : NormedModule R_AbsRing}.

Lemma is_derive_RInt_0 (f If : R V) (a : R) :
  locally a (fun b : Ris_RInt f a b (If b))
   continuous f a
   is_derive If a (f a).

Lemma is_derive_RInt (f If : R V) (a b : R) :
  locally b (fun bis_RInt f a b (If b))
   continuous f b
   is_derive If b (f b).

Lemma is_derive_RInt' (f If : R V) (a b : R) :
  locally a (fun ais_RInt f a b (If a))
   continuous f a
   is_derive If a (opp (f a)).

Lemma filterdiff_RInt (f : R V) (If : R R V) (a b : R) :
  locally (a,b) (fun u : R × Ris_RInt f (fst u) (snd u) (If (fst u) (snd u)))
   continuous f a continuous f b
   filterdiff (fun u : R × RIf (fst u) (snd u)) (locally (a,b))
                (fun u : R × Rminus (scal (snd u) (f b)) (scal (fst u) (f a))).

End Derive.

Lemma Derive_RInt (f : R R) (a b : R) :
  locally b (ex_RInt f a) continuous f b
   Derive (RInt f a) b = f b.
Lemma Derive_RInt' (f : R R) (a b : R) :
  locally a (fun aex_RInt f a b) continuous f a
   Derive (fun aRInt f a b) a = - f a.

Section Derive'.

Context {V : CompleteNormedModule R_AbsRing}.

Lemma is_RInt_derive (f df : R V) (a b : R) :
  ( x : R, Rmin a b x Rmax a b is_derive f x (df x))
  ( x : R, Rmin a b x Rmax a b continuous df x)
  is_RInt df a b (minus (f b) (f a)).

End Derive'.

Lemma RInt_Derive (f : R R) (a b : R):
  ( x, Rmin a b x Rmax a b ex_derive f x)
  ( x, Rmin a b x Rmax a b continuous (Derive f) x)
  RInt (Derive f) a b = f b - f a.

Composition


Section Comp.

Context {V : CompleteNormedModule R_AbsRing}.


Lemma IVT_gen_consistent (f : R R) (a b y : R) :
  ( x, continuous f x)
   Rmin (f a) (f b) y Rmax (f a) (f b)
   { x : R | Rmin a b x Rmax a b f x = y }.

Lemma continuous_ab_maj_consistent :
(f : R R) (a b : R),
a b
( c : R, a c b continuous f c)
Mx : R, ( c : R, a c b f c f Mx) a Mx b.

Lemma continuous_ab_min_consistent :
(f : R R) (a b : R),
a b
( c : R, a c b continuous f c)
mx : R, ( c : R, a c b f mx f c) a mx b.

Lemma is_RInt_comp (f : R V) (g dg : R R) (a b : R) :
  ( x, Rmin a b x Rmax a b continuous f (g x))
  ( x, Rmin a b x Rmax a b is_derive g x (dg x) continuous dg x)
  is_RInt (fun yscal (dg y) (f (g y))) a b (RInt f (g a) (g b)).

Lemma RInt_comp (f : R V) (g dg : R R) (a b : R) :
  ( x, Rmin a b x Rmax a b continuous f (g x))
  ( x, Rmin a b x Rmax a b is_derive g x (dg x) continuous dg x)
  RInt (fun yscal (dg y) (f (g y))) a b = RInt f (g a) (g b).

End Comp.

Lemma RInt_Chasles_bound_comp_l_loc (f : R R R) (a : R R) (b x : R) :
  locally x (fun yex_RInt (f y) (a x) b)
  ( eps : posreal, locally x (fun yex_RInt (f y) (a x - eps) (a x + eps)))
  continuous a x
  locally x (fun x'RInt (f x') (a x') (a x) + RInt (f x') (a x) b =
    RInt (f x') (a x') b).

Lemma RInt_Chasles_bound_comp_loc (f : R R R) (a b : R R) (x : R) :
  locally x (fun yex_RInt (f y) (a x) (b x))
  ( eps : posreal, locally x (fun yex_RInt (f y) (a x - eps) (a x + eps)))
  ( eps : posreal, locally x (fun yex_RInt (f y) (b x - eps) (b x + eps)))
  continuous a x
  continuous b x
  locally x (fun x'RInt (f x') (a x') (a x) + RInt (f x') (a x) (b x') =
    RInt (f x') (a x') (b x')).

Section RInt_comp.

Context {V : NormedModule R_AbsRing}.

Lemma is_derive_RInt_bound_comp (f : R V) (If : R R V) (a b : R R) (da db x : R) :
  locally (a x, b x)
    (fun u : R × Ris_RInt f (fst u) (snd u) (If (fst u) (snd u)))
  continuous f (a x)
  continuous f (b x)
  is_derive a x da
  is_derive b x db
  is_derive (fun xIf (a x) (b x)) x (minus (scal db (f (b x))) (scal da (f (a x)))).

End RInt_comp.

Parametric integrals


Lemma is_derive_RInt_param_aux : (f : R R R) (a b x : R),
  locally x (fun x : R t, Rmin a b t Rmax a b ex_derive (fun u : Rf u t) x)
  ( t, Rmin a b t Rmax a b continuity_2d_pt (fun u vDerive (fun zf z v) u) x t)
  locally x (fun y : Rex_RInt (fun tf y t) a b)
  ex_RInt (fun tDerive (fun uf u t) x) a b
  is_derive (fun x : RRInt (fun tf x t) a b) x
    (RInt (fun tDerive (fun uf u t) x) a b).

Lemma is_derive_RInt_param : f a b x,
  locally x (fun x t, Rmin a b t Rmax a b ex_derive (fun uf u t) x)
  ( t, Rmin a b t Rmax a b continuity_2d_pt (fun u vDerive (fun zf z v) u) x t)
  locally x (fun yex_RInt (fun tf y t) a b)
  is_derive (fun xRInt (fun tf x t) a b) x
    (RInt (fun tDerive (fun uf u t) x) a b).

Lemma is_derive_RInt_param_bound_comp_aux1 :
   (f : R R R) (a : R R) (x : R),
  ( eps:posreal, locally x (fun y : Rex_RInt (fun tf y t) (a x - eps) (a x + eps)))
  ( eps:posreal, locally x
    (fun x0 : R
        t : R,
        a x-eps t a x+eps
        ex_derive (fun u : Rf u t) x0))
  (locally_2d (fun x' t
         continuity_2d_pt (fun u v : RDerive (fun z : Rf z v) u) x' t) x (a x))

  continuity_2d_pt
     (fun u v : RDerive (fun z : RRInt (fun t : Rf z t) v (a x)) u) x (a x).

Lemma is_derive_RInt_param_bound_comp_aux2 :
   (f : R R R) (a : R R) (b x da : R),
  (locally x (fun y : Rex_RInt (fun tf y t) (a x) b))
  ( eps:posreal, locally x (fun y : Rex_RInt (fun tf y t) (a x - eps) (a x + eps)))
  is_derive a x da
  ( eps:posreal, locally x
    (fun x0 : R
        t : R,
        Rmin (a x-eps) b t Rmax (a x+eps) b
        ex_derive (fun u : Rf u t) x0))
  ( t : R,
          Rmin (a x) b t Rmax (a x) b
         continuity_2d_pt (fun u v : RDerive (fun z : Rf z v) u) x t)
  (locally_2d (fun x' t
         continuity_2d_pt (fun u v : RDerive (fun z : Rf z v) u) x' t) x (a x))
   continuity_pt (fun tf x t) (a x)

  is_derive (fun x : RRInt (fun tf x t) (a x) b) x
    (RInt (fun t : RDerive (fun uf u t) x) (a x) b+(-f x (a x))*da).

Lemma is_derive_RInt_param_bound_comp_aux3 :
   (f : R R R) a (b : R R) (x db : R),
  (locally x (fun y : Rex_RInt (fun tf y t) a (b x)))
  ( eps:posreal, locally x (fun y : Rex_RInt (fun tf y t) (b x - eps) (b x + eps)))
  is_derive b x db
  ( eps:posreal, locally x
    (fun x0 : R
        t : R,
        Rmin a (b x-eps) t Rmax a (b x+eps)
        ex_derive (fun u : Rf u t) x0))
  ( t : R,
          Rmin a (b x) t Rmax a (b x)
         continuity_2d_pt (fun u v : RDerive (fun z : Rf z v) u) x t)
  (locally_2d (fun x' t
         continuity_2d_pt (fun u v : RDerive (fun z : Rf z v) u) x' t) x (b x))
   continuity_pt (fun tf x t) (b x)

  is_derive (fun x : RRInt (fun tf x t) a (b x)) x
    (RInt (fun t : RDerive (fun uf u t) x) a (b x) +f x (b x)×db).

Lemma is_derive_RInt_param_bound_comp :
  (f : R R R) (a b : R R) (x da db : R),
  (locally x (fun y : Rex_RInt (fun tf y t) (a x) (b x)))
  ( eps:posreal, locally x (fun y : Rex_RInt (fun tf y t) (a x - eps) (a x + eps)))
  ( eps:posreal, locally x (fun y : Rex_RInt (fun tf y t) (b x - eps) (b x + eps)))
  is_derive a x da
  is_derive b x db
  ( eps:posreal, locally x
    (fun x0 : R
        t : R,
        Rmin (a x-eps) (b x -eps) t Rmax (a x+eps) (b x+eps)
        ex_derive (fun u : Rf u t) x0))
  ( t : R,
          Rmin (a x) (b x) t Rmax (a x) (b x)
         continuity_2d_pt (fun u v : RDerive (fun z : Rf z v) u) x t)
  (locally_2d (fun x' t
         continuity_2d_pt (fun u v : RDerive (fun z : Rf z v) u) x' t) x (a x))
  (locally_2d (fun x' t
         continuity_2d_pt (fun u v : RDerive (fun z : Rf z v) u) x' t) x (b x))
   continuity_pt (fun tf x t) (a x)
   continuity_pt (fun tf x t) (b x)

  is_derive (fun x : RRInt (fun tf x t) (a x) (b x)) x
    (RInt (fun t : RDerive (fun uf u t) x) (a x) (b x)+(-f x (a x))*da+(f x (b x))*db).

Power series


Definition PS_Int (a : nat R) (n : nat) : R :=
  match n with
    | O ⇒ 0
    | S na n / INR (S n)
  end.

Lemma CV_radius_Int (a : nat R) :
  CV_radius (PS_Int a) = CV_radius a.

Lemma is_RInt_PSeries (a : nat R) (x : R) :
  Rbar_lt (Rabs x) (CV_radius a)
   is_RInt (PSeries a) 0 x (PSeries (PS_Int a) x).

Lemma ex_RInt_PSeries (a : nat R) (x : R) :
  Rbar_lt (Rabs x) (CV_radius a)
   ex_RInt (PSeries a) 0 x.

Lemma RInt_PSeries (a : nat R) (x : R) :
  Rbar_lt (Rabs x) (CV_radius a)
   RInt (PSeries a) 0 x = PSeries (PS_Int a) x.

Lemma is_pseries_RInt (a : nat R) :
   x, Rbar_lt (Rabs x) (CV_radius a)
     is_pseries (PS_Int a) x (RInt (PSeries a) 0 x).

Integration by parts


Section ByParts.

Context {V : CompleteNormedModule R_AbsRing}.

Lemma is_RInt_scal_derive :
   (f : R R) (g : R V) (f' : R R) (g' : R V) (a b : R),
  ( t, Rmin a b t Rmax a b is_derive f t (f' t))
  ( t, Rmin a b t Rmax a b is_derive g t (g' t))
  ( t, Rmin a b t Rmax a b continuous f' t)
  ( t, Rmin a b t Rmax a b continuous g' t)
  is_RInt (fun tplus (scal (f' t) (g t)) (scal (f t) (g' t))) a b (minus (scal (f b) (g b)) (scal (f a) (g a))).

Lemma is_RInt_scal_derive_r :
   (f : R R) (g : R V) (f' : R R) (g' : R V) (a b : R) (l : V),
  ( t, Rmin a b t Rmax a b is_derive f t (f' t))
  ( t, Rmin a b t Rmax a b is_derive g t (g' t))
  ( t, Rmin a b t Rmax a b continuous f' t)
  ( t, Rmin a b t Rmax a b continuous g' t)
  is_RInt (fun tscal (f' t) (g t)) a b l
  is_RInt (fun tscal (f t) (g' t)) a b (minus (minus (scal (f b) (g b)) (scal (f a) (g a))) l).

Lemma is_RInt_scal_derive_l :
   (f : R R) (g : R V) (f' : R R) (g' : R V) (a b : R) (l : V),
  ( t, Rmin a b t Rmax a b is_derive f t (f' t))
  ( t, Rmin a b t Rmax a b is_derive g t (g' t))
  ( t, Rmin a b t Rmax a b continuous f' t)
  ( t, Rmin a b t Rmax a b continuous g' t)
  is_RInt (fun tscal (f t) (g' t)) a b l
  is_RInt (fun tscal (f' t) (g t)) a b (minus (minus (scal (f b) (g b)) (scal (f a) (g a))) l).

End ByParts.