Library Coq.Reals.RiemannInt

Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis_reg.
Require Import Rbase.
Require Import RiemannInt_SF.
Require Import Classical_Prop.
Require Import Classical_Pred_Type.
Require Import Max.
Local Open Scope R_scope.

Set Implicit Arguments.

Definition Riemann_integrable (f:R -> R) (a b:R) : Type :=
  forall eps:posreal,
    { phi:StepFun a b &
      { psi:StepFun a b |
        (forall t:R,
          Rmin a b <= t <= Rmax a b -> Rabs (f t - phi t) <= psi t) /\
        Rabs (RiemannInt_SF psi) < eps } }.

Definition phi_sequence (un:nat -> posreal) (f:R -> R)
  (a b:R) (pr:Riemann_integrable f a b) (n:nat) :=
  projT1 (pr (un n)).

Lemma phi_sequence_prop :
  forall (un:nat -> posreal) (f:R -> R) (a b:R) (pr:Riemann_integrable f a b)
    (N:nat),
    { psi:StepFun a b |
      (forall t:R,
        Rmin a b <= t <= Rmax a b ->
        Rabs (f t - phi_sequence un pr N t) <= psi t) /\
      Rabs (RiemannInt_SF psi) < un N }.

Lemma RiemannInt_P1 :
  forall (f:R -> R) (a b:R),
    Riemann_integrable f a b -> Riemann_integrable f b a.

Lemma RiemannInt_P2 :
  forall (f:R -> R) (a b:R) (un:nat -> posreal) (vn wn:nat -> StepFun a b),
    Un_cv un 0 ->
    a <= b ->
    (forall n:nat,
      (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\
      Rabs (RiemannInt_SF (wn n)) < un n) ->
    { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }.

Lemma RiemannInt_P3 :
  forall (f:R -> R) (a b:R) (un:nat -> posreal) (vn wn:nat -> StepFun a b),
    Un_cv un 0 ->
    (forall n:nat,
      (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\
      Rabs (RiemannInt_SF (wn n)) < un n) ->
    { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }.

Lemma RiemannInt_exists :
  forall (f:R -> R) (a b:R) (pr:Riemann_integrable f a b)
    (un:nat -> posreal),
    Un_cv un 0 ->
    { l:R | Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr N)) l }.

Lemma RiemannInt_P4 :
  forall (f:R -> R) (a b l:R) (pr1 pr2:Riemann_integrable f a b)
    (un vn:nat -> posreal),
    Un_cv un 0 ->
    Un_cv vn 0 ->
    Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr1 N)) l ->
    Un_cv (fun N:nat => RiemannInt_SF (phi_sequence vn pr2 N)) l.

Lemma RinvN_pos : forall n:nat, 0 < / (INR n + 1).

Definition RinvN (N:nat) : posreal := mkposreal _ (RinvN_pos N).

Lemma RinvN_cv : Un_cv RinvN 0.

Definition RiemannInt (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) : R :=
  let (a,_) := RiemannInt_exists pr RinvN RinvN_cv in a.

Lemma RiemannInt_P5 :
  forall (f:R -> R) (a b:R) (pr1 pr2:Riemann_integrable f a b),
    RiemannInt pr1 = RiemannInt pr2.

Lemma maxN :
  forall (a b:R) (del:posreal),
    a < b -> { n:nat | a + INR n * del < b /\ b <= a + INR (S n) * del }.

Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : Rlist :=
  match N with
    | O => cons y nil
    | S p => cons x (SubEquiN p (x + del) y del)
  end.

Definition max_N (a b:R) (del:posreal) (h:a < b) : nat :=
  let (N,_) := maxN del h in N.

Definition SubEqui (a b:R) (del:posreal) (h:a < b) : Rlist :=
  SubEquiN (S (max_N del h)) a b del.

Lemma Heine_cor1 :
  forall (f:R -> R) (a b:R),
    a < b ->
    (forall x:R, a <= x <= b -> continuity_pt f x) ->
    forall eps:posreal,
      { delta:posreal |
        delta <= b - a /\
        (forall x y:R,
          a <= x <= b ->
          a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps) }.

Lemma Heine_cor2 :
  forall (f:R -> R) (a b:R),
    (forall x:R, a <= x <= b -> continuity_pt f x) ->
    forall eps:posreal,
      { delta:posreal |
        forall x y:R,
          a <= x <= b ->
          a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps }.

Lemma SubEqui_P1 :
  forall (a b:R) (del:posreal) (h:a < b), pos_Rl (SubEqui del h) 0 = a.

Lemma SubEqui_P2 :
  forall (a b:R) (del:posreal) (h:a < b),
    pos_Rl (SubEqui del h) (pred (Rlength (SubEqui del h))) = b.

