# Library Coq.Reals.RiemannInt_SF

Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis_reg.
Require Import Classical_Prop.
Require Import List.
Require Import RList.
Local Open Scope R_scope.

Set Implicit Arguments.

# Each bounded subset of N has a maximal element

Definition Nbound (I:nat -> Prop) : Prop :=
exists n : nat, (forall i:nat, I i -> (i <= n)%nat).

Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z.of_nat n}.

Lemma Nzorn :
forall I:nat -> Prop,
(exists n : nat, I n) ->
Nbound I -> { n:nat | I n /\ (forall i:nat, I i -> (i <= n)%nat) }.

# Step functions

Definition open_interval (a b x:R) : Prop := a < x < b.
Definition co_interval (a b x:R) : Prop := a <= x < b.

Definition adapted_couple (f:R -> R) (a b:R) (l lf:list R) : Prop :=
ordered_Rlist l /\
pos_Rl l 0 = Rmin a b /\
pos_Rl l (pred (length l)) = Rmax a b /\
length l = S (length lf) /\
(forall i:nat,
(i < pred (length l))%nat ->
constant_D_eq f (open_interval (pos_Rl l i) (pos_Rl l (S i)))
(pos_Rl lf i)).

Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:list R) :=
adapted_couple f a b l lf /\
(forall i:nat,
(i < pred (length lf))%nat ->
pos_Rl lf i <> pos_Rl lf (S i) \/ f (pos_Rl l (S i)) <> pos_Rl lf i) /\
(forall i:nat, (i < pred (length l))%nat -> pos_Rl l i <> pos_Rl l (S i)).

Definition is_subdivision (f:R -> R) (a b:R) (l:list R) : Type :=
{ l0:list R & adapted_couple f a b l l0 }.

Definition IsStepFun (f:R -> R) (a b:R) : Type :=
{ l:list R & is_subdivision f a b l }.

## Class of step functions

Record StepFun (a b:R) : Type := mkStepFun
{fe :> R -> R; pre : IsStepFun fe a b}.

Definition subdivision (a b:R) (f:StepFun a b) : list R := projT1 (pre f).

Definition subdivision_val (a b:R) (f:StepFun a b) : list R :=
match projT2 (pre f) with
| existT _ a b => a
end.

Fixpoint Int_SF (l k:list R) : R :=
match l with
| nil => 0
| cons a l' =>
match k with
| nil => 0
| cons x nil => 0
| cons x (cons y k') => a * (y - x) + Int_SF l' (cons y k')
end
end.

## Integral of step functions

Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R :=
match Rle_dec a b with
| left _ => Int_SF (subdivision_val f) (subdivision f)
| right _ => - Int_SF (subdivision_val f) (subdivision f)
end.

## Properties of step functions

Lemma StepFun_P1 :
forall (a b:R) (f:StepFun a b),
adapted_couple f a b (subdivision f) (subdivision_val f).

Lemma StepFun_P2 :
forall (a b:R) (f:R -> R) (l lf:list R),
adapted_couple f a b l lf -> adapted_couple f b a l lf.

Lemma StepFun_P3 :
forall a b c:R,
a <= b ->
adapted_couple (fct_cte c) a b (cons a (cons b nil)) (cons c nil).

Lemma StepFun_P4 : forall a b c:R, IsStepFun (fct_cte c) a b.

Lemma StepFun_P5 :
forall (a b:R) (f:R -> R) (l:list R),
is_subdivision f a b l -> is_subdivision f b a l.

Lemma StepFun_P6 :
forall (f:R -> R) (a b:R), IsStepFun f a b -> IsStepFun f b a.

Lemma StepFun_P7 :
forall (a b r1 r2 r3:R) (f:R -> R) (l lf:list R),
a <= b ->
adapted_couple f a b (cons r1 (cons r2 l)) (cons r3 lf) ->
adapted_couple f r2 b (cons r2 l) lf.

Lemma StepFun_P8 :
forall (f:R -> R) (l1 lf1:list R) (a b:R),
adapted_couple f a b l1 lf1 -> a = b -> Int_SF lf1 l1 = 0.

Lemma StepFun_P9 :
forall (a b:R) (f:R -> R) (l lf:list R),
adapted_couple f a b l lf -> a <> b -> (2 <= length l)%nat.

Lemma StepFun_P10 :
forall (f:R -> R) (l lf:list R) (a b:R),
a <= b ->
adapted_couple f a b l lf ->
exists l' : list R,
(exists lf' : list R, adapted_couple_opt f a b l' lf').

Lemma StepFun_P11 :
forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:list R)
(f:R -> R),
a < b ->
adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) ->
adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2.

Lemma StepFun_P12 :
forall (a b:R) (f:R -> R) (l lf:list R),
adapted_couple_opt f a b l lf -> adapted_couple_opt f b a l lf.

Lemma StepFun_P13 :
forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:list R)
(f:R -> R),
a <> b ->
adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) ->
adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2.

