Library Coq.Reals.RiemannInt_SF
Each bounded subset of N has a maximal element
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) }.
Integral of step functions
Properties of step functions
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).
The set of step functions on a,b is a vectorial space
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.