:: Properties of Caratheodory's Measure
:: by J\'ozef Bia{\l}as
::
:: Received June 25, 1992
:: Copyright (c) 1992-2017 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, SUPINF_1, PROB_1, XBOOLE_0, SETFAM_1, FUNCT_1, SUBSET_1,
TARSKI, RELAT_1, CARD_1, ARYTM_3, NAT_1, XXREAL_0, ZFMISC_1, MEASURE1,
SUPINF_2, VALUED_0, FUNCOP_1, XREAL_0, ARYTM_1, MEASURE3, MEASURE4;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, VALUED_0,
XCMPLX_0, FUNCOP_1, REAL_1, NAT_1, SETFAM_1, PROB_1, SUPINF_1, SUPINF_2,
MEASURE1, MEASURE3;
constructors ENUMSET1, PARTFUN1, REAL_1, NAT_1, PROB_2, MEASURE3, SUPINF_1,
FUNCOP_1, RELSET_1, XREAL_0;
registrations SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEASURE1, VALUED_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Some theorems about R_eal numbers
reserve
A,B,X for set,
S for SigmaField of X;
theorem :: MEASURE4:1
for S being non empty Subset-Family of X, F, G being sequence of S,
A being Element of S st for n being Element of NAT holds G.n = A /\ F.n
holds union rng G = A /\ union rng F;
theorem :: MEASURE4:2
for S being non empty Subset-Family of X for F, G being sequence of S
st (G.0 = F.0 & for n being Nat holds G.(n+1) = F.(n+1) \/
G.n) holds for H being sequence of S st (H.0 = F.0 & for n being Nat
holds H.(n+1) = F.(n+1) \ G.n) holds union rng F = union rng H;
theorem :: MEASURE4:3
bool X is SigmaField of X;
definition
let X be set;
mode C_Measure of X -> Function of bool X,ExtREAL means
:: MEASURE4:def 1
it is
nonnegative zeroed & for A,B being Subset of X st A c= B holds it.A <= it.B &
for F being sequence of bool X holds it.(union rng F) <= SUM(it*F);
end;
reserve C for C_Measure of X;
definition
let X be set;
let C be C_Measure of X;
func sigma_Field(C) -> non empty Subset-Family of X means
:: MEASURE4:def 2
for A being
Subset of X holds (A in it iff for W,Z being Subset of X holds (W c= A & Z c= X
\ A implies C.W + C.Z <= C.(W \/ Z)));
end;
theorem :: MEASURE4:4
for W,Z being Subset of X holds C.(W \/ Z) <= C.W + C.Z;
theorem :: MEASURE4:5
for A being Subset of X holds (A in sigma_Field(C) iff for W,Z
being Subset of X holds (W c= A & Z c= X \ A implies C.W + C.Z = C.(W \/ Z)))
;
theorem :: MEASURE4:6
for W,Z being Subset of X holds W in sigma_Field(C) & Z misses W
implies C.(W \/ Z) = C.W + C.Z;
theorem :: MEASURE4:7
A in sigma_Field(C) implies X \ A in sigma_Field(C);
theorem :: MEASURE4:8
A in sigma_Field(C) & B in sigma_Field(C) implies A \/ B in sigma_Field(C);
theorem :: MEASURE4:9
A in sigma_Field(C) & B in sigma_Field(C) implies A /\ B in sigma_Field(C);
theorem :: MEASURE4:10
A in sigma_Field(C) & B in sigma_Field(C) implies A \ B in sigma_Field(C);
theorem :: MEASURE4:11
for N being sequence of S holds for A being Element of S
holds ex F being sequence of S st for n being Element of NAT holds F.n = A
/\ N.n;
theorem :: MEASURE4:12
sigma_Field(C) is SigmaField of X;
registration
let X be set;
let C be C_Measure of X;
cluster sigma_Field(C) -> sigma-additive compl-closed non empty;
end;
definition
let X be set;
let S be SigmaField of X;
let A be N_Sub_fam of S;
redefine func union A -> Element of S;
end;
definition
let X be set;
let C be C_Measure of X;
func sigma_Meas(C) -> Function of sigma_Field(C),ExtREAL means
:: MEASURE4:def 3
for A being Subset of X st A in sigma_Field(C) holds it.A = C.A;
end;
theorem :: MEASURE4:13
sigma_Meas(C) is Measure of sigma_Field(C);
::$N Caratheodory's Theorem
theorem :: MEASURE4:14
sigma_Meas(C) is sigma_Measure of sigma_Field(C);
registration
let X be set;
let C be C_Measure of X;
cluster sigma_Meas(C) -> nonnegative sigma-additive zeroed;
end;
theorem :: MEASURE4:15
for A being Subset of X holds C.A = 0. implies A in sigma_Field(C);
theorem :: MEASURE4:16
sigma_Meas(C) is_complete sigma_Field(C);