Lemma SubEqui_P3 :
  forall (N:nat) (a b:R) (del:posreal), Rlength (SubEquiN N a b del) = S N.

Lemma SubEqui_P4 :
  forall (N:nat) (a b:R) (del:posreal) (i:nat),
    (i < S N)%nat -> pos_Rl (SubEquiN (S N) a b del) i = a + INR i * del.

Lemma SubEqui_P5 :
  forall (a b:R) (del:posreal) (h:a < b),
    Rlength (SubEqui del h) = S (S (max_N del h)).

Lemma SubEqui_P6 :
  forall (a b:R) (del:posreal) (h:a < b) (i:nat),
    (i < S (max_N del h))%nat -> pos_Rl (SubEqui del h) i = a + INR i * del.

Lemma SubEqui_P7 :
  forall (a b:R) (del:posreal) (h:a < b), ordered_Rlist (SubEqui del h).

Lemma SubEqui_P8 :
  forall (a b:R) (del:posreal) (h:a < b) (i:nat),
    (i < Rlength (SubEqui del h))%nat -> a <= pos_Rl (SubEqui del h) i <= b.

Lemma SubEqui_P9 :
  forall (a b:R) (del:posreal) (f:R -> R) (h:a < b),
    { g:StepFun a b |
      g b = f b /\
      (forall i:nat,
        (i < pred (Rlength (SubEqui del h)))%nat ->
        constant_D_eq g
        (co_interval (pos_Rl (SubEqui del h) i)
          (pos_Rl (SubEqui del h) (S i)))
        (f (pos_Rl (SubEqui del h) i))) }.

Lemma RiemannInt_P6 :
  forall (f:R -> R) (a b:R),
    a < b ->
    (forall x:R, a <= x <= b -> continuity_pt f x) -> Riemann_integrable f a b.

Lemma RiemannInt_P7 : forall (f:R -> R) (a:R), Riemann_integrable f a a.

Lemma continuity_implies_RiemannInt :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall x:R, a <= x <= b -> continuity_pt f x) -> Riemann_integrable f a b.

Lemma RiemannInt_P8 :
  forall (f:R -> R) (a b:R) (pr1:Riemann_integrable f a b)
    (pr2:Riemann_integrable f b a), RiemannInt pr1 = - RiemannInt pr2.

Lemma RiemannInt_P9 :
  forall (f:R -> R) (a:R) (pr:Riemann_integrable f a a), RiemannInt pr = 0.

Lemma Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.

Lemma RiemannInt_P10 :
  forall (f g:R -> R) (a b l:R),
    Riemann_integrable f a b ->
    Riemann_integrable g a b ->
    Riemann_integrable (fun x:R => f x + l * g x) a b.

Lemma RiemannInt_P11 :
  forall (f:R -> R) (a b l:R) (un:nat -> posreal)
    (phi1 phi2 psi1 psi2:nat -> StepFun a b),
    Un_cv un 0 ->
    (forall n:nat,
      (forall t:R,
        Rmin a b <= t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi1 n t) /\
      Rabs (RiemannInt_SF (psi1 n)) < un n) ->
    (forall n:nat,
      (forall t:R,
        Rmin a b <= t <= Rmax a b -> Rabs (f t - phi2 n t) <= psi2 n t) /\
      Rabs (RiemannInt_SF (psi2 n)) < un n) ->
    Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) l ->
    Un_cv (fun N:nat => RiemannInt_SF (phi2 N)) l.

Lemma RiemannInt_P12 :
  forall (f g:R -> R) (a b l:R) (pr1:Riemann_integrable f a b)
    (pr2:Riemann_integrable g a b)
    (pr3:Riemann_integrable (fun x:R => f x + l * g x) a b),
    a <= b -> RiemannInt pr3 = RiemannInt pr1 + l * RiemannInt pr2.

Lemma RiemannInt_P13 :
  forall (f g:R -> R) (a b l:R) (pr1:Riemann_integrable f a b)
    (pr2:Riemann_integrable g a b)
    (pr3:Riemann_integrable (fun x:R => f x + l * g x) a b),
    RiemannInt pr3 = RiemannInt pr1 + l * RiemannInt pr2.

Lemma RiemannInt_P14 : forall a b c:R, Riemann_integrable (fct_cte c) a b.

Lemma RiemannInt_P15 :
  forall (a b c:R) (pr:Riemann_integrable (fct_cte c) a b),
    RiemannInt pr = c * (b - a).

Lemma RiemannInt_P16 :
  forall (f:R -> R) (a b:R),
    Riemann_integrable f a b -> Riemann_integrable (fun x:R => Rabs (f x)) a b.

