Library Coquelicot.RInt

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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 SF_seq.
Require Import Continuity Hierarchy.

This file contains the definition and properties of the Riemann integral, defined on a normed module on R. For real functions, a total function RInt is available.

Section is_RInt.

Definition of Riemann integral

Context {V : NormedModule R_AbsRing}.

Definition is_RInt (f : R → V) (a b : R) (If : V) :=
filterlim (fun ptd ⇒ scal (sign (b -a)) (Riemann_sum f ptd)) (Riemann_fine a b) (locally If).

Definition ex_RInt (f : R → V) (a b : R) :=
∃ If : V , is_RInt f a b If.

Usual properties

The integral between a and a is null

Lemma is_RInt_point :
  ∀ (f : R → V) (a : R),
  is_RInt f a a zero.

Lemma ex_RInt_point :
  ∀ (f : R → V) a,
  ex_RInt f a a.

Swapping bounds

Lemma is_RInt_swap :
  ∀ (f : R → V) (a b : R) (If : V),
  is_RInt f b a If → is_RInt f a b (opp If).

Lemma ex_RInt_swap :
  ∀ (f : R → V) (a b : R),
  ex_RInt f a b → ex_RInt f b a.

Integrable implies bounded

Lemma ex_RInt_ub (f : R → V) (a b : R) :
ex_RInt f a b → ∃ M : R , ∀ t : R,
Rmin a b ≤ t ≤ Rmax a b → norm (f t) ≤ M.

Extensionality

Lemma is_RInt_ext :
  ∀ (f g : R → V) (a b : R) (l : V),
  (∀ x, Rmin a b < x < Rmax a b → f x = g x ) →
  is_RInt f a b l → is_RInt g a b l.

Lemma ex_RInt_ext :
  ∀ (f g : R → V) (a b : R),
  (∀ x, Rmin a b < x < Rmax a b → f x = g x ) →
  ex_RInt f a b → ex_RInt g a b.

Constant functions

Lemma is_RInt_const :
  ∀ (a b : R) (v : V),
  is_RInt (fun _ ⇒ v) a b (scal (b - a) v).

Lemma ex_RInt_const :
  ∀ (a b : R) (v : V),
  ex_RInt (fun _ ⇒ v) a b.

Composition

Lemma is_RInt_comp_opp :
  ∀ (f : R → V) (a b : R) (l : V),
  is_RInt f (-a) (-b) l →
  is_RInt (fun y ⇒ opp (f (- y))) a b l.

Lemma ex_RInt_comp_opp :
  ∀ (f : R → V) (a b : R),
  ex_RInt f (-a) (-b) →
  ex_RInt (fun y ⇒ opp (f (- y))) a b.

Lemma is_RInt_comp_lin
  (f : R → V) (u v a b : R) (l : V) :
  is_RInt f (u × a + v) (u × b + v) l
    → is_RInt (fun y ⇒ scal u (f (u × y + v))) a b l.

Lemma ex_RInt_comp_lin (f : R → V) (u v a b : R) :
  ex_RInt f (u × a + v) (u × b + v)
    → ex_RInt (fun y ⇒ scal u (f (u × y + v))) a b.

Chasles

Lemma is_RInt_Chasles_0 (f : R → V) (a b c : R) (l1 l2 : V) :
  a < b < c → is_RInt f a b l1 → is_RInt f b c l2
  → is_RInt f a c (plus l1 l2).

Lemma ex_RInt_Chasles_0 (f : R → V) (a b c : R) :
  a ≤ b ≤ c → ex_RInt f a b → ex_RInt f b c
  → ex_RInt f a c.

Lemma is_RInt_Chasles_1 (f : R → V) (a b c : R) l1 l2 :
  a < b < c → is_RInt f a c l1 → is_RInt f b c l2 → is_RInt f a b (minus l1 l2).

Lemma is_RInt_Chasles_2 (f : R → V) (a b c : R) l1 l2 :
  a < b < c → is_RInt f a c l1 → is_RInt f a b l2 → is_RInt f b c (minus l1 l2).

