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

Set Implicit Arguments.

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

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:Rlist) : Prop :=
  ordered_Rlist l /\
  pos_Rl l 0 = Rmin a b /\
  pos_Rl l (pred (Rlength l)) = Rmax a b /\
  Rlength l = S (Rlength lf) /\
  (forall i:nat,
    (i < pred (Rlength 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:Rlist) :=
  adapted_couple f a b l lf /\
  (forall i:nat,
    (i < pred (Rlength 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 (Rlength l))%nat -> pos_Rl l i <> pos_Rl l (S i)).

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

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

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

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

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

Fixpoint Int_SF (l k:Rlist) : 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.

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.

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:Rlist),
    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:Rlist),
    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:Rlist),
    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:Rlist) (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:Rlist),
    adapted_couple f a b l lf -> a <> b -> (2 <= Rlength l)%nat.

Lemma StepFun_P10 :
  forall (f:R -> R) (l lf:Rlist) (a b:R),
    a <= b ->
    adapted_couple f a b l lf ->
    exists l' : Rlist,
      (exists lf' : Rlist, 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:Rlist)
    (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:Rlist),
    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:Rlist)
    (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:Rlist) (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:Rlist) (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:Rlist) (a b:R),
    adapted_couple f a b l lf ->
    exists l' : Rlist,
      (exists lf' : Rlist, adapted_couple_opt f a b l' lf').

Lemma StepFun_P17 :
  forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (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:Rlist) (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:Rlist) (f:R -> R),
    (0 < Rlength l)%nat -> Rlength l = S (Rlength (FF l f)).

Lemma StepFun_P21 :
  forall (a b:R) (f:R -> R) (l:Rlist),
    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:Rlist),
    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:Rlist),
    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:Rlist),
    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:Rlist),
    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:Rlist),
    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:Rlist),
    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).

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:Rlist),
    adapted_couple f a b l lf ->
    adapted_couple (fun x:R => Rabs (f x)) a b l (app_Rlist lf Rabs).

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:Rlist,
    ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (app_Rlist l2 Rabs) 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:Rlist) (a b:R) (f g:R -> R),
    ordered_Rlist l ->
    pos_Rl l 0 = a ->
    pos_Rl l (pred (Rlength 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:Rlist),
    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:Rlist) (a b:R) (f:R -> R),
    ordered_Rlist l ->
    pos_Rl l 0 = a ->
    pos_Rl l (pred (Rlength l)) = b ->
    { g:StepFun a b |
      g b = f b /\
      (forall i:nat,
        (i < pred (Rlength 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:Rlist),
    a < b ->
    b < c ->
    adapted_couple f a b l1 lf1 ->
    adapted_couple f b c l2 lf2 ->
    adapted_couple f a c (cons_Rlist l1 l2) (FF (cons_Rlist 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:Rlist) (f:R -> R),
    pos_Rl l1 (pred (Rlength l1)) = pos_Rl l2 0 ->
    Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist 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.