begin
:: deftheorem Def1 defines closed-interval INTEGRA1:def 1 :
for IT being set holds
( IT is closed-interval iff ex a, b being Real st
( a <= b & IT = [.a,b.] ) );
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
:: deftheorem Def2 defines Division INTEGRA1:def 2 :
for A being non empty compact Subset of REAL
for b2 being non empty increasing FinSequence of REAL holds
( b2 is Division of A iff ( rng b2 c= A & b2 . (len b2) = upper_bound A ) );
:: deftheorem Def3 defines divs INTEGRA1:def 3 :
for A being non empty compact Subset of REAL
for b2 being set holds
( b2 = divs A iff for x1 being set holds
( x1 in b2 iff x1 is Division of A ) );
theorem
canceled;
theorem Th8:
theorem Th9:
:: deftheorem INTEGRA1:def 4 :
canceled;
:: deftheorem Def5 defines divset INTEGRA1:def 5 :
for A being closed-interval Subset of REAL
for D being Division of A
for i being Nat st i in dom D holds
for b4 being closed-interval Subset of REAL holds
( ( i = 1 implies ( b4 = divset D,i iff ( lower_bound b4 = lower_bound A & upper_bound b4 = D . i ) ) ) & ( not i = 1 implies ( b4 = divset D,i iff ( lower_bound b4 = D . (i - 1) & upper_bound b4 = D . i ) ) ) );
theorem Th10:
:: deftheorem defines vol INTEGRA1:def 6 :
for A being Subset of REAL holds vol A = (upper_bound A) - (lower_bound A);
theorem
begin
definition
let A be
closed-interval Subset of
REAL ;
let f be
PartFunc of
A,
REAL ;
let D be
Division of
A;
func upper_volume f,
D -> FinSequence of
REAL means :
Def7:
(
len it = len D & ( for
i being
Nat st
i in dom D holds
it . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) )
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) & len b2 = len D & ( for i being Nat st i in dom D holds
b2 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) holds
b1 = b2
func lower_volume f,
D -> FinSequence of
REAL means :
Def8:
(
len it = len D & ( for
i being
Nat st
i in dom D holds
it . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) )
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) & len b2 = len D & ( for i being Nat st i in dom D holds
b2 . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) holds
b1 = b2
end;
:: deftheorem Def7 defines upper_volume INTEGRA1:def 7 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for D being Division of A
for b4 being FinSequence of REAL holds
( b4 = upper_volume f,D iff ( len b4 = len D & ( for i being Nat st i in dom D holds
b4 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) ) );
:: deftheorem Def8 defines lower_volume INTEGRA1:def 8 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for D being Division of A
for b4 being FinSequence of REAL holds
( b4 = lower_volume f,D iff ( len b4 = len D & ( for i being Nat st i in dom D holds
b4 . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) ) );
:: deftheorem defines upper_sum INTEGRA1:def 9 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for D being Division of A holds upper_sum f,D = Sum (upper_volume f,D);
:: deftheorem defines lower_sum INTEGRA1:def 10 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for D being Division of A holds lower_sum f,D = Sum (lower_volume f,D);
definition
let A be
closed-interval Subset of
REAL ;
let f be
PartFunc of
A,
REAL ;
set S =
divs A;
func upper_sum_set f -> PartFunc of
(divs A),
REAL means :
Def11:
(
dom it = divs A & ( for
D being
Division of
A st
D in dom it holds
it . D = upper_sum f,
D ) );
existence
ex b1 being PartFunc of (divs A),REAL st
( dom b1 = divs A & ( for D being Division of A st D in dom b1 holds
b1 . D = upper_sum f,D ) )
uniqueness
for b1, b2 being PartFunc of (divs A),REAL st dom b1 = divs A & ( for D being Division of A st D in dom b1 holds
b1 . D = upper_sum f,D ) & dom b2 = divs A & ( for D being Division of A st D in dom b2 holds
b2 . D = upper_sum f,D ) holds
b1 = b2
func lower_sum_set f -> PartFunc of
(divs A),
REAL means :
Def12:
(
dom it = divs A & ( for
D being
Division of
A st
D in dom it holds
it . D = lower_sum f,
D ) );
existence
ex b1 being PartFunc of (divs A),REAL st
( dom b1 = divs A & ( for D being Division of A st D in dom b1 holds
b1 . D = lower_sum f,D ) )
uniqueness
for b1, b2 being PartFunc of (divs A),REAL st dom b1 = divs A & ( for D being Division of A st D in dom b1 holds
b1 . D = lower_sum f,D ) & dom b2 = divs A & ( for D being Division of A st D in dom b2 holds
b2 . D = lower_sum f,D ) holds
b1 = b2
end;
:: deftheorem Def11 defines upper_sum_set INTEGRA1:def 11 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for b3 being PartFunc of (divs A),REAL holds
( b3 = upper_sum_set f iff ( dom b3 = divs A & ( for D being Division of A st D in dom b3 holds
b3 . D = upper_sum f,D ) ) );
:: deftheorem Def12 defines lower_sum_set INTEGRA1:def 12 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for b3 being PartFunc of (divs A),REAL holds
( b3 = lower_sum_set f iff ( dom b3 = divs A & ( for D being Division of A st D in dom b3 holds
b3 . D = lower_sum f,D ) ) );
:: deftheorem Def13 defines upper_integrable INTEGRA1:def 13 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL holds
( f is upper_integrable iff rng (upper_sum_set f) is bounded_below );
:: deftheorem Def14 defines lower_integrable INTEGRA1:def 14 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL holds
( f is lower_integrable iff rng (lower_sum_set f) is bounded_above );
:: deftheorem defines upper_integral INTEGRA1:def 15 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL holds upper_integral f = lower_bound (rng (upper_sum_set f));
:: deftheorem defines lower_integral INTEGRA1:def 16 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL holds lower_integral f = upper_bound (rng (lower_sum_set f));
:: deftheorem Def17 defines integrable INTEGRA1:def 17 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL holds
( f is integrable iff ( f is upper_integrable & f is lower_integrable & upper_integral f = lower_integral f ) );
:: deftheorem defines integral INTEGRA1:def 18 :
for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL holds integral f = upper_integral f;
begin
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
theorem
begin
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
begin
theorem Th27:
theorem
theorem Th29:
theorem Th30:
:: deftheorem INTEGRA1:def 19 :
canceled;
:: deftheorem Def20 defines <= INTEGRA1:def 20 :
for D1, D2 being FinSequence holds
( D1 <= D2 iff ( len D1 <= len D2 & rng D1 c= rng D2 ) );
theorem
theorem Th32:
theorem Th33:
theorem
theorem Th35:
:: deftheorem Def21 defines indx INTEGRA1:def 21 :
for A being closed-interval Subset of REAL
for D1, D2 being Division of A
for i being Nat st D1 <= D2 holds
for b5 being Element of NAT holds
( ( i in dom D1 implies ( b5 = indx D2,D1,i iff ( b5 in dom D2 & D1 . i = D2 . b5 ) ) ) & ( not i in dom D1 implies ( b5 = indx D2,D1,i iff b5 = 0 ) ) );
theorem Th36:
theorem Th37:
Th38a:
for i, j being Element of NAT
for f being FinSequence st i in dom f & j in dom f & i <= j holds
len (mid f,i,j) = (j - i) + 1
theorem Th38:
theorem Th39:
:: deftheorem Def22 defines PartSums INTEGRA1:def 22 :
for p, b2 being FinSequence of REAL holds
( b2 = PartSums p iff ( len b2 = len p & ( for i being Nat st i in dom p holds
b2 . i = Sum (p | i) ) ) );
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
begin
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem
theorem