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

begin

theorem :: INTEGRA2:1

for A being closed-interval Subset of REAL
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 Relation-like NAT -defined REAL -valued Function-like V28() V29() V30() V47() FinSequence-like FinSubsequence-like 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 ;
:: original: **
redefine func x ** A -> Subset of REAL;
coherence
x ** A is Subset of REAL

proof end;

canceled;

end;

:: deftheorem INTEGRA2:def 2 :
canceled;

theorem :: INTEGRA2:5

for X, Y being non empty set
for f being PartFunc of X,REAL 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 X,REAL st f | X is bounded_below & Y c= X holds
(f | Y) | Y is bounded_below

proof end;

theorem :: 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 REAL 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 REAL 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 REAL 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 REAL 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 REAL 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 REAL 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 REAL 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 REAL 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 REAL 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 X,REAL 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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 REAL
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 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 & integral (f - g) = (integral f) - (integral g) )

proof end;

theorem :: INTEGRA2:34

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 & ( 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 REAL
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 REAL
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 REAL;
mode DivSequence of A is Function of NAT,(divs A);

end;

definition

let A be closed-interval Subset of REAL;
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;

canceled;

end;

:: deftheorem INTEGRA2:def 3 :
canceled;

definition

let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
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 REAL
for f being PartFunc of A,REAL
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 REAL
for f being PartFunc of A,REAL
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 :: INTEGRA2:37

for A being closed-interval Subset of REAL
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 :: INTEGRA2:40

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

proof end;

theorem :: INTEGRA2:41

for A being Subset of REAL
for a, x being Real st x in a ** A holds
ex b being Real st
( b in A & x = a * b )

proof end;

begin

theorem :: INTEGRA2:42

for A being non empty ext-real-membered set holds 0 ** A = {0}

proof end;