:: Scalar Multiple of Riemann Definite Integral
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999 Association of Mizar Users

begin

theorem :: INTEGRA2:1

for A being closed-interval Subset of
for x being real number holds
( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )

proof end;

definition

let IT be FinSequence of REAL ;
attr IT is non-decreasing means :Def1: :: INTEGRA2:def 1
for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n <= IT . (n + 1);

end;

:: deftheorem Def1 defines non-decreasing INTEGRA2:def 1 :

for IT being FinSequence of REAL holds
( IT is non-decreasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n <= IT . (n + 1) );

registration

cluster non-decreasing FinSequence of REAL ;
existence
ex b₁ being FinSequence of REAL st b₁ is non-decreasing

proof end;

end;

theorem :: INTEGRA2:2

for p being non-decreasing FinSequence of REAL
for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
p . i <= p . j

proof end;

theorem :: INTEGRA2:3

for p being FinSequence of REAL ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent

proof end;

theorem :: INTEGRA2:4

for D being non empty set
for f being FinSequence of D
for k1, k2, k3 being Element of NAT st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds
(mid f,k1,k2) ^ (mid f,(k2 + 1),k3) = mid f,k1,k3

proof end;

begin

definition

let A be real-membered set ;
let x be real number ;
func x ** A -> Subset of means :Def2: :: INTEGRA2:def 2
for y being Real holds
( y in it iff ex z being Real st
( z in A & y = x * z ) );
existence
ex b₁ being Subset of st
for y being Real holds
( y in b₁ iff ex z being Real st
( z in A & y = x * z ) )

proof end;

