Library Coquelicot.SF_seq

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.
Require Import Rcomplements Rbar Lub.
Require Import Hierarchy.
Require Import Ssreflect.ssreflect Ssreflect.seq Ssreflect.ssrbool.

This file describes many properties about sequences of real numbers. Several formalizations are provided. They are mainly used for defining pointed subvivision in order to define Riemann sums.

Open Scope R_scope.

Complements abouts lists

seq R <-> Rlist
Fixpoint seq2Rlist (s : seq R) :=
  match s with
    | [::]RList.nil
    | h::tRList.cons h (seq2Rlist t)
  end.
Fixpoint Rlist2seq (s : Rlist) : seq R :=
  match s with
    | RList.nil[::]
    | RList.cons h th::(Rlist2seq t)
  end.

Lemma seq2Rlist_bij (s : Rlist) :
  seq2Rlist (Rlist2seq s) = s.
Lemma Rlist2seq_bij (s : seq R) :
  Rlist2seq (seq2Rlist s) = s.

Lemma size_compat (s : seq R) :
  Rlength (seq2Rlist s) = size s.

Lemma nth_compat (s : seq R) (n : nat) :
  pos_Rl (seq2Rlist s) n = nth 0 s n.

Various properties

Lemma rev_rev {T} (l : seq T) : rev (rev l) = l.
Lemma head_rev {T} (x0 : T) (l : seq T) :
  head x0 (rev l) = last x0 l.
Lemma last_rev {T} (x0 : T) (l : seq T) :
  last x0 (rev l) = head x0 l.

Lemma last_unzip1 {S T} x0 y0 (s : seq (S × T)) :
  last x0 (unzip1 s) = fst (last (x0,y0) s).

sorted

Fixpoint sorted {T : Type} (Ord : TTProp) (s : seq T) :=
  match s with
    | [::] | [:: _]True
    | h0 :: (h1 :: t1) as t0Ord h0 h1 sorted Ord t0
  end.
Lemma sorted_nth {T : Type} (Ord : TTProp) (s : seq T) :
  sorted Ord s ( i : nat,
    (i < Peano.pred (size s))%nat x0 : T, Ord (nth x0 s i) (nth x0 s (S i))).
Lemma sorted_cat {T : Type} (Ord : TTProp) (s1 s2 : seq T) x0 :
  sorted Ord s1sorted Ord s2Ord (last x0 s1) (head x0 s2)
  → sorted Ord (s1 ++ s2).

Lemma sorted_head (s : seq R) i :
  sorted Rle s → (i < size s)%nat x0, head x0 s nth x0 s i.

Lemma sorted_incr (s : seq R) i j : sorted Rle s → (i j)%nat → (j < size s)%nat
  → x0, nth x0 s i nth x0 s j.

Lemma sorted_last (s : seq R) i :
  sorted Rle s → (i < size s)%nat x0, nth x0 s i last x0 s.

Lemma sorted_dec (s : seq R) x0 (x : R) :
  sorted Rle shead x0 s x last x0 s
    {i : nat | nth x0 s i x < nth x0 s (S i) (S (S i) < size s)%nat}
    + {nth x0 s (size s - 2)%nat x nth x0 s (size s - 1)%nat}.

Lemma sorted_compat (s : seq R) :
  sorted Rle s ordered_Rlist (seq2Rlist s).

seq_step

Definition seq_step (s : seq R) :=
  foldr Rmax 0 (pairmap (fun x yRabs (Rminus y x)) (head 0 s) (behead s)).

Lemma seq_step_ge_0 x : (0 seq_step x).
Lemma seq_step_cat (x y : seq R) :
  (0 < size x)%nat → (0 < size y)%nat
  last 0 x = head 0 y
  seq_step (cat x (behead y)) = Rmax (seq_step x) (seq_step y).

Lemma seq_step_rev (l : seq R) : seq_step (rev l) = seq_step l.

Lemma nth_le_seq_step x0 (l : seq R) (i : nat) : (S i < size l)%nat
  Rabs (nth x0 l (S i) - nth x0 l i) seq_step l.

Definitions of SF_seq


Section SF_seq.
Context {T : Type}.

Record SF_seq := mkSF_seq {SF_h : R ; SF_t : seq (R × T)}.
Definition SF_lx (s : SF_seq) : seq R := (SF_h s)::(unzip1 (SF_t s)).
Definition SF_ly (s : SF_seq) : seq T := unzip2 (SF_t s).
Definition SF_make (lx : seq R) (ly : seq T) (Hs : size lx = S (size ly)) : SF_seq :=
  mkSF_seq (head 0 lx) (zip (behead lx) ly).

Lemma SF_size_lx_ly (s : SF_seq) : size (SF_lx s) = S (size (SF_ly s)).
Lemma SF_seq_bij (s : SF_seq) :
  SF_make (SF_lx s) (SF_ly s) (SF_size_lx_ly s) = s.
Lemma SF_seq_bij_lx (lx : seq R) (ly : seq T)
  (Hs : size lx = S (size ly)) : SF_lx (SF_make lx ly Hs) = lx.
Lemma SF_seq_bij_ly (lx : seq R) (ly : seq T)
  (Hs : size lx = S (size ly)) : SF_ly (SF_make lx ly Hs) = ly.

Constructors


