begin
theorem LM001:
:: deftheorem INTEGR16:def 1 :
canceled;
:: deftheorem INTEGR16:def 2 :
canceled;
:: deftheorem Def5 defines middle_volume INTEGR16:def 3 :
for A being closed-interval Subset of REAL
for f being Function of A,COMPLEX
for D being Division of A
for b4 being FinSequence of COMPLEX holds
( b4 is middle_volume of f,D iff ( len b4 = len D & ( for i being Nat st i in dom D holds
ex c being Element of COMPLEX st
( c in rng (f | (divset D,i)) & b4 . i = c * (vol (divset D,i)) ) ) ) );
:: deftheorem defines middle_sum INTEGR16:def 4 :
for A being closed-interval Subset of REAL
for f being Function of A,COMPLEX
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 INTEGR16:def 5 :
for A being closed-interval Subset of REAL
for f being Function of A,COMPLEX
for T being DivSequence of A
for b4 being Function of NAT ,(COMPLEX * ) holds
( b4 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b4 . k is middle_volume of f,T . k );
:: deftheorem Def8 defines middle_sum INTEGR16:def 6 :
for A being closed-interval Subset of REAL
for f being Function of A,COMPLEX
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b5 being Complex_Sequence holds
( b5 = middle_sum f,S iff for i being Element of NAT holds b5 . i = middle_sum f,(S . i) );
begin
theorem
theorem
theorem LMDef5:
RVSUM1102:
Sum (<*> COMPLEX ) = 0
by BINOP_2:1, FINSOP_1:11;
RVSUM1104:
for F being FinSequence of COMPLEX
for x being Element of COMPLEX holds Sum (F ^ <*x*>) = (Sum F) + x
theorem RVSUM1105:
theorem RVSUM2105:
theorem LMDefR0:
theorem LMDefI0:
theorem
theorem
:: deftheorem Def13 defines integrable INTEGR16:def 7 :
for A being closed-interval Subset of REAL
for f being Function of A,COMPLEX holds
( f is integrable iff ( Re f is integrable & Im f is integrable ) );
theorem BND01A:
theorem
theorem BND01:
:: deftheorem defines integral INTEGR16:def 8 :
for A being closed-interval Subset of REAL
for f being Function of A,COMPLEX holds integral f = (integral (Re f)) + ((integral (Im f)) * <i> );
theorem Th11:
theorem
:: deftheorem Def16 defines is_integrable_on INTEGR16:def 9 :
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,COMPLEX holds
( f is_integrable_on A iff ( Re f is_integrable_on A & Im f is_integrable_on A ) );
:: deftheorem defines integral INTEGR16:def 10 :
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,COMPLEX holds integral f,A = (integral (Re f),A) + ((integral (Im f),A) * <i> );
Lm6:
for f being PartFunc of REAL ,COMPLEX
for A being Subset of REAL holds
( Re (f | A) = (Re f) | A & Im (f | A) = (Im f) | A )
theorem
theorem
definition
let a,
b be
real number ;
let f be
PartFunc of
REAL ,
COMPLEX ;
func integral f,
a,
b -> Element of
COMPLEX equals
(integral (Re f),a,b) + ((integral (Im f),a,b) * <i> );
correctness
coherence
(integral (Re f),a,b) + ((integral (Im f),a,b) * <i> ) is Element of COMPLEX ;
;
end;
:: deftheorem defines integral INTEGR16:def 11 :
for a, b being real number
for f being PartFunc of REAL ,COMPLEX holds integral f,a,b = (integral (Re f),a,b) + ((integral (Im f),a,b) * <i> );
begin
theorem Th16C:
theorem
theorem
theorem
theorem
theorem