:: INTEGRA4 semantic presentation

theorem Th1: :: INTEGRA4:1

for A being closed-interval Subset of REAL
for D being Element of divs 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_on A & 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_on A & 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 is_bounded_on A )

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_on A & 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_on A & 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_on A & 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 is_bounded_on A & f is_integrable_on A holds
ex a being Real st
( inf (rng f) <= a & a <= sup (rng f) & integral f = a * (vol A) )

proof end;

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 is_bounded_on A & 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 is_bounded_on A & 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 is_bounded_on A holds
( f is_upper_integrable_on A & f is_lower_integrable_on A )

proof end;

definition

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

end;

:: deftheorem Def1 defines divide_into_equal INTEGRA4:def 1 :

Lm3: for A being closed-interval Subset of REAL
for n being Nat st n > 0 & vol A > 0 holds
ex D being Element of divs A st
( len D = n & ( for i being Nat st i in dom D holds
D . i = (inf 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 is_bounded_on A holds
( f is_integrable_on A 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 is_bounded_above_on X holds
max+ f is_bounded_above_on X

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 is_bounded_below_on X

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 is_bounded_below_on X holds
max- f is_bounded_above_on X

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 is_bounded_below_on X

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 is_bounded_above_on A 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 is_bounded_below_on A 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 is_bounded_on A & f is_integrable_on A holds
max+ f is_integrable_on A

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 is_bounded_on A & f is_integrable_on A holds
max- f is_integrable_on A

proof end;

theorem :: INTEGRA4:23

for A being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A & f is_integrable_on A holds
( abs f is_integrable_on A & 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
(sup (rng f)) - (inf (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 is_bounded_on A & 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
(sup (rng g)) - (inf (rng g)) <= a * ((sup (rng f)) - (inf (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 is_bounded_on A & g is_bounded_on A & 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
(sup (rng h)) - (inf (rng h)) <= a * (((sup (rng f)) - (inf (rng f))) + ((sup (rng g)) - (inf (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 is_bounded_on A & f is_integrable_on A & g is_bounded_on A & 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_on A

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 is_bounded_on A & f is_integrable_on A & g is_bounded_on A & g is_integrable_on A & h is_bounded_on A & 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_on A

proof end;

theorem :: INTEGRA4:29

for A being closed-interval Subset of REAL
for f, g being Function of A, REAL st f is_bounded_on A & f is_integrable_on A & g is_bounded_on A & g is_integrable_on A holds
f (#) g is_integrable_on A

proof end;

theorem :: INTEGRA4:30

for A being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A & f is_integrable_on A & not 0 in rng f & f ^ is_bounded_on A holds
f ^ is_integrable_on A

proof end;