:: by Noboru Endou and Artur Korni{\l}owicz

::

:: Received March 13, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

registration

coherence

for b_{1} being Subset of REAL st b_{1} is closed_interval holds

b_{1} is compact

end;
for b

b

proof end;

theorem Th3: :: INTEGRA1:3

for A being non empty closed_interval Subset of REAL holds

( A is bounded_below & A is bounded_above )

( A is bounded_below & A is bounded_above )

proof end;

registration

coherence

for b_{1} being Subset of REAL st not b_{1} is empty & b_{1} is closed_interval holds

b_{1} is real-bounded

end;
for b

b

proof end;

theorem Th5: :: INTEGRA1:5

for A being non empty closed_interval Subset of REAL

for a1, a2, b1, b2 being real number st A = [.a1,b1.] & A = [.a2,b2.] holds

( a1 = a2 & b1 = b2 )

for a1, a2, b1, b2 being real number st A = [.a1,b1.] & A = [.a2,b2.] holds

( a1 = a2 & b1 = b2 )

proof end;

begin

definition

canceled;

let A be non empty compact Subset of REAL;

ex b_{1} being non empty increasing FinSequence of REAL st

( rng b_{1} c= A & b_{1} . (len b_{1}) = upper_bound A )

end;
let A be non empty compact Subset of REAL;

mode Division of A -> non empty increasing FinSequence of REAL means :Def2: :: INTEGRA1:def 2

( rng it c= A & it . (len it) = upper_bound A );

existence ( rng it c= A & it . (len it) = upper_bound A );

ex b

