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.

Require Import Reals Psatz.
Require Import mathcomp.ssreflect.ssreflect mathcomp.ssreflect.ssrbool mathcomp.ssreflect.eqtype mathcomp.ssreflect.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 x ⇒ is_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 : R ⇒ is_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 : R ⇒ is_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 × R ⇒ is_RInt f (fst z) (snd z) (If (fst z) (snd z)))
  → continuous (fun z : R × R ⇒ If (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 × R ⇒ ex_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 ⇒ is_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 b ⇒ is_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 a ⇒ is_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 × R ⇒ is_RInt f (fst u) (snd u) (If (fst u) (snd u)))
  → continuous f a → continuous f b
  → filterdiff (fun u : R × R ⇒ If (fst u) (snd u)) (locally (a,b))
                (fun u : R × R ⇒ minus (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 a ⇒ ex_RInt f a b) → continuous f a
  → Derive (fun a ⇒ RInt 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 y ⇒ scal (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 y ⇒ scal (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 y ⇒ ex_RInt (f y) (a x) b) →
  (∃ eps : posreal, locally x (fun y ⇒ ex_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 y ⇒ ex_RInt (f y) (a x) (b x)) →
  (∃ eps : posreal, locally x (fun y ⇒ ex_RInt (f y) (a x - eps) (a x + eps))) →
  (∃ eps : posreal, locally x (fun y ⇒ ex_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 × R ⇒ is_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 x ⇒ If (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 : R ⇒ f u t) x) →
  (∀ t, Rmin a b ≤ t ≤ Rmax a b → continuity_2d_pt (fun u v ⇒ Derive (fun z ⇒ f z v) u) x t) →
  locally x (fun y : R ⇒ ex_RInt (fun t ⇒ f y t) a b) →
  ex_RInt (fun t ⇒ Derive (fun u ⇒ f u t) x) a b →
  is_derive (fun x : R ⇒ RInt (fun t ⇒ f x t) a b) x
    (RInt (fun t ⇒ Derive (fun u ⇒ f 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 u ⇒ f u t) x) →
  (∀ t, Rmin a b ≤ t ≤ Rmax a b → continuity_2d_pt (fun u v ⇒ Derive (fun z ⇒ f z v) u) x t) →
  locally x (fun y ⇒ ex_RInt (fun t ⇒ f y t) a b) →
  is_derive (fun x ⇒ RInt (fun t ⇒ f x t) a b) x
    (RInt (fun t ⇒ Derive (fun u ⇒ f 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 : R ⇒ ex_RInt (fun t ⇒ f 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 : R ⇒ f u t) x0)) →
  (locally_2d (fun x' t ⇒
         continuity_2d_pt (fun u v : R ⇒ Derive (fun z : R ⇒ f z v) u) x' t) x (a x)) →

  continuity_2d_pt
     (fun u v : R ⇒ Derive (fun z : R ⇒ RInt (fun t : R ⇒ f 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 : R ⇒ ex_RInt (fun t ⇒ f y t) (a x) b)) →
  (∃ eps:posreal, locally x (fun y : R ⇒ ex_RInt (fun t ⇒ f 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 : R ⇒ f u t) x0)) →
  (∀ t : R,
          Rmin (a x) b ≤ t ≤ Rmax (a x) b →
         continuity_2d_pt (fun u v : R ⇒ Derive (fun z : R ⇒ f z v) u) x t) →
  (locally_2d (fun x' t ⇒
         continuity_2d_pt (fun u v : R ⇒ Derive (fun z : R ⇒ f z v) u) x' t) x (a x)) →
   continuity_pt (fun t ⇒ f x t) (a x) →

  is_derive (fun x : R ⇒ RInt (fun t ⇒ f x t) (a x) b) x
    (RInt (fun t : R ⇒ Derive (fun u ⇒ f 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 : R ⇒ ex_RInt (fun t ⇒ f y t) a (b x))) →
  (∃ eps:posreal, locally x (fun y : R ⇒ ex_RInt (fun t ⇒ f 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 : R ⇒ f u t) x0)) →
  (∀ t : R,
          Rmin a (b x) ≤ t ≤ Rmax a (b x) →
         continuity_2d_pt (fun u v : R ⇒ Derive (fun z : R ⇒ f z v) u) x t) →
  (locally_2d (fun x' t ⇒
         continuity_2d_pt (fun u v : R ⇒ Derive (fun z : R ⇒ f z v) u) x' t) x (b x)) →
   continuity_pt (fun t ⇒ f x t) (b x) →

  is_derive (fun x : R ⇒ RInt (fun t ⇒ f x t) a (b x)) x
    (RInt (fun t : R ⇒ Derive (fun u ⇒ f 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 : R ⇒ ex_RInt (fun t ⇒ f y t) (a x) (b x))) →
  (∃ eps:posreal, locally x (fun y : R ⇒ ex_RInt (fun t ⇒ f y t) (a x - eps) (a x + eps))) →
  (∃ eps:posreal, locally x (fun y : R ⇒ ex_RInt (fun t ⇒ f 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 : R ⇒ f u t) x0)) →
  (∀ t : R,
          Rmin (a x) (b x) ≤ t ≤ Rmax (a x) (b x) →
         continuity_2d_pt (fun u v : R ⇒ Derive (fun z : R ⇒ f z v) u) x t) →
  (locally_2d (fun x' t ⇒
         continuity_2d_pt (fun u v : R ⇒ Derive (fun z : R ⇒ f z v) u) x' t) x (a x)) →
  (locally_2d (fun x' t ⇒
         continuity_2d_pt (fun u v : R ⇒ Derive (fun z : R ⇒ f z v) u) x' t) x (b x)) →
   continuity_pt (fun t ⇒ f x t) (a x) →
   continuity_pt (fun t ⇒ f x t) (b x) →

  is_derive (fun x : R ⇒ RInt (fun t ⇒ f x t) (a x) (b x)) x
    (RInt (fun t : R ⇒ Derive (fun u ⇒ f 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 n ⇒ a 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 t ⇒ plus (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 t ⇒ scal (f' t) (g t)) a b l →
  is_RInt (fun t ⇒ scal (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 t ⇒ scal (f t) (g' t)) a b l →
  is_RInt (fun t ⇒ scal (f' t) (g t)) a b (minus (minus (scal (f b) (g b)) (scal (f a) (g a))) l).

End ByParts.