Definition SF_nil (x0 : R) : SF_seq := mkSF_seq x0 [::].
Definition SF_cons (h : R×T) (s : SF_seq) :=
  mkSF_seq (fst h) ((SF_h s,snd h)::(SF_t s)).
Definition SF_rcons (s : SF_seq) (t : R×T) :=
  mkSF_seq (SF_h s) (rcons (SF_t s) t).

Lemma SF_cons_dec (P : SF_seqType) :
  ( x0 : R, P (SF_nil x0)) → ( h s, P (SF_cons h s))
    → ( s, P s).
Lemma SF_cons_ind (P : SF_seqType) :
  ( x0 : R, P (SF_nil x0)) → ( h s, P sP (SF_cons h s))
    → ( s, P s).

Lemma SF_rcons_dec (P : SF_seqType) :
  ( x0 : R, P (SF_nil x0)) → ( s t, P (SF_rcons s t))
    → ( s, P s).
Lemma SF_rcons_ind (P : SF_seqType) :
  ( x0 : R, P (SF_nil x0)) → ( s t, P sP (SF_rcons s t))
    → ( s, P s).

Lemma SF_cons_rcons (h : R×T) (s : SF_seq) (l : R×T) :
  SF_cons h (SF_rcons s l) = SF_rcons (SF_cons h s) l.

SF_seq and seq


Lemma SF_lx_nil (x0 : R) :
  SF_lx (SF_nil x0) = [:: x0].
Lemma SF_ly_nil (x0 : R) :
  SF_ly (SF_nil x0) = [::].

Lemma SF_lx_cons (h : R×T) (s : SF_seq) :
  SF_lx (SF_cons h s) = (fst h) :: (SF_lx s).
Lemma SF_ly_cons (h : R×T) (s : SF_seq) :
  SF_ly (SF_cons h s) = (snd h) :: (SF_ly s).
Lemma SF_lx_rcons (s : SF_seq) (h : R×T) :
  SF_lx (SF_rcons s h) = rcons (SF_lx s) (fst h).
Lemma SF_ly_rcons (s : SF_seq) (h : R×T) :
  SF_ly (SF_rcons s h) = rcons (SF_ly s) (snd h).

Lemma SF_lx_surj (s s0 : SF_seq) :
  s = s0SF_lx s = SF_lx s0.
Lemma SF_ly_surj (s s0 : SF_seq) :
  s = s0SF_ly s = SF_ly s0.
Lemma SF_lx_ly_inj (s s0 : SF_seq) :
  SF_lx s = SF_lx s0SF_ly s = SF_ly s0s = s0.

SF_size


Definition SF_size (s : SF_seq) := size (SF_t s).

Lemma SF_size_cons (h : R×T) (s : SF_seq) : SF_size (SF_cons h s) = S (SF_size s).

Lemma SF_size_rcons (s : SF_seq) (t : R×T) : SF_size (SF_rcons s t) = S (SF_size s).

Lemma SF_size_lx (s : SF_seq) : size (SF_lx s) = S (SF_size s).
Lemma SF_size_ly (s : SF_seq) : size (SF_ly s) = SF_size s.

SF_rev


Lemma SF_rev_0 (s : SF_seq) :
  size (rev (SF_lx s)) = S (size (rev (SF_ly s))).
Definition SF_rev (s : SF_seq) : SF_seq :=
  SF_make (rev (SF_lx s)) (rev (SF_ly s)) (SF_rev_0 s).

Lemma SF_rev_cons (h : R×T) (s : SF_seq) :
  SF_rev (SF_cons h s) = SF_rcons (SF_rev s) h.
Lemma SF_rev_rcons (s : SF_seq) (t : R×T) :
  SF_rev (SF_rcons s t) = SF_cons t (SF_rev s).

Lemma SF_rev_invol (s : SF_seq) :
  SF_rev (SF_rev s) = s.

Lemma SF_lx_rev (s : SF_seq) : SF_lx (SF_rev s) = rev (SF_lx s).
Lemma SF_ly_rev (s : SF_seq) : SF_ly (SF_rev s) = rev (SF_ly s).

Lemma SF_size_rev (s : SF_seq) : SF_size (SF_rev s) = SF_size s.

Lemma SF_rev_surj (s s0 : SF_seq) :
  s = s0SF_rev s = SF_rev s0.
Lemma SF_rev_inj (s s0 : SF_seq) :
  SF_rev s = SF_rev s0s = s0.

SF_cat


Definition SF_cat (x y : SF_seq) := mkSF_seq (SF_h x) ((SF_t x) ++ (SF_t y)).
Lemma SF_lx_cat (x y : SF_seq) :
  SF_lx (SF_cat x y) = (SF_lx x) ++ (behead (SF_lx y)).
Lemma SF_last_cat (x y : SF_seq) :
  last (SF_h x) (SF_lx x) = head (SF_h y) (SF_lx y) →
  last (SF_h (SF_cat x y)) (SF_lx (SF_cat x y)) = (last (SF_h y) (SF_lx y)).
Lemma SF_cons_cat x0 (x y : SF_seq) :
  SF_cons x0 (SF_cat x y) = SF_cat (SF_cons x0 x) y.

first and last pair


Definition SF_head (y0 : T) (s : SF_seq) := (SF_h s, head y0 (SF_ly s)).
Definition SF_behead (s : SF_seq) :=
  mkSF_seq (head (SF_h s) (unzip1 (SF_t s))) (behead (SF_t s)).

