INTEGRA1: The Definition of Riemann Definite Integral and some Related Lemmas

:: The Definition of Riemann Definite Integral and some Related Lemmas
:: by Noboru Endou and Artur Korni{\l}owicz
::
:: Received March 13, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users

begin

definition

let IT be set ;
attr IT is closed-interval means :Def1: :: INTEGRA1:def 1
ex a, b being Real st
( a <= b & IT = [.a,b.] );

end;

:: deftheorem Def1 defines closed-interval INTEGRA1:def 1 :

registration

cluster complex-membered ext-real-membered real-membered closed-interval Element of bool REAL;
existence

proof end;

end;

theorem Th1: :: INTEGRA1:1

for A being closed-interval Subset of REAL holds A is compact

proof end;

theorem Th2: :: INTEGRA1:2

for A being closed-interval Subset of REAL holds not A is empty

proof end;

registration

cluster closed-interval -> non empty compact Element of bool REAL;
coherence by Th1, Th2;

end;

theorem Th3: :: INTEGRA1:3

for A being closed-interval Subset of REAL holds
( A is bounded_below & A is bounded_above )

proof end;

registration

cluster closed-interval -> bounded Element of bool REAL;
coherence

proof end;

end;

registration

cluster complex-membered ext-real-membered real-membered closed-interval Element of bool REAL;
existence

proof end;

end;

theorem Th4: :: INTEGRA1:4

for A being closed-interval Subset of REAL holds lower_bound A <= upper_bound A by SEQ_4:24;

theorem Th5: :: INTEGRA1:5

for A being closed-interval Subset of REAL holds A = [.(lower_bound A),(upper_bound A).]

proof end;

theorem Th6: :: INTEGRA1:6

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

proof end;

begin

definition

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

proof end;

end;

:: deftheorem Def2 defines Division INTEGRA1:def 2 :

definition

let A be non empty compact Subset of REAL;
func divs A -> set means :Def3: :: INTEGRA1:def 3
for x1 being set holds
( x1 in it iff x1 is Division of A );
existence

proof end;

proof end;

end;

:: deftheorem Def3 defines divs INTEGRA1:def 3 :

registration

let A be non empty compact Subset of REAL;
cluster divs A -> non empty ;
coherence

proof end;

end;

registration

let A be non empty compact Subset of REAL;
cluster -> Relation-like Function-like Element of divs A;
coherence by Def3;

end;

registration

let A be non empty compact Subset of REAL;
cluster -> FinSequence-like real-valued Element of divs A;
coherence by Def3;

end;

theorem :: INTEGRA1:7

canceled;

theorem Th8: :: INTEGRA1:8

for i being Element of NAT
for A being closed-interval Subset of REAL
for D being Division of A st i in dom D holds
D . i in A

proof end;

theorem Th9: :: INTEGRA1:9

for i being Element of NAT
for A being 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

