Require Import Reals Psatz.
Require Import mathcomp.ssreflect.ssreflect mathcomp.ssreflect.seq mathcomp.ssreflect.ssrbool.
Require Import Rcomplements Rbar Lub.
Require Import Hierarchy.

Open Scope R_scope.

Fixpoint seq2Rlist (s : seq R) :=
  match s with
    | [::] ⇒ RList.nil
    | h::t ⇒ RList.cons h (seq2Rlist t)
  end.
Fixpoint Rlist2seq (s : Rlist) : seq R :=
  match s with
    | RList.nil ⇒ [::]
    | RList.cons h t ⇒ h::(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.

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).

Fixpoint sorted {T : Type} (Ord : T → T → Prop) (s : seq T) :=
  match s with
    | [::] | [:: _] ⇒ True
    | h0 :: (h1 :: t1) as t0 ⇒ Ord h0 h1 ∧ sorted Ord t0
  end.
Lemma sorted_nth {T : Type} (Ord : T → T → Prop) (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 : T → T → Prop) (s1 s2 : seq T) x0 :
  sorted Ord s1 → sorted Ord s2 → Ord (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 s → head 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).

Definition seq_step (s : seq R) :=
  foldr Rmax 0 (pairmap (fun x y ⇒ Rabs (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.

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.

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_seq → Type) :
  (∀ x0 : R, P (SF_nil x0)) → (∀ h s, P (SF_cons h s))
    → (∀ s, P s).
Lemma SF_cons_ind (P : SF_seq → Type) :
  (∀ x0 : R, P (SF_nil x0)) → (∀ h s, P s → P (SF_cons h s))
    → (∀ s, P s).

Lemma SF_rcons_dec (P : SF_seq → Type) :
  (∀ x0 : R, P (SF_nil x0)) → (∀ s t, P (SF_rcons s t))
    → (∀ s, P s).
Lemma SF_rcons_ind (P : SF_seq → Type) :
  (∀ x0 : R, P (SF_nil x0)) → (∀ s t, P s → P (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.

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 = s0 → SF_lx s = SF_lx s0.
Lemma SF_ly_surj (s s0 : SF_seq) :
  s = s0 → SF_ly s = SF_ly s0.
Lemma SF_lx_ly_inj (s s0 : SF_seq) :
  SF_lx s = SF_lx s0 → SF_ly s = SF_ly s0 → s = s0.

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.

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 = s0 → SF_rev s = SF_rev s0.
Lemma SF_rev_inj (s s0 : SF_seq) :
  SF_rev s = SF_rev s0 → s = s0.

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.

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).

Definition SF_sorted (Ord : R → R → Prop) (s : SF_seq) :=
  sorted Ord (SF_lx s).

End SF_seq.

Section SF_map.

Context {T T0 : Type}.

Definition SF_map (f : T → T0) (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 : T → T0) (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 : T → T0) (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 : T → T0) (s : SF_seq) :
  SF_lx (SF_map f s) = SF_lx s.

Lemma SF_map_ly (f : T → T0) (s : SF_seq) :
  SF_ly (SF_map f s) = map f (SF_ly s).

Lemma SF_map_rev (f : T → T0) s :
  SF_rev (SF_map f s) = SF_map f (SF_rev s).

Lemma SF_map_sort (f : T → T0) (s : SF_seq) (Ord : R → R → Prop) :
  SF_sorted Ord s → SF_sorted Ord (SF_map f s).

Lemma SF_size_map (f : T → T0) s :
  SF_size (SF_map f s) = SF_size s.

End SF_map.

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 ptd → SF_sorted Rle ptd.
Lemma ptd_sort' ptd :
  pointed_subdiv ptd → sorted 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 x → pointed_subdiv y
  → pointed_subdiv (SF_cat x y).

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 ≤ x → pointed_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 ≤ x → SF_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 h → SF_cut_down (SF_cons h ptd) x = SF_nil x.
Lemma SF_cut_up_cons_0 h ptd x :
  x < fst h → SF_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 ptd → SF_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 ptd → SF_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 ≤ x → SF_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 ≤ x → SF_cut_up (SF_cons h ptd) x = SF_cut_up ptd x.

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 :: s0 ⇒ match 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 H ⇒ nth 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 : T → T0) (s : SF_seq) y0 :
  ∀ x, SF_fun (SF_map f s) (f y0) x = f (SF_fun s y0 x).

Definition SF_seq_f1 {T : Type} (f1 : R → T) (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 : R → R → T) (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 : R → T) (h : R) (P : seq R) :
  (0 < size P)%nat → SF_seq_f1 f1 (h::P) = SF_cons (h,f1 h) (SF_seq_f1 f1 P).
Lemma SF_cons_f2 {T : Type} (f2 : R → R → T) (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 : R → T) P :
  SF_size (SF_seq_f1 f1 P) = Peano.pred (size P).
Lemma SF_size_f2 {T : Type} (f2 : R → R → T) P :
  SF_size (SF_seq_f2 f2 P) = Peano.pred (size P).

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

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

Lemma SF_sorted_f1 {T : Type} (f1 : R → T) P Ord :
  (sorted Ord P) ↔ (SF_sorted Ord (SF_seq_f1 f1 P)).
Lemma SF_sorted_f2 {T : Type} (f2 : R → R → T) P Ord :
  (sorted Ord P) ↔ (SF_sorted Ord (SF_seq_f2 f2 P)).

Lemma SF_rev_f2 {T : Type} (f2 : R → R → T) 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 : T → T0) (f1 : R → T) P :
  SF_map f (SF_seq_f1 f1 P) = SF_seq_f1 (fun x ⇒ f (f1 x)) P.
Lemma SF_map_f2 {T T0 : Type} (f : T → T0) (f2 : R → R → T) P :
  SF_map f (SF_seq_f2 f2 P) = SF_seq_f2 (fun x y ⇒ f (f2 x y)) P.

Lemma ptd_f2 (f : R → R → R) s :
  sorted Rle s → (∀ x y, x ≤ y → x ≤ f x y ≤ y)
  → pointed_subdiv (SF_seq_f2 f s).

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

Definition unif_part (a b : R) (n : nat) : seq R :=
  mkseq (fun i ⇒ a + (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 ≤ b → sorted Rle (unif_part a b 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 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 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 : R → T) (a b : R) (n : nat) : SF_seq :=
  SF_seq_f2 (fun x y ⇒ f ((x+y)/2)) (unif_part a b n).
Definition SF_val_fun {T} (f : R → T) (a b : R) (n : nat) (x : R) : T :=
  SF_fun_f2 (fun x y ⇒ f ((x+y)/2)) (unif_part a b n) x.

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

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

Lemma Riemann_fine_unif_part :
  ∀ (f : R → R → R) (a b : R) (n : nat),
  (∀ a b, a ≤ b → a ≤ 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 ptd ⇒ pointed_subdiv ptd ∧ SF_h ptd = Rmin a b ∧ last (SF_h ptd) (SF_lx ptd) = Rmax a b)
    (locally_dist (fun ptd ⇒ seq_step (SF_lx ptd))).

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

Section Riemann_sum.

Context {V : ModuleSpace R_Ring}.

Definition Riemann_sum (f : R → V) (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 : R → V) (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 : R → V) 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 : R → V) 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 : R → V) (g : R → R) ptd :
  Riemann_sum (fun x ⇒ f (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 : R → V) ptd :
  Riemann_sum (fun x ⇒ scal a (f x)) ptd = scal a (Riemann_sum f ptd).

Lemma Riemann_sum_opp (f : R → V) ptd :
  Riemann_sum (fun x ⇒ opp (f x)) ptd = opp (Riemann_sum f ptd).

Lemma Riemann_sum_plus (f g : R → V) ptd :
  Riemann_sum (fun x ⇒ plus (f x) (g x)) ptd =
    plus (Riemann_sum f ptd) (Riemann_sum g ptd).

Lemma Riemann_sum_minus (f g : R → V) ptd :
  Riemann_sum (fun x ⇒ minus (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 : R → V) (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 : R → V) (g : R → R) 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 : R → R) (g : R → R) 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.

Lemma Riemann_sum_pair {U : ModuleSpace R_Ring} {V : ModuleSpace R_Ring}
  (f : R → U × V) ptd :
  Riemann_sum f ptd =
    (Riemann_sum (fun t ⇒ fst (f t)) ptd, Riemann_sum (fun t ⇒ snd (f t)) ptd).

Section RInt_val.

Context {V : ModuleSpace R_Ring}.

Definition RInt_val (f : R → V) (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 : R → V) (a : R) (n : nat) :
  RInt_val f a a n = zero.

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

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

Lemma RInt_val_comp_opp (f : R → V) (a b : R) (n : nat) :
  RInt_val (fun x ⇒ f (- x)) a b n = opp (RInt_val f (- a) (- b) n).

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

End RInt_val.

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 : R → V) (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.

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)).

Lemma ad_SF_val_fun (f : R → R) (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 : R → R) (a b : R) (n : nat) : StepFun a b.
Lemma SF_val_subdiv (f : R → R) (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 : R → R) (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 : R → R) (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 H ⇒ f (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 : R → R) (a b : R) (n : nat) :
  RInt_val f a b n = RiemannInt_SF (sf_SF_val_fun f a b n).