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.

From Coq Require Import Reals Psatz.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype seq.

Require Import Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy.

Local Tactic Notation "intuition" := (intuition auto with arith zarith real rorders).

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.