:: Several Properties of the $\sigma$-additive Measure
:: by J\'ozef Bia{\l}as
::
:: Received July 3, 1991
:: Copyright (c) 1991-2019 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 PROB_1, MEASURE1, FUNCT_1, NUMBERS, RELAT_1, SUPINF_2, TARSKI,
XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ARYTM_3, XXREAL_0, NAT_1, ZFMISC_1,
VALUED_0, ORDINAL2, MEASURE2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
XCMPLX_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, PROB_1,
SUPINF_2, MEASURE1;
constructors PARTFUN1, NAT_1, PROB_2, MEASURE1, SUPINF_1, XREAL_0, RELSET_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0,
MEASURE1, MEMBERED, RELSET_1, NAT_1, XCMPLX_0;
requirements NUMERALS, SUBSET, BOOLE;
begin
::
:: Some useful theorems about measures and functions
::
reserve X for set;
theorem :: MEASURE2:1
for S being SigmaField of X, M being sigma_Measure of S, F being
sequence of S holds M*F is nonnegative;
definition
let X be set;
let S be SigmaField of X;
mode N_Measure_fam of S -> N_Sub_set_fam of X means
:: MEASURE2:def 1
it c= S;
end;
theorem :: MEASURE2:2
for S being SigmaField of X, T being N_Measure_fam of S holds
meet T in S & union T in S;
definition
let X be set, S be SigmaField of X, T be N_Measure_fam of S;
redefine func meet T -> Element of S;
redefine func union T -> Element of S;
end;
theorem :: MEASURE2:3
for S being SigmaField of X, N being sequence of S holds ex F
being sequence of S st F.0 = N.0 & for n being Nat holds F.(n+1)
= N.(n+1) \ N.n;
theorem :: MEASURE2:4
for S being SigmaField of X, N being sequence of S holds ex F
being sequence of S st F.0 = N.0 & for n being Nat holds F.(n+1)
= N.(n+1) \/ F.n;
theorem :: MEASURE2:5
for S being non empty Subset-Family of X, N,F being sequence of S
holds F.0 = N.0 & (for n being Nat holds F.(n+1) = N.(n+1) \/
F.n) implies for r being set for n being Nat holds (r in F.n iff ex
k being Nat st k <= n & r in N.k);
theorem :: MEASURE2:6
for S being non empty Subset-Family of X, N,F being sequence of S holds
(F.0 = N.0 & (for n being Nat holds F.(n+1) = N.(n+1) \/
F.n) implies for n,m being Nat st n < m holds F.n c= F.m);
theorem :: MEASURE2:7
for S being non empty Subset-Family of X, N, G, F being sequence of S holds
G.0 = N.0 & (for n being Nat holds G.(n+1) = N.(n+1)
\/ G.n) & F.0 = N.0 & (for n being Nat holds F.(n+1) = N.(n+1) \ G.n
) implies for n,m being Nat st n <= m holds F.n c= G.m;
theorem :: MEASURE2:8
for S being SigmaField of X holds for N, G being sequence of
S holds ex F being sequence of S st F.0 = N.0 & for n being Nat
holds F.(n+1) = N.(n+1) \ G.n;
theorem :: MEASURE2:9
for S being SigmaField of X holds for N being sequence of S holds
ex F being sequence of S st F.0 = {} & for n being Nat holds F.(
n+1) = N.0 \ N.n;
theorem :: MEASURE2:10
for S being SigmaField of X holds for N, G, F being sequence of S holds
G.0 = N.0 & (for n being Nat holds G.(n+1) = N.(n+1) \/
G.n) & F.0 = N.0 & (for n being Nat holds F.(n+1) = N.(n+1) \ G.n)
implies for n,m being Nat st n < m holds F.n misses F.m;
theorem :: MEASURE2:11
for S being SigmaField of X, M being sigma_Measure of S, T being
N_Measure_fam of S, F being sequence of S st T = rng F holds M.(union T) <=
SUM(M*F);
theorem :: MEASURE2:12
for S being SigmaField of X, T being N_Measure_fam of S holds ex
F being sequence of S st T = rng F;
theorem :: MEASURE2:13
for N, F being Function st (F.0 = {} & for n being Nat
holds F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n )
for n being Nat holds F.n c= F.(n+1);
theorem :: MEASURE2:14
for S being SigmaField of X, M being sigma_Measure of S, T being
N_Measure_fam of S st (for A being set st A in T holds A is measure_zero of M)
holds union T is measure_zero of M;
theorem :: MEASURE2:15
for S being SigmaField of X, M being sigma_Measure of S, T being
N_Measure_fam of S st (ex A being set st A in T & A is measure_zero of M) holds
meet T is measure_zero of M;
theorem :: MEASURE2:16
for S being SigmaField of X, M being sigma_Measure of S, T being
N_Measure_fam of S st (for A being set st A in T holds A is measure_zero of M)
holds meet T is measure_zero of M;
definition
let X be set;
let S be SigmaField of X;
let IT be N_Measure_fam of S;
attr IT is non-decreasing means
:: MEASURE2:def 2
ex F being sequence of S st IT =
rng F & for n being Nat holds F.n c= F.(n+1);
end;
registration
let X be set;
let S be SigmaField of X;
cluster non-decreasing for N_Measure_fam of S;
end;
definition
let X be set;
let S be SigmaField of X;
let IT be N_Measure_fam of S;
attr IT is non-increasing means
:: MEASURE2:def 3
ex F being sequence of S st IT = rng F &
for n being Element of NAT holds F.(n+1) c= F.n;
end;
registration
let X be set;
let S be SigmaField of X;
cluster non-increasing for N_Measure_fam of S;
end;
theorem :: MEASURE2:17
for S being SigmaField of X, N,F being sequence of S holds (F.0 =
{} & for n being Nat holds F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n )
implies rng F is non-decreasing N_Measure_fam of S;
theorem :: MEASURE2:18
for N being Function st (for n being Nat holds N.n c=
N.(n+1)) holds for m,n being Nat st n <= m holds N.n c= N.m;
theorem :: MEASURE2:19
for N,F being Function st (F.0 = N.0 & for n being Nat
holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1))
for n,m being Nat st n < m holds F.n misses F.m;
theorem :: MEASURE2:20
for S being SigmaField of X, N,F being sequence of S holds (
F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \ N.n & N.n c= N
.(n+1) ) implies union rng F = union rng N;
theorem :: MEASURE2:21
for S being SigmaField of X, N,F being sequence of S holds (
F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \ N.n & N.n c= N
.(n+1) ) implies F is Sep_Sequence of S;
theorem :: MEASURE2:22
for S being SigmaField of X, N,F being sequence of S holds (F.0 =
N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)
) implies (N.0 = F.0 & for n being Element of NAT holds N.(n+1) = F.(n+1) \/ N.
n);
theorem :: MEASURE2:23
for S being SigmaField of X, M being sigma_Measure of S, F being
sequence of S st (for n being Nat holds F.n c= F.(n+1)) holds M.
(union rng F) = sup(rng (M*F));