Lemma is_RInt_Chasles (f : R → V) (a b c : R) (l1 l2 : V) :
  is_RInt f a b l1 → is_RInt f b c l2
  → is_RInt f a c (plus l1 l2).
Lemma ex_RInt_Chasles (f : R → V) (a b c : R) :
  ex_RInt f a b → ex_RInt f b c → ex_RInt f a c.

Operations

Lemma is_RInt_scal :
  ∀ (f : R → V) (a b : R) (k : R) (If : V),
  is_RInt f a b If →
  is_RInt (fun y ⇒ scal k (f y)) a b (scal k If).

Lemma ex_RInt_scal :
  ∀ (f : R → V) (a b : R) (k : R),
  ex_RInt f a b →
  ex_RInt (fun y ⇒ scal k (f y)) a b.

Lemma is_RInt_opp :
  ∀ (f : R → V) (a b : R) (If : V),
  is_RInt f a b If →
  is_RInt (fun y ⇒ opp (f y)) a b (opp If).

Lemma ex_RInt_opp :
  ∀ (f : R → V) (a b : R),
  ex_RInt f a b →
  ex_RInt (fun x ⇒ opp (f x)) a b.

Lemma is_RInt_plus :
  ∀ (f g : R → V) (a b : R) (If Ig : V),
  is_RInt f a b If →
  is_RInt g a b Ig →
  is_RInt (fun y ⇒ plus (f y) (g y)) a b (plus If Ig).

Lemma ex_RInt_plus :
  ∀ (f g : R → V) (a b : R),
  ex_RInt f a b →
  ex_RInt g a b →
  ex_RInt (fun y ⇒ plus (f y) (g y)) a b.

Lemma is_RInt_minus :
  ∀ (f g : R → V) (a b : R) (If Ig : V),
  is_RInt f a b If →
  is_RInt g a b Ig →
  is_RInt (fun y ⇒ minus (f y) (g y)) a b (minus If Ig).

Lemma ex_RInt_minus :
  ∀ (f g : R → V) (a b : R),
  ex_RInt f a b →
  ex_RInt g a b →
  ex_RInt (fun y ⇒ minus (f y) (g y)) a b.

End is_RInt.

Lemma ex_RInt_Chasles_1 {V : CompleteNormedModule R_AbsRing}
  (f : R → V) (a b c : R) :
  a ≤ b ≤ c → ex_RInt f a c → ex_RInt f a b.

Lemma ex_RInt_Chasles_2 {V : CompleteNormedModule R_AbsRing}
  (f : R → V) (a b c : R) :
   a ≤ b ≤ c → ex_RInt f a c → ex_RInt f b c.

Lemma ex_RInt_inside {V : CompleteNormedModule R_AbsRing} :
  ∀ (f : R → V) (a b x e : R),
  ex_RInt f (x -e) (x +e) → Rabs (a -x) ≤ e → Rabs (b -x) ≤ e →
  ex_RInt f a b.

Exchange limit and integral

Lemma filterlim_RInt {U} {V : CompleteNormedModule R_AbsRing} :
  ∀ (f : U → R → V) (a b : R) F (FF : ProperFilter F)
    g h,
  (∀ x, is_RInt (f x) a b (h x))
  → (filterlim f F (locally g))
  → ∃ If, filterlim h F (locally If) ∧ is_RInt g a b If.

Continuous imply Riemann-integrable

Section StepFun.

Context {V : NormedModule R_AbsRing}.

Lemma is_RInt_SF (f : R → V) (s : SF_seq) :
  SF_sorted Rle s →
  let a := SF_h s in
  let b := last (SF_h s) (unzip1 (SF_t s)) in
  is_RInt (SF_fun (SF_map f s) zero) a b (Riemann_sum f s).

Lemma ex_RInt_SF (f : R → V) (s : SF_seq) :
  SF_sorted Rle s →
  let a := SF_h s in
  let b := last (SF_h s) (unzip1 (SF_t s)) in
  ex_RInt (SF_fun (SF_map f s) zero) a b.

End StepFun.

Lemma ex_RInt_continuous {V : CompleteNormedModule R_AbsRing} (f : R → V) (a b : R) :
  (∀ z, Rmin a b ≤ z ≤ Rmax a b → continuous f z )
  → ex_RInt f a b.