Lemma StepFun_P14 :
forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R),
a <= b ->
adapted_couple f a b l1 lf1 ->
adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2.

Lemma StepFun_P15 :
forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R),
adapted_couple f a b l1 lf1 ->
adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2.

Lemma StepFun_P16 :
forall (f:R -> R) (l lf:list R) (a b:R),
adapted_couple f a b l lf ->
exists l' : list R,
(exists lf' : list R, adapted_couple_opt f a b l' lf').

Lemma StepFun_P17 :
forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R),
adapted_couple f a b l1 lf1 ->
adapted_couple f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2.

Lemma StepFun_P18 :
forall a b c:R, RiemannInt_SF (mkStepFun (StepFun_P4 a b c)) = c * (b - a).

Lemma StepFun_P19 :
forall (l1:list R) (f g:R -> R) (l:R),
Int_SF (FF l1 (fun x:R => f x + l * g x)) l1 =
Int_SF (FF l1 f) l1 + l * Int_SF (FF l1 g) l1.

Lemma StepFun_P20 :
forall (l:list R) (f:R -> R),
(0 < length l)%nat -> length l = S (length (FF l f)).

Lemma StepFun_P21 :
forall (a b:R) (f:R -> R) (l:list R),
is_subdivision f a b l -> adapted_couple f a b l (FF l f).

Lemma StepFun_P22 :
forall (a b:R) (f g:R -> R) (lf lg:list R),
a <= b ->
is_subdivision f a b lf ->
is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg).

Lemma StepFun_P23 :
forall (a b:R) (f g:R -> R) (lf lg:list R),
is_subdivision f a b lf ->
is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg).

Lemma StepFun_P24 :
forall (a b:R) (f g:R -> R) (lf lg:list R),
a <= b ->
is_subdivision f a b lf ->
is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg).

Lemma StepFun_P25 :
forall (a b:R) (f g:R -> R) (lf lg:list R),
is_subdivision f a b lf ->
is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg).

Lemma StepFun_P26 :
forall (a b l:R) (f g:R -> R) (l1:list R),
is_subdivision f a b l1 ->
is_subdivision g a b l1 ->
is_subdivision (fun x:R => f x + l * g x) a b l1.

Lemma StepFun_P27 :
forall (a b l:R) (f g:R -> R) (lf lg:list R),
is_subdivision f a b lf ->
is_subdivision g a b lg ->
is_subdivision (fun x:R => f x + l * g x) a b (cons_ORlist lf lg).

The set of step functions on a,b is a vectorial space
Lemma StepFun_P28 :
forall (a b l:R) (f g:StepFun a b), IsStepFun (fun x:R => f x + l * g x) a b.

Lemma StepFun_P29 :
forall (a b:R) (f:StepFun a b), is_subdivision f a b (subdivision f).

