:: The First Mean Value Theorem for Integrals
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received October 30, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users

begin

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

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)

proof end;

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

proof end;

begin

registration

let X be non empty set ;
cluster Relation-like X -defined ExtREAL -valued V18() extreal-yielding nonnegative Element of K6(K7(X,ExtREAL));
existence
ex b₁ being PartFunc of X,ExtREAL st b₁ is nonnegative

proof end;

end;

registration

let X be non empty set ;
let f be PartFunc of X,ExtREAL;
cluster |.f.| -> nonnegative PartFunc of X,ExtREAL;
correctness
coherence
for b₁ being PartFunc of X,ExtREAL st b₁ = |.f.| holds
b₁ is nonnegative ;

proof end;

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 Function of NAT,S st
( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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;

begin

notation

let F be Relation;
synonym extreal-yielding F for ext-real-valued ;

end;

registration

cluster Relation-like V18() V31() FinSequence-like FinSubsequence-like extreal-yielding set ;
existence
ex b₁ being FinSequence st b₁ is extreal-yielding

proof end;

end;

definition

canceled;
func multextreal -> BinOp of ExtREAL means :Def2: :: MESFUNC7:def 2
for x, y being Element of ExtREAL holds it . (x,y) = x * y;
existence
ex b₁ being BinOp of ExtREAL st
for x, y being Element of ExtREAL holds b₁ . (x,y) = x * y from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of ExtREAL st ( for x, y being Element of ExtREAL holds b₁ . (x,y) = x * y ) & ( for x, y being Element of ExtREAL holds b₂ . (x,y) = x * y ) holds
b₁ = b₂ from BINOP_2:sch 2();

end;

:: deftheorem MESFUNC7:def 1 :
canceled;

:: deftheorem Def2 defines multextreal MESFUNC7:def 2 :
for b₁ being BinOp of ExtREAL holds
( b₁ = multextreal iff for x, y being Element of ExtREAL holds b₁ . (x,y) = x * y );

registration

cluster multextreal -> commutative associative ;
coherence
( multextreal is commutative & multextreal is associative )

proof end;

end;

Lm1: 1. is_a_unity_wrt multextreal

proof end;

theorem Th5: :: MESFUNC7:5

the_unity_wrt multextreal = 1 by Lm1, BINOP_1:def 8;

registration

cluster multextreal -> having_a_unity ;
coherence
multextreal is having_a_unity by Lm1, Th5, SETWISEO:22;

end;

definition

let F be extreal-yielding FinSequence;
func Product F -> Element of ExtREAL means :Def3: :: MESFUNC7:def 3
ex f being FinSequence of ExtREAL st
( f = F & it = multextreal $$ f );
existence
ex b₁ being Element of ExtREAL ex f being FinSequence of ExtREAL st
( f = F & b₁ = multextreal $$ f )

proof end;

uniqueness
for b₁, b₂ being Element of ExtREAL st ex f being FinSequence of ExtREAL st
( f = F & b₁ = multextreal $$ f ) & ex f being FinSequence of ExtREAL st
( f = F & b₂ = multextreal $$ f ) holds
b₁ = b₂ ;

end;

:: deftheorem Def3 defines Product MESFUNC7:def 3 :
for F being extreal-yielding FinSequence
for b₂ being Element of ExtREAL holds
( b₂ = Product F iff ex f being FinSequence of ExtREAL st
( f = F & b₂ = multextreal $$ f ) );

registration

let x be Element of ExtREAL ;
let n be natural number ;
cluster n |-> x -> extreal-yielding ;
coherence
n |-> x is extreal-yielding ;

end;

definition

let x be Element of ExtREAL ;
let k be natural number ;
func x |^ k -> set equals :: MESFUNC7:def 4
Product (k |-> x);
coherence
Product (k |-> x) is set ;

end;

:: deftheorem defines |^ MESFUNC7:def 4 :
for x being Element of ExtREAL
for k being natural number holds x |^ k = Product (k |-> x);

definition

let x be Element of ExtREAL ;
let k be natural number ;
:: original: |^
redefine func x |^ k -> R_eal;
coherence
x |^ k is R_eal ;

end;

registration

cluster <*> ExtREAL -> extreal-yielding ;
coherence
<*> ExtREAL is extreal-yielding ;

end;

registration

let r be Element of ExtREAL ;
cluster <*r*> -> extreal-yielding ;
coherence
<*r*> is extreal-yielding ;

end;

theorem Th6: :: MESFUNC7:6

Product (<*> ExtREAL) = 1

proof end;

theorem Th7: :: MESFUNC7:7

for r being Element of ExtREAL holds Product <*r*> = r

proof end;

registration

let f, g be extreal-yielding FinSequence;
cluster f ^ g -> extreal-yielding ;
coherence
f ^ g is extreal-yielding

proof end;

end;

theorem Th8: :: MESFUNC7:8

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

proof end;

theorem Th9: :: MESFUNC7:9

for x being Element of ExtREAL holds x |^ 1 = x

proof end;

theorem Th10: :: MESFUNC7:10

for x being Element of ExtREAL
for k being natural number holds x |^ (k + 1) = (x |^ k) * x

proof end;

definition

let k be natural number ;
let X be non empty set ;
let f be PartFunc of X,ExtREAL;
func f |^ k -> PartFunc of X,ExtREAL means :Def5: :: MESFUNC7:def 5
( dom it = dom f & ( for x being Element of X st x in dom it holds
it . x = (f . x) |^ k ) );
existence
ex b₁ being PartFunc of X,ExtREAL st
( dom b₁ = dom f & ( for x being Element of X st x in dom b₁ holds
b₁ . x = (f . x) |^ k ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of X,ExtREAL st dom b₁ = dom f & ( for x being Element of X st x in dom b₁ holds
b₁ . x = (f . x) |^ k ) & dom b₂ = dom f & ( for x being Element of X st x in dom b₂ holds
b₂ . x = (f . x) |^ k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines |^ MESFUNC7:def 5 :
for k being natural number
for X being non empty set
for f, b₄ being PartFunc of X,ExtREAL holds
( b₄ = f |^ k iff ( dom b₄ = dom f & ( for x being Element of X st x in dom b₄ holds
b₄ . x = (f . x) |^ k ) ) );

theorem Th11: :: MESFUNC7:11

for x being Element of ExtREAL
for y being real number
for k being natural number st x = y holds
x |^ k = y |^ k

proof end;

theorem Th12: :: MESFUNC7:12

for x being Element of ExtREAL
for k being natural number st 0 <= x holds
0 <= x |^ k

proof end;

theorem Th13: :: MESFUNC7:13

for k being natural number st 1 <= k holds
+infty |^ k = +infty

proof end;

theorem Th14: :: MESFUNC7:14

for k being natural number
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 real-valued & g is real-valued & 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 bounded holds
f is real-valued

proof end;

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 real-valued & f is_measurable_on E & rng f is 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)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )

proof end;

begin

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

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

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

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

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

proof end;

theorem Th23: :: MESFUNC7:23

for X being non empty set
for A being set holds max+ (chi (A,X)) = chi (A,X)

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 )

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)

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 number 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
( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) )

proof end;