canceled;
let A be closed-interval Subset of REAL;
let D be Division of A;
let i be Nat;
assume A1: i in dom D ;
func divset (D,i) -> closed-interval Subset of REAL means :Def5: :: INTEGRA1:def 5
( 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

proof end;

proof end;

end;

:: deftheorem INTEGRA1:def 4 :

:: deftheorem Def5 defines divset INTEGRA1:def 5 :

theorem Th10: :: INTEGRA1:10

for i being Element of NAT
for A being 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

let A be Subset of REAL;
func vol A -> Real equals :: INTEGRA1:def 6
(upper_bound A) - (lower_bound A);
correctness ;

end;

:: deftheorem defines vol INTEGRA1:def 6 :

theorem :: INTEGRA1:11

for A being non empty bounded Subset of REAL holds 0 <= vol A by SEQ_4:24, XREAL_1:50;

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: :: INTEGRA1:def 7
( 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

proof end;

proof end;

func lower_volume (f,D) -> FinSequence of REAL means :Def8: :: INTEGRA1:def 8
( 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

proof end;

proof end;

end;

:: deftheorem Def7 defines upper_volume INTEGRA1:def 7 :

:: deftheorem Def8 defines lower_volume INTEGRA1:def 8 :

definition

let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
let D be Division of A;
func upper_sum (f,D) -> Real equals :: INTEGRA1:def 9
Sum (upper_volume (f,D));
correctness ;
func lower_sum (f,D) -> Real equals :: INTEGRA1:def 10
Sum (lower_volume (f,D));
correctness ;

end;

:: deftheorem defines upper_sum INTEGRA1:def 9 :

:: deftheorem defines lower_sum INTEGRA1:def 10 :

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: :: INTEGRA1:def 11
( dom it = divs A & ( for D being Division of A st D in dom it holds
it . D = upper_sum (f,D) ) );
existence

proof end;

proof end;

func lower_sum_set f -> PartFunc of (divs A),REAL means :Def12: :: INTEGRA1:def 12
( dom it = divs A & ( for D being Division of A st D in dom it holds
it . D = lower_sum (f,D) ) );
existence

proof end;

proof end;

end;

:: deftheorem Def11 defines upper_sum_set INTEGRA1:def 11 :

:: deftheorem Def12 defines lower_sum_set INTEGRA1:def 12 :

definition

let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
attr f is upper_integrable means :Def13: :: INTEGRA1:def 13
rng (upper_sum_set f) is bounded_below ;
attr f is lower_integrable means :Def14: :: INTEGRA1:def 14
rng (lower_sum_set f) is bounded_above ;

end;

:: deftheorem Def13 defines upper_integrable INTEGRA1:def 13 :

:: deftheorem Def14 defines lower_integrable INTEGRA1:def 14 :

definition

let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
func upper_integral f -> Real equals :: INTEGRA1:def 15
lower_bound (rng (upper_sum_set f));
correctness ;

end;

:: deftheorem defines upper_integral INTEGRA1:def 15 :

definition

let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
func lower_integral f -> Real equals :: INTEGRA1:def 16
upper_bound (rng (lower_sum_set f));
coherence ;

end;

:: deftheorem defines lower_integral INTEGRA1:def 16 :

definition

let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
attr f is integrable means :Def17: :: INTEGRA1:def 17
( f is upper_integrable & f is lower_integrable & upper_integral f = lower_integral f );

end;

:: deftheorem Def17 defines integrable INTEGRA1:def 17 :

definition

let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
func integral f -> Real equals :: INTEGRA1:def 18
upper_integral f;
coherence ;

end;

:: deftheorem defines integral INTEGRA1:def 18 :

begin

theorem Th12: :: INTEGRA1:12

for X being non empty set
for f, g being PartFunc of X,REAL holds rng (f + g) c= (rng f) ++ (rng g)

proof end;

theorem Th13: :: INTEGRA1:13

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

proof end;

theorem :: INTEGRA1:14

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

proof end;

theorem Th15: :: INTEGRA1:15

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

proof end;

theorem :: INTEGRA1:16

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

proof end;

theorem :: INTEGRA1:17

for X being non empty set
for f being PartFunc of X,REAL st f | X is bounded holds
rng f is bounded

proof end;

begin

theorem Th18: :: INTEGRA1:18

for A being non empty set holds (chi (A,A)) | A is constant

proof end;

theorem Th19: :: INTEGRA1:19

for X being non empty set
for A being non empty Subset of X holds rng (chi (A,A)) = {1}

proof end;

theorem Th20: :: INTEGRA1:20

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}

proof end;

theorem Th21: :: INTEGRA1:21

for i being Element of NAT
for A being 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 Th22: :: INTEGRA1:22

for i being Element of NAT
for A being 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:23

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)

proof end;

theorem Th24: :: INTEGRA1:24

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)

proof end;

theorem Th25: :: INTEGRA1:25

for A being closed-interval Subset of REAL
for D being Division of A holds Sum (lower_volume ((chi (A,A)),D)) = vol A

proof end;

theorem Th26: :: INTEGRA1:26

for A being closed-interval Subset of REAL
for D being Division of A holds Sum (upper_volume ((chi (A,A)),D)) = vol A

proof end;

begin

registration

let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
let D be Division of A;
cluster upper_volume (f,D) -> non empty ;
coherence

proof end;

cluster lower_volume (f,D) -> non empty ;
coherence

proof end;

end;

theorem Th27: :: INTEGRA1:27

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

proof end;

theorem :: INTEGRA1:28