Definition SF_last y0 (s : SF_seq) : (R×T) :=
  last (SF_h s,y0) (SF_t s).
Definition SF_belast (s : SF_seq) : SF_seq :=
  mkSF_seq (SF_h s) (Rcomplements.belast (SF_t s)).

Lemma SF_last_lx x0 (s : SF_seq) :
  fst (SF_last x0 s) = last 0 (SF_lx s).

SF_sorted


Definition SF_sorted (Ord : RRProp) (s : SF_seq) :=
  sorted Ord (SF_lx s).

End SF_seq.

SF_map


Section SF_map.

Context {T T0 : Type}.

Definition SF_map (f : TT0) (s : SF_seq) : SF_seq :=
  mkSF_seq (SF_h s) (map (fun x(fst x,f (snd x))) (SF_t s)).

Lemma SF_map_cons (f : TT0) (h : R×T) (s : SF_seq) :
  SF_map f (SF_cons h s) = SF_cons (fst h, f (snd h)) (SF_map f s).

Lemma SF_map_rcons (f : TT0) (s : SF_seq) (h : R×T) :
  SF_map f (SF_rcons s h) = SF_rcons (SF_map f s) (fst h, f (snd h)).

Lemma SF_map_lx (f : TT0) (s : SF_seq) :
  SF_lx (SF_map f s) = SF_lx s.

Lemma SF_map_ly (f : TT0) (s : SF_seq) :
  SF_ly (SF_map f s) = map f (SF_ly s).

Lemma SF_map_rev (f : TT0) s :
  SF_rev (SF_map f s) = SF_map f (SF_rev s).

Lemma SF_map_sort (f : TT0) (s : SF_seq) (Ord : RRProp) :
  SF_sorted Ord sSF_sorted Ord (SF_map f s).

Lemma SF_size_map (f : TT0) s :
  SF_size (SF_map f s) = SF_size s.

End SF_map.

Pointed subvivision


Definition pointed_subdiv (ptd : @SF_seq R) :=
   i : nat, (i < SF_size ptd)%nat
    nth 0 (SF_lx ptd) i nth 0 (SF_ly ptd) i nth 0 (SF_lx ptd) (S i).

Lemma ptd_cons h s : pointed_subdiv (SF_cons h s) → pointed_subdiv s.
Lemma ptd_sort ptd :
  pointed_subdiv ptdSF_sorted Rle ptd.
Lemma ptd_sort' ptd :
  pointed_subdiv ptdsorted Rle (SF_ly ptd).

Lemma SF_cat_pointed (x y : SF_seq) :
  last (SF_h x) (SF_lx x) = head (SF_h y) (SF_lx y) →
  pointed_subdiv xpointed_subdiv y
  → pointed_subdiv (SF_cat x y).

SF_seq for Chasles


Fixpoint seq_cut_down (s : seq (R×R)) (x : R) : seq (R×R) :=
  match s with
    | [::][:: (x,x)]
    | h :: t
        match Rle_dec (fst h) x with
          | right _[:: (x,Rmin (snd h) x)]
          | left _h :: (seq_cut_down t x)
        end
  end.
Fixpoint seq_cut_up (s : seq (R×R)) (x : R) : seq (R×R) :=
  match s with
    | [::][:: (x,x)]
    | h :: t
        match Rle_dec (fst h) x with
          | right _(x,x)::(fst h,Rmax (snd h) x)::t
          | left _seq_cut_up t x
        end
  end.

Definition SF_cut_down (sf : @SF_seq R) (x : R) :=
  let s := seq_cut_down ((SF_h sf,SF_h sf) :: (SF_t sf)) x in
  mkSF_seq (fst (head (SF_h sf,SF_h sf) s)) (behead s).
Definition SF_cut_up (sf : @SF_seq R) (x : R) :=
  let s := seq_cut_up ((SF_h sf,SF_h sf) :: (SF_t sf)) x in
  mkSF_seq (fst (head (SF_h sf,SF_h sf) s)) (behead s).

Lemma SF_cut_down_step s x eps :
  SF_h s x last (SF_h s) (SF_lx s) →
  seq_step (SF_lx s) < eps
    → seq_step (SF_lx (SF_cut_down s x)) < eps.
Lemma SF_cut_up_step s x eps :
  SF_h s x last (SF_h s) (SF_lx s) →
  seq_step (SF_lx s) < eps
    → seq_step (SF_lx (SF_cut_up s x)) < eps.

Lemma SF_cut_down_pointed s x :
  SF_h s xpointed_subdiv s
  → pointed_subdiv (SF_cut_down s x).

Lemma SF_cut_up_pointed s x :
  SF_h s x
  pointed_subdiv s
  → pointed_subdiv (SF_cut_up s x).
Lemma SF_cut_down_h s x :
  SF_h s xSF_h (SF_cut_down s x) = SF_h s.
Lemma SF_cut_up_h s x :
  SF_h (SF_cut_up s x) = x.
Lemma SF_cut_down_l s x :
  last (SF_h (SF_cut_down s x)) (SF_lx (SF_cut_down s x)) = x.
Lemma SF_cut_up_l s x :
  x last (SF_h s) (SF_lx s) →
  last (SF_h (SF_cut_up s x)) (SF_lx (SF_cut_up s x)) = last (SF_h s) (SF_lx s).

