:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama

::

:: Received February 1, 2000

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

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 )

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

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

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 )

for r being Real ex f being Function of A,REAL st

( rng f = {r} & f | A is bounded )

proof end;

Lm1: 0 in REAL

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 )

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

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 (delta T) = 0 holds

( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f )

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 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 (delta T) = 0 holds

( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

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

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

( f is upper_integrable & f is lower_integrable )

proof end;

definition
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 = (lower_bound A) + (((vol A) / (len IT)) * i) ) ) );

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 = (lower_bound A) + (((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 = (lower_bound A) + (((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 (delta T) = 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 (delta T) = 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 (delta T) = 0 )

( delta T is convergent & lim (delta T) = 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 (delta T) = 0 holds

(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )

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 )

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

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

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

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

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

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

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

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

max+ f is integrable

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

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 f).| <= integral (abs f) )

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

( abs f is integrable & |.(integral f).| <= 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

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

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

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

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

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

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

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;