:: Riemann Integral of Functions from $\mathbbbR$ into Real Normed Space
:: by Keiichi Miyajima , Takahiro Kato and Yasunari Shidama
::
:: Received May 20, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let D be Division of A;
mode middle_volume of f,D ->  FinSequence of X means :Def1: :: INTEGR18:def 1
( len it = len D & ( for i being Nat st i in dom D holds
ex c being Point of X st
( c in rng (f | (divset (D,i))) & it . i = (vol (divset (D,i))) * c ) ) );
correctness
existence
ex b1 being FinSequence of X st
( len b1 = len D & ( for i being Nat st i in dom D holds
ex c being Point of X st
( c in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * c ) ) );
proofend;
end;

:: deftheorem Def1 defines middle_volume INTEGR18:def_1_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for D being Division of A
for b5 being FinSequence of X holds
( b5 is middle_volume of f,D iff ( len b5 = len D & ( for i being Nat st i in dom D holds
ex c being Point of X st
( c in rng (f | (divset (D,i))) & b5 . i = (vol (divset (D,i))) * c ) ) ) );

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let D be Division of A;
let F be middle_volume of f,D;
func middle_sum (f,F) ->  Point of X equals :: INTEGR18:def 2
 Sum F;
coherence
 Sum F is Point of X ;
end;

:: deftheorem  defines middle_sum INTEGR18:def_2_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for D being Division of A
for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let T be DivSequence of A;
mode middle_volume_Sequence of f,T ->  Function of NAT,( the carrier of X *) means :Def3: :: INTEGR18:def 3
 for k being Element of NAT holds it . k is middle_volume of f,T . k;
correctness
existence
ex b1 being Function of NAT,( the carrier of X *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k;
proofend;
end;

:: deftheorem Def3 defines middle_volume_Sequence INTEGR18:def_3_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for T being DivSequence of A
for b5 being Function of NAT,( the carrier of X *) holds
( b5 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b5 . k is middle_volume of f,T . k );

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original:.
redefine funcS . k ->  middle_volume of f,T . k;
coherence
 S . k is middle_volume of f,T . k by Def3;
end;

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
func middle_sum (f,S) ->  sequence of X means :Def4: :: INTEGR18:def 4
 for i being Element of NAT holds it . i = middle_sum (f,(S . i));
existence
 ex b1 being sequence of X st
for i being Element of NAT holds b1 . i = middle_sum (f,(S . i))
proofend;
uniqueness
 for b1, b2 being sequence of X st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines middle_sum INTEGR18:def_4_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b6 being sequence of X holds
( b6 = middle_sum (f,S) iff for i being Element of NAT holds b6 . i = middle_sum (f,(S . i)) );

begin

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
attrf is integrable  means :Def5: :: INTEGR18:def 5
 ex I being Point of X st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I );
end;

:: deftheorem Def5 defines integrable INTEGR18:def_5_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X holds
( f is integrable iff ex I being Point of X st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) );

theorem Th1: :: INTEGR18:1
for X being RealNormSpace
for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 + R2 holds
Sum R3 = (Sum R1) + (Sum R2)
proofend;

theorem :: INTEGR18:2
for X being RealNormSpace
for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds
Sum R3 = (Sum R1) - (Sum R2)
proofend;

theorem Th3: :: INTEGR18:3
for X being RealNormSpace
for R1, R2 being FinSequence of X
for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
proofend;

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
assume A1: f is integrable ;
func integral f ->  Point of X means :Def6: :: INTEGR18:def 6
 for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = it );
existence
 ex b1 being Point of X st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = b1 ) by A1, Def5;
uniqueness
 for b1, b2 being Point of X st ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = b1 ) ) & ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = b2 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines integral INTEGR18:def_6_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X st f is integrable holds
for b4 being Point of X holds
( b4 = integral f iff for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = b4 ) );

theorem Th4: :: INTEGR18:4
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for r being Real
for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds
( h is integrable & integral h = r * (integral f) )
proofend;

theorem Th5: :: INTEGR18:5
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f, h being Function of A, the carrier of X st h = - f & f is integrable holds
( h is integrable & integral h = - (integral f) )
proofend;

theorem Th6: :: INTEGR18:6
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) + (integral g) )
proofend;

theorem :: INTEGR18:7
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) - (integral g) )
proofend;

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL, the carrier of X;
predf is_integrable_on A means :Def7: :: INTEGR18:def 7
 ex g being Function of A, the carrier of X st
( g = f | A & g is integrable );
end;

:: deftheorem Def7 defines is_integrable_on INTEGR18:def_7_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X holds
( f is_integrable_on A iff ex g being Function of A, the carrier of X st
( g = f | A & g is integrable ) );

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL, the carrier of X;
assume A1: A c= dom f ;
func integral (f,A) ->  Element of X means :Def8: :: INTEGR18:def 8
 ex g being Function of A, the carrier of X st
( g = f | A & it = integral g );
correctness
existence
ex b1 being Element of X ex g being Function of A, the carrier of X st
( g = f | A & b1 = integral g );
uniqueness
for b1, b2 being Element of X st ex g being Function of A, the carrier of X st
( g = f | A & b1 = integral g ) & ex g being Function of A, the carrier of X st
( g = f | A & b2 = integral g ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def8 defines integral INTEGR18:def_8_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X st A c= dom f holds
for b4 being Element of X holds
( b4 = integral (f,A) iff ex g being Function of A, the carrier of X st
( g = f | A & b4 = integral g ) );

theorem Th8: :: INTEGR18:8
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st f | A = g holds
( f is_integrable_on A iff g is integrable )
proofend;

theorem :: INTEGR18:9
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st A c= dom f & f | A = g holds
integral (f,A) = integral g by Def8;

theorem Th10: :: INTEGR18:10
for X, Y being non empty set
for V being RealNormSpace
for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 + f1 = g + f
proofend;

theorem :: INTEGR18:11
for X, Y being non empty set
for V being RealNormSpace
for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 - f1 = g - f
proofend;

theorem Th12: :: INTEGR18:12
for r being Real
for X, Y being non empty set
for V being RealNormSpace
for g being PartFunc of X, the carrier of V
for g1 being PartFunc of Y, the carrier of V st g = g1 holds
r (#) g1 = r (#) g
proofend;

begin

theorem Th13: :: INTEGR18:13
for X being RealNormSpace
for r being Real
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
proofend;

theorem Th14: :: INTEGR18:14
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) )
proofend;

theorem :: INTEGR18:15
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
proofend;

definition
let X be RealNormSpace;
let f be PartFunc of REAL, the carrier of X;
let a, b be real number ;
func integral (f,a,b) ->  Element of X equals :Def9: :: INTEGR18:def 9
 integral (f,['a,b']) if a <= b
otherwise  - (integral (f,['b,a']));
correctness
coherence
( ( a <= b implies integral (f,['a,b']) is Element of X ) &amp; ( not a <= b implies - (integral (f,['b,a'])) is Element of X ) );
consistency
for b1 being Element of X holds verum;
;
end;

:: deftheorem Def9 defines integral INTEGR18:def_9_:_
 for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for a, b being real number holds
( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) &amp; ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) );

theorem Th16: :: INTEGR18:16
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
proofend;

theorem Th17: :: INTEGR18:17
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for A being non empty closed_interval Subset of REAL st vol A = 0 &amp; A c= dom f holds
( f is_integrable_on A &amp; integral (f,A) = 0. X )
proofend;

theorem :: INTEGR18:18
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] &amp; A c= dom f holds
- (integral (f,A)) = integral (f,a,b)
proofend;