# Library Coq.Reals.RiemannInt

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

Set Implicit Arguments.

Riemann's Integral

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.

Lemma Riemann_integrable_ext :
forall f g a b,
(forall x, Rmin a b <= x <= Rmax a b -> f x = g x) ->
Riemann_integrable f a b -> Riemann_integrable g a b.
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.

C°(a,b) is included in L1(a,b)

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

Lemma RiemannInt_const_bound :
forall f a b l u (h : Riemann_integrable f a b), a <= b ->
(forall x, a < x < b -> l <= f x <= u) ->
l * (b - a) <= RiemannInt h <= u * (b - a).

Lemma Riemann_integrable_scal :
forall f a b k,
Riemann_integrable f a b ->
Riemann_integrable (fun x => k * f x) a b.

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