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
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.
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 : RV) (a : R) If,
    locally a (fun xis_RInt f a x (If x))
    → continuous If a.

Lemma continuous_RInt_1 (f : RV) (a b : R) (If : RV) :
  locally b (fun z : Ris_RInt f a z (If z))
  → continuous If b.
Lemma continuous_RInt_2 (f : RV) (a b : R) (If : RV) :
  locally a (fun z : Ris_RInt f z b (If z))
  → continuous If a.
Lemma continuous_RInt (f : RV) (a b : R) (If : RRV) :
  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.

Riemann integral and differentiability


Section Derive.

Context {V : NormedModule R_AbsRing}.

Lemma is_derive_RInt_0 (f If : RV) (a : R) :
  locally a (fun bis_RInt f a b (If b))
  → continuous f a
  → is_derive If a (f a).
Lemma is_derive_RInt (f If : RV) (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 : RV) (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 : RV) (If : RRV) (a b : R) :
  locally (a,b) (fun u : R × Ris_RInt f (fst u) (snd u) (If (fst u) (snd u)))
  → continuous f acontinuous 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 is_RInt_derive (f df : RR) (a b : R) :
  ( x : R, Rmin a b x Rmax a bis_derive f x (df x)) →
  ( x : R, Rmin a b x Rmax a bcontinuous df x) →
    is_RInt df a b (f b - f a)%R.

Lemma RInt_Derive (f : RR) (a b : R):
  ( x, Rmin a b x Rmax a bex_derive f x) →
  ( x, Rmin a b x Rmax a bcontinuous (Derive f) x) →
  RInt (Derive f) a b = f b - f a.

Composition


Lemma is_RInt_comp (f g dg : RR) (a b : R) :
  ( x, Rmin a b x Rmax a bcontinuous f (g x))
  → ( x, Rmin a b x Rmax a bis_derive g x (dg x) continuous dg x)
  → is_RInt (fun ydg y × f (g y)) a b (RInt f (g a) (g b)).

Lemma RInt_Chasles_bound_comp_l_loc :
   f a b x,
  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))) →
  continuity_pt 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 a b x,
  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))) →
  continuity_pt a x
  continuity_pt 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')).

Lemma is_derive_RInt_bound_comp :
   f a b da db x,
  ex_RInt f (a x) (b x) →
  ( eps : posreal, ex_RInt f (a x - eps) (a x + eps)) →
  ( eps : posreal, ex_RInt f (b x - eps) (b x + eps)) →
  continuity_pt f (a x) →
  continuity_pt f (b x) →
  is_derive a x da
  is_derive b x db
  is_derive (fun xRInt f (a x) (b x)) x (db × f (b x) - da × f (a x)).

Parametric integrals


Lemma is_derive_RInt_param_aux : f a b x,
  locally x (fun x t, Rmin a b t Rmax a bex_derive (fun uf u t) x) →
  ( t, Rmin a b t Rmax a bcontinuity_2d_pt (fun u vDerive (fun zf z v) u) x t) →
  locally x (fun yex_RInt (fun tf y t) a b) →
  ex_RInt (fun tDerive (fun uf u t) x) 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 : f a b x,
  locally x (fun x t, Rmin a b t Rmax a bex_derive (fun uf u t) x) →
  ( t, Rmin a b t Rmax a bcontinuity_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 a x,
  ( eps:posreal, locally x (fun yex_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 a b x da,
  (locally x (fun yex_RInt (fun tf y t) (a x) b)) →
  ( eps:posreal, locally x (fun yex_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 xRInt (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 a b x db,
  (locally x (fun yex_RInt (fun tf y t) a (b x))) →
  ( eps:posreal, locally x (fun yex_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 xRInt (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 a b x da db,
  (locally x (fun yex_RInt (fun tf y t) (a x) (b x))) →
  ( eps:posreal, locally x (fun yex_RInt (fun tf y t) (a x - eps) (a x + eps))) →
  ( eps:posreal, locally x (fun yex_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 xRInt (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 : natR) (n : nat) : R :=
  match n with
    | O ⇒ 0
    | S na n / INR (S n)
  end.

Lemma CV_radius_Int (a : natR) :
  CV_radius (PS_Int a) = CV_radius a.

Lemma is_RInt_PSeries (a : natR) (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 : natR) (x : R) :
  Rbar_lt (Rabs x) (CV_radius a)
  → ex_RInt (PSeries a) 0 x.

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

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