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

theorem Th1: :: INTEGRA4:1
for A being non empty 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 non empty 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 non empty 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 non empty 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 non empty 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:
by XREAL_0:def 1;

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

Lm3: for A being non empty 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 non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL st vol A = 0 holds
( f is integrable & integral f = 0 )
proof end;

theorem :: INTEGRA4:7
for A being non empty 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;

theorem Th8: :: INTEGRA4:8
for A being non empty 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 () = 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 non empty 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 () = 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 non empty 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 non empty closed_interval Subset of REAL;
let IT be Division of A;
let n be Nat;
pred IT divide_into_equal n means :: INTEGRA4:def 1
( len IT = n & ( for i being Nat st i in dom IT holds
IT . i = () + (((vol A) / (len IT)) * i) ) );
end;

:: deftheorem defines divide_into_equal INTEGRA4:def 1 :
for A being non empty closed_interval Subset of REAL
for IT being Division of A
for n being Nat holds
( IT divide_into_equal n iff ( len IT = n & ( for i being Nat st i in dom IT holds
IT . i = () + (((vol A) / (len IT)) * i) ) ) );

Lm4: for A being non empty closed_interval Subset of REAL
for n being Nat st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Nat st i in dom D holds
D . i = () + (((vol A) / n) * i) ) )

proof end;

Lm5: for A being non empty closed_interval Subset of REAL st vol A > 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim () = 0 )

proof end;

Lm6: for A being non empty closed_interval Subset of REAL st vol A = 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim () = 0 )

proof end;

theorem Th11: :: INTEGRA4:11
for A being non empty closed_interval Subset of REAL ex T being DivSequence of A st
( delta T is convergent & lim () = 0 )
proof end;

theorem Th12: :: INTEGRA4:12
for A being non empty 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 () = 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 & |.().| <= integral (abs f) )
proof end;

theorem Th24: :: INTEGRA4:24
for a being Real
for A being non empty 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
|.((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 non empty 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
|.((g . x) - (g . y)).| <= a * |.((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 non empty 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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((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 non empty 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
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| ) holds
g is integrable
proof end;

theorem Th28: :: INTEGRA4:28
for a being Real
for A being non empty 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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|) ) holds
h is integrable
proof end;

theorem :: INTEGRA4:29
for A being non empty 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 non empty 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;