Norm

Section norm_RInt.

Context {V : NormedModule R_AbsRing}.

Lemma norm_RInt_le :
  ∀ (f : R → V) (g : R → R) (a b : R) (lf : V) (lg : R),
  a ≤ b →
  (∀ x, a ≤ x ≤ b → norm (f x) ≤ g x ) →
  is_RInt f a b lf →
  is_RInt g a b lg →
  norm lf ≤ lg.

Lemma norm_RInt_le_const :
  ∀ (f : R → V) (a b : R) (lf : V) (M : R),
  a ≤ b →
  (∀ x, a ≤ x ≤ b → norm (f x) ≤ M ) →
  is_RInt f a b lf →
  norm lf ≤ (b - a ) × M.

Lemma norm_RInt_le_const_abs :
  ∀ (f : R → V) (a b : R) (lf : V) (M : R),
  (∀ x, Rmin a b ≤ x ≤ Rmax a b → norm (f x) ≤ M ) →
  is_RInt f a b lf →
  norm lf ≤ Rabs (b - a) × M.

End norm_RInt.

Specific Normed Modules

Pairs

Section prod.

Context {U V : NormedModule R_AbsRing}.

Lemma is_RInt_fct_extend_fst
  (f : R → U × V) (a b : R) (l : U × V) :
  is_RInt f a b l → is_RInt (fun t ⇒ fst (f t)) a b (fst l).

Lemma is_RInt_fct_extend_snd
  (f : R → U × V) (a b : R) (l : U × V) :
  is_RInt f a b l → is_RInt (fun t ⇒ snd (f t)) a b (snd l).

Lemma is_RInt_fct_extend_pair
  (f : R → U × V) (a b : R) lu lv :
  is_RInt (fun t ⇒ fst (f t)) a b lu →
  is_RInt (fun t ⇒ snd (f t)) a b lv
    → is_RInt f a b (lu ,lv ).

Lemma ex_RInt_fct_extend_fst
  (f : R → U × V) (a b : R) :
  ex_RInt f a b → ex_RInt (fun t ⇒ fst (f t)) a b.

Lemma ex_RInt_fct_extend_snd
  (f : R → U × V) (a b : R) :
  ex_RInt f a b → ex_RInt (fun t ⇒ snd (f t)) a b.

Lemma ex_RInt_fct_extend_pair
  (f : R → U × V) (a b : R) :
  ex_RInt (fun t ⇒ fst (f t)) a b →
  ex_RInt (fun t ⇒ snd (f t)) a b
    → ex_RInt f a b.

Lemma RInt_fct_extend_pair
   (U_RInt : (R → U ) → R → R → U) (V_RInt : (R → V ) → R → R → V) :
  (∀ f a b l, is_RInt f a b l → U_RInt f a b = l )
  → (∀ f a b l, is_RInt f a b l → V_RInt f a b = l )
  → ∀ f a b l, is_RInt f a b l
    → (U_RInt (fun t ⇒ fst (f t)) a b , V_RInt (fun t ⇒ snd (f t)) a b ) = l.

End prod.

The total function RInt

Section RInt.

Context {V : CompleteNormedModule R_AbsRing}.

Definition RInt (f : R → V) (a b : R) := iota (is_RInt f a b).

Lemma is_RInt_unique (f : R → V) (a b : R) (l : V) :
  is_RInt f a b l → RInt f a b = l.

Lemma RInt_correct (f : R → V) (a b : R) :
  ex_RInt f a b → is_RInt f a b (RInt f a b).

Lemma opp_RInt_swap :
  ∀ f a b,
  ex_RInt f a b →
  opp (RInt f a b) = RInt f b a.

Correction of RInt

Usual rewritings

Lemma RInt_ext (f g : R → V) (a b : R) :
  (∀ x, Rmin a b < x < Rmax a b → f x = g x ) →
  RInt f a b = RInt g a b.

Lemma RInt_point (a : R) (f : R → V) :
  RInt f a a = zero.

Lemma RInt_const (a b : R) (c : V) :
  RInt (fun _ ⇒ c) a b = scal (b - a) c.

