:: Measurability of Extended Real Valued Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 6, 2000
:: Copyright (c) 2000-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, PARTFUN1, PROB_1, FUNCT_1, RAT_1,
REAL_1, NAT_1, VALUED_0, RELAT_1, COMPLEX1, ARYTM_3, XXREAL_0, TARSKI,
VALUED_1, ARYTM_1, MESFUNC1, SUPINF_2, RFUNCT_3, CARD_1, FUNCT_3, PROB_2,
FINSEQ_1, FUNCOP_1, MEASURE1, SUPINF_1, ORDINAL4, MESFUNC2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3, XCMPLX_0,
XREAL_0, VALUED_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
NAT_1, WELLORD2, RAT_1, FINSEQ_1, PROB_1, XXREAL_0, SUPINF_1, FUNCOP_1,
SUPINF_2, FUNCT_3, PROB_2, MEASURE1, MEASURE2, MEASURE3, MEASURE6,
EXTREAL1, MESFUNC1;
constructors PARTFUN1, WELLORD2, FUNCT_3, FUNCOP_1, REAL_1, NAT_1, RAT_1,
FINSEQ_1, PROB_2, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1, SUPINF_1,
RELSET_1, BINOP_2, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, RAT_1, MEMBERED,
FINSEQ_1, MEASURE1, VALUED_0, FUNCT_2, CARD_1, XXREAL_3;
requirements NUMERALS, REAL, BOOLE, SUBSET;
begin :: Finite Valued Function ::
reserve X for non empty set;
reserve e for set;
reserve x for Element of X;
reserve f,g for PartFunc of X,ExtREAL;
reserve S for SigmaField of X;
reserve F for Function of RAT,S;
reserve p,q for Rational;
reserve r for Real;
reserve n,m for Nat;
reserve A,B for Element of S;
definition
let X, f;
redefine attr f is real-valued means
:: MESFUNC2:def 1
for x st x in dom f holds |. f.x .| < +infty;
end;
theorem :: MESFUNC2:1
f = 1(#)f;
theorem :: MESFUNC2:2
f is real-valued or g is real-valued implies
dom (f+g) = dom f /\ dom g & dom (f-g) = dom f /\ dom g;
theorem :: MESFUNC2:3
for f,g,F,r,A st f is real-valued & g is real-valued &
(for p holds F.p = (A /\ less_dom(f, p)) /\ (A /\
less_dom(g, (r-p)))) holds A /\ less_dom(f+g, r) = union (rng F);
begin :: Measurability of f+g and f-g ::
theorem :: MESFUNC2:4
ex F being sequence of RAT st F is one-to-one & dom F = NAT & rng F = RAT;
theorem :: MESFUNC2:5
for X,Y,Z be non empty set, F be Function of X,Z st X,Y are_equipotent holds
ex G be Function of Y,Z st rng F = rng G;
theorem :: MESFUNC2:6
for S,f,g,A st f is_measurable_on A & g is_measurable_on A holds
ex F being Function of RAT,S st for p being Rational holds
F.p = (A /\ less_dom(f, p)) /\ (A /\ less_dom(g, (r-p)));
theorem :: MESFUNC2:7
for f,g,A st f is real-valued & g is real-valued & f is_measurable_on A &
g is_measurable_on A holds f+g is_measurable_on A;
theorem :: MESFUNC2:8
for C being non empty set, f1,f2 being PartFunc of C,ExtREAL holds
f1 - f2 = f1 + (-f2);
theorem :: MESFUNC2:9
for C being non empty set, f being PartFunc of C,ExtREAL holds -f = (-1)(#)f;
theorem :: MESFUNC2:10
for C being non empty set, f being PartFunc of C,ExtREAL, r be Real
st f is real-valued holds r(#)f is real-valued;
theorem :: MESFUNC2:11
for f,g,A st f is real-valued & g is real-valued & f is_measurable_on A &
g is_measurable_on A & A c= dom g holds f-g is_measurable_on A;
begin ::definitions of extended real valued functions max+(f) and max-(f) ::
:: and their basic properties ::
definition
let C be non empty set, f be PartFunc of C,ExtREAL;
func max+(f) -> PartFunc of C,ExtREAL means
:: MESFUNC2:def 2
dom it = dom f &
for x be Element of C st x in dom it holds it.x = max(f.x,0.);
func max-(f) -> PartFunc of C,ExtREAL means
:: MESFUNC2:def 3
dom it = dom f &
for x be Element of C st x in dom it holds it.x = max(-(f.x),0.);
end;
theorem :: MESFUNC2:12
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C holds 0. <= (max+(f)).x;
theorem :: MESFUNC2:13
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C holds 0. <= (max-(f)).x;
theorem :: MESFUNC2:14
for C being non empty set, f being PartFunc of C,ExtREAL holds
max-(f) = max+(-f);
theorem :: MESFUNC2:15
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
st 0. < max+(f).x holds max-(f).x = 0.;
theorem :: MESFUNC2:16
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C st 0. < max-(f).x holds max+(f).x = 0.;
theorem :: MESFUNC2:17
for C being non empty set, f being PartFunc of C,ExtREAL holds
dom f = dom (max+(f)-max-(f)) & dom f = dom (max+(f)+max-(f));
theorem :: MESFUNC2:18
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
holds
(max+(f).x = f.x or max+(f).x = 0.) & (max-(f).x = -(f.x) or max-(f).x = 0.);
theorem :: MESFUNC2:19
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
st max+(f).x = f.x holds max-(f).x = 0.;
theorem :: MESFUNC2:20
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
st x in dom f & max+(f).x = 0. holds max-(f).x = -(f.x);
theorem :: MESFUNC2:21
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C st max-(f).x = -(f.x) holds max+(f).x = 0.;
theorem :: MESFUNC2:22
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C st x in dom f & max-(f).x = 0. holds max+(f).x = f.x;
theorem :: MESFUNC2:23
for C being non empty set, f being PartFunc of C,ExtREAL holds
f = max+(f) - max-(f);
theorem :: MESFUNC2:24
for C being non empty set, f being PartFunc of C,ExtREAL holds
|.f.| = max+(f) + max-(f);
begin :: Measurability of max+(f), max-(f) and |.f.|
theorem :: MESFUNC2:25
f is_measurable_on A implies max+(f) is_measurable_on A;
theorem :: MESFUNC2:26
f is_measurable_on A & A c= dom f implies max-(f) is_measurable_on A;
theorem :: MESFUNC2:27
for f,A st f is_measurable_on A & A c= dom f holds |.f.| is_measurable_on A;
begin
definition
let A,X be set;
redefine func chi(A,X) -> PartFunc of X,ExtREAL;
end;
theorem :: MESFUNC2:28
chi(A,X) is real-valued;
theorem :: MESFUNC2:29
chi(A,X) is_measurable_on B;
begin :: Definition and measurability of simple function
registration
let X be set;
let S be SigmaField of X;
cluster disjoint_valued for FinSequence of S;
end;
definition
let X be set;
let S be SigmaField of X;
mode Finite_Sep_Sequence of S is disjoint_valued FinSequence of S;
end;
theorem :: MESFUNC2:30
for F being Function st F is Finite_Sep_Sequence of S holds
ex G being Sep_Sequence of S st union rng F = union rng G &
(for n st n in dom F holds F.n = G.n) &
for m st not m in dom F holds G.m = {};
theorem :: MESFUNC2:31
for F being Function st F is Finite_Sep_Sequence of S holds union rng F in S;
definition
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
pred f is_simple_func_in S means
:: MESFUNC2:def 4
f is real-valued &
ex F being Finite_Sep_Sequence of S st (dom f = union rng F &
for n being Nat,x,y being Element of X st
n in dom F & x in F.n & y in F.n holds f.x = f.y);
end;
theorem :: MESFUNC2:32
f is real-valued implies rng f is Subset of REAL;
theorem :: MESFUNC2:33
for F being Relation st F is Finite_Sep_Sequence of S holds
F|(Seg n) is Finite_Sep_Sequence of S;
theorem :: MESFUNC2:34
f is_simple_func_in S implies f is_measurable_on A;