Lemma Rle_cv_lim :
  forall (Un Vn:nat -> R) (l1 l2:R),
    (forall n:nat, Un n <= Vn n) -> Un_cv Un l1 -> Un_cv Vn l2 -> l1 <= l2.

Lemma RiemannInt_P17 :
  forall (f:R -> R) (a b:R) (pr1:Riemann_integrable f a b)
    (pr2:Riemann_integrable (fun x:R => Rabs (f x)) a b),
    a <= b -> Rabs (RiemannInt pr1) <= RiemannInt pr2.

Lemma RiemannInt_P18 :
  forall (f g:R -> R) (a b:R) (pr1:Riemann_integrable f a b)
    (pr2:Riemann_integrable g a b),
    a <= b ->
    (forall x:R, a < x < b -> f x = g x) -> RiemannInt pr1 = RiemannInt pr2.

Lemma RiemannInt_P19 :
  forall (f g:R -> R) (a b:R) (pr1:Riemann_integrable f a b)
    (pr2:Riemann_integrable g a b),
    a <= b ->
    (forall x:R, a < x < b -> f x <= g x) -> RiemannInt pr1 <= RiemannInt pr2.

Lemma FTC_P1 :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall x:R, a <= x <= b -> continuity_pt f x) ->
    forall x:R, a <= x -> x <= b -> Riemann_integrable f a x.

Definition primitive (f:R -> R) (a b:R) (h:a <= b)
  (pr:forall x:R, a <= x -> x <= b -> Riemann_integrable f a x)
  (x:R) : R :=
  match Rle_dec a x with
    | left r =>
      match Rle_dec x b with
        | left r0 => RiemannInt (pr x r r0)
        | right _ => f b * (x - b) + RiemannInt (pr b h (Rle_refl b))
      end
    | right _ => f a * (x - a)
  end.

Lemma RiemannInt_P20 :
  forall (f:R -> R) (a b:R) (h:a <= b)
    (pr:forall x:R, a <= x -> x <= b -> Riemann_integrable f a x)
    (pr0:Riemann_integrable f a b),
    RiemannInt pr0 = primitive h pr b - primitive h pr a.

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

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

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

Lemma RiemannInt_P24 :
  forall (f:R -> R) (a b c:R),
    Riemann_integrable f a b ->
    Riemann_integrable f b c -> Riemann_integrable f a c.

Lemma RiemannInt_P25 :
  forall (f:R -> R) (a b c:R) (pr1:Riemann_integrable f a b)
    (pr2:Riemann_integrable f b c) (pr3:Riemann_integrable f a c),
    a <= b -> b <= c -> RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3.

Lemma RiemannInt_P26 :
  forall (f:R -> R) (a b c:R) (pr1:Riemann_integrable f a b)
    (pr2:Riemann_integrable f b c) (pr3:Riemann_integrable f a c),
    RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3.

Lemma RiemannInt_P27 :
  forall (f:R -> R) (a b x:R) (h:a <= b)
    (C0:forall x:R, a <= x <= b -> continuity_pt f x),
    a < x < b -> derivable_pt_lim (primitive h (FTC_P1 h C0)) x (f x).

Lemma RiemannInt_P28 :
  forall (f:R -> R) (a b x:R) (h:a <= b)
    (C0:forall x:R, a <= x <= b -> continuity_pt f x),
    a <= x <= b -> derivable_pt_lim (primitive h (FTC_P1 h C0)) x (f x).

Lemma RiemannInt_P29 :
  forall (f:R -> R) a b (h:a <= b)
    (C0:forall x:R, a <= x <= b -> continuity_pt f x),
    antiderivative f (primitive h (FTC_P1 h C0)) a b.

Lemma RiemannInt_P30 :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall x:R, a <= x <= b -> continuity_pt f x) ->
    { g:R -> R | antiderivative f g a b }.

Record C1_fun : Type := mkC1
  {c1 :> R -> R; diff0 : derivable c1; cont1 : continuity (derive c1 diff0)}.

Lemma RiemannInt_P31 :
  forall (f:C1_fun) (a b:R),
    a <= b -> antiderivative (derive f (diff0 f)) f a b.

Lemma RiemannInt_P32 :
  forall (f:C1_fun) (a b:R), Riemann_integrable (derive f (diff0 f)) a b.

Lemma RiemannInt_P33 :
  forall (f:C1_fun) (a b:R) (pr:Riemann_integrable (derive f (diff0 f)) a b),
    a <= b -> RiemannInt pr = f b - f a.

Lemma FTC_Riemann :
  forall (f:C1_fun) (a b:R) (pr:Riemann_integrable (derive f (diff0 f)) a b),
    RiemannInt pr = f b - f a.