begin
:: 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 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 ) ) ) );
:: 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;
:: 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 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 );
:: 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 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
:: 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:
theorem
theorem SM3:
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:
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 AS, Def13;
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
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 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 LMth03:
theorem LMth03a:
theorem LMth01:
theorem
:: 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 ) );
:: 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 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 Th01:
theorem
theorem Th03A:
theorem
theorem Th03C:
begin
theorem th001:
theorem th002:
theorem
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:
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 b1 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:
theorem th46C:
theorem