begin
:: deftheorem Def1 defines middle_volume INTEGR15:def 1 :
Lm1:
for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume f,D) . i <= F . i
Lm2:
for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume f,D) . i <= F . i & F . i < ((lower_volume f,D) . i) + e )
Lm3:
for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < F . i )
Lm4:
for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume f,D) . i
:: deftheorem defines middle_sum INTEGR15:def 2 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
:: deftheorem Def3 defines middle_volume_Sequence INTEGR15:def 3 :
:: deftheorem Def4 defines middle_sum INTEGR15:def 4 :
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
Lm5:
for p, q, r being Real_Sequence st p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) holds
( q is convergent & lim p = lim q & lim r = lim q )
theorem Th9:
theorem Th10:
:: deftheorem Def5 defines middle_volume INTEGR15:def 5 :
:: deftheorem Def6 defines middle_sum INTEGR15:def 6 :
:: deftheorem Def7 defines middle_volume_Sequence INTEGR15:def 7 :
:: deftheorem Def8 defines middle_sum INTEGR15:def 8 :
definition
let n be
Element of
NAT ;
let Z be non
empty set ;
let f,
g be
PartFunc of
Z,
(REAL n);
deffunc H1(
Element of
Z)
-> Element of
REAL n =
(f /. $1) + (g /. $1);
deffunc H2(
Element of
Z)
-> Element of
REAL n =
(f /. $1) - (g /. $1);
defpred S1[
set ]
means $1
in (dom f) /\ (dom g);
set X =
(dom f) /\ (dom g);
func f + g -> PartFunc of
Z,
(REAL n) means :
Def9:
(
dom it = (dom f) /\ (dom g) & ( for
c being
Element of
Z st
c in dom it holds
it /. c = (f /. c) + (g /. c) ) );
existence
ex b1 being PartFunc of Z,(REAL n) st
( dom b1 = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b1 holds
b1 /. c = (f /. c) + (g /. c) ) )
uniqueness
for b1, b2 being PartFunc of Z,(REAL n) st dom b1 = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b1 holds
b1 /. c = (f /. c) + (g /. c) ) & dom b2 = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b2 holds
b2 /. c = (f /. c) + (g /. c) ) holds
b1 = b2
func f - g -> PartFunc of
Z,
(REAL n) means :
Def10:
(
dom it = (dom f) /\ (dom g) & ( for
c being
Element of
Z st
c in dom it holds
it /. c = (f /. c) - (g /. c) ) );
existence
ex b1 being PartFunc of Z,(REAL n) st
( dom b1 = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b1 holds
b1 /. c = (f /. c) - (g /. c) ) )
uniqueness
for b1, b2 being PartFunc of Z,(REAL n) st dom b1 = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b1 holds
b1 /. c = (f /. c) - (g /. c) ) & dom b2 = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b2 holds
b2 /. c = (f /. c) - (g /. c) ) holds
b1 = b2
end;
:: deftheorem Def9 defines + INTEGR15:def 9 :
:: deftheorem Def10 defines - INTEGR15:def 10 :
:: deftheorem Def11 defines (#) INTEGR15:def 11 :
begin
:: deftheorem Def12 defines bounded INTEGR15:def 12 :
Lm6:
for n, i being Element of NAT
for f being PartFunc of REAL ,(REAL n)
for i being Element of NAT
for A being Subset of REAL holds (proj i,n) * (f | A) = ((proj i,n) * f) | A
:: deftheorem Def13 defines integrable INTEGR15:def 13 :
:: deftheorem Def14 defines integral INTEGR15:def 14 :
theorem Th11:
theorem
:: deftheorem Def15 defines bounded INTEGR15:def 15 :
:: deftheorem Def16 defines is_integrable_on INTEGR15:def 16 :
definition
let n be
Element of
NAT ;
let A be
closed-interval Subset of
REAL ;
let f be
PartFunc of
REAL ,
(REAL n);
func integral f,
A -> Element of
REAL n means :
Def17:
(
dom it = Seg n & ( for
i being
Element of
NAT st
i in Seg n holds
it . i = integral ((proj i,n) * f),
A ) );
existence
ex b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral ((proj i,n) * f),A ) )
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral ((proj i,n) * f),A ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral ((proj i,n) * f),A ) holds
b1 = b2
end;
:: deftheorem Def17 defines integral INTEGR15:def 17 :
theorem
theorem
definition
let a,
b be
real number ;
let n be
Element of
NAT ;
let f be
PartFunc of
REAL ,
(REAL n);
func integral f,
a,
b -> Element of
REAL n means :
Def18:
(
dom it = Seg n & ( for
i being
Element of
NAT st
i in Seg n holds
it . i = integral ((proj i,n) * f),
a,
b ) );
existence
ex b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral ((proj i,n) * f),a,b ) )
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral ((proj i,n) * f),a,b ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral ((proj i,n) * f),a,b ) holds
b1 = b2
end;
:: deftheorem Def18 defines integral INTEGR15:def 18 :
begin
theorem Th15:
theorem Th16:
theorem
theorem
theorem
theorem