Lemma StepFun_P30 :
forall (a b l:R) (f g:StepFun a b),
RiemannInt_SF (mkStepFun (StepFun_P28 l f g)) =
RiemannInt_SF f + l * RiemannInt_SF g.

Lemma StepFun_P31 :
forall (a b:R) (f:R -> R) (l lf:list R),
adapted_couple f a b l lf ->
adapted_couple (fun x:R => Rabs (f x)) a b l (map Rabs lf).

Lemma StepFun_P32 :
forall (a b:R) (f:StepFun a b), IsStepFun (fun x:R => Rabs (f x)) a b.

Lemma StepFun_P33 :
forall l2 l1:list R,
ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (map Rabs l2) l1.

Lemma StepFun_P34 :
forall (a b:R) (f:StepFun a b),
a <= b ->
Rabs (RiemannInt_SF f) <= RiemannInt_SF (mkStepFun (StepFun_P32 f)).

Lemma StepFun_P35 :
forall (l:list R) (a b:R) (f g:R -> R),
ordered_Rlist l ->
pos_Rl l 0 = a ->
pos_Rl l (pred (length l)) = b ->
(forall x:R, a < x < b -> f x <= g x) ->
Int_SF (FF l f) l <= Int_SF (FF l g) l.

Lemma StepFun_P36 :
forall (a b:R) (f g:StepFun a b) (l:list R),
a <= b ->
is_subdivision f a b l ->
is_subdivision g a b l ->
(forall x:R, a < x < b -> f x <= g x) ->
RiemannInt_SF f <= RiemannInt_SF g.

Lemma StepFun_P37 :
forall (a b:R) (f g:StepFun a b),
a <= b ->
(forall x:R, a < x < b -> f x <= g x) ->
RiemannInt_SF f <= RiemannInt_SF g.

Lemma StepFun_P38 :
forall (l:list R) (a b:R) (f:R -> R),
ordered_Rlist l ->
pos_Rl l 0 = a ->
pos_Rl l (pred (length l)) = b ->
{ g:StepFun a b |
g b = f b /\
(forall i:nat,
(i < pred (length l))%nat ->
constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i)))
(f (pos_Rl l i))) }.

Lemma StepFun_P39 :
forall (a b:R) (f:StepFun a b),
RiemannInt_SF f = - RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))).

Lemma StepFun_P40 :
forall (f:R -> R) (a b c:R) (l1 l2 lf1 lf2:list R),
a < b ->
b < c ->
adapted_couple f a b l1 lf1 ->
adapted_couple f b c l2 lf2 ->
adapted_couple f a c (app l1 l2) (FF (app l1 l2) f).

Lemma StepFun_P41 :
forall (f:R -> R) (a b c:R),
a <= b -> b <= c -> IsStepFun f a b -> IsStepFun f b c -> IsStepFun f a c.

Lemma StepFun_P42 :
forall (l1 l2:list R) (f:R -> R),
pos_Rl l1 (pred (length l1)) = pos_Rl l2 0 ->
Int_SF (FF (app l1 l2) f) (app l1 l2) =
Int_SF (FF l1 f) l1 + Int_SF (FF l2 f) l2.

Lemma StepFun_P43 :
forall (f:R -> R) (a b c:R) (pr1:IsStepFun f a b)
(pr2:IsStepFun f b c) (pr3:IsStepFun f a c),
RiemannInt_SF (mkStepFun pr1) + RiemannInt_SF (mkStepFun pr2) =
RiemannInt_SF (mkStepFun pr3).

Lemma StepFun_P44 :
forall (f:R -> R) (a b c:R),
IsStepFun f a b -> a <= c <= b -> IsStepFun f a c.

Lemma StepFun_P45 :
forall (f:R -> R) (a b c:R),
IsStepFun f a b -> a <= c <= b -> IsStepFun f c b.

Lemma StepFun_P46 :
forall (f:R -> R) (a b c:R),
IsStepFun f a b -> IsStepFun f b c -> IsStepFun f a c.