( rng b

proof end;

:: deftheorem Def2 defines Division INTEGRA1:def 2 :

for A being non empty compact Subset of REAL

for b_{2} being non empty increasing FinSequence of REAL holds

( b_{2} is Division of A iff ( rng b_{2} c= A & b_{2} . (len b_{2}) = upper_bound A ) );

for A being non empty compact Subset of REAL

for b

( b

definition

let A be non empty compact Subset of REAL;

ex b_{1} being set st

for x1 being set holds

( x1 in b_{1} iff x1 is Division of A )

for b_{1}, b_{2} being set st ( for x1 being set holds

( x1 in b_{1} iff x1 is Division of A ) ) & ( for x1 being set holds

( x1 in b_{2} iff x1 is Division of A ) ) holds

b_{1} = b_{2}

end;
func divs A -> set means :Def3: :: INTEGRA1:def 3

for x1 being set holds

( x1 in it iff x1 is Division of A );

existence for x1 being set holds

( x1 in it iff x1 is Division of A );

ex b

for x1 being set holds

( x1 in b

proof end;

uniqueness for b

( x1 in b

( x1 in b

b

proof end;

:: deftheorem Def3 defines divs INTEGRA1:def 3 :

for A being non empty compact Subset of REAL

for b_{2} being set holds

( b_{2} = divs A iff for x1 being set holds

( x1 in b_{2} iff x1 is Division of A ) );

for A being non empty compact Subset of REAL

for b

( b

( x1 in b

registration
end;

registration

let A be non empty compact Subset of REAL;

coherence

for b_{1} being Element of divs A holds

( b_{1} is Function-like & b_{1} is Relation-like )
by Def3;

end;
coherence

for b

( b

registration

let A be non empty compact Subset of REAL;

coherence

for b_{1} being Element of divs A holds

( b_{1} is real-valued & b_{1} is FinSequence-like )
by Def3;

end;
coherence

for b

( b

theorem Th6: :: INTEGRA1:6

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

D . i in A

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

D . i in A

proof end;

theorem Th7: :: INTEGRA1:7

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & i <> 1 holds

( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT )

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & i <> 1 holds

( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT )

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let D be Division of A;

let i be Nat;

assume A1: i in dom D ;

( ( i = 1 implies ex b_{1} being non empty closed_interval Subset of REAL st

( lower_bound b_{1} = lower_bound A & upper_bound b_{1} = D . i ) ) & ( not i = 1 implies ex b_{1} being non empty closed_interval Subset of REAL st

( lower_bound b_{1} = D . (i - 1) & upper_bound b_{1} = D . i ) ) )

for b_{1}, b_{2} being non empty closed_interval Subset of REAL holds

( ( i = 1 & lower_bound b_{1} = lower_bound A & upper_bound b_{1} = D . i & lower_bound b_{2} = lower_bound A & upper_bound b_{2} = D . i implies b_{1} = b_{2} ) & ( not i = 1 & lower_bound b_{1} = D . (i - 1) & upper_bound b_{1} = D . i & lower_bound b_{2} = D . (i - 1) & upper_bound b_{2} = D . i implies b_{1} = b_{2} ) )

consistency

for b_{1} being non empty closed_interval Subset of REAL holds verum;

;

end;
let D be Division of A;

let i be Nat;

assume A1: i in dom D ;

func divset (D,i) -> non empty closed_interval Subset of REAL means :Def4: :: INTEGRA1:def 4

( lower_bound it = lower_bound A & upper_bound it = D . i ) if i = 1

otherwise ( lower_bound it = D . (i - 1) & upper_bound it = D . i );

existence ( lower_bound it = lower_bound A & upper_bound it = D . i ) if i = 1

otherwise ( lower_bound it = D . (i - 1) & upper_bound it = D . i );

( ( i = 1 implies ex b

( lower_bound b

( lower_bound b

proof end;

uniqueness for b

( ( i = 1 & lower_bound b

proof end;

correctness consistency

for b

;

:: deftheorem Def4 defines divset INTEGRA1:def 4 :

for A being non empty closed_interval Subset of REAL

for D being Division of A

for i being Nat st i in dom D holds

for b_{4} being non empty closed_interval Subset of REAL holds

( ( i = 1 implies ( b_{4} = divset (D,i) iff ( lower_bound b_{4} = lower_bound A & upper_bound b_{4} = D . i ) ) ) & ( not i = 1 implies ( b_{4} = divset (D,i) iff ( lower_bound b_{4} = D . (i - 1) & upper_bound b_{4} = D . i ) ) ) );

for A being non empty closed_interval Subset of REAL

for D being Division of A

for i being Nat st i in dom D holds

for b

( ( i = 1 implies ( b

theorem Th8: :: INTEGRA1:8

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

divset (D,i) c= A

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

divset (D,i) c= A

proof end;

definition
end;

:: deftheorem defines vol INTEGRA1:def 5 :

for A being Subset of REAL holds vol A = (upper_bound A) - (lower_bound A);

for A being Subset of REAL holds vol A = (upper_bound A) - (lower_bound A);

theorem :: INTEGRA1:9

begin

definition

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

let D be Division of A;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len D & ( for i being Nat st i in dom D holds

b_{1} . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len D & ( for i being Nat st i in dom D holds

b_{1} . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) & len b_{2} = len D & ( for i being Nat st i in dom D holds

b_{2} . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) holds

b_{1} = b_{2}

ex b_{1} being FinSequence of REAL st

( len b_{1} = len D & ( for i being Nat st i in dom D holds

b_{1} . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len D & ( for i being Nat st i in dom D holds

b_{1} . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) & len b_{2} = len D & ( for i being Nat st i in dom D holds

b_{2} . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of A,REAL;

let D be Division of A;

func upper_volume (f,D) -> FinSequence of REAL means :Def6: :: INTEGRA1:def 6

( 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 ( 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))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

func lower_volume (f,D) -> FinSequence of REAL means :Def7: :: INTEGRA1:def 7

( 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 ( 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))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines upper_volume INTEGRA1:def 6 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for D being Division of A

for b_{4} being FinSequence of REAL holds

( b_{4} = upper_volume (f,D) iff ( len b_{4} = len D & ( for i being Nat st i in dom D holds

b_{4} . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) ) );

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for D being Division of A

for b

( b

b

:: deftheorem Def7 defines lower_volume INTEGRA1:def 7 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for D being Division of A

for b_{4} being FinSequence of REAL holds

( b_{4} = lower_volume (f,D) iff ( len b_{4} = len D & ( for i being Nat st i in dom D holds

b_{4} . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) ) );

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for D being Division of A

for b

( b

b

definition

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

let D be Division of A;

correctness

coherence

Sum (upper_volume (f,D)) is Real;

;

correctness

coherence

Sum (lower_volume (f,D)) is Real;

;

end;
let f be PartFunc of A,REAL;

let D be Division of A;

correctness

coherence

Sum (upper_volume (f,D)) is Real;

;

correctness

coherence

Sum (lower_volume (f,D)) is Real;

;

:: deftheorem defines upper_sum INTEGRA1:def 8 :

for A being non empty 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));

for A being non empty 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 9 :

for A being non empty 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));

for A being non empty 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 non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

set S = divs A;

ex b_{1} being Function of (divs A),REAL st

for D being Division of A holds b_{1} . D = upper_sum (f,D)

for b_{1}, b_{2} being Function of (divs A),REAL st ( for D being Division of A holds b_{1} . D = upper_sum (f,D) ) & ( for D being Division of A holds b_{2} . D = upper_sum (f,D) ) holds

b_{1} = b_{2}

ex b_{1} being Function of (divs A),REAL st

for D being Division of A holds b_{1} . D = lower_sum (f,D)

for b_{1}, b_{2} being Function of (divs A),REAL st ( for D being Division of A holds b_{1} . D = lower_sum (f,D) ) & ( for D being Division of A holds b_{2} . D = lower_sum (f,D) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of A,REAL;

set S = divs A;

func upper_sum_set f -> Function of (divs A),REAL means :Def10: :: INTEGRA1:def 10

for D being Division of A holds it . D = upper_sum (f,D);

existence for D being Division of A holds it . D = upper_sum (f,D);

ex b

for D being Division of A holds b

proof end;

uniqueness for b

b

proof end;

func lower_sum_set f -> Function of (divs A),REAL means :Def11: :: INTEGRA1:def 11

for D being Division of A holds it . D = lower_sum (f,D);

existence for D being Division of A holds it . D = lower_sum (f,D);

ex b

for D being Division of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines upper_sum_set INTEGRA1:def 10 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for b_{3} being Function of (divs A),REAL holds

( b_{3} = upper_sum_set f iff for D being Division of A holds b_{3} . D = upper_sum (f,D) );

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for b

( b

:: deftheorem Def11 defines lower_sum_set INTEGRA1:def 11 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for b_{3} being Function of (divs A),REAL holds

( b_{3} = lower_sum_set f iff for D being Division of A holds b_{3} . D = lower_sum (f,D) );

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for b

( b

definition

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

end;
let f be PartFunc of A,REAL;

attr f is upper_integrable means :Def12: :: INTEGRA1:def 12

rng (upper_sum_set f) is bounded_below ;

rng (upper_sum_set f) is bounded_below ;

attr f is lower_integrable means :Def13: :: INTEGRA1:def 13

rng (lower_sum_set f) is bounded_above ;

rng (lower_sum_set f) is bounded_above ;

:: deftheorem Def12 defines upper_integrable INTEGRA1:def 12 :

for A being non empty 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 );

for A being non empty 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 Def13 defines lower_integrable INTEGRA1:def 13 :

for A being non empty 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 );

for A being non empty 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 );

definition

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

correctness

coherence

lower_bound (rng (upper_sum_set f)) is Real;

;

end;
let f be PartFunc of A,REAL;

correctness

coherence

lower_bound (rng (upper_sum_set f)) is Real;

;

:: deftheorem defines upper_integral INTEGRA1:def 14 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL holds upper_integral f = lower_bound (rng (upper_sum_set f));

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL holds upper_integral f = lower_bound (rng (upper_sum_set f));

definition

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

coherence

upper_bound (rng (lower_sum_set f)) is Real ;

end;
let f be PartFunc of A,REAL;

coherence

upper_bound (rng (lower_sum_set f)) is Real ;

:: deftheorem defines lower_integral INTEGRA1:def 15 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL holds lower_integral f = upper_bound (rng (lower_sum_set f));

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL holds lower_integral f = upper_bound (rng (lower_sum_set f));

definition

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

end;
let f be PartFunc of A,REAL;

attr f is integrable means :Def16: :: INTEGRA1:def 16

( f is upper_integrable & f is lower_integrable & upper_integral f = lower_integral f );

( f is upper_integrable & f is lower_integrable & upper_integral f = lower_integral f );

:: deftheorem Def16 defines integrable INTEGRA1:def 16 :

for A being non empty 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 ) );

for A being non empty 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 ) );

definition

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

coherence

upper_integral f is Real ;

end;
let f be PartFunc of A,REAL;

coherence

upper_integral f is Real ;

:: deftheorem defines integral INTEGRA1:def 17 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL holds integral f = upper_integral f;

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL holds integral f = upper_integral f;

begin

theorem Th11: :: INTEGRA1:11

for X being non empty set

for f being PartFunc of X,REAL st f | X is bounded_below holds

rng f is bounded_below

for f being PartFunc of X,REAL st f | X is bounded_below holds

rng f is bounded_below

proof end;

theorem :: INTEGRA1:12

for X being non empty set

for f being PartFunc of X,REAL st rng f is bounded_below holds

f | X is bounded_below

for f being PartFunc of X,REAL st rng f is bounded_below holds

f | X is bounded_below

proof end;

theorem Th13: :: INTEGRA1:13

for X being non empty set

for f being PartFunc of X,REAL st f | X is bounded_above holds

rng f is bounded_above

for f being PartFunc of X,REAL st f | X is bounded_above holds

rng f is bounded_above

proof end;

theorem :: INTEGRA1:14

for X being non empty set

for f being PartFunc of X,REAL st rng f is bounded_above holds

f | X is bounded_above

for f being PartFunc of X,REAL st rng f is bounded_above holds

f | X is bounded_above

proof end;

theorem :: INTEGRA1:15

for X being non empty set

for f being PartFunc of X,REAL st f | X is bounded holds

rng f is real-bounded

for f being PartFunc of X,REAL st f | X is bounded holds

rng f is real-bounded

proof end;

begin

theorem Th18: :: INTEGRA1:18

for X being non empty set

for A being non empty Subset of X

for B being set st B meets dom (chi (A,A)) holds

rng ((chi (A,A)) | B) = {1}

for A being non empty Subset of X

for B being set st B meets dom (chi (A,A)) holds

rng ((chi (A,A)) | B) = {1}

proof end;

theorem Th19: :: INTEGRA1:19

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

vol (divset (D,i)) = (lower_volume ((chi (A,A)),D)) . i

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

vol (divset (D,i)) = (lower_volume ((chi (A,A)),D)) . i

proof end;

theorem Th20: :: INTEGRA1:20

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

vol (divset (D,i)) = (upper_volume ((chi (A,A)),D)) . i

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

vol (divset (D,i)) = (upper_volume ((chi (A,A)),D)) . i

proof end;

theorem :: INTEGRA1:21

for F, G, H being FinSequence of REAL st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G)

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G)

proof end;

theorem Th22: :: INTEGRA1:22

for F, G, H being FinSequence of REAL st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds

H . k = (F /. k) - (G /. k) ) holds

Sum H = (Sum F) - (Sum G)

H . k = (F /. k) - (G /. k) ) holds

Sum H = (Sum F) - (Sum G)

proof end;

theorem Th23: :: INTEGRA1:23

for A being non empty closed_interval Subset of REAL

for D being Division of A holds Sum (lower_volume ((chi (A,A)),D)) = vol A

for D being Division of A holds Sum (lower_volume ((chi (A,A)),D)) = vol A

proof end;

theorem Th24: :: INTEGRA1:24

for A being non empty closed_interval Subset of REAL

for D being Division of A holds Sum (upper_volume ((chi (A,A)),D)) = vol A

for D being Division of A holds Sum (upper_volume ((chi (A,A)),D)) = vol A

proof end;

begin

registration

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

let D be Division of A;

coherence

not upper_volume (f,D) is empty

not lower_volume (f,D) is empty

end;
let f be PartFunc of A,REAL;

let D be Division of A;

coherence

not upper_volume (f,D) is empty

proof end;

coherence not lower_volume (f,D) is empty

proof end;

theorem Th25: :: INTEGRA1:25

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded_below holds

(lower_bound (rng f)) * (vol A) <= lower_sum (f,D)

for D being Division of A

for f being Function of A,REAL st f | A is bounded_below holds

(lower_bound (rng f)) * (vol A) <= lower_sum (f,D)

proof end;

theorem :: INTEGRA1:26

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded_above & i in dom D holds

(upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded_above & i in dom D holds

(upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))

proof end;

theorem Th27: :: INTEGRA1:27

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded_above holds

upper_sum (f,D) <= (upper_bound (rng f)) * (vol A)

for D being Division of A

for f being Function of A,REAL st f | A is bounded_above holds

upper_sum (f,D) <= (upper_bound (rng f)) * (vol A)

proof end;

theorem Th28: :: INTEGRA1:28

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded holds

lower_sum (f,D) <= upper_sum (f,D)

for D being Division of A

for f being Function of A,REAL st f | A is bounded holds

lower_sum (f,D) <= upper_sum (f,D)

proof end;

definition

let D1, D2 be FinSequence;

reflexivity

for D1 being FinSequence holds

( len D1 <= len D1 & rng D1 c= rng D1 ) ;

end;
reflexivity

for D1 being FinSequence holds

( len D1 <= len D1 & rng D1 c= rng D1 ) ;

:: deftheorem Def18 defines <= INTEGRA1:def 18 :

for D1, D2 being FinSequence holds

( D1 <= D2 iff ( len D1 <= len D2 & rng D1 c= rng D2 ) );

for D1, D2 being FinSequence holds

( D1 <= D2 iff ( len D1 <= len D2 & rng D1 c= rng D2 ) );

theorem :: INTEGRA1:29

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st len D1 = 1 holds

D1 <= D2

for D1, D2 being Division of A st len D1 = 1 holds

D1 <= D2

proof end;

theorem Th30: :: INTEGRA1:30

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st f | A is bounded_above & len D1 = 1 holds

upper_sum (f,D1) >= upper_sum (f,D2)

for D1, D2 being Division of A

for f being Function of A,REAL st f | A is bounded_above & len D1 = 1 holds

upper_sum (f,D1) >= upper_sum (f,D2)

proof end;

theorem Th31: :: INTEGRA1:31

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st f | A is bounded_below & len D1 = 1 holds

lower_sum (f,D1) <= lower_sum (f,D2)

for D1, D2 being Division of A

for f being Function of A,REAL st f | A is bounded_below & len D1 = 1 holds

lower_sum (f,D1) <= lower_sum (f,D2)

proof end;

theorem :: INTEGRA1:32

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

ex A1, A2 being non empty closed_interval Subset of REAL st

( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D holds

ex A1, A2 being non empty closed_interval Subset of REAL st

( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )

proof end;

theorem Th33: :: INTEGRA1:33

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st i in dom D1 & D1 <= D2 holds

ex j being Element of NAT st

( j in dom D2 & D1 . i = D2 . j )

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st i in dom D1 & D1 <= D2 holds

ex j being Element of NAT st

( j in dom D2 & D1 . i = D2 . j )

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let D1, D2 be Division of A;

let i be Nat;

assume A1: D1 <= D2 ;

( ( i in dom D1 implies ex b_{1} being Element of NAT st

( b_{1} in dom D2 & D1 . i = D2 . b_{1} ) ) & ( not i in dom D1 implies ex b_{1} being Element of NAT st b_{1} = 0 ) )
by A1, Th33;

uniqueness

for b_{1}, b_{2} being Element of NAT holds

( ( i in dom D1 & b_{1} in dom D2 & D1 . i = D2 . b_{1} & b_{2} in dom D2 & D1 . i = D2 . b_{2} implies b_{1} = b_{2} ) & ( not i in dom D1 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

consistency

for b_{1} being Element of NAT holds verum;

;

end;
let D1, D2 be Division of A;

let i be Nat;

assume A1: D1 <= D2 ;

func indx (D2,D1,i) -> Element of NAT means :Def19: :: INTEGRA1:def 19

( it in dom D2 & D1 . i = D2 . it ) if i in dom D1

otherwise it = 0 ;

existence ( it in dom D2 & D1 . i = D2 . it ) if i in dom D1

otherwise it = 0 ;

( ( i in dom D1 implies ex b

( b

uniqueness

for b

( ( i in dom D1 & b

proof end;

correctness consistency

for b

;

:: deftheorem Def19 defines indx INTEGRA1:def 19 :

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for i being Nat st D1 <= D2 holds

for b_{5} being Element of NAT holds

( ( i in dom D1 implies ( b_{5} = indx (D2,D1,i) iff ( b_{5} in dom D2 & D1 . i = D2 . b_{5} ) ) ) & ( not i in dom D1 implies ( b_{5} = indx (D2,D1,i) iff b_{5} = 0 ) ) );

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for i being Nat st D1 <= D2 holds

for b

( ( i in dom D1 implies ( b

theorem Th34: :: INTEGRA1:34

for p being increasing FinSequence of REAL

for n being Element of NAT st n <= len p holds

p /^ n is increasing FinSequence of REAL

for n being Element of NAT st n <= len p holds

p /^ n is increasing FinSequence of REAL

proof end;

theorem Th35: :: INTEGRA1:35

for p being increasing FinSequence of REAL

for i, j being Element of NAT st j in dom p & i <= j holds

mid (p,i,j) is increasing FinSequence of REAL

for i, j being Element of NAT st j in dom p & i <= j holds

mid (p,i,j) is increasing FinSequence of REAL

proof end;

Lm1: 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

proof end;

theorem Th36: :: INTEGRA1:36

for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j holds

ex B being non empty closed_interval Subset of REAL st

( lower_bound B = (mid (D,i,j)) . 1 & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j holds

ex B being non empty closed_interval Subset of REAL st

( lower_bound B = (mid (D,i,j)) . 1 & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

proof end;

theorem Th37: :: INTEGRA1:37

for i, j being Element of NAT

for A, B being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j & D . i >= lower_bound B & D . j = upper_bound B holds

mid (D,i,j) is Division of B

for A, B being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j & D . i >= lower_bound B & D . j = upper_bound B holds

mid (D,i,j) is Division of B

proof end;

definition

let p be FinSequence of REAL ;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len p & ( for i being Nat st i in dom p holds

b_{1} . i = Sum (p | i) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len p & ( for i being Nat st i in dom p holds

b_{1} . i = Sum (p | i) ) & len b_{2} = len p & ( for i being Nat st i in dom p holds

b_{2} . i = Sum (p | i) ) holds

b_{1} = b_{2}

end;
func PartSums p -> FinSequence of REAL means :Def20: :: INTEGRA1:def 20

( len it = len p & ( for i being Nat st i in dom p holds

it . i = Sum (p | i) ) );

existence ( len it = len p & ( for i being Nat st i in dom p holds

it . i = Sum (p | i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def20 defines PartSums INTEGRA1:def 20 :

for p, b_{2} being FinSequence of REAL holds

( b_{2} = PartSums p iff ( len b_{2} = len p & ( for i being Nat st i in dom p holds

b_{2} . i = Sum (p | i) ) ) );

for p, b

( b

b

theorem Th38: :: INTEGRA1:38

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds

for i being non empty Element of NAT st i in dom D1 holds

Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds

for i being non empty Element of NAT st i in dom D1 holds

Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))

proof end;

theorem Th39: :: INTEGRA1:39

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds

for i being non empty Element of NAT st i in dom D1 holds

Sum ((lower_volume (f,D1)) | i) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i)))

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds

for i being non empty Element of NAT st i in dom D1 holds

Sum ((lower_volume (f,D1)) | i) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i)))

proof end;

theorem Th40: :: INTEGRA1:40

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & i in dom D1 & f | A is bounded_above holds

(PartSums (upper_volume (f,D1))) . i >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,i))

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & i in dom D1 & f | A is bounded_above holds

(PartSums (upper_volume (f,D1))) . i >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,i))

proof end;

theorem Th41: :: INTEGRA1:41

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & i in dom D1 & f | A is bounded_below holds

(PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_volume (f,D2))) . (indx (D2,D1,i))

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & i in dom D1 & f | A is bounded_below holds

(PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_volume (f,D2))) . (indx (D2,D1,i))

proof end;

theorem Th42: :: INTEGRA1:42

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL holds (PartSums (upper_volume (f,D))) . (len D) = upper_sum (f,D)

for D being Division of A

for f being Function of A,REAL holds (PartSums (upper_volume (f,D))) . (len D) = upper_sum (f,D)

proof end;

theorem Th43: :: INTEGRA1:43

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL holds (PartSums (lower_volume (f,D))) . (len D) = lower_sum (f,D)

for D being Division of A

for f being Function of A,REAL holds (PartSums (lower_volume (f,D))) . (len D) = lower_sum (f,D)

proof end;

theorem Th44: :: INTEGRA1:44

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st D1 <= D2 holds

indx (D2,D1,(len D1)) = len D2

for D1, D2 being Division of A st D1 <= D2 holds

indx (D2,D1,(len D1)) = len D2

proof end;

theorem Th45: :: INTEGRA1:45

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds

upper_sum (f,D2) <= upper_sum (f,D1)

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds

upper_sum (f,D2) <= upper_sum (f,D1)

proof end;

theorem Th46: :: INTEGRA1:46

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds

lower_sum (f,D2) >= lower_sum (f,D1)

for D1, D2 being Division of A

for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds

lower_sum (f,D2) >= lower_sum (f,D1)

proof end;

theorem Th47: :: INTEGRA1:47

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A ex D being Division of A st

( D1 <= D & D2 <= D )

for D1, D2 being Division of A ex D being Division of A st

( D1 <= D & D2 <= D )

proof end;

theorem Th48: :: INTEGRA1:48

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st f | A is bounded holds

lower_sum (f,D1) <= upper_sum (f,D2)

for D1, D2 being Division of A

for f being Function of A,REAL st f | A is bounded holds

lower_sum (f,D1) <= upper_sum (f,D2)

proof end;

begin

theorem Th49: :: INTEGRA1:49

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f | A is bounded holds

upper_integral f >= lower_integral f

for f being Function of A,REAL st f | A is bounded holds

upper_integral f >= lower_integral f

proof end;

theorem Th51: :: INTEGRA1:51

for X, Y being Subset of REAL st X is bounded_above & Y is bounded_above holds

X ++ Y is bounded_above

X ++ Y is bounded_above

proof end;

theorem Th52: :: INTEGRA1:52

for X, Y being non empty Subset of REAL st X is bounded_above & Y is bounded_above holds

upper_bound (X ++ Y) = (upper_bound X) + (upper_bound Y)

upper_bound (X ++ Y) = (upper_bound X) + (upper_bound Y)

proof end;

theorem Th53: :: INTEGRA1:53

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f, g being Function of A,REAL st i in dom D & f | A is bounded_above & g | A is bounded_above holds

(upper_volume ((f + g),D)) . i <= ((upper_volume (f,D)) . i) + ((upper_volume (g,D)) . i)

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f, g being Function of A,REAL st i in dom D & f | A is bounded_above & g | A is bounded_above holds

(upper_volume ((f + g),D)) . i <= ((upper_volume (f,D)) . i) + ((upper_volume (g,D)) . i)

proof end;

theorem Th54: :: INTEGRA1:54

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f, g being Function of A,REAL st i in dom D & f | A is bounded_below & g | A is bounded_below holds

((lower_volume (f,D)) . i) + ((lower_volume (g,D)) . i) <= (lower_volume ((f + g),D)) . i

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f, g being Function of A,REAL st i in dom D & f | A is bounded_below & g | A is bounded_below holds

((lower_volume (f,D)) . i) + ((lower_volume (g,D)) . i) <= (lower_volume ((f + g),D)) . i

proof end;

theorem Th55: :: INTEGRA1:55

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f, g being Function of A,REAL st f | A is bounded_above & g | A is bounded_above holds

upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D))

for D being Division of A

for f, g being Function of A,REAL st f | A is bounded_above & g | A is bounded_above holds

upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D))

proof end;

theorem Th56: :: INTEGRA1:56

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f, g being Function of A,REAL st f | A is bounded_below & g | A is bounded_below holds

(lower_sum (f,D)) + (lower_sum (g,D)) <= lower_sum ((f + g),D)

for D being Division of A

for f, g being Function of A,REAL st f | A is bounded_below & g | A is bounded_below holds

(lower_sum (f,D)) + (lower_sum (g,D)) <= lower_sum ((f + g),D)

proof end;

theorem :: INTEGRA1:57

for A being non empty closed_interval Subset of REAL

for f, g being Function of A,REAL st f | A is bounded & g | A is bounded & f is integrable & g is integrable holds

( f + g is integrable & integral (f + g) = (integral f) + (integral g) )

for f, g being Function of A,REAL st f | A is bounded & g | A is bounded & f is integrable & g is integrable holds

( f + g is integrable & integral (f + g) = (integral f) + (integral g) )

proof end;

theorem :: INTEGRA1:58