uniqueness
for b₁, b₂ being Subset of st ( for y being Real holds
( y in b₁ iff ex z being Real st
( z in A & y = x * z ) ) ) & ( for y being Real holds
( y in b₂ iff ex z being Real st
( z in A & y = x * z ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ** INTEGRA2:def 2 :

for A being real-membered set
for x being real number
for b₃ being Subset of holds
( b₃ = x ** A iff for y being Real holds
( y in b₃ iff ex z being Real st
( z in A & y = x * z ) ) );

theorem :: INTEGRA2:5

for X, Y being non empty set
for f being PartFunc of , st f | X is bounded_above & Y c= X holds
(f | Y) | Y is bounded_above

proof end;

theorem :: INTEGRA2:6

for X, Y being non empty set
for f being PartFunc of , st f | X is bounded_below & Y c= X holds
(f | Y) | Y is bounded_below

proof end;

theorem Th7: :: INTEGRA2:7

for X being real-membered set
for a being real number holds
( X is empty iff a ** X is empty )

proof end;

theorem Th8: :: INTEGRA2:8

for r being Real
for X being Subset of holds r ** X = { (r * x) where x is Real : x in X }

proof end;

theorem :: INTEGRA2:9

for r being Real
for X being non empty Subset of st X is bounded_above & 0 <= r holds
r ** X is bounded_above

proof end;

theorem :: INTEGRA2:10

for r being Real
for X being non empty Subset of st X is bounded_above & r <= 0 holds
r ** X is bounded_below

proof end;

theorem :: INTEGRA2:11

for r being Real
for X being non empty Subset of st X is bounded_below & 0 <= r holds
r ** X is bounded_below

proof end;

theorem :: INTEGRA2:12

for r being Real
for X being non empty Subset of st X is bounded_below & r <= 0 holds
r ** X is bounded_above

proof end;

theorem Th13: :: INTEGRA2:13

for r being Real
for X being non empty Subset of st X is bounded_above & 0 <= r holds
upper_bound (r ** X) = r * (upper_bound X)

proof end;

theorem Th14: :: INTEGRA2:14

for r being Real
for X being non empty Subset of st X is bounded_above & r <= 0 holds
lower_bound (r ** X) = r * (upper_bound X)

proof end;

theorem Th15: :: INTEGRA2:15

for r being Real
for X being non empty Subset of st X is bounded_below & 0 <= r holds
lower_bound (r ** X) = r * (lower_bound X)

proof end;

theorem Th16: :: INTEGRA2:16

for r being Real
for X being non empty Subset of st X is bounded_below & r <= 0 holds
upper_bound (r ** X) = r * (lower_bound X)

proof end;

begin

theorem Th17: :: INTEGRA2:17

for r being Real
for X being non empty set
for f being Function of X, REAL holds rng (r (#) f) = r ** (rng f)

proof end;

theorem Th18: :: INTEGRA2:18

for r being Real
for X, Z being non empty set
for f being PartFunc of , holds rng (r (#) (f | Z)) = r ** (rng (f | Z))

proof end;

theorem Th19: :: INTEGRA2:19

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

proof end;

theorem Th20: :: INTEGRA2:20

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)

proof end;

theorem Th21: :: INTEGRA2:21

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)

proof end;

theorem Th22: :: INTEGRA2:22

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)

proof end;

theorem Th23: :: INTEGRA2:23

for r being Real
for i being Element of NAT
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds
(upper_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)

proof end;

theorem Th24: :: INTEGRA2:24

for r being Real
for i being Element of NAT
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)

proof end;

theorem Th25: :: INTEGRA2:25

for r being Real
for i being Element of NAT
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume (r (#) f),D) . i = r * ((lower_volume f,D) . i)

proof end;

theorem Th26: :: INTEGRA2:26

for r being Real
for i being Element of NAT
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds
(upper_volume (r (#) f),D) . i = r * ((lower_volume f,D) . i)

proof end;

theorem Th27: :: INTEGRA2:27

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st f | A is bounded_above & r >= 0 holds
upper_sum (r (#) f),D = r * (upper_sum f,D)

proof end;

theorem Th28: :: INTEGRA2:28

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st f | A is bounded_above & r <= 0 holds
lower_sum (r (#) f),D = r * (upper_sum f,D)

proof end;

theorem Th29: :: INTEGRA2:29

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st f | A is bounded_below & r >= 0 holds
lower_sum (r (#) f),D = r * (lower_sum f,D)

proof end;

theorem Th30: :: INTEGRA2:30

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL
for D being Division of A st f | A is bounded_below & r <= 0 holds
upper_sum (r (#) f),D = r * (lower_sum f,D)

proof end;

theorem Th31: :: INTEGRA2:31

for r being Real
for A being closed-interval Subset of
for f being Function of A, REAL st f | A is bounded & f is integrable holds
( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

proof end;

begin

theorem Th32: :: INTEGRA2:32

for A being closed-interval Subset of
for f being Function of A, REAL st f | A is bounded & ( for x being Real st x in A holds
f . x >= 0 ) holds
integral f >= 0

proof end;

theorem Th33: :: INTEGRA2:33

for A being closed-interval Subset of
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 & integral (f - g) = (integral f) - (integral g) )

proof end;

theorem :: INTEGRA2:34

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

proof end;

begin

theorem :: INTEGRA2:35

for A being closed-interval Subset of
for f being Function of A, REAL st f | A is bounded holds
rng (upper_sum_set f) is bounded_below

proof end;

theorem :: INTEGRA2:36

for A being closed-interval Subset of
for f being Function of A, REAL st f | A is bounded holds
rng (lower_sum_set f) is bounded_above

proof end;

definition

let A be closed-interval Subset of ;
mode DivSequence of A is Function of NAT , divs A;

end;

definition

let A be closed-interval Subset of ;
let T be DivSequence of A;
let i be Element of NAT ;
:: original: .
redefine func T . i -> Division of A;
coherence
T . i is Division of A

proof end;

end;

definition

let A be closed-interval Subset of ;
let T be DivSequence of A;
func delta T -> Real_Sequence means :: INTEGRA2:def 3
for i being Element of NAT holds it . i = delta (T . i);
existence
ex b₁ being Real_Sequence st
for i being Element of NAT holds b₁ . i = delta (T . i)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Element of NAT holds b₁ . i = delta (T . i) ) & ( for i being Element of NAT holds b₂ . i = delta (T . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines delta INTEGRA2:def 3 :

for A being closed-interval Subset of
for T being DivSequence of A
for b₃ being Real_Sequence holds
( b₃ = delta T iff for i being Element of NAT holds b₃ . i = delta (T . i) );

definition

let A be closed-interval Subset of ;
let f be PartFunc of ,;
let T be DivSequence of A;
func upper_sum f,T -> Real_Sequence means :: INTEGRA2:def 4
for i being Element of NAT holds it . i = upper_sum f,(T . i);
existence
ex b₁ being Real_Sequence st
for i being Element of NAT holds b₁ . i = upper_sum f,(T . i)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Element of NAT holds b₁ . i = upper_sum f,(T . i) ) & ( for i being Element of NAT holds b₂ . i = upper_sum f,(T . i) ) holds
b₁ = b₂

proof end;

func lower_sum f,T -> Real_Sequence means :: INTEGRA2:def 5
for i being Element of NAT holds it . i = lower_sum f,(T . i);
existence
ex b₁ being Real_Sequence st
for i being Element of NAT holds b₁ . i = lower_sum f,(T . i)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Element of NAT holds b₁ . i = lower_sum f,(T . i) ) & ( for i being Element of NAT holds b₂ . i = lower_sum f,(T . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines upper_sum INTEGRA2:def 4 :

for A being closed-interval Subset of
for f being PartFunc of ,
for T being DivSequence of A
for b₄ being Real_Sequence holds
( b₄ = upper_sum f,T iff for i being Element of NAT holds b₄ . i = upper_sum f,(T . i) );

:: deftheorem defines lower_sum INTEGRA2:def 5 :

for A being closed-interval Subset of
for f being PartFunc of ,
for T being DivSequence of A
for b₄ being Real_Sequence holds
( b₄ = lower_sum f,T iff for i being Element of NAT holds b₄ . i = lower_sum f,(T . i) );

theorem Th37: :: INTEGRA2:37

for A being closed-interval Subset of
for D1, D2 being Division of A st D1 <= D2 holds
for j being Element of NAT st j in dom D2 holds
ex i being Element of NAT st
( i in dom D1 & divset D2,j c= divset D1,i )

proof end;

theorem :: INTEGRA2:38

canceled;

theorem :: INTEGRA2:39

canceled;

theorem Th40: :: INTEGRA2:40

for A, B being closed-interval Subset of st A c= B holds
vol A <= vol B

proof end;

theorem :: INTEGRA2:41

for A being closed-interval Subset of
for D1, D2 being Division of A st D1 <= D2 holds
delta D1 >= delta D2

proof end;

begin

theorem :: INTEGRA2:42

for A being non empty Subset of holds 0 ** A = {0 }

proof end;