Library Coquelicot.RInt

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 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 : RV) (a b : R) (If : V) :=
  filterlim (fun ptdscal (sign (b-a)) (Riemann_sum f ptd)) (Riemann_fine a b) (locally If).

Definition ex_RInt (f : RV) (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 : RV) (a : R),
  is_RInt f a a zero.

Lemma ex_RInt_point :
   (f : RV) a,
  ex_RInt f a a.

Swapping bounds

Lemma is_RInt_swap :
   (f : RV) (a b : R) (If : V),
  is_RInt f b a Ifis_RInt f a b (opp If).

Lemma ex_RInt_swap :
   (f : RV) (a b : R),
  ex_RInt f a bex_RInt f b a.

Integrable implies bounded

Lemma ex_RInt_ub (f : RV) (a b : R) :
  ex_RInt f a b M : R, t : R,
    Rmin a b t Rmax a bnorm (f t) M.

Extensionality

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

Lemma ex_RInt_ext :
   (f g : RV) (a b : R),
  ( x, Rmin a b < x < Rmax a bf x = g x) →
  ex_RInt f a bex_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 : RV) (a b : R) (l : V),
  is_RInt f (-a) (-b) l
  is_RInt (fun yopp (f (- y))) a b l.

Lemma ex_RInt_comp_opp :
   (f : RV) (a b : R),
  ex_RInt f (-a) (-b) →
  ex_RInt (fun yopp (f (- y))) a b.

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

Lemma ex_RInt_comp_lin (f : RV) (u v a b : R) :
  ex_RInt f (u × a + v) (u × b + v)
    → ex_RInt (fun yscal u (f (u × y + v))) a b.

Chasles


Lemma is_RInt_Chasles_0 (f : RV) (a b c : R) (l1 l2 : V) :
  a < b < cis_RInt f a b l1is_RInt f b c l2
  → is_RInt f a c (plus l1 l2).
Lemma ex_RInt_Chasles_0 (f : RV) (a b c : R) :
  a b cex_RInt f a bex_RInt f b c
  → ex_RInt f a c.

Lemma is_RInt_Chasles_1 (f : RV) (a b c : R) l1 l2 :
  a < b < cis_RInt f a c l1is_RInt f b c l2is_RInt f a b (minus l1 l2).

Lemma is_RInt_Chasles_2 (f : RV) (a b c : R) l1 l2 :
  a < b < cis_RInt f a c l1is_RInt f a b l2is_RInt f b c (minus l1 l2).

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

Operations


Lemma is_RInt_scal :
   (f : RV) (a b : R) (k : R) (If : V),
  is_RInt f a b If
  is_RInt (fun yscal k (f y)) a b (scal k If).

Lemma ex_RInt_scal :
   (f : RV) (a b : R) (k : R),
  ex_RInt f a b
  ex_RInt (fun yscal k (f y)) a b.

Lemma is_RInt_opp :
   (f : RV) (a b : R) (If : V),
  is_RInt f a b If
  is_RInt (fun yopp (f y)) a b (opp If).

Lemma ex_RInt_opp :
   (f : RV) (a b : R),
  ex_RInt f a b
  ex_RInt (fun xopp (f x)) a b.

Lemma is_RInt_plus :
   (f g : RV) (a b : R) (If Ig : V),
  is_RInt f a b If
  is_RInt g a b Ig
  is_RInt (fun yplus (f y) (g y)) a b (plus If Ig).

Lemma ex_RInt_plus :
   (f g : RV) (a b : R),
  ex_RInt f a b
  ex_RInt g a b
  ex_RInt (fun yplus (f y) (g y)) a b.

Lemma is_RInt_minus :
   (f g : RV) (a b : R) (If Ig : V),
  is_RInt f a b If
  is_RInt g a b Ig
  is_RInt (fun yminus (f y) (g y)) a b (minus If Ig).

Lemma ex_RInt_minus :
   (f g : RV) (a b : R),
  ex_RInt f a b
  ex_RInt g a b
  ex_RInt (fun yminus (f y) (g y)) a b.

End is_RInt.

Lemma ex_RInt_Chasles_1 {V : CompleteNormedModule R_AbsRing}
  (f : RV) (a b c : R) :
  a b cex_RInt f a cex_RInt f a b.

Lemma ex_RInt_Chasles_2 {V : CompleteNormedModule R_AbsRing}
  (f : RV) (a b c : R) :
   a b cex_RInt f a cex_RInt f b c.

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

Exchange limit and integral


Lemma filterlim_RInt {U} {V : CompleteNormedModule R_AbsRing} :
   (f : URV) (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 : RV) (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 : RV) (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 : RV) (a b : R) :
  ( z, Rmin a b z Rmax a bcontinuous f z)
  → ex_RInt f a b.

Norm


Section norm_RInt.

Context {V : NormedModule R_AbsRing}.

