:: Integrability of Bounded Total Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received February 1, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users

begin

theorem Th1: :: INTEGRA4:1

for A being closed-interval Subset of REAL
for D being Division of A st vol A = 0 holds
len D = 1

proof end;

theorem Th2: :: INTEGRA4:2

for A being closed-interval Subset of REAL holds
( chi (A,A) is integrable & integral (chi (A,A)) = vol A )

proof end;

theorem Th3: :: INTEGRA4:3

for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for r being Real holds
( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) )

proof end;

theorem Th4: :: INTEGRA4:4

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for r being Real st rng f = {r} holds
( f is integrable & integral f = r * (vol A) )

proof end;

theorem Th5: :: INTEGRA4:5

for A being closed-interval Subset of REAL
for r being Real ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded )

proof end;

Lm1: for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )

proof end;

Lm2: for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is lower_integrable & lower_integral f = 0 )

proof end;

theorem Th6: :: INTEGRA4:6

for A being closed-interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is integrable & integral f = 0 )

proof end;

theorem :: INTEGRA4:7

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )

proof end;

begin

theorem Th8: :: INTEGRA4:8

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds
( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f )

proof end;

theorem Th9: :: INTEGRA4:9

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

proof end;

theorem Th10: :: INTEGRA4:10

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
( f is upper_integrable & f is lower_integrable )

proof end;

definition

let A be closed-interval Subset of REAL;
let IT be Division of A;
let n be Element of NAT ;
pred IT divide_into_equal n means :Def1: :: INTEGRA4:def 1
( len IT = n & ( for i being Element of NAT st i in dom IT holds
IT . i = (lower_bound A) + (((vol A) / (len IT)) * i) ) );

end;

:: deftheorem Def1 defines divide_into_equal INTEGRA4:def 1 :
for A being closed-interval Subset of REAL
for IT being Division of A
for n being Element of NAT holds
( IT divide_into_equal n iff ( len IT = n & ( for i being Element of NAT st i in dom IT holds
IT . i = (lower_bound A) + (((vol A) / (len IT)) * i) ) ) );

Lm3: for A being closed-interval Subset of REAL
for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )

proof end;

Lm4: for A being closed-interval Subset of REAL st vol A > 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )

proof end;

Lm5: for A being closed-interval Subset of REAL st vol A = 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )

proof end;

theorem Th11: :: INTEGRA4:11

for A being closed-interval Subset of REAL ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )

proof end;

theorem Th12: :: INTEGRA4:12

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )

proof end;

theorem Th13: :: INTEGRA4:13

for C being non empty set
for f being Function of C,REAL holds
( max+ f is total & max- f is total )

proof end;

theorem Th14: :: INTEGRA4:14

for C being non empty set
for X being set
for f being PartFunc of C,REAL st f | X is bounded_above holds
(max+ f) | X is bounded_above

proof end;

theorem Th15: :: INTEGRA4:15

for C being non empty set
for X being set
for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below

proof end;

theorem Th16: :: INTEGRA4:16

for C being non empty set
for X being set
for f being PartFunc of C,REAL st f | X is bounded_below holds
(max- f) | X is bounded_above

proof end;

theorem Th17: :: INTEGRA4:17

for C being non empty set
for X being set
for f being PartFunc of C,REAL holds (max- f) | X is bounded_below

proof end;

theorem Th18: :: INTEGRA4:18

for A being closed-interval Subset of REAL
for X being set
for f being PartFunc of A,REAL st f | A is bounded_above holds
rng (f | X) is bounded_above

proof end;

theorem Th19: :: INTEGRA4:19

for A being closed-interval Subset of REAL
for X being set
for f being PartFunc of A,REAL st f | A is bounded_below holds
rng (f | X) is bounded_below

proof end;

theorem Th20: :: INTEGRA4:20

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
max+ f is integrable

proof end;

theorem Th21: :: INTEGRA4:21

for C being non empty set
for f being PartFunc of C,REAL holds max- f = max+ (- f)

proof end;

theorem Th22: :: INTEGRA4:22

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
max- f is integrable

proof end;

theorem :: INTEGRA4:23

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
( abs f is integrable & abs (integral f) <= integral (abs f) )

proof end;

theorem Th24: :: INTEGRA4:24

for a being Real
for A being closed-interval Subset of REAL
for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= a ) holds
(upper_bound (rng f)) - (lower_bound (rng f)) <= a

proof end;

theorem Th25: :: INTEGRA4:25

for a being Real
for A being closed-interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
(upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))

proof end;

theorem Th26: :: INTEGRA4:26

for a being Real
for A being closed-interval Subset of REAL
for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
(upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))

proof end;

theorem Th27: :: INTEGRA4:27

for a being Real
for A being closed-interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
g is integrable

proof end;

theorem Th28: :: INTEGRA4:28

for a being Real
for A being closed-interval Subset of REAL
for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
h is integrable

proof end;

theorem :: INTEGRA4:29

for A being closed-interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds
f (#) g is integrable

proof end;

theorem :: INTEGRA4:30

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded holds
f ^ is integrable

proof end;