Library Coq.Reals.RiemannInt
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.
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) {
struct N} :
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.