:: Definitions and Basic Properties of Measurable Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 7, 2000
:: Copyright (c) 2000-2021 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, SUBSET_1, REAL_1, INT_1, RAT_1, ARYTM_1, CARD_1,
XBOOLE_0, TARSKI, FUNCT_1, FUNCT_2, RELAT_1, NAT_1, ARYTM_3, ZFMISC_1,
CARD_3, ORDINAL1, PARTFUN1, XXREAL_0, VALUED_1, SUPINF_2, SUPINF_1,
COMPLEX1, PROB_1, VALUED_0, SETFAM_1, MESFUNC1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XXREAL_3, XCMPLX_0, XREAL_0, MEASURE6, REAL_1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, INT_1, NAT_1, RAT_1, CARD_3, XXREAL_0, VALUED_0,
PROB_1, SUPINF_1, SUPINF_2, MEASURE2, MEASURE3, EXTREAL1, RELSET_2;
constructors WELLORD2, REAL_1, NAT_1, RAT_1, MEASURE3, MEASURE6, EXTREAL1,
SUPINF_1, RELSET_2, PARTFUN1, EQREL_1, RELAT_2, RELSET_1, BINOP_2,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, MEASURE1, VALUED_0, XXREAL_3,
FUNCT_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin :: Cardinal numbers of INT and RAT
reserve k for Element of NAT;
reserve r,r1 for Real;
reserve i for Integer;
reserve q for Rational;
definition
func INT- -> Subset of REAL means
:: MESFUNC1:def 1
r in it iff ex k st r = - k;
end;
registration
cluster INT- -> non empty;
end;
theorem :: MESFUNC1:1
NAT,INT- are_equipotent;
theorem :: MESFUNC1:2
INT=INT- \/ NAT;
theorem :: MESFUNC1:3
NAT,INT are_equipotent;
definition
let n be Nat;
func RAT_with_denominator n -> Subset of RAT means
:: MESFUNC1:def 2
q in it iff ex i st q = i/n;
end;
registration
let n be Nat;
cluster RAT_with_denominator(n+1) -> non empty;
end;
theorem :: MESFUNC1:4
for n being Nat holds INT,RAT_with_denominator (n+1) are_equipotent;
theorem :: MESFUNC1:5
NAT,RAT are_equipotent;
begin :: Basic operations on R_EAL valued functions
definition
let C be non empty set;
let f1,f2 be C-defined ExtREAL-valued Function;
func f1+f2 -> PartFunc of C,ExtREAL means
:: MESFUNC1:def 3
dom it = (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty}) \/ (f1"{+infty} /\
f2"{-infty}))
& for c being Element of C st c in dom it holds it.c = f1.c + f2.c;
commutativity;
func f1-f2 -> PartFunc of C,ExtREAL means
:: MESFUNC1:def 4
dom it = (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty}) \/ (f1"{-infty} /\
f2"{-infty}))
& for c being Element of C st c in dom it holds it.c = f1.c - f2.c;
func f1(#)f2 -> PartFunc of C,ExtREAL means
:: MESFUNC1:def 5
dom it = dom f1 /\ dom f2
& for c being Element of C st c in dom it holds it.c = f1.c * f2.c;
commutativity;
end;
definition
let C be non empty set,
f be C-defined ExtREAL-valued Function,
r be Real;
func r(#)f -> PartFunc of C,ExtREAL means
:: MESFUNC1:def 6
dom it = dom f
& for c being Element of C st c in dom it holds it.c = r * f.c;
end;
theorem :: MESFUNC1:6
for C being non empty set, f being PartFunc of C,ExtREAL, r
st r <> 0 holds
for c being Element of C st c in dom(r(#)f) holds f.c = (r(#)f).c / r;
definition
let C be non empty set;
let f be C-defined ExtREAL-valued Function;
func -f -> PartFunc of C,ExtREAL means
:: MESFUNC1:def 7
dom it = dom f & for c being Element of C st c in dom it holds it.c = -(f.c);
end;
::$CD
definition
let C be non empty set;
let f be C-defined ExtREAL-valued Function;
let r be Real;
func r/f -> PartFunc of C,ExtREAL means
:: MESFUNC1:def 9
dom it = dom f \ f"{0.} &
for c being Element of C st c in dom it holds it.c = r/(f.c);
end;
theorem :: MESFUNC1:7
for C being non empty set, f being PartFunc of C,ExtREAL holds
dom (1/f) = dom f \ f"{0.} &
for c being Element of C st c in dom (1/f) holds (1/f).c = 1./(f.c);
definition
let C be non empty set;
let f be C-defined ExtREAL-valued Function;
func |.f.| -> PartFunc of C,ExtREAL means
:: MESFUNC1:def 10
dom it = dom f &
for c being Element of C st c in dom it holds it.c = |. f.c .|;
end;
begin :: Level sets
theorem :: MESFUNC1:8
ex n being Element of NAT st r <= n;
theorem :: MESFUNC1:9
ex n being Nat st -n <= r;
theorem :: MESFUNC1:10
for r,s being Real st r < s holds
ex n being Element of NAT st 1/(n+1) < s-r;
theorem :: MESFUNC1:11
for r,s being Real st for n being Element of NAT
holds r-1/(n+1) <= s holds r <= s;
theorem :: MESFUNC1:12
for a being R_eal st for r being Real holds r < a
holds a = +infty;
theorem :: MESFUNC1:13
for a being R_eal st for r being Real holds a < r
holds a = -infty;
reserve X for set;
reserve f for PartFunc of X,ExtREAL;
reserve S for SigmaField of X;
reserve F for sequence of S;
reserve A for set;
reserve a for ExtReal;
reserve r,s for Real;
reserve n,m for Element of NAT;
notation
let f be ext-real-valued Function, a be ExtReal;
synonym eq_dom(f,a) for Coim(f,a);
end;
definition
let f be ext-real-valued Function, a be ExtReal;
func less_dom(f,a) -> set means
:: MESFUNC1:def 11
for x being object holds x in it iff x in dom f & f.x < a;
func less_eq_dom(f,a) -> set means
:: MESFUNC1:def 12
for x being object holds x in it iff x in dom f & f.x <= a;
func great_dom(f,a) -> set means
:: MESFUNC1:def 13
for x being object holds x in it iff x in dom f & a < f.x;
func great_eq_dom(f,a) -> set means
:: MESFUNC1:def 14
for x being object holds x in it iff x in dom f & a <= f.x;
redefine func eq_dom(f,a) means
:: MESFUNC1:def 15
for x being set holds x in it iff x in dom f & f.x = a;
end;
definition
let X be set, f be PartFunc of X,ExtREAL, a be ExtReal;
redefine func less_dom(f,a) -> Subset of X;
redefine func less_eq_dom(f,a) -> Subset of X;
redefine func great_dom(f,a) -> Subset of X;
redefine func great_eq_dom(f,a) -> Subset of X;
redefine func eq_dom(f,a) -> Subset of X;
end;
theorem :: MESFUNC1:14
A c= dom f implies A /\ great_eq_dom(f,a) = A\(A /\ less_dom(f,a));
theorem :: MESFUNC1:15
A c= dom f implies A /\ great_dom(f,a) = A\(A /\ less_eq_dom(f,a));
theorem :: MESFUNC1:16
A c= dom f implies A /\ less_eq_dom(f,a) = A\(A /\ great_dom(f,a));
theorem :: MESFUNC1:17
A c= dom f implies A /\ less_dom(f,a) = A\(A /\ great_eq_dom(f,a));
theorem :: MESFUNC1:18
A /\ eq_dom(f,a) = A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a);
theorem :: MESFUNC1:19
for X, S, F, f, A, r st for n holds F.n = A /\ great_dom(f,(r-1/(n+1)))
holds A /\ great_eq_dom(f,r) = meet rng F;
theorem :: MESFUNC1:20
for r being Real st for n holds F.n = A /\ less_dom(f,(r+1/(n+1)))
holds A /\ less_eq_dom(f,r) = meet rng F;
theorem :: MESFUNC1:21
for r being Real st for n
holds F.n = A /\ less_eq_dom(f,(r-1/(n+1)))
holds A /\ less_dom(f,r) = union rng F;
theorem :: MESFUNC1:22
for X, S, F, f, A, r st for n holds F.n = A /\
great_eq_dom(f,(r+1/(n+1)))
holds A /\ great_dom(f,r) = union rng F;
theorem :: MESFUNC1:23
for X, S, F, f, A st for n holds F.n = A /\ great_dom(f,n)
holds A /\ eq_dom(f,+infty) = meet rng F;
theorem :: MESFUNC1:24
for X, S, F, f, A st for n holds F.n = A /\ less_dom(f,n)
holds A /\ less_dom(f,+infty) = union rng F;
theorem :: MESFUNC1:25
for X, S, F, f, A st for n being Nat holds F.n = A /\ less_dom(f,(-n))
holds A /\ eq_dom(f,-infty) = meet rng F;
theorem :: MESFUNC1:26
for X, S, F, f, A st for n holds F.n = A /\ great_dom(f,(-n))
holds A /\ great_dom(f,-infty) = union rng F;
begin :: Measurable functions
definition
let X be non empty set;
let S be SigmaField of X;
let A be Element of S;
let f be PartFunc of X,ExtREAL;
attr f is A-measurable means
:: MESFUNC1:def 16
for r being Real holds A /\ less_dom(f,r) in S;
end;
reserve X for non empty set;
reserve x for Element of X;
reserve f,g for PartFunc of X,ExtREAL;
reserve S for SigmaField of X;
reserve A,B for Element of S;
theorem :: MESFUNC1:27
for X,S,f,A st A c= dom f holds f is A-measurable iff
for r being Real holds A /\ great_eq_dom(f,r) in S;
theorem :: MESFUNC1:28
for X,S,f,A holds f is A-measurable iff
for r being Real holds A /\ less_eq_dom(f,r) in S;
theorem :: MESFUNC1:29
for X,S,f,A st A c= dom f holds f is A-measurable iff
for r being Real holds A /\ great_dom(f,r) in S;
theorem :: MESFUNC1:30
for X,S,f,A,B st B c= A & f is A-measurable holds f is B-measurable;
theorem :: MESFUNC1:31
for X,S,f,A,B st f is A-measurable & f is B-measurable holds
f is (A \/ B)-measurable;
theorem :: MESFUNC1:32
for X,S,f,A,r,s st f is A-measurable & A c= dom f holds
(A /\ great_dom(f,r) /\ less_dom(f,s)) in S;
theorem :: MESFUNC1:33
for X,S,f,A st f is A-measurable & A c= dom f holds
A /\ eq_dom(f,+infty) in S;
theorem :: MESFUNC1:34
for X,S,f,A st f is A-measurable holds A /\ eq_dom(f,-infty) in S;
theorem :: MESFUNC1:35
for X,S,f,A st f is A-measurable & A c= dom f holds
A /\ great_dom(f,-infty) /\ less_dom(f,+infty) in S;
theorem :: MESFUNC1:36
for X,S,f,g,A,r st f is A-measurable & g is A-measurable & A c= dom g
holds A /\ less_dom(f,r) /\ great_dom(g,r) in S;
theorem :: MESFUNC1:37
for X,S,f,A,r st f is A-measurable & A c= dom f
holds r(#)f is A-measurable;