:: The First Mean Value Theorem for Integrals
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received October 30, 2007
:: Copyright (c) 2007-2012 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
proofend;

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

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 &amp; g is_integrable_on M &amp; g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) &amp; Integral (M,(f | E)) <= Integral (M,(g | E)) )
proofend;

begin

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

registration
let X be non empty set ;
let f be PartFunc of X,ExtREAL;
cluster|.f.| ->  nonnegative for PartFunc of X,ExtREAL;
correctness
coherence
for b1 being PartFunc of X,ExtREAL st b1 = |.f.| holds
b1 is nonnegative ;
proofend;
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))))) ) &amp; (dom f) \ (eq_dom (f,0.)) = union (rng F) &amp; ( for n being Element of NAT holds
( F . n in S &amp; M . (F . n) < +infty ) ) )
proofend;

begin

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

registration
cluster Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like extreal-yielding for set ;
existence
 ex b1 being FinSequence st b1 is extreal-yielding
proofend;
end;

definition
func multextreal  ->  BinOp of ExtREAL means :Def1: :: MESFUNC7:def 1
 for x, y being Element of ExtREAL holds it . (x,y) = x * y;
existence
 ex b1 being BinOp of ExtREAL st
for x, y being Element of ExtREAL holds b1 . (x,y) = x * y from BINOP_1:sch_4();
uniqueness
 for b1, b2 being BinOp of ExtREAL st ( for x, y being Element of ExtREAL holds b1 . (x,y) = x * y ) &amp; ( for x, y being Element of ExtREAL holds b2 . (x,y) = x * y ) holds
b1 = b2 from BINOP_2:sch_2();
end;

:: deftheorem Def1 defines multextreal MESFUNC7:def_1_:_
 for b1 being BinOp of ExtREAL holds
( b1 = multextreal iff for x, y being Element of ExtREAL holds b1 . (x,y) = x * y );

registration
cluster multextreal  ->  commutative associative ;
coherence
 ( multextreal is commutative &amp; multextreal is associative )
proofend;
end;

Lm1:  1. is_a_unity_wrt multextreal
proofend;

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:14;
end;

definition
let F be extreal-yielding FinSequence;
func Product F ->  Element of ExtREAL  means :Def2: :: MESFUNC7:def 2
 ex f being FinSequence of ExtREAL st
( f = F &amp; it = multextreal $$ f );
existence
 ex b1 being Element of ExtREAL ex f being FinSequence of ExtREAL st
( f = F &amp; b1 = multextreal $$ f )
proofend;
uniqueness
 for b1, b2 being Element of ExtREAL st ex f being FinSequence of ExtREAL st
( f = F &amp; b1 = multextreal $$ f ) &amp; ex f being FinSequence of ExtREAL st
( f = F &amp; b2 = multextreal $$ f ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines Product MESFUNC7:def_2_:_
 for F being extreal-yielding FinSequence
for b2 being Element of ExtREAL holds
( b2 = Product F iff ex f being FinSequence of ExtREAL st
( f = F &amp; b2 = multextreal $$ f ) );

registration
let x be Element of ExtREAL ;
let n be Nat;
clustern |-> x ->  extreal-yielding ;
coherence
 n |-> x is extreal-yielding ;
end;

definition
let x be Element of ExtREAL ;
let k be Nat;
funcx |^ k ->  set  equals :: MESFUNC7:def 3
 Product (k |-> x);
coherence
 Product (k |-> x) is set ;
end;

:: deftheorem  defines |^ MESFUNC7:def_3_:_
 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 funcx |^ 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
proofend;

theorem Th7: :: MESFUNC7:7
for r being Element of ExtREAL holds Product <*r*> = r
proofend;

registration
let f, g be extreal-yielding FinSequence;
clusterf ^ g ->  extreal-yielding ;
coherence
 f ^ g is extreal-yielding
proofend;
end;

theorem Th8: :: MESFUNC7:8
for F being extreal-yielding FinSequence
for r being Element of ExtREAL holds Product (F ^ <*r*>) = (Product F) * r
proofend;

theorem Th9: :: MESFUNC7:9
for x being Element of ExtREAL holds x |^ 1 = x
proofend;

theorem Th10: :: MESFUNC7:10
for x being Element of ExtREAL
for k being Nat holds x |^ (k + 1) = (x |^ k) * x
proofend;

definition
let k be Nat;
let X be non empty set ;
let f be PartFunc of X,ExtREAL;
funcf |^ k ->  PartFunc of X,ExtREAL means :Def4: :: MESFUNC7:def 4
( dom it = dom f &amp; ( for x being Element of X st x in dom it holds
it . x = (f . x) |^ k ) );
existence
 ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom f &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = (f . x) |^ k ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom f &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = (f . x) |^ k ) &amp; dom b2 = dom f &amp; ( for x being Element of X st x in dom b2 holds
b2 . x = (f . x) |^ k ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines |^ MESFUNC7:def_4_:_
 for k being Nat
for X being non empty set
for f, b4 being PartFunc of X,ExtREAL holds
( b4 = f |^ k iff ( dom b4 = dom f &amp; ( for x being Element of X st x in dom b4 holds
b4 . x = (f . x) |^ k ) ) );

theorem Th11: :: MESFUNC7:11
for x being Element of ExtREAL
for y being real number
for k being Nat st x = y holds
x |^ k = y |^ k
proofend;

theorem Th12: :: MESFUNC7:12
for x being Element of ExtREAL
for k being Nat st 0 <= x holds
0 <= x |^ k
proofend;

theorem Th13: :: MESFUNC7:13
for k being Nat st 1 <= k holds
+infty |^ k = +infty
proofend;

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 &amp; f is_measurable_on E holds
|.f.| |^ k is_measurable_on E
proofend;

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 &amp; f is V67() &amp; g is V67() &amp; f is_measurable_on E &amp; g is_measurable_on E holds
f (#) g is_measurable_on E
proofend;

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 V67()
proofend;

:: [WP: ] 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 &amp; rng f = F &amp; g is V67() &amp; f is_measurable_on E &amp; rng f is real-bounded &amp; g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M &amp; ex c being Element of REAL st
( c >= inf F &amp; c <= sup F &amp; Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )
proofend;

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

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) &amp; dom |.(f + g).| c= dom |.f.| )
proofend;

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

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

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 &amp; g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) &amp; Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
proofend;

theorem Th23: :: MESFUNC7:23
for X being non empty set
for A being set holds max+ (chi (A,X)) = chi (A,X)
proofend;

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 &amp; Integral (M,(chi (E,X))) = M . E &amp; Integral (M,((chi (E,X)) | E)) = M . E )
proofend;

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

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 &amp; E c= dom f &amp; M . E < +infty &amp; ( for x being Element of X st x in E holds
( a <= f . x &amp; f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral (M,(f | E)) &amp; Integral (M,(f | E)) <= (R_EAL b) * (M . E) )
proofend;