Lemma RInt_comp_lin (f : R → V) (u v a b : R) :
  ex_RInt f (u × a + v) (u × b + v) →
  RInt (fun y ⇒ scal u (f (u × y + v))) a b = RInt f (u × a + v) (u × b + v).

Lemma RInt_Chasles :
  ∀ f a b c,
  ex_RInt f a b → ex_RInt f b c →
  plus (RInt f a b) (RInt f b c) = RInt f a c.

Lemma RInt_scal (f : R → V) (a b l : R) :
  ex_RInt f a b →
  RInt (fun x ⇒ scal l (f x)) a b = scal l (RInt f a b).

Lemma RInt_opp (f : R → V) (a b : R) :
  ex_RInt f a b →
  RInt (fun x ⇒ opp (f x)) a b = opp (RInt f a b).

Lemma RInt_plus :
  ∀ f g a b, ex_RInt f a b → ex_RInt g a b →
  RInt (fun x ⇒ plus (f x) (g x)) a b = plus (RInt f a b) (RInt g a b).

Lemma RInt_minus :
  ∀ f g a b, ex_RInt f a b → ex_RInt g a b →
  RInt (fun x ⇒ minus (f x) (g x)) a b = minus (RInt f a b) (RInt g a b).

End RInt.

Order

Lemma is_RInt_ge_0 (f : R → R) (a b If : R) :
  a ≤ b → is_RInt f a b If →
  (∀ x, a < x < b → 0 ≤ f x ) → 0 ≤ If.

Lemma RInt_ge_0 (f : R → R) (a b : R) :
  a ≤ b → ex_RInt f a b
  → (∀ x, a < x < b → 0 ≤ f x ) → 0 ≤ RInt f a b.

Lemma is_RInt_le (f g : R → R) (a b If Ig : R) :
  a ≤ b →
  is_RInt f a b If → is_RInt g a b Ig →
  (∀ x, a < x < b → f x ≤ g x ) →
  If ≤ Ig.

Lemma RInt_le (f g : R → R) (a b : R) :
  a ≤ b →
  ex_RInt f a b → ex_RInt g a b →
  (∀ x, a < x < b → f x ≤ g x ) →
  RInt f a b ≤ RInt g a b.

Lemma RInt_gt_0 (g : R → R) (a b : R) :
  (a < b ) → (∀ x, a < x < b → (0 < g x )) →
  (∀ x, a ≤ x ≤ b → continuous g x ) →
  0 < RInt g a b.

Lemma RInt_lt (f g : R → R) (a b : R) :
  a < b →
  (∀ x : R, a ≤ x ≤ b →continuous g x ) →
  (∀ x : R, a ≤ x ≤ b →continuous f x ) →
  (∀ x : R, a < x < b → f x < g x ) →
  RInt f a b < RInt g a b.

Lemma abs_RInt_le_const :
  ∀ (f : R → R) a b M,
  a ≤ b → ex_RInt f a b →
  (∀ t, a ≤ t ≤ b → Rabs (f t) ≤ M ) →
  Rabs (RInt f a b) ≤ (b - a ) × M.

Equivalence with standard library

Lemma ex_RInt_Reals_aux_1 (f : R → R) (a b : R) :
  ∀ pr : Riemann_integrable f a b,
    is_RInt f a b (RiemannInt pr).

Lemma ex_RInt_Reals_1 (f : R → R) (a b : R) :
  Riemann_integrable f a b → ex_RInt f a b.

Lemma ex_RInt_Reals_0 (f : R → R) (a b : R) :
  ex_RInt f a b → Riemann_integrable f a b.

Lemma RInt_Reals (f : R → R) (a b : R) :
  ∀ pr, RInt f a b = @RiemannInt f a b pr.

Theorems proved using standard library

Lemma ex_RInt_norm :
  ∀ (f : R → R) a b, ex_RInt f a b →
  ex_RInt (fun x ⇒ norm (f x)) a b.

Lemma abs_RInt_le :
  ∀ (f : R → R) a b,
  a ≤ b → ex_RInt f a b →
  Rabs (RInt f a b) ≤ RInt (fun t ⇒ Rabs (f t)) a b.