:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received July 30, 2008

:: Copyright (c) 2008-2018 Association of Mizar Users

theorem :: MESFUN6C:1

definition

let X be non empty set ;

let S be SigmaField of X;

let f be PartFunc of X,COMPLEX;

let E be Element of S;

end;
let S be SigmaField of X;

let f be PartFunc of X,COMPLEX;

let E be Element of S;

pred f is_measurable_on E means :: MESFUN6C:def 1

( Re f is_measurable_on E & Im f is_measurable_on E );

( Re f is_measurable_on E & Im f is_measurable_on E );

:: deftheorem defines is_measurable_on MESFUN6C:def 1 :

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 ) );

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: :: MESFUN6C:2

for X being non empty set

for f being PartFunc of X,COMPLEX

for r being Real holds

( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )

for f being PartFunc of X,COMPLEX

for r being Real holds

( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )

proof end;

theorem Th3: :: MESFUN6C:3

for X being non empty set

for f being PartFunc of X,COMPLEX

for c being Complex holds

( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )

for f being PartFunc of X,COMPLEX

for c being Complex holds

( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )

proof end;

theorem Th4: :: MESFUN6C:4

for X being non empty set

for f being PartFunc of X,COMPLEX holds

( - (Im f) = Re (<i> (#) f) & Re f = Im (<i> (#) f) )

for f being PartFunc of X,COMPLEX holds

( - (Im f) = Re (<i> (#) f) & Re f = Im (<i> (#) f) )

proof end;

theorem Th5: :: MESFUN6C:5

for X being non empty set

for f, g being PartFunc of X,COMPLEX holds

( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) )

for f, g being PartFunc of X,COMPLEX holds

( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) )

proof end;

theorem Th6: :: MESFUN6C:6

for X being non empty set

for f, g being PartFunc of X,COMPLEX holds

( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) )

for f, g being PartFunc of X,COMPLEX holds

( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) )

proof end;

theorem Th7: :: MESFUN6C:7

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

proof end;

theorem :: MESFUN6C:9

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A, B being Element of S st B c= A & f is_measurable_on A holds

f is_measurable_on B by MESFUNC6:16;

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A, B being Element of S st B c= A & f is_measurable_on A holds

f is_measurable_on B by MESFUNC6:16;

theorem :: MESFUN6C:10

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds

f is_measurable_on A \/ B by MESFUNC6:17;

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds

f is_measurable_on A \/ B by MESFUNC6:17;

theorem :: MESFUN6C:11

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX

for A being Element of S st f is_measurable_on A & g is_measurable_on A holds

f + g is_measurable_on A

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX

for A being Element of S st f is_measurable_on A & g is_measurable_on A holds

f + g is_measurable_on A

proof end;

theorem :: MESFUN6C:12

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX

for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds

f - g is_measurable_on A

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX

for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds

f - g is_measurable_on A

proof end;

theorem :: MESFUN6C:13

for X being non empty set

for Y being set

for f, g being PartFunc of X,COMPLEX st Y c= dom (f + g) holds

( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )

for Y being set

for f, g being PartFunc of X,COMPLEX st Y c= dom (f + g) holds

( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )

proof end;

theorem :: MESFUN6C:14

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A, B being Element of S st f is_measurable_on B & A = (dom f) /\ B holds

f | B is_measurable_on A

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A, B being Element of S st f is_measurable_on B & A = (dom f) /\ B holds

f | B is_measurable_on A

proof end;

theorem :: MESFUN6C:15

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX st dom f in S & dom g in S holds

dom (f + g) in S

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX st dom f in S & dom g in S holds

dom (f + g) in S

proof end;

theorem :: MESFUN6C:16

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A, B being Element of S st dom f = A holds

( f is_measurable_on B iff f is_measurable_on A /\ B )

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A, B being Element of S st dom f = A holds

( f is_measurable_on B iff f is_measurable_on A /\ B )

proof end;

theorem Th17: :: MESFUN6C:17

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for c being Complex

for A being Element of S st f is_measurable_on A & A c= dom f holds

c (#) f is_measurable_on A

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for c being Complex

for A being Element of S st f is_measurable_on A & A c= dom f holds

c (#) f is_measurable_on A

proof end;

theorem :: MESFUN6C:18

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds

for c being Complex

for B being Element of S st f is_measurable_on B holds

c (#) f is_measurable_on B

for S being SigmaField of X

for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds

for c being Complex

for B being Element of S st f is_measurable_on B holds

c (#) f is_measurable_on B

proof end;

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;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,COMPLEX;

pred f is_integrable_on M means :: MESFUN6C:def 2

( Re f is_integrable_on M & Im f is_integrable_on M );

( Re f is_integrable_on M & Im f is_integrable_on M );

:: deftheorem defines is_integrable_on MESFUN6C:def 2 :

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 ) );

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 ;

ex b_{1} being Complex ex R, I being Real st

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b_{1} = R + (I * <i>) )

for b_{1}, b_{2} being Complex st ex R, I being Real st

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b_{1} = R + (I * <i>) ) & ex R, I being Real st

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b_{2} = R + (I * <i>) ) holds

b_{1} = b_{2}
;

end;
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 means :Def3: :: MESFUN6C:def 3

ex R, I being Real st

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & it = R + (I * <i>) );

