begin
theorem Th1:
begin
:: deftheorem MESFUN6C:def 1 :
canceled;
:: deftheorem MESFUN6C:def 2 :
canceled;
:: deftheorem Def3 defines is_measurable_on MESFUN6C:def 3 :
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for E being Element of S holds
( f is_measurable_on E iff ( Re f is_measurable_on E & Im f is_measurable_on E ) );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th17:
theorem
begin
:: deftheorem Def4 defines is_integrable_on MESFUN6C:def 4 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX holds
( f is_integrable_on M iff ( Re f is_integrable_on M & Im f is_integrable_on M ) );
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
let f be
PartFunc of
X,
COMPLEX ;
assume A1:
f is_integrable_on M
;
func Integral M,
f -> complex number means :
Def5:
ex
R,
I being
Real st
(
R = Integral M,
(Re f) &
I = Integral M,
(Im f) &
it = R + (I * <i> ) );
existence
ex b1 being complex number ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & b1 = R + (I * <i> ) )
uniqueness
for b1, b2 being complex number st ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & b1 = R + (I * <i> ) ) & ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & b2 = R + (I * <i> ) ) holds
b1 = b2
;
end;
:: deftheorem Def5 defines Integral MESFUN6C:def 5 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
for b5 being complex number holds
( b5 = Integral M,f iff ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & b5 = R + (I * <i> ) ) );
Lm1:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( max+ f is nonnegative & max- f is nonnegative )
theorem Th19:
theorem Th20:
theorem
theorem
theorem Th23:
theorem
theorem
:: deftheorem Def6 defines to_power MESFUN6C:def 6 :
for k being real number
for X being non empty set
for f, b4 being PartFunc of X,REAL holds
( b4 = f to_power k iff ( dom b4 = dom f & ( for x being Element of X st x in dom b4 holds
b4 . x = (f . x) to_power k ) ) );
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
Lm2:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral M,f = 0 holds
|.(Integral M,f).| <= Integral M,|.f.|
theorem Th41:
theorem Th42:
Lm3:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral M,f <> 0 holds
|.(Integral M,f).| <= Integral M,|.f.|
theorem
:: deftheorem defines Integral_on MESFUN6C:def 7 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for B being Element of S holds Integral_on M,B,f = Integral M,(f | B);
theorem
theorem
begin
theorem
theorem
theorem
theorem