Lemma SF_cut_down_cons_0 h ptd x :
  x < fst hSF_cut_down (SF_cons h ptd) x = SF_nil x.
Lemma SF_cut_up_cons_0 h ptd x :
  x < fst hSF_cut_up (SF_cons h ptd) x = SF_cons (x,Rmax (fst h) x) (SF_cons h ptd).
Lemma SF_cut_down_cons_1 h ptd x :
  fst h x < SF_h ptdSF_cut_down (SF_cons h ptd) x = SF_cons (fst h, Rmin (snd h) x) (SF_nil x).
Lemma SF_cut_up_cons_1 h ptd x :
  fst h x < SF_h ptdSF_cut_up (SF_cons h ptd) x = SF_cons (x,Rmax (snd h) x) ptd.
Lemma SF_cut_down_cons_2 h ptd x :
  fst h SF_h ptd xSF_cut_down (SF_cons h ptd) x = SF_cons h (SF_cut_down ptd x).
Lemma SF_cut_up_cons_2 h ptd x :
  fst h SF_h ptd xSF_cut_up (SF_cons h ptd) x = SF_cut_up ptd x.

Definition of SF_fun


Section SF_fun.

Context {T : Type}.

Fixpoint SF_fun_aux (h : R×T) (s : seq (R×T)) (y0 : T) (x : R) :=
  match s with
    | [::]match Rle_dec x (fst h) with
        | left _snd h
        | right _y0
      end
    | h0 :: s0match Rlt_dec x (fst h) with
        | left _snd h
        | right _SF_fun_aux h0 s0 y0 x
      end
  end.
Definition SF_fun (s : SF_seq) (y0 : T) (x : R) :=
  SF_fun_aux (SF_h s,y0) (SF_t s) y0 x.

Lemma SF_fun_incr (s : SF_seq) (y0 : T) (x : R) Hs Hx :
  SF_fun s y0 x =
  match (sorted_dec (SF_lx s) 0 x Hs Hx) with
    | inleft Hnth y0 (SF_ly s) (proj1_sig H)
    | inright _nth y0 (SF_ly s) (SF_size s -1)%nat
  end.

End SF_fun.

Lemma SF_fun_map {T T0 : Type} (f : TT0) (s : SF_seq) y0 :
   x, SF_fun (SF_map f s) (f y0) x = f (SF_fun s y0 x).

Particular SF_seq


Definition SF_seq_f1 {T : Type} (f1 : RT) (P : seq R) : SF_seq :=
  mkSF_seq (head 0 P) (pairmap (fun x y(y, f1 x)) (head 0 P) (behead P)).
Definition SF_seq_f2 {T : Type} (f2 : RRT) (P : seq R) : SF_seq :=
  mkSF_seq (head 0 P) (pairmap (fun x y(y, f2 x y)) (head 0 P) (behead P)).

Lemma SF_cons_f1 {T : Type} (f1 : RT) (h : R) (P : seq R) :
  (0 < size P)%natSF_seq_f1 f1 (h::P) = SF_cons (h,f1 h) (SF_seq_f1 f1 P).
Lemma SF_cons_f2 {T : Type} (f2 : RRT) (h : R) (P : seq R) :
  (0 < size P)%nat
    SF_seq_f2 f2 (h::P) = SF_cons (h,f2 h (head 0 P)) (SF_seq_f2 f2 P).

Lemma SF_size_f1 {T : Type} (f1 : RT) P :
  SF_size (SF_seq_f1 f1 P) = Peano.pred (size P).
Lemma SF_size_f2 {T : Type} (f2 : RRT) P :
  SF_size (SF_seq_f2 f2 P) = Peano.pred (size P).

Lemma SF_lx_f1 {T : Type} (f1 : RT) P :
  (0 < size P)%natSF_lx (SF_seq_f1 f1 P) = P.
Lemma SF_lx_f2 {T : Type} (f2 : RRT) P :
  (0 < size P)%nat
  SF_lx (SF_seq_f2 f2 P) = P.

Lemma SF_ly_f1 {T : Type} (f1 : RT) P :
  SF_ly (SF_seq_f1 f1 P) = Rcomplements.belast (map f1 P).
Lemma SF_ly_f2 {T : Type} (f2 : RRT) P :
  SF_ly (SF_seq_f2 f2 P) = behead (pairmap f2 0 P).

Lemma SF_sorted_f1 {T : Type} (f1 : RT) P Ord :
  (sorted Ord P) (SF_sorted Ord (SF_seq_f1 f1 P)).
Lemma SF_sorted_f2 {T : Type} (f2 : RRT) P Ord :
  (sorted Ord P) (SF_sorted Ord (SF_seq_f2 f2 P)).

Lemma SF_rev_f2 {T : Type} (f2 : RRT) P : ( x y, f2 x y = f2 y x) →
  SF_rev (SF_seq_f2 f2 P) = SF_seq_f2 f2 (rev P).

Lemma SF_map_f1 {T T0 : Type} (f : TT0) (f1 : RT) P :
  SF_map f (SF_seq_f1 f1 P) = SF_seq_f1 (fun xf (f1 x)) P.
Lemma SF_map_f2 {T T0 : Type} (f : TT0) (f2 : RRT) P :
  SF_map f (SF_seq_f2 f2 P) = SF_seq_f2 (fun x yf (f2 x y)) P.

Lemma ptd_f2 (f : RRR) s :
  sorted Rle s → ( x y, x yx f x y y)
  → pointed_subdiv (SF_seq_f2 f s).

