:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received October 30, 2007

:: Copyright (c) 2007-2016 Association of Mizar Users

theorem Th1: :: MESFUNC7:1

for X being non empty set

for f, g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom f holds

f . x <= g . x ) holds

g - f is nonnegative

for f, g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom f holds

f . x <= g . x ) holds

g - f is nonnegative

proof end;

theorem Th2: :: MESFUNC7:2

for X being non empty set

for Y being set

for f being PartFunc of X,ExtREAL

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

for Y being set

for f being PartFunc of X,ExtREAL

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

proof end;

reconsider jj = 1 as Real ;

theorem Th3: :: MESFUNC7:3

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,ExtREAL st 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,ExtREAL st 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;

registration

let X be non empty set ;

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

end;
cluster Relation-like X -defined ExtREAL -valued Function-like extreal-yielding nonnegative for Element of K16(K17(X,ExtREAL));

existence ex b

proof end;

registration

let X be non empty set ;

let f be PartFunc of X,ExtREAL;

correctness

coherence

for b_{1} being PartFunc of X,ExtREAL st b_{1} = |.f.| holds

b_{1} is nonnegative ;

end;
let f be PartFunc of X,ExtREAL;

correctness

coherence

for b

b

proof end;

theorem :: MESFUNC7: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,ExtREAL st f is_integrable_on M holds

ex F being sequence of S st

( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds

( F . n in S & M . (F . n) < +infty ) ) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

ex F being sequence of S st

( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds

( F . n in S & M . (F . n) < +infty ) ) )

proof end;

registration

ex b_{1} being FinSequence st b_{1} is extreal-yielding
end;

cluster Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like extreal-yielding for set ;

existence ex b

proof end;

definition

ex b_{1} being BinOp of ExtREAL st

for x, y being Element of ExtREAL holds b_{1} . (x,y) = x * y
from BINOP_1:sch 4();

uniqueness

for b_{1}, b_{2} being BinOp of ExtREAL st ( for x, y being Element of ExtREAL holds b_{1} . (x,y) = x * y ) & ( for x, y being Element of ExtREAL holds b_{2} . (x,y) = x * y ) holds

b_{1} = b_{2}
from BINOP_2:sch 2();

end;

func multextreal -> BinOp of ExtREAL means :Def1: :: MESFUNC7:def 1

for x, y being Element of ExtREAL holds it . (x,y) = x * y;

existence for x, y being Element of ExtREAL holds it . (x,y) = x * y;

ex b

for x, y being Element of ExtREAL holds b

uniqueness

for b

b

:: deftheorem Def1 defines multextreal MESFUNC7:def 1 :

for b_{1} being BinOp of ExtREAL holds

( b_{1} = multextreal iff for x, y being Element of ExtREAL holds b_{1} . (x,y) = x * y );

for b

( b

Lm1: 1. is_a_unity_wrt multextreal

proof end;

definition

let F be extreal-yielding FinSequence;

ex b_{1} being Element of ExtREAL ex f being FinSequence of ExtREAL st

( f = F & b_{1} = multextreal $$ f )

for b_{1}, b_{2} being Element of ExtREAL st ex f being FinSequence of ExtREAL st

( f = F & b_{1} = multextreal $$ f ) & ex f being FinSequence of ExtREAL st

( f = F & b_{2} = multextreal $$ f ) holds

b_{1} = b_{2}
;

end;
func Product F -> Element of ExtREAL means :Def2: :: MESFUNC7:def 2

ex f being FinSequence of ExtREAL st

( f = F & it = multextreal $$ f );

existence ex f being FinSequence of ExtREAL st

( f = F & it = multextreal $$ f );

ex b

( f = F & b

proof end;

uniqueness for b

( f = F & b

( f = F & b

b

:: deftheorem Def2 defines Product MESFUNC7:def 2 :

for F being extreal-yielding FinSequence

for b_{2} being Element of ExtREAL holds

( b_{2} = Product F iff ex f being FinSequence of ExtREAL st

( f = F & b_{2} = multextreal $$ f ) );

for F being extreal-yielding FinSequence

for b

( b

( f = F & b

registration
end;

:: deftheorem defines |^ MESFUNC7:def 3 :

for x being Element of ExtREAL

for k being Nat holds x |^ k = Product (k |-> x);

for x being Element of ExtREAL

for k being Nat holds x |^ k = Product (k |-> x);

definition

let x be Element of ExtREAL ;

let k be Nat;

:: original: |^

redefine func x |^ k -> R_eal;

coherence

x |^ k is R_eal ;

end;
let k be Nat;

:: original: |^

redefine func x |^ k -> R_eal;

coherence

x |^ k is R_eal ;

registration
end;

registration
end;

theorem Th8: :: MESFUNC7:8

for F being extreal-yielding FinSequence

for r being Element of ExtREAL holds Product (F ^ <*r*>) = (Product F) * r

for r being Element of ExtREAL holds Product (F ^ <*r*>) = (Product F) * r

proof end;

definition

let k be Nat;

let X be non empty set ;

let f be PartFunc of X,ExtREAL;

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

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

b_{1} . x = (f . x) |^ k ) )

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

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

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

b_{1} = b_{2}

end;
let X be non empty set ;

let f be PartFunc of X,ExtREAL;

func f |^ k -> PartFunc of X,ExtREAL means :Def4: :: MESFUNC7:def 4

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

it . x = (f . x) |^ k ) );

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

it . x = (f . x) |^ k ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines |^ MESFUNC7:def 4 :

for k being Nat

for X being non empty set

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

( b_{4} = f |^ 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) |^ k ) ) );

