Library Coq.Reals.RiemannInt

Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis_reg.
Require Import Rbase.
Require Import RiemannInt_SF.
Require Import Max.
Require Import RList.
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 { n :nat | a + INR n * del 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) : list R :=
 SubEquiN (S (max_N del h)) a b del.

Lemma Heine_cor1 :
 forall (f:R -> R) (a b:R),
 a 
 (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 (length (SubEqui del h))) = b.

Lemma SubEqui_P3 :
 forall (N:nat) (a b:R) (del:posreal), length (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),
 length (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 < length (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 (length (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 
 (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 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 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 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 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.

Library Coq.Reals.RiemannInt

Navigation