Lemma norm_RInt_le :
   (f : RV) (g : RR) (a b : R) (lf : V) (lg : R),
  a b
  ( x, a x bnorm (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 : RV) (a b : R) (lf : V) (M : R),
  a b
  ( x, a x bnorm (f x) M) →
  is_RInt f a b lf
  norm lf (b - a) × M.

Lemma norm_RInt_le_const_abs :
   (f : RV) (a b : R) (lf : V) (M : R),
  ( x, Rmin a b x Rmax a bnorm (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 : RU × V) (a b : R) (l : U × V) :
  is_RInt f a b lis_RInt (fun tfst (f t)) a b (fst l).

Lemma is_RInt_fct_extend_snd
  (f : RU × V) (a b : R) (l : U × V) :
  is_RInt f a b lis_RInt (fun tsnd (f t)) a b (snd l).

Lemma is_RInt_fct_extend_pair
  (f : RU × V) (a b : R) lu lv :
  is_RInt (fun tfst (f t)) a b lu
  is_RInt (fun tsnd (f t)) a b lv
    → is_RInt f a b (lu,lv).

Lemma ex_RInt_fct_extend_fst
  (f : RU × V) (a b : R) :
  ex_RInt f a bex_RInt (fun tfst (f t)) a b.

Lemma ex_RInt_fct_extend_snd
  (f : RU × V) (a b : R) :
  ex_RInt f a bex_RInt (fun tsnd (f t)) a b.

Lemma ex_RInt_fct_extend_pair
  (f : RU × V) (a b : R) :
  ex_RInt (fun tfst (f t)) a b
  ex_RInt (fun tsnd (f t)) a b
    → ex_RInt f a b.

Lemma RInt_fct_extend_pair
   (U_RInt : (RU) → RRU) (V_RInt : (RV) → RRV) :
  ( f a b l, is_RInt f a b lU_RInt f a b = l)
  → ( f a b l, is_RInt f a b lV_RInt f a b = l)
  → f a b l, is_RInt f a b l
    → (U_RInt (fun tfst (f t)) a b, V_RInt (fun tsnd (f t)) a b) = l.

End prod.

The total function RInt


Definition RInt (f : RR) (a b : R) :=
  match Rle_dec a b with
    | left _real (Lim_seq (RInt_val f a b))
    | right _- real (Lim_seq (RInt_val f b a))
  end.

Lemma RInt_point :
   f a, RInt f a a = 0.

Lemma RInt_swap :
   f a b,
  - RInt f a b = RInt f b a.

Correction of RInt

Lemma is_RInt_lim_seq (f : RR) (a b : R) :
   If : R, is_RInt f a b Ifis_lim_seq (RInt_val f a b) If.

Lemma is_RInt_unique (f : RR) (a b l : R) :
  is_RInt f a b lRInt f a b = l.

Lemma RInt_correct (f : RR) (a b : R) :
  ex_RInt f a bis_RInt f a b (RInt f a b).

Usual rewritings


Lemma RInt_ext :
   f g a b,
  ( x, Rmin a b x Rmax a bf x = g x) →
  RInt f a b = RInt g a b.

Lemma RInt_const (a b c : R) :
  RInt (fun _c) a b = (b - a) × c.

Lemma RInt_comp_opp (f : RR) (a b : R) :
  RInt (fun y- f (- y)) a b = RInt f (-a) (-b).

Lemma RInt_comp_lin (f : RR) (u v a b : R) :
  RInt (fun yu × 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 bex_RInt f b c
  RInt f a b + RInt f b c = RInt f a c.

Lemma RInt_scal :
   f l a b,
  RInt (fun xl × f x) a b = l × RInt f a b.

Lemma RInt_opp :
   f a b,
  RInt (fun x- f x) a b = - RInt f a b.

Lemma RInt_plus :
   f g a b, ex_RInt f a bex_RInt g a b
  RInt (fun xf x + g x) a b = RInt f a b + RInt g a b.

Lemma RInt_minus :
   f g a b, ex_RInt f a bex_RInt g a b
  RInt (fun xf x - g x) a b = RInt f a b - RInt g a b.

Order


Lemma is_RInt_ge_0 (g : RR) (a b Ig : R) :
  (a b) → (is_RInt g a b Ig) →
  ( x, a < x < b → 0 g x) → 0 Ig.

Lemma RInt_ge_0 (f : RR) (a b : R) :
  a bex_RInt f a b
  → ( x, a < x < b → 0 f x) → 0 RInt f a b.

Lemma is_RInt_le (f g : RR) (a b If Ig : R) :
  a b
  is_RInt f a b Ifis_RInt g a b Ig
  ( x, a < x < bf x g x) →
  If Ig.

Lemma RInt_le (f g : RR) (a b : R) :
  a b
  ex_RInt f a bex_RInt g a b
  ( x, a < x < bf x g x) →
  RInt f a b RInt g a b.

Lemma RInt_gt_0 (g : RR) (a b : R) :
  (a < b) → ( x, a < x < b → (0 < g x)) →
  ( x, a x bcontinuous g x) →
  0 < RInt g a b.

Lemma RInt_lt (f g : RR) (a b : R) :
  a < b
  ( x : R, a x bcontinuous g x) →
  ( x : R, a x bcontinuous f x) →
  ( x : R, a < x < bf x < g x) →
  RInt f a b < RInt g a b.

Lemma abs_RInt_le_const :
   (f : RR) a b M,
  a bex_RInt f a b
  ( t, a t bRabs (f t) M) →
  Rabs (RInt f a b) (b - a) × M.

Equivalence with standard library


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

Lemma ex_RInt_Reals_1 (f : RR) (a b : R) :
  Riemann_integrable f a bex_RInt f a b.

Lemma ex_RInt_Reals_0 (f : RR) (a b : R) :
  ex_RInt f a bRiemann_integrable f a b.

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

Theorems proved using standard library


Lemma ex_RInt_norm :
   (f : RR) a b, ex_RInt f a b
  ex_RInt (fun xnorm (f x)) a b.

Lemma abs_RInt_le :
   (f : RR) a b,
  a bex_RInt f a b
  Rabs (RInt f a b) RInt (fun tRabs (f t)) a b.