existence ex R, I being Real st

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & it = R + (I * <i>) );

ex b

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b

proof end;

uniqueness for b

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b

b

:: deftheorem Def3 defines Integral MESFUN6C:def 3 :

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 b_{5} being Complex holds

( b_{5} = Integral (M,f) iff ex R, I being Real st

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b_{5} = R + (I * <i>) ) );

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 b

( b

( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b

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 )

proof end;

theorem Th19: :: MESFUN6C:19

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

for A being Element of S st ex E being Element of S st

( E = dom f & f is_measurable_on E ) & M . A = 0 holds

f | A is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st ex E being Element of S st

( E = dom f & f is_measurable_on E ) & M . A = 0 holds

f | A is_integrable_on M

proof end;

theorem Th20: :: MESFUN6C:20

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,REAL

for E, A being Element of S st ex E being Element of S st

( E = dom f & f is_measurable_on E ) & M . A = 0 holds

f | A is_integrable_on M by Th19;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for E, A being Element of S st ex E being Element of S st

( E = dom f & f is_measurable_on E ) & M . A = 0 holds

f | A is_integrable_on M by Th19;

theorem :: MESFUN6C:21

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 A being Element of S st ex E being Element of S st

( E = dom f & f is_measurable_on E ) & M . A = 0 holds

( f | A is_integrable_on M & Integral (M,(f | A)) = 0 )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for A being Element of S st ex E being Element of S st

( E = dom f & f is_measurable_on E ) & M . A = 0 holds

( f | A is_integrable_on M & Integral (M,(f | A)) = 0 )

proof end;

theorem :: MESFUN6C:22

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 E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds

Integral (M,(f | (E \ A))) = Integral (M,f)

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds

Integral (M,(f | (E \ A))) = Integral (M,f)

proof end;

theorem Th23: :: MESFUN6C:23

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 A being Element of S st f is_integrable_on M holds

f | A is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for A being Element of S st f is_integrable_on M holds

f | A is_integrable_on M

proof end;

theorem :: MESFUN6C:24

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 A, B being Element of S st f is_integrable_on M & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for A, B being Element of S st f is_integrable_on M & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

proof end;

theorem :: MESFUN6C:25

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 A, B being Element of S st f is_integrable_on M & B = (dom f) \ A holds

( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for A, B being Element of S st f is_integrable_on M & B = (dom f) \ A holds

( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )

proof end;

definition

let k be Real;

let X be non empty set ;

let f be PartFunc of X,REAL;

ex b_{1} being PartFunc of X,REAL st

( dom b_{1} = dom f & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = (f . x) to_power k ) )

for b_{1}, b_{2} being PartFunc of X,REAL st dom b_{1} = dom f & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = (f . x) to_power k ) & dom b_{2} = dom f & ( for x being Element of X st x in dom b_{2} holds

b_{2} . x = (f . x) to_power k ) holds

b_{1} = b_{2}

end;
let X be non empty set ;

let f be PartFunc of X,REAL;

func f to_power k -> PartFunc of X,REAL means :Def4: :: MESFUN6C:def 4

( dom it = dom f & ( for x being Element of X st x in dom it holds

it . x = (f . x) to_power k ) );