SF_fun


Definition SF_fun_f1 {T : Type} (f1 : RT) (P : seq R) x : T :=
  SF_fun (SF_seq_f1 f1 P) (f1 0) x.
Definition SF_fun_f2 {T : Type} (f2 : RRT) (P : seq R) x :=
  SF_fun (SF_seq_f2 f2 P) (f2 0 0) x.

Uniform partition


Definition unif_part (a b : R) (n : nat) : seq R :=
  mkseq (fun ia + (INR i) × (b - a) / (INR n + 1)) (S (S n)).

Lemma unif_part_bound (a b : R) (n : nat) :
  unif_part a b n = rev (unif_part b a n).

Lemma unif_part_sort (a b : R) (n : nat) : a bsorted Rle (unif_part a b n).

Lemma unif_part_nat (a b : R) (n : nat) (x : R) : (a x b) →
  {i : nat |
  nth 0 (unif_part a b n) i x < nth 0 (unif_part a b n) (S i)
  (S (S i) < size (unif_part a b n))%nat} +
  {nth 0 (unif_part a b n) (n) x
   nth 0 (unif_part a b n) (S n)}.

Lemma head_unif_part x0 (a b : R) (n : nat) :
  head x0 (unif_part a b n) = a.
Lemma last_unif_part x0 (a b : R) (n : nat) :
  last x0 (unif_part a b n) = b.
Lemma seq_step_unif_part (a b : R) (n : nat) :
  seq_step (unif_part a b n) = Rabs ((b - a) / (INR n + 1)).

Lemma seq_step_unif_part_ex (a b : R) (eps : posreal) :
  {n : nat | seq_step (unif_part a b n) < eps}.

Lemma unif_part_S a b n :
  unif_part a b (S n) = a :: unif_part ((a × INR (S n) + b) / INR (S (S n))) b n.

Definition SF_val_seq {T} (f : RT) (a b : R) (n : nat) : SF_seq :=
  SF_seq_f2 (fun x yf ((x+y)/2)) (unif_part a b n).
Definition SF_val_fun {T} (f : RT) (a b : R) (n : nat) (x : R) : T :=
  SF_fun_f2 (fun x yf ((x+y)/2)) (unif_part a b n) x.

Definition SF_val_ly {T} (f : RT) (a b : R) (n : nat) : seq T :=
  behead (pairmap (fun x yf ((x+y)/2)) 0 (unif_part a b n)).

Lemma SF_val_ly_bound {T} (f : RT) (a b : R) (n : nat) :
  SF_val_ly f a b n = rev (SF_val_ly f b a n).

A proper filter on SF_seq


Lemma Riemann_fine_unif_part :
   (f : RRR) (a b : R) (n : nat),
  ( a b, a ba f a b b) →
  a b
  seq_step (SF_lx (SF_seq_f2 f (unif_part a b n))) (b - a) / (INR n + 1)
  pointed_subdiv (SF_seq_f2 f (unif_part a b n))
  SF_h (SF_seq_f2 f (unif_part a b n)) = a
  last (SF_h (SF_seq_f2 f (unif_part a b n))) (SF_lx (SF_seq_f2 f (unif_part a b n))) = b.

Definition Riemann_fine (a b : R) :=
  within (fun ptdpointed_subdiv ptd SF_h ptd = Rmin a b last (SF_h ptd) (SF_lx ptd) = Rmax a b)
    (locally_dist (fun ptdseq_step (SF_lx ptd))).

Global Instance Riemann_fine_filter :
   a b, ProperFilter (Riemann_fine a b).

Riemann sums

Riemann_sum

Section Riemann_sum.

Context {V : ModuleSpace R_Ring}.

Definition Riemann_sum (f : RV) (ptd : SF_seq) : V :=
  foldr plus zero (pairmap (fun x y ⇒ (scal (fst y - fst x) (f (snd y)))) (SF_h ptd,zero) (SF_t ptd)).

Lemma Riemann_sum_cons (f : RV) (h0 : R × R) (ptd : SF_seq) :
  Riemann_sum f (SF_cons h0 ptd) =
    plus (scal (SF_h ptd - fst h0) (f (snd h0))) (Riemann_sum f ptd).

Lemma Riemann_sum_rcons (f : RV) ptd l0 :
  Riemann_sum f (SF_rcons ptd l0) =
    plus (Riemann_sum f ptd) (scal (fst l0 - last (SF_h ptd) (SF_lx ptd)) (f (snd l0))).

Lemma Riemann_sum_zero (f : RV) ptd :
  SF_sorted Rle ptd
  SF_h ptd = last (SF_h ptd) (SF_lx ptd) →
  Riemann_sum f ptd = zero.

Lemma Riemann_sum_map (f : RV) (g : RR) ptd :
  Riemann_sum (fun xf (g x)) ptd = Riemann_sum f (SF_map g ptd).

Lemma Riemann_sum_const (v : V) ptd :
  Riemann_sum (fun _v) ptd = scal (last (SF_h ptd) (SF_lx ptd) - SF_h ptd) v.

Lemma Riemann_sum_scal (a : R) (f : RV) ptd :
  Riemann_sum (fun xscal a (f x)) ptd = scal a (Riemann_sum f ptd).

