:: 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 Association of Mizar Users

begin

definition

let X be RealNormSpace;
let A be 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 :Def5: :: 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 b₁ being FinSequence of X st
( len b₁ = 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)) & b₁ . i = (vol (divset D,i)) * c ) ) );

proof end;

end;

:: deftheorem Def5 defines middle_volume INTEGR18:def 1 :
for X being RealNormSpace
for A being closed-interval Subset of REAL
for f being Function of A,the carrier of X
for D being Division of A
for b₅ being FinSequence of X holds
( b₅ is middle_volume of f,D iff ( len b₅ = 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)) & b₅ . i = (vol (divset D,i)) * c ) ) ) );

definition

let X be RealNormSpace;
let A be 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 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 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 :Def7: :: INTEGR18:def 3
for k being Element of NAT holds it . k is middle_volume of f,T . k;
correctness
existence
ex b₁ being Function of NAT ,(the carrier of X * ) st
for k being Element of NAT holds b₁ . k is middle_volume of f,T . k;

proof end;

end;

:: deftheorem Def7 defines middle_volume_Sequence INTEGR18:def 3 :
for X being RealNormSpace
for A being closed-interval Subset of REAL
for f being Function of A,the carrier of X
for T being DivSequence of A
for b₅ being Function of NAT ,(the carrier of X * ) holds
( b₅ is middle_volume_Sequence of f,T iff for k being Element of NAT holds b₅ . k is middle_volume of f,T . k );

definition

let X be RealNormSpace;
let A be 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 func S . k -> middle_volume of f,T . k;
coherence
S . k is middle_volume of f,T . k by Def7;

end;

definition

let X be RealNormSpace;
let A be 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 :Def8: :: INTEGR18:def 4
for i being Element of NAT holds it . i = middle_sum f,(S . i);
existence
ex b₁ being sequence of X st
for i being Element of NAT holds b₁ . i = middle_sum f,(S . i)

proof end;

uniqueness
for b₁, b₂ being sequence of X st ( for i being Element of NAT holds b₁ . i = middle_sum f,(S . i) ) & ( for i being Element of NAT holds b₂ . i = middle_sum f,(S . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines middle_sum INTEGR18:def 4 :
for X being RealNormSpace
for A being 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 b₆ being sequence of X holds
( b₆ = middle_sum f,S iff for i being Element of NAT holds b₆ . i = middle_sum f,(S . i) );

begin

definition

let X be RealNormSpace;
let A be closed-interval Subset of REAL ;
let f be Function of A,the carrier of X;
attr f is integrable means :Def13: :: 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 Def13 defines integrable INTEGR18:def 5 :
for X being RealNormSpace
for A being 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 SM1: :: 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)

proof end;

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)

proof end;

theorem SM3: :: 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)

proof end;

definition

let X be RealNormSpace;
let A be closed-interval Subset of REAL ;
let f be Function of A,the carrier of X;
assume AS: f is integrable ;
func integral f -> Point of X means :Def14: :: 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 b₁ 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) = b₁ ) by AS, Def13;
uniqueness
for b₁, b₂ 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) = b₁ ) ) & ( 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) = b₂ ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines integral INTEGR18:def 6 :
for X being RealNormSpace
for A being closed-interval Subset of REAL
for f being Function of A,the carrier of X st f is integrable holds
for b₄ being Point of X holds
( b₄ = 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) = b₄ ) );

theorem LMth03: :: INTEGR18:4

for X being RealNormSpace
for A being 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) )

proof end;

theorem LMth03a: :: INTEGR18:5

for X being RealNormSpace
for A being 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) )

proof end;

theorem LMth01: :: INTEGR18:6

for X being RealNormSpace
for A being 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) )

proof end;

theorem :: INTEGR18:7

for X being RealNormSpace
for A being 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) )

proof end;

definition

let X be RealNormSpace;
let A be closed-interval Subset of REAL ;
let f be PartFunc of REAL ,the carrier of X;
pred f is_integrable_on A means :Def16: :: INTEGR18:def 7
ex g being Function of A,the carrier of X st
( g = f | A & g is integrable );

end;

:: deftheorem Def16 defines is_integrable_on INTEGR18:def 7 :
for X being RealNormSpace
for A being 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 closed-interval Subset of REAL ;
let f be PartFunc of REAL ,the carrier of X;
assume AS: A c= dom f ;
func integral f,A -> Element of X means :Def17: :: INTEGR18:def 8
ex g being Function of A,the carrier of X st
( g = f | A & it = integral g );
correctness
existence
ex b₁ being Element of X ex g being Function of A,the carrier of X st
( g = f | A & b₁ = integral g );
uniqueness
for b₁, b₂ being Element of X st ex g being Function of A,the carrier of X st
( g = f | A & b₁ = integral g ) & ex g being Function of A,the carrier of X st
( g = f | A & b₂ = integral g ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def17 defines integral INTEGR18:def 8 :
for X being RealNormSpace
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,the carrier of X st A c= dom f holds
for b₄ being Element of X holds
( b₄ = integral f,A iff ex g being Function of A,the carrier of X st
( g = f | A & b₄ = integral g ) );

theorem Th01: :: INTEGR18:8

for X being RealNormSpace
for A being 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 )

proof end;

theorem :: INTEGR18:9

for X being RealNormSpace
for A being 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 Def17;

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

proof end;

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

proof end;

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

proof end;

begin

theorem th001: :: INTEGR18:13

for X being RealNormSpace
for r being Real
for A being 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) )

proof end;

theorem th002: :: INTEGR18:14

for X being RealNormSpace
for A being 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) )

proof end;

theorem :: INTEGR18:15

for X being RealNormSpace
for A being 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) )

proof end;

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 :Def18: :: 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 ) & ( not a <= b implies - (integral f,['b,a']) is Element of X ) );
consistency
for b₁ being Element of X holds verum;
;

end;

:: deftheorem Def18 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'] ) & ( not a <= b implies integral f,a,b = - (integral f,['b,a']) ) );

theorem th100: :: INTEGR18:16

for X being RealNormSpace
for f being PartFunc of REAL ,the carrier of X
for A being closed-interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral f,A = integral f,a,b

proof end;

theorem th46C: :: INTEGR18:17

for X being RealNormSpace
for f being PartFunc of REAL ,the carrier of X
for A being closed-interval Subset of REAL st vol A = 0 & A c= dom f holds
( f is_integrable_on A & integral f,A = 0. X )

proof end;

theorem :: INTEGR18:18

for X being RealNormSpace
for f being PartFunc of REAL ,the carrier of X
for A being closed-interval Subset of REAL
for a, b being Real st A = [.b,a.] & A c= dom f holds
- (integral f,A) = integral f,a,b

proof end;