existence ( dom it = dom f & ( for x being Element of X st x in dom it holds

it . x = (f . x) to_power k ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines to_power MESFUN6C:def 4 :

for k being Real

for X being non empty set

for f, b_{4} being PartFunc of X,REAL holds

( b_{4} = f to_power k iff ( dom b_{4} = dom f & ( for x being Element of X st x in dom b_{4} holds

b_{4} . x = (f . x) to_power k ) ) );

for k being Real

for X being non empty set

for f, b

( b

b

registration

let X be non empty set ;

ex b_{1} being PartFunc of X,REAL st b_{1} is nonnegative

end;
cluster Relation-like X -defined REAL -valued Function-like V54() V55() V56() nonnegative for PartFunc of ,;

existence ex b

proof end;

registration

let k be non negative Real;

let X be non empty set ;

let f be nonnegative PartFunc of X,REAL;

coherence

f to_power k is nonnegative

end;
let X be non empty set ;

let f be nonnegative PartFunc of X,REAL;

coherence

f to_power k is nonnegative

proof end;

theorem Th26: :: MESFUN6C:26

for k being Real

for X being non empty set

for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k holds

f to_power k is nonnegative ;

for X being non empty set

for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k holds

f to_power k is nonnegative ;

theorem Th27: :: MESFUN6C:27

for x being object

for X being non empty set

for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative holds

(f . x) to_power (1 / 2) = sqrt (f . x)

for X being non empty set

for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative holds

(f . x) to_power (1 / 2) = sqrt (f . x)

proof end;

theorem Th28: :: MESFUN6C:28

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))

proof end;

reconsider jj = 1 as Real ;

theorem Th29: :: MESFUN6C:29

for k being Real

for X being non empty set

for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds

f to_power k is_measurable_on E

for X being non empty set

for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds

f to_power k is_measurable_on E

proof end;

theorem Th30: :: MESFUN6C:30

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S st f is_measurable_on A & A c= dom f holds

|.f.| is_measurable_on A

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S st f is_measurable_on A & A c= dom f holds

|.f.| is_measurable_on A

proof end;

theorem Th31: :: MESFUN6C:31

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 ) holds

( f is_integrable_on M iff |.f.| is_integrable_on M )

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 ) holds

( f is_integrable_on M iff |.f.| is_integrable_on M )

proof end;

theorem :: MESFUN6C:32

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

proof end;

theorem Th33: :: MESFUN6C:33

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

proof end;

theorem Th34: :: MESFUN6C:34

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds

f - g is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds

f - g is_integrable_on M

proof end;

theorem :: MESFUN6C:35

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

f - g is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

f - g is_integrable_on M

proof end;

theorem Th36: :: MESFUN6C:36

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

proof end;

theorem :: MESFUN6C:37

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )

proof end;

theorem Th38: :: MESFUN6C:38

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 r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

proof end;

theorem Th39: :: MESFUN6C:39

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

( <i> (#) f is_integrable_on M & Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) )

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

( <i> (#) f is_integrable_on M & Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) )

proof end;

theorem Th40: :: MESFUN6C:40

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 c being Complex st f is_integrable_on M holds

( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for c being Complex st f is_integrable_on M holds

( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) )

proof end;

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.|)

proof end;

theorem Th41: :: MESFUN6C:41

for X being non empty set

for f being PartFunc of X,REAL

for Y being set

for r being Real holds (r (#) f) | Y = r (#) (f | Y)

for f being PartFunc of X,REAL

for Y being set

for r being Real holds (r (#) f) | Y = r (#) (f | Y)

proof end;

theorem Th42: :: MESFUN6C:42

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st ex A being Element of S st

( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st ex A being Element of S st

( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

proof end;

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.|)

proof end;

theorem :: MESFUN6C:43

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 holds

|.(Integral (M,f)).| <= Integral (M,|.f.|)

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 holds

|.(Integral (M,f)).| <= Integral (M,|.f.|)

proof end;

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;

let B be Element of S;

coherence

Integral (M,(f | B)) is Complex ;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,COMPLEX;

let B be Element of S;

coherence

Integral (M,(f | B)) is Complex ;

:: deftheorem defines Integral_on 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

for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));

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 :: MESFUN6C:44

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX

for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds

( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX

for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds

( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )

proof end;

theorem :: MESFUN6C:45

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 c being Complex

for B being Element of S st f is_integrable_on M holds

Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for c being Complex

for B being Element of S st f is_integrable_on M holds

Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))

proof end;

theorem :: MESFUN6C:46

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))

proof end;

theorem :: MESFUN6C:47

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

proof end;

theorem :: MESFUN6C:48

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))

proof end;

theorem :: MESFUN6C:49

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL

for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))

proof end;