Lemma Riemann_sum_opp (f : RV) ptd :
  Riemann_sum (fun xopp (f x)) ptd = opp (Riemann_sum f ptd).

Lemma Riemann_sum_plus (f g : RV) ptd :
  Riemann_sum (fun xplus (f x) (g x)) ptd =
    plus (Riemann_sum f ptd) (Riemann_sum g ptd).

Lemma Riemann_sum_minus (f g : RV) ptd :
  Riemann_sum (fun xminus (f x) (g x)) ptd =
    minus (Riemann_sum f ptd) (Riemann_sum g ptd).

End Riemann_sum.

Section Riemann_sum_Normed.

Context {V : NormedModule R_AbsRing}.

Lemma Riemann_sum_Chasles_0
  (f : RV) (M : R) (x : R) ptd :
   (eps : posreal),
  ( x, SF_h ptd x last (SF_h ptd) (SF_lx ptd) → norm (f x) < M) →
  SF_h ptd x last (SF_h ptd) (SF_lx ptd) →
  pointed_subdiv ptd
  seq_step (SF_lx ptd) < eps
  norm (minus (plus (Riemann_sum f (SF_cut_down ptd x)) (Riemann_sum f (SF_cut_up ptd x)))
    (Riemann_sum f ptd)) < 2 × eps × M.

Lemma Riemann_sum_norm (f : RV) (g : RR) ptd :
  pointed_subdiv ptd
  ( t, SF_h ptd t last (SF_h ptd) (SF_lx ptd) → norm (f t) g t)
  → norm (Riemann_sum f ptd) Riemann_sum g ptd.

End Riemann_sum_Normed.

Lemma Riemann_sum_le (f : RR) (g : RR) ptd :
  pointed_subdiv ptd
  ( t, SF_h ptd t last (SF_h ptd) (SF_lx ptd) → f t g t) →
  Riemann_sum f ptd Riemann_sum g ptd.

Structures

Lemma Riemann_sum_pair {U : ModuleSpace R_Ring} {V : ModuleSpace R_Ring}
  (f : RU × V) ptd :
  Riemann_sum f ptd =
    (Riemann_sum (fun tfst (f t)) ptd, Riemann_sum (fun tsnd (f t)) ptd).

RInt_val

Section RInt_val.

Context {V : ModuleSpace R_Ring}.

Definition RInt_val (f : RV) (a b : R) (n : nat) :=
  Riemann_sum f (SF_seq_f2 (fun x y(x + y) / 2) (unif_part a b n)).

Lemma RInt_val_point (f : RV) (a : R) (n : nat) :
  RInt_val f a a n = zero.

Lemma RInt_val_swap :
   (f : RV) (a b : R) (n : nat),
  RInt_val f a b n = opp (RInt_val f b a n).

Lemma RInt_val_ext (f g : RV) (a b : R) (n : nat) :
  ( x, Rmin a b x Rmax a bf x = g x)
  → RInt_val g a b n = RInt_val f a b n.

Lemma RInt_val_comp_opp (f : RV) (a b : R) (n : nat) :
  RInt_val (fun xf (- x)) a b n = opp (RInt_val f (- a) (- b) n).

Lemma RInt_val_comp_lin (f : RV) (u v : R) (a b : R) (n : nat) :
  scal u (RInt_val (fun xf (u × x + v)) a b n) = RInt_val f (u × a + v) (u × b + v) n.

End RInt_val.

From SF_seq to StepFun

Alternative Chasles relation