for k being Nat

for X being non empty set

for f, b

( b

b

theorem Th14: :: MESFUNC7:14

for k being Nat

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

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

|.f.| |^ k is_measurable_on E

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

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

|.f.| |^ k is_measurable_on E

proof end;

theorem Th15: :: MESFUNC7:15

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for E being Element of S st (dom f) /\ (dom g) = E & f is V71() & g is V71() & f is_measurable_on E & g is_measurable_on E holds

f (#) g is_measurable_on E

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for E being Element of S st (dom f) /\ (dom g) = E & f is V71() & g is V71() & f is_measurable_on E & g is_measurable_on E holds

f (#) g is_measurable_on E

proof end;

theorem Th16: :: MESFUNC7:16

for X being non empty set

for f being PartFunc of X,ExtREAL st rng f is real-bounded holds

f is V71()

for f being PartFunc of X,ExtREAL st rng f is real-bounded holds

f is V71()

proof end;

:: Mean value theorem for integrals (first)

theorem :: MESFUNC7:17

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

for E being Element of S

for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V71() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds

( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st

( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL

for E being Element of S

for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V71() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds

( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st

( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )

proof end;

theorem Th18: :: MESFUNC7:18

for X being non empty set

for f being PartFunc of X,ExtREAL

for A being set holds |.f.| | A = |.(f | A).|

for f being PartFunc of X,ExtREAL

for A being set holds |.f.| | A = |.(f | A).|

proof end;

theorem Th19: :: MESFUNC7:19

for X being non empty set

for f, g being PartFunc of X,ExtREAL holds

( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )

for f, g being PartFunc of X,ExtREAL holds

( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )

proof end;

theorem Th20: :: MESFUNC7:20

for X being non empty set

for f, g being PartFunc of X,ExtREAL holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)

for f, g being PartFunc of X,ExtREAL holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)

proof end;

theorem Th21: :: MESFUNC7:21

for X being non empty set

for f, g being PartFunc of X,ExtREAL

for x being set st x in dom |.(f + g).| holds

|.(f + g).| . x <= (|.f.| + |.g.|) . x

for f, g being PartFunc of X,ExtREAL

for x being set st x in dom |.(f + g).| holds

|.(f + g).| . x <= (|.f.| + |.g.|) . x

proof end;

theorem :: MESFUNC7:22

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,ExtREAL st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (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,ExtREAL st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )

proof end;

theorem Th24: :: MESFUNC7:24

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S st M . E < +infty holds

( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S st M . E < +infty holds

( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )

proof end;

theorem Th25: :: MESFUNC7:25

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds

Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds

Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)

proof end;

theorem :: MESFUNC7:26

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

for a, b being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds

( a <= f . x & f . x <= b ) ) holds

( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S

for a, b being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds

( a <= f . x & f . x <= b ) ) holds

( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )

proof end;