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.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
Copyright (C) 2016-2017 Thomas Sibut-Pinote
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 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)).
Section Derive.
Context {V : NormedModule R_AbsRing}.
Lemma is_derive_RInt_0 (f If : R → V) (a : R) :
locally a (fun b : R ⇒ 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.
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.
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).
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).
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.