for i being Element of NAT
for A being 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 Th29: :: INTEGRA1:29

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

proof end;

theorem Th30: :: INTEGRA1:30

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

proof end;

definition

let D1, D2 be FinSequence;
canceled;
pred D1 <= D2 means :Def20: :: INTEGRA1:def 20
( len D1 <= len D2 & rng D1 c= rng D2 );
reflexivity ;

end;

:: deftheorem INTEGRA1:def 19 :

:: deftheorem Def20 defines <= INTEGRA1:def 20 :

notation

let D1, D2 be FinSequence;
synonym D2 >= D1 for D1 <= D2;

end;

theorem :: INTEGRA1:31

for A being closed-interval Subset of REAL
for D1, D2 being Division of A st len D1 = 1 holds
D1 <= D2

proof end;

theorem Th32: :: INTEGRA1:32

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

proof end;

theorem Th33: :: INTEGRA1:33

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

proof end;

theorem :: INTEGRA1:34

for i being Element of NAT
for A being closed-interval Subset of REAL
for D being Division of A st i in dom D holds
ex A1, A2 being closed-interval Subset of REAL st
( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )

proof end;

theorem Th35: :: INTEGRA1:35

for i being Element of NAT
for A being 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 closed-interval Subset of REAL;
let D1, D2 be Division of A;
let i be Nat;
assume A1: D1 <= D2 ;
func indx (D2,D1,i) -> Element of NAT means :Def21: :: INTEGRA1:def 21
( it in dom D2 & D1 . i = D2 . it ) if i in dom D1
otherwise it = 0 ;
existence by A1, Th35;
uniqueness

proof end;

end;

:: deftheorem Def21 defines indx INTEGRA1:def 21 :

theorem Th36: :: INTEGRA1:36

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

proof end;

theorem Th37: :: INTEGRA1:37

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

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 Th38: :: INTEGRA1:38

for i, j being Element of NAT
for A being 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 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 Th39: :: INTEGRA1:39

for i, j being Element of NAT
for A, B being 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 ;
func PartSums p -> FinSequence of REAL means :Def22: :: INTEGRA1:def 22
( len it = len p & ( for i being Nat st i in dom p holds
it . i = Sum (p | i) ) );
existence

proof end;

proof end;

end;

:: deftheorem Def22 defines PartSums INTEGRA1:def 22 :

theorem Th40: :: INTEGRA1:40

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

proof end;

theorem Th41: :: INTEGRA1:41

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

proof end;

theorem Th42: :: INTEGRA1:42

for i being Element of NAT
for A being 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 Th43: :: INTEGRA1:43

for i being Element of NAT
for A being 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 Th44: :: INTEGRA1:44

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

proof end;

theorem Th45: :: INTEGRA1:45

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

proof end;

theorem Th46: :: INTEGRA1:46

for A being closed-interval Subset of REAL
for D1, D2 being Division of A st D1 <= D2 holds
indx (D2,D1,(len D1)) = len D2

proof end;

theorem Th47: :: INTEGRA1:47

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

proof end;

theorem Th48: :: INTEGRA1:48

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

proof end;

theorem Th49: :: INTEGRA1:49

for A being closed-interval Subset of REAL
for D1, D2 being Division of A ex D being Division of A st
( D1 <= D & D2 <= D )

proof end;

theorem Th50: :: INTEGRA1:50

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

proof end;

begin

theorem Th51: :: INTEGRA1:51

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
upper_integral f >= lower_integral f

proof end;

theorem Th52: :: INTEGRA1:52

for X, Y being Subset of REAL holds (-- X) ++ (-- Y) = -- (X ++ Y)

proof end;

theorem Th53: :: INTEGRA1:53

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

proof end;

theorem Th54: :: INTEGRA1:54

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)

proof end;

theorem Th55: :: INTEGRA1:55

for i being Element of NAT
for A being 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 Th56: :: INTEGRA1:56

for i being Element of NAT
for A being 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 Th57: :: INTEGRA1:57

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

proof end;

theorem Th58: :: INTEGRA1:58

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

proof end;

theorem :: INTEGRA1:59

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

proof end;

theorem :: INTEGRA1:60

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 by Lm1;