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


begin

theorem :: INTEGRA2:1
for A being non empty 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 V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing for FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st b1 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 by MEMBERED:3;
end;

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

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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 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 & integral (f - g) = (integral f) - (integral g) )
proof end;

theorem :: INTEGRA2:34
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 & ( 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 non empty 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 non empty 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 non empty closed_interval Subset of REAL;
mode DivSequence of A is Function of NAT,(divs A);
end;

definition
let A be non empty 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;
end;

definition
let A be non empty 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 2
 for i being Element of NAT holds it . i = upper_sum (f,(T . i));
existence
ex b1 being Real_Sequence st
for i being Element of NAT holds b1 . i = upper_sum (f,(T . i))
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = upper_sum (f,(T . i)) ) & ( for i being Element of NAT holds b2 . i = upper_sum (f,(T . i)) ) holds
b1 = b2
proof end;
func lower_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 3
 for i being Element of NAT holds it . i = lower_sum (f,(T . i));
existence
ex b1 being Real_Sequence st
for i being Element of NAT holds b1 . i = lower_sum (f,(T . i))
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = lower_sum (f,(T . i)) ) & ( for i being Element of NAT holds b2 . i = lower_sum (f,(T . i)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines upper_sum INTEGRA2:def 2 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for T being DivSequence of A
for b4 being Real_Sequence holds
( b4 = upper_sum (f,T) iff for i being Element of NAT holds b4 . i = upper_sum (f,(T . i)) );

:: deftheorem defines lower_sum INTEGRA2:def 3 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for T being DivSequence of A
for b4 being Real_Sequence holds
( b4 = lower_sum (f,T) iff for i being Element of NAT holds b4 . i = lower_sum (f,(T . i)) );

theorem :: INTEGRA2:37
for A being non empty 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
for A, B being non empty closed_interval Subset of REAL st A c= B holds
vol A <= vol B
proof end;

theorem :: INTEGRA2:39
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

:: missing, 2008.06.10
theorem :: INTEGRA2:40
for A being non empty ext-real-membered set holds 0 ** A = {0}
proof end;