Library Coq.Reals.RiemannInt_SF
Each bounded subset of N has a maximal element
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:
list R),
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:
list R),
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:
list R),
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:
list R) (
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:
list R),
adapted_couple f a b l lf -> a <> b -> (2
<= length l)%
nat.
Lemma StepFun_P10 :
forall (
f:
R -> R) (
l lf:
list R) (
a b:
R),
a <= b ->
adapted_couple f a b l lf ->
exists l' :
list R,
(exists lf' :
list R, 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:
list R)
(
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:
list R),
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:
list R)
(
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:
list R) (
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:
list R) (
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:
list R) (
a b:
R),
adapted_couple f a b l lf ->
exists l' :
list R,
(exists lf' :
list R, adapted_couple_opt f a b l' lf').
Lemma StepFun_P17 :
forall (
f:
R -> R) (
l1 l2 lf1 lf2:
list R) (
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:
list R) (
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:
list R) (
f:
R -> R),
(0
< length l)%
nat -> length l = S (
length (
FF l f)).
Lemma StepFun_P21 :
forall (
a b:
R) (
f:
R -> R) (
l:
list R),
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:
list R),
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:
list R),
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:
list R),
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:
list R),
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:
list R),
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:
list R),
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:
list R),
adapted_couple f a b l lf ->
adapted_couple (
fun x:
R =>
Rabs (
f x))
a b l (
map Rabs lf).
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:
list R,
ordered_Rlist l1 -> Rabs (
Int_SF l2 l1)
<= Int_SF (
map Rabs l2)
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:
list R) (
a b:
R) (
f g:
R -> R),
ordered_Rlist l ->
pos_Rl l 0
= a ->
pos_Rl l (
pred (
length 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:
list R),
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:
list R) (
a b:
R) (
f:
R -> R),
ordered_Rlist l ->
pos_Rl l 0
= a ->
pos_Rl l (
pred (
length l))
= b ->
{ g:StepFun a b |
g b = f b /\
(forall i:
nat,
(
i < pred (
length 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:
list R),
a < b ->
b < c ->
adapted_couple f a b l1 lf1 ->
adapted_couple f b c l2 lf2 ->
adapted_couple f a c (
app l1 l2) (
FF (
app 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:
list R) (
f:
R -> R),
pos_Rl l1 (
pred (
length l1))
= pos_Rl l2 0
->
Int_SF (
FF (
app l1 l2)
f) (
app 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.