Fixpoint seq_cut_down' (s : seq (R×R)) (x x0 : R) : seq (R×R) :=
  match s with
    | [::][:: (x,x0)]
    | h :: t
        match Rle_dec (fst h) x with
          | right _[:: (x,snd h)]
          | left _h :: (seq_cut_down' t x (snd h))
        end
  end.
Fixpoint seq_cut_up' (s : seq (R×R)) (x x0 : R) : seq (R×R) :=
  match s with
    | [::][:: (x,x0)]
    | h :: t
        match Rle_dec (fst h) x with
          | right _(x,x0)::h::t
          | left _seq_cut_up' t x (snd h)
        end
  end.

Definition SF_cut_down' (sf : @SF_seq R) (x : R) x0 :=
  let s := seq_cut_down' ((SF_h sf,x0) :: (SF_t sf)) x x0 in
  mkSF_seq (fst (head (SF_h sf,x0) s)) (behead s).
Definition SF_cut_up' (sf : @SF_seq R) (x : R) x0 :=
  let s := seq_cut_up' ((SF_h sf,x0) :: (SF_t sf)) x x0 in
  mkSF_seq (fst (head (SF_h sf,x0) s)) (behead s).
Lemma SF_Chasles {V : ModuleSpace R_AbsRing} (f : RV) (s : SF_seq) x x0 :
  (SF_h s x last (SF_h s) (unzip1 (SF_t s))) →
  Riemann_sum f s =
  plus (Riemann_sum f (SF_cut_down' s x x0)) (Riemann_sum f (SF_cut_up' s x x0)).

Lemma seq_cut_up_head' (s : seq (R×R)) x x0 z :
  fst (head z (seq_cut_up' s x x0)) = x.

Build StepFun using SF_seq

Lemma ad_SF_compat z0 (s : SF_seq) (pr : SF_sorted Rle s) :
  adapted_couple (SF_fun s z0) (head 0 (SF_lx s)) (last 0 (SF_lx s))
    (seq2Rlist (SF_lx s)) (seq2Rlist (SF_ly s)).

Definition SF_compat_le (s : @SF_seq R) (pr : SF_sorted Rle s) :
  StepFun (head 0 (SF_lx s)) (last 0 (SF_lx s)).

Lemma Riemann_sum_compat f (s : SF_seq) (pr : SF_sorted Rle s) :
  Riemann_sum f s = RiemannInt_SF (SF_compat_le (SF_map f s) (SF_map_sort f s _ pr)).

Build StepFun using uniform partition

Lemma ad_SF_val_fun (f : RR) (a b : R) (n : nat) :
  ((a b) → adapted_couple (SF_val_fun f a b n) a b
      (seq2Rlist (unif_part a b n)) (seq2Rlist (SF_val_ly f a b n)))
   (~(a b)adapted_couple (SF_val_fun f b a n) a b
      (seq2Rlist (unif_part b a n)) (seq2Rlist (SF_val_ly f b a n))).

Definition sf_SF_val_fun (f : RR) (a b : R) (n : nat) : StepFun a b.
Lemma SF_val_subdiv (f : RR) (a b : R) (n : nat) :
  subdivision (sf_SF_val_fun f a b n) =
  match (Rle_dec a b) with
    | left _seq2Rlist (unif_part a b n)
    | right _seq2Rlist (unif_part b a n)
  end.
Lemma SF_val_subdiv_val (f : RR) (a b : R) (n : nat) :
  subdivision_val (sf_SF_val_fun f a b n) =
  match (Rle_dec a b) with
    | left _seq2Rlist (SF_val_ly f a b n)
    | right _seq2Rlist (SF_val_ly f b a n)
  end.

Lemma SF_val_fun_rw (f : RR) (a b : R) (n : nat) (x : R) (Hx : a x b) :
  SF_val_fun f a b n x =
    match (unif_part_nat a b n x Hx) with
      | inleft Hf (a + (INR (proj1_sig H) + /2) × (b-a) / (INR n + 1))
      | inright _f (a + (INR n + /2) × (b-a) / (INR n + 1))
    end.

Lemma RInt_val_Reals (f : RR) (a b : R) (n : nat) :
  RInt_val f a b n = RiemannInt_SF (sf_SF_val_fun f a b n).

Upper and lower step functions


Lemma ex_Im_fct (f : RR) (a b : R) : a b
   x, (fun y x, y = f x Rmin a b < x < Rmax a b) x.

Definition Sup_fct (f : RR) (a b : R) : Rbar :=
  match Req_EM_T a b with
    | right HabLub_Rbar (fun y x, y = f x Rmin a b < x < Rmax a b)
    | left _Finite 0
  end.
Definition Inf_fct (f : RR) (a b : R) : Rbar :=
  match Req_EM_T a b with
    | right HabGlb_Rbar (fun y x, y = f x Rmin a b < x < Rmax a b)
    | left _Finite 0
  end.

Lemma Sup_fct_bound (f : RR) (a b : R) :
  Sup_fct f a b = Sup_fct f b a.
Lemma Inf_fct_bound (f : RR) (a b : R) :
  Inf_fct f a b = Inf_fct f b a.

Lemma Sup_fct_le (f : RR) (a b : R) (x : R) :
  (Rmin a b < x < Rmax a b) →
    Rbar_le (Finite (f x)) (Sup_fct f a b).
Lemma Inf_fct_le (f : RR) (a b : R) (x : R) : (Rmin a b < x < Rmax a b) →
  Rbar_le (Inf_fct f a b) (Finite (f x)).

Lemma Sup_fct_maj (f : RR) (a b : R) (M : R) :
  ( x, Rmin a b < x < Rmax a bf x M) →
  is_finite (Sup_fct f a b).
Lemma Inf_fct_min (f : RR) (a b : R) (m : R) :
  ( x, Rmin a b < x < Rmax a bm f x) →
  is_finite (Inf_fct f a b).

SF_sup and SF_inf

Definition SF_sup_seq (f : RR) (a b : R) (n : nat) : SF_seq :=
  SF_seq_f2 (Sup_fct f) (unif_part a b n).
Lemma SF_sup_lx (f : RR) (a b : R) (n : nat) :
  SF_lx (SF_sup_seq f a b n) = unif_part a b n.
Lemma SF_sup_ly (f : RR) (a b : R) (n : nat) :
  SF_ly (SF_sup_seq f a b n) = behead (pairmap (Sup_fct f) 0 (unif_part a b n)).

Definition SF_inf_seq (f : RR) (a b : R) (n : nat) : SF_seq :=
  SF_seq_f2 (Inf_fct f) (unif_part a b n).
Lemma SF_inf_lx (f : RR) (a b : R) (n : nat) :
  SF_lx (SF_inf_seq f a b n) = unif_part a b n.
Lemma SF_inf_ly (f : RR) (a b : R) (n : nat) :
  SF_ly (SF_inf_seq f a b n) = behead (pairmap (Inf_fct f) 0 (unif_part a b n)).

Lemma SF_sup_bound (f : RR) (a b : R) (n : nat) :
  SF_rev (SF_sup_seq f a b n) = SF_sup_seq f b a n.
Lemma SF_inf_bound (f : RR) (a b : R) (n : nat) :
  SF_rev (SF_inf_seq f a b n) = SF_inf_seq f b a n.

Definition SF_sup_fun (f : RR) (a b : R) (n : nat) (x : R) : Rbar :=
  match (Rle_dec a b) with
    | left _SF_fun (SF_sup_seq f a b n) (Finite 0) x
    | right _SF_fun (SF_sup_seq f b a n) (Finite 0) x
  end.
Definition SF_inf_fun (f : RR) (a b : R) (n : nat) (x : R) : Rbar :=
  match (Rle_dec a b) with
    | left _SF_fun (SF_inf_seq f a b n) (Finite 0) x
    | right _SF_fun (SF_inf_seq f b a n) (Finite 0) x
  end.

Lemma SF_sup_fun_bound (f : RR) (a b : R) (n : nat) (x : R) :
  SF_sup_fun f a b n x = SF_sup_fun f b a n x.
Lemma SF_inf_fun_bound (f : RR) (a b : R) (n : nat) (x : R) :
  SF_inf_fun f a b n x = SF_inf_fun f b a n x.

Lemma SF_sup_fun_rw (f : RR) (a b : R) (n : nat) (x : R) (Hx : a x b) :
  SF_sup_fun f a b n x =
    match (unif_part_nat a b n x Hx) with
      | inleft HSup_fct f (nth 0 (unif_part a b n) (proj1_sig H))
          (nth 0 (unif_part a b n) (S (proj1_sig H)))
      | inright _Sup_fct f (nth 0 (unif_part a b n) (n))
          (nth 0 (unif_part a b n) (S n))
    end.

Lemma SF_inf_fun_rw (f : RR) (a b : R) (n : nat) (x : R) (Hx : a x b) :
  SF_inf_fun f a b n x =
    match (unif_part_nat a b n x Hx) with
      | inleft HInf_fct f (nth 0 (unif_part a b n) (proj1_sig H))
          (nth 0 (unif_part a b n) (S (proj1_sig H)))
      | inright _Inf_fct f (nth 0 (unif_part a b n) (n))
          (nth 0 (unif_part a b n) (S n))
    end.

SF_sup_real is a StepFun


Lemma ad_SF_sup_r (f : RR) (a b : R) (n : nat) :
  ((a b) → adapted_couple (fun xreal (SF_sup_fun f a b n x)) a b
      (seq2Rlist (unif_part a b n))
      (seq2Rlist (behead (pairmap (fun x yreal (Sup_fct f x y)) 0 (unif_part a b n)))))
   (~(a b)adapted_couple (fun xreal (SF_sup_fun f a b n x)) a b
      (seq2Rlist (unif_part b a n))
      (seq2Rlist (behead (pairmap (fun x yreal (Sup_fct f x y)) 0 (unif_part b a n))))).

Definition SF_sup_r (f : RR) (a b : R) (n : nat) : StepFun a b.
Lemma SF_sup_subdiv (f : RR) (a b : R) (n : nat) :
  subdivision (SF_sup_r f a b n) =
  match (Rle_dec a b) with
    | left _seq2Rlist (unif_part a b n)
    | right _seq2Rlist (unif_part b a n)
  end.
Lemma SF_sup_subdiv_val (f : RR) (a b : R) (n : nat) :
  subdivision_val (SF_sup_r f a b n) =
  match (Rle_dec a b) with
    | left _ ⇒ (seq2Rlist (behead (pairmap (fun x yreal (Sup_fct f x y)) 0 (unif_part a b n))))
    | right _ ⇒ (seq2Rlist (behead (pairmap (fun x yreal (Sup_fct f x y)) 0 (unif_part b a n))))
  end.

Lemma SF_sup_r_bound (f : RR) (a b : R) (n : nat) :
   x, SF_sup_r f a b n x = SF_sup_r f b a n x.

SF_inf_real is a StepFun


Lemma ad_SF_inf_r (f : RR) (a b : R) (n : nat) :
  ((a b) → adapted_couple (fun xreal (SF_inf_fun f a b n x)) a b
      (seq2Rlist (unif_part a b n))
      (seq2Rlist (behead (pairmap (fun x yreal (Inf_fct f x y)) 0 (unif_part a b n)))))
   (~(a b)adapted_couple (fun xreal (SF_inf_fun f a b n x)) a b
      (seq2Rlist (unif_part b a n))
      (seq2Rlist (behead (pairmap (fun x yreal (Inf_fct f x y)) 0 (unif_part b a n))))).

Definition SF_inf_r (f : RR) (a b : R) (n : nat) : StepFun a b.
Lemma SF_inf_subdiv (f : RR) (a b : R) (n : nat) :
  subdivision (SF_inf_r f a b n) =
  match (Rle_dec a b) with
    | left _seq2Rlist (unif_part a b n)
    | right _seq2Rlist (unif_part b a n)
  end.
Lemma SF_inf_subdiv_val (f : RR) (a b : R) (n : nat) :
  subdivision_val (SF_inf_r f a b n) =
  match (Rle_dec a b) with
    | left _ ⇒ (seq2Rlist (behead (pairmap (fun x yreal (Inf_fct f x y)) 0 (unif_part a b n))))
    | right _ ⇒ (seq2Rlist (behead (pairmap (fun x yreal (Inf_fct f x y)) 0 (unif_part b a n))))
  end.

Lemma SF_inf_r_bound (f : RR) (a b : R) (n : nat) :
   x, SF_inf_r f a b n x = SF_inf_r f b a n x.