:: Fubini's Theorem on Measure
:: by Noboru Endou
::
:: Received February 23, 2017
:: Copyright (c) 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, XXREAL_0, SUBSET_1, CARD_1, ARYTM_3, ARYTM_1, RELAT_1,
NAT_1, REAL_1, CARD_3, FUNCT_1, FINSEQ_1, XBOOLE_0, TARSKI, ZFMISC_1,
ORDINAL4, PROB_1, FINSUB_1, SETFAM_1, PROB_2, MEASURE9, FUNCOP_1,
SUPINF_2, VALUED_0, FUNCT_2, PARTFUN1, MEASURE1, ORDINAL2, SERIES_1,
MESFUNC5, SEQ_2, SEQFUNC, PBOOLE, MESFUNC9, VALUED_1, MESFUNC1, SRINGS_3,
MEASUR10, MESFUNC8, FUNCT_3, MEASURE7, MEASURE4, MEASURE8, MEASUR11,
PROB_3, SEQM_3, EQREL_1, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XXREAL_3, XXREAL_0, XREAL_0,
NUMBERS, KURATO_0, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1, FINSUB_1, CARD_3, FUNCT_3, BINOP_1, XTUPLE_0, PROB_1,
PROB_3, NAT_1, VALUED_0, MEASURE8, FINSEQ_1, FINSEQOP, SUPINF_2, PROB_2,
SEQFUNC, MEASURE1, MESFUNC1, MEASURE3, MEASURE4, MESFUNC2, MESFUNC5,
MESFUNC8, DBLSEQ_3, MESFUNC9, EXTREAL1, SRINGS_3, MEASURE9, MEASUR10,
SETLIM_1, SETLIM_2, MCART_1;
constructors SEQFUNC, PROB_3, FINSEQOP, MEASURE3, MESFUNC8, MESFUNC9,
EXTREAL1, RINFSUP2, MEASUR10, SETLIM_1, SUPINF_1, MEASURE8, MESFUNC2,
KURATO_0, SETLIM_2, DBLSEQ_3;
registrations ORDINAL1, XBOOLE_0, RELAT_1, SUBSET_1, ROUGHS_1, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, FUNCT_1, FINSEQ_1, FUNCT_2, NUMBERS,
VALUED_0, MESFUNC9, RELSET_1, MEASURE1, PARTFUN1, XXREAL_3, CARD_1,
SIMPLEX0, SRINGS_3, DBLSEQ_3, MEASURE4, MEASURE9, PROB_1, MEASUR10;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Preliminaries
theorem :: MEASUR11:1
for F be disjoint_valued FinSequence, n,m be Nat
st n < m holds union rng(F|n) misses F.m;
theorem :: MEASUR11:2
for F be FinSequence, m,n be Nat st m <= n holds len(F|m) <= len(F|n);
theorem :: MEASUR11:3
for F be FinSequence, n be Nat holds
union rng(F|n) \/ F.(n+1) = union rng(F|(n+1));
theorem :: MEASUR11:4
for F be disjoint_valued FinSequence, n be Nat holds
Union(F|n) misses F.(n+1);
theorem :: MEASUR11:5
for P be set, F be FinSequence st
P is cup-closed & {} in P & (for n be Nat st n in dom F holds F.n in P)
holds Union F in P;
definition
let A,X be set;
redefine func chi(A,X) -> Function of X,ExtREAL;
end;
definition
let X be non empty set, S be SigmaField of X, F be FinSequence of S;
redefine func Union F -> Element of S;
end;
definition
let X be non empty set, S be SigmaField of X, F be sequence of S;
redefine func Union F -> Element of S;
end;
definition
let X be non empty set;
let F be FinSequence of PFuncs(X,ExtREAL);
let x be Element of X;
func F#x -> FinSequence of ExtREAL means
:: MEASUR11:def 1
dom it = dom F & (for n be Element of NAT st n in dom it holds
it.n = (F.n).x);
end;
theorem :: MEASUR11:6
for X be non empty set, S be non empty Subset-Family of X,
f be FinSequence of S, F be FinSequence of PFuncs(X,ExtREAL) st
dom f = dom F & f is disjoint_valued
& (for n be Nat st n in dom F holds F.n = chi(f.n,X))
holds (for x be Element of X holds chi(Union f,X).x = Sum (F#x));
begin :: Product measure and product sigma measure
theorem :: MEASUR11:7
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2
holds
sigma DisUnion measurable_rectangles(S1,S2)
= sigma measurable_rectangles(S1,S2);
definition
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2;
func product_Measure(M1,M2) ->
induced_Measure of measurable_rectangles(S1,S2),
product-pre-Measure(M1,M2) means
:: MEASUR11:def 2
for E be set st E in Field_generated_by measurable_rectangles(S1,S2) holds
for F be disjoint_valued FinSequence of measurable_rectangles(S1,S2)
st E = Union F holds it.E = Sum(product-pre-Measure(M1,M2)*F);
end;
definition
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2;
func product_sigma_Measure(M1,M2) ->
induced_sigma_Measure of measurable_rectangles(S1,S2),
product_Measure(M1,M2) equals
:: MEASUR11:def 3
(sigma_Meas(C_Meas product_Measure(M1,M2)))
|(sigma measurable_rectangles(S1,S2));
end;
theorem :: MEASUR11:8
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2 holds
product_sigma_Measure(M1,M2) is
sigma_Measure of sigma measurable_rectangles(S1,S2);
theorem :: MEASUR11:9
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
F1 be Set_Sequence of S1, F2 be Set_Sequence of S2, n be Nat holds
[:F1.n,F2.n:] is Element of sigma measurable_rectangles(S1,S2);
theorem :: MEASUR11:10
for X1,X2 be set, F1 be SetSequence of X1, F2 be SetSequence of X2, n be Nat
st F1 is non-descending & F2 is non-descending
holds [:F1.n,F2.n:] c= [:F1.(n+1),F2.(n+1):];
theorem :: MEASUR11:11
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
A be Element of S1, B be Element of S2 holds
product_Measure(M1,M2).([:A,B:]) = M1.A * M2.B;
theorem :: MEASUR11:12
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
F1 be Set_Sequence of S1, F2 be Set_Sequence of S2, n be Nat holds
product_Measure(M1,M2).([:F1.n,F2.n:]) = M1.(F1.n) * M2.(F2.n);
theorem :: MEASUR11:13
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
F1 be FinSequence of S1, F2 be FinSequence of S2, n be Nat
st n in dom F1 & n in dom F2 holds
product_Measure(M1,M2).([:F1.n,F2.n:]) = M1.(F1.n) * M2.(F2.n);
theorem :: MEASUR11:14
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Subset of [:X1,X2:] holds
(C_Meas product_Measure(M1,M2)).E = inf(Svc(product_Measure(M1,M2),E));
theorem :: MEASUR11:15
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2 holds
sigma measurable_rectangles(S1,S2)
c= sigma_Field(C_Meas product_Measure(M1,M2));
theorem :: MEASUR11:16
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st E = [:A,B:] holds product_sigma_Measure(M1,M2).E = M1.A * M2.B;
theorem :: MEASUR11:17
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
F1 be Set_Sequence of S1, F2 be Set_Sequence of S2, n be Nat holds
product_sigma_Measure(M1,M2).([:F1.n,F2.n:]) = M1.(F1.n) * M2.(F2.n);
theorem :: MEASUR11:18
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E1,E2 be Element of sigma measurable_rectangles(S1,S2)
st E1 misses E2 holds
product_sigma_Measure(M1,M2).(E1 \/ E2)
= product_sigma_Measure(M1,M2).E1 + product_sigma_Measure(M1,M2).E2;
theorem :: MEASUR11:19
for X1,X2,A,B be set, F1 be SetSequence of X1, F2 be SetSequence of X2,
F be SetSequence of [:X1,X2:] st
F1 is non-descending & lim F1 = A & F2 is non-descending & lim F2 = B &
(for n be Nat holds F.n = [:F1.n,F2.n:])
holds lim F = [:A,B:];
begin :: Sections
definition
let X be set, Y be non empty set, E be Subset of [:X,Y:], x be set;
func X-section(E,x) -> Subset of Y equals
:: MEASUR11:def 4
{y where y is Element of Y: [x,y] in E};
end;
definition
let X be non empty set, Y be set, E be Subset of [:X,Y:], y be set;
func Y-section(E,y) -> Subset of X equals
:: MEASUR11:def 5
{x where x is Element of X: [x,y] in E};
end;
theorem :: MEASUR11:20
for X be set, Y be non empty set, E1,E2 be Subset of [:X,Y:], p be set
st E1 c= E2 holds X-section(E1,p) c= X-section(E2,p);
theorem :: MEASUR11:21
for X be non empty set, Y be set, E1,E2 be Subset of [:X,Y:], p be set
st E1 c= E2 holds Y-section(E1,p) c= Y-section(E2,p);
theorem :: MEASUR11:22
for X,Y be non empty set, A be Subset of X, B be Subset of Y, p be set
holds
(p in A implies X-section([:A,B:],p) = B)
& (not p in A implies X-section([:A,B:],p) = {})
& (p in B implies Y-section([:A,B:],p) = A)
& (not p in B implies Y-section([:A,B:],p) = {});
theorem :: MEASUR11:23
for X,Y be non empty set, E be Subset of [:X,Y:], p be set holds
( not p in X implies X-section(E,p) = {} )
& ( not p in Y implies Y-section(E,p) = {} );
theorem :: MEASUR11:24
for X,Y be non empty set, p be set holds
X-section({}[:X,Y:],p) = {} & Y-section({}[:X,Y:],p) = {}
& ( p in X implies X-section([#][:X,Y:],p) = Y )
& ( p in Y implies Y-section([#][:X,Y:],p) = X );
theorem :: MEASUR11:25
for X,Y be non empty set, E be Subset of [:X,Y:], p be set holds
( p in X implies X-section([:X,Y:] \ E,p) = Y \ X-section(E,p) )
& ( p in Y implies Y-section([:X,Y:] \ E,p) = X \ Y-section(E,p) );
theorem :: MEASUR11:26
for X,Y be non empty set, E1,E2 be Subset of [:X,Y:], p be set holds
X-section(E1\/E2,p) = X-section(E1,p) \/ X-section(E2,p)
& Y-section(E1\/E2,p) = Y-section(E1,p) \/ Y-section(E2,p);
theorem :: MEASUR11:27
for X,Y be non empty set, E1,E2 be Subset of [:X,Y:], p be set holds
X-section(E1/\E2,p) = X-section(E1,p) /\ X-section(E2,p)
& Y-section(E1/\E2,p) = Y-section(E1,p) /\ Y-section(E2,p);
theorem :: MEASUR11:28
for X be set, Y be non empty set, F be FinSequence of bool [:X,Y:],
Fy be FinSequence of bool Y, p be set st
dom F = dom Fy
& ( for n be Nat st n in dom Fy holds Fy.n = X-section(F.n,p) )
holds X-section(union rng F,p) = union rng Fy;
theorem :: MEASUR11:29
for X be non empty set, Y be set, F be FinSequence of bool [:X,Y:],
Fx be FinSequence of bool X, p be set st
dom F = dom Fx
& ( for n be Nat st n in dom Fx holds Fx.n = Y-section(F.n,p) )
holds Y-section(union rng F,p) = union rng Fx;
theorem :: MEASUR11:30
for X be set, Y be non empty set, p be set, F be SetSequence of [:X,Y:],
Fy be SetSequence of Y st
( for n be Nat holds Fy.n = X-section(F.n,p) )
holds X-section(union rng F,p) = union rng Fy;
theorem :: MEASUR11:31
for X be set, Y be non empty set, p be set, F be SetSequence of [:X,Y:],
Fy be SetSequence of Y st
( for n be Nat holds Fy.n = X-section(F.n,p) )
holds X-section(meet rng F,p) = meet rng Fy;
theorem :: MEASUR11:32
for X be non empty set, Y be set, p be set, F be SetSequence of [:X,Y:],
Fx be SetSequence of X st
( for n be Nat holds Fx.n = Y-section(F.n,p) )
holds Y-section(union rng F,p) = union rng Fx;
theorem :: MEASUR11:33
for X be non empty set, Y be set, p be set, F be SetSequence of [:X,Y:],
Fx be SetSequence of X st
( for n be Nat holds Fx.n = Y-section(F.n,p) )
holds Y-section(meet rng F,p) = meet rng Fx;
theorem :: MEASUR11:34
for X,Y be non empty set, x,y be set, E be Subset of [:X,Y:]
holds chi(E,[:X,Y:]).(x,y) = chi(X-section(E,x),Y).y &
chi(E,[:X,Y:]).(x,y) = chi(Y-section(E,y),X).x;
theorem :: MEASUR11:35
for X,Y be non empty set, E1,E2 be Subset of [:X,Y:], p be set
st E1 misses E2
holds X-section(E1,p) misses X-section(E2,p)
& Y-section(E1,p) misses Y-section(E2,p);
theorem :: MEASUR11:36
for X,Y be non empty set, F be disjoint_valued FinSequence of bool [:X,Y:],
p be set holds
( ex Fy be disjoint_valued FinSequence of bool X st
( dom F = dom Fy
& for n be Nat st n in dom Fy holds Fy.n = Y-section(F.n,p) ) )
&
( ex Fx be disjoint_valued FinSequence of bool Y st
( dom F = dom Fx
& for n be Nat st n in dom Fx holds Fx.n = X-section(F.n,p) ) );
theorem :: MEASUR11:37
for X,Y be non empty set, F be disjoint_valued SetSequence of [:X,Y:],
p be set holds
( ex Fy be disjoint_valued SetSequence of X st
(for n be Nat holds Fy.n = Y-section(F.n,p)) )
& ( ex Fx be disjoint_valued SetSequence of Y st
(for n be Nat holds Fx.n = X-section(F.n,p)) );
theorem :: MEASUR11:38
for X,Y be non empty set, x,y be set, E1,E2 be Subset of [:X,Y:]
st E1 misses E2 holds
chi(E1 \/ E2,[:X,Y:]).(x,y)
= chi(X-section(E1,x),Y).y + chi(X-section(E2,x),Y).y
& chi(E1 \/ E2,[:X,Y:]).(x,y)
= chi(Y-section(E1,y),X).x + chi(Y-section(E2,y),X).x;
theorem :: MEASUR11:39
for X be set, Y be non empty set, x be set, E be SetSequence of [:X,Y:],
G be SetSequence of Y
st E is non-descending & (for n be Nat holds G.n = X-section(E.n,x))
holds G is non-descending;
theorem :: MEASUR11:40
for X be non empty set, Y be set, x be set, E be SetSequence of [:X,Y:],
G be SetSequence of X
st E is non-descending & (for n be Nat holds G.n = Y-section(E.n,x))
holds G is non-descending;
theorem :: MEASUR11:41
for X be set, Y be non empty set, x be set, E be SetSequence of [:X,Y:],
G be SetSequence of Y
st E is non-ascending & (for n be Nat holds G.n = X-section(E.n,x))
holds G is non-ascending;
theorem :: MEASUR11:42
for X be non empty set, Y be set, x be set, E be SetSequence of [:X,Y:],
G be SetSequence of X
st E is non-ascending & (for n be Nat holds G.n = Y-section(E.n,x))
holds G is non-ascending;
theorem :: MEASUR11:43
for X be set, Y be non empty set, E be SetSequence of [:X,Y:], x be set
st E is non-descending
ex G be SetSequence of Y st G is non-descending
& (for n be Nat holds G.n = X-section(E.n,x));
theorem :: MEASUR11:44
for X be non empty set, Y be set, E be SetSequence of [:X,Y:], x be set
st E is non-descending
ex G be SetSequence of X st G is non-descending
& (for n be Nat holds G.n = Y-section(E.n,x));
theorem :: MEASUR11:45
for X be set, Y be non empty set, E be SetSequence of [:X,Y:], x be set
st E is non-ascending
ex G be SetSequence of Y st G is non-ascending
& (for n be Nat holds G.n = X-section(E.n,x));
theorem :: MEASUR11:46
for X be non empty set, Y be set, E be SetSequence of [:X,Y:], x be set
st E is non-ascending
ex G be SetSequence of X st G is non-ascending
& (for n be Nat holds G.n = Y-section(E.n,x));
begin :: Measurable sections
theorem :: MEASUR11:47
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
E be Element of sigma(measurable_rectangles(S1,S2)), K be set st
K = {C where C is Subset of [:X1,X2:] :
for p be set holds X-section(C,p) in S2}
holds Field_generated_by measurable_rectangles(S1,S2) c= K
& K is SigmaField of [:X1,X2:];
theorem :: MEASUR11:48
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
E be Element of sigma(measurable_rectangles(S1,S2)), K be set st
K = {C where C is Subset of [:X1,X2:] :
for p be set holds Y-section(C,p) in S1}
holds Field_generated_by measurable_rectangles(S1,S2) c= K
& K is SigmaField of [:X1,X2:];
theorem :: MEASUR11:49
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
E be Element of sigma(measurable_rectangles(S1,S2)) holds
( for p be set holds X-section(E,p) in S2 )
& ( for p be set holds Y-section(E,p) in S1 );
definition
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
E be Element of sigma(measurable_rectangles(S1,S2)), x be set;
func Measurable-X-section(E,x) -> Element of S2 equals
:: MEASUR11:def 6
X-section(E,x);
end;
definition
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
E be Element of sigma(measurable_rectangles(S1,S2)), y be set;
func Measurable-Y-section(E,y) -> Element of S1 equals
:: MEASUR11:def 7
Y-section(E,y);
end;
theorem :: MEASUR11:50
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
F be FinSequence of sigma measurable_rectangles(S1,S2),
Fy be FinSequence of S2, p be set st
dom F = dom Fy
& ( for n be Nat st n in dom Fy holds Fy.n = Measurable-X-section(F.n,p) )
holds Measurable-X-section(Union F,p) = Union Fy;
theorem :: MEASUR11:51
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
F be FinSequence of sigma measurable_rectangles(S1,S2),
Fx be FinSequence of S1, p be set st
dom F = dom Fx
& ( for n be Nat st n in dom Fx holds Fx.n = Measurable-Y-section(F.n,p) )
holds Measurable-Y-section(Union F,p) = Union Fx;
theorem :: MEASUR11:52
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2,
A be Element of S1, B be Element of S2, x be Element of X1 holds
M2.B * chi(A,X1).x = Integral(M2,ProjMap1(chi([:A,B:],[:X1,X2:]),x));
theorem :: MEASUR11:53
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2,
E be Element of sigma(measurable_rectangles(S1,S2)),
A be Element of S1, B be Element of S2, x be Element of X1
st E = [:A,B:] holds M2.(Measurable-X-section(E,x)) = M2.B * chi(A,X1).x;
theorem :: MEASUR11:54
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1,
A be Element of S1, B be Element of S2, y be Element of X2 holds
M1.A * chi(B,X2).y = Integral(M1,ProjMap2(chi([:A,B:],[:X1,X2:]),y));
theorem :: MEASUR11:55
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1,
E be Element of sigma(measurable_rectangles(S1,S2)),
A be Element of S1, B be Element of S2, y be Element of X2
st E = [:A,B:] holds M1.(Measurable-Y-section(E,y)) = M1.A * chi(B,X2).y;
begin :: Finite sequence of functions
definition
let X,Y be non empty set, G be FUNCTION_DOMAIN of X,Y,
F be FinSequence of G, n be Nat;
redefine func F/.n -> Element of G;
end;
definition
let X be set;
let F be FinSequence of Funcs(X,ExtREAL);
attr F is without_+infty-valued means
:: MEASUR11:def 8
for n be Nat st n in dom F holds F.n is without+infty;
attr F is without_-infty-valued means
:: MEASUR11:def 9
for n be Nat st n in dom F holds F.n is without-infty;
end;
theorem :: MEASUR11:56
for X be non empty set holds
<* X --> 0 *> is FinSequence of Funcs(X,ExtREAL) &
(for n be Nat st n in dom <* X --> 0 *>
holds <* X --> 0 *>.n is without+infty) &
(for n be Nat st n in dom <* X --> 0 *>
holds <* X --> 0 *>.n is without-infty);
registration
let X be non empty set;
cluster without_+infty-valued without_-infty-valued
for FinSequence of Funcs(X,ExtREAL);
end;
theorem :: MEASUR11:57
for X be non empty set, F be without_+infty-valued FinSequence of
Funcs(X,ExtREAL), n be Nat st n in dom F holds (F/.n)"{+infty} = {};
theorem :: MEASUR11:58
for X be non empty set, F be without_-infty-valued FinSequence of
Funcs(X,ExtREAL), n be Nat st n in dom F holds (F/.n)"{-infty} = {};
theorem :: MEASUR11:59
for X be non empty set, F be FinSequence of Funcs(X,ExtREAL) st
F is without_+infty-valued or F is without_-infty-valued holds
for n,m be Nat st n in dom F & m in dom F holds dom(F/.n + F/.m) = X;
definition
let X be non empty set;
let F be FinSequence of Funcs(X,ExtREAL);
attr F is summable means
:: MEASUR11:def 10
F is without_+infty-valued or F is without_-infty-valued;
end;
registration
let X be non empty set;
cluster summable for FinSequence of Funcs(X,ExtREAL);
end;
definition
let X be non empty set;
let F be summable FinSequence of Funcs(X,ExtREAL);
func Partial_Sums F -> FinSequence of Funcs(X,ExtREAL) means
:: MEASUR11:def 11
len F = len it & F.1 = it.1 &
(for n be Nat st 1 <= n < len F holds it.(n+1) = (it/.n) + (F/.(n+1)));
end;
registration
let X be non empty set;
cluster without_+infty-valued -> summable for FinSequence of Funcs(X,ExtREAL);
cluster without_-infty-valued -> summable for FinSequence of Funcs(X,ExtREAL);
end;
theorem :: MEASUR11:60
for X be non empty set, F be without_+infty-valued FinSequence
of Funcs(X,ExtREAL) holds Partial_Sums F is without_+infty-valued;
theorem :: MEASUR11:61
for X be non empty set, F be without_-infty-valued FinSequence
of Funcs(X,ExtREAL) holds Partial_Sums F is without_-infty-valued;
theorem :: MEASUR11:62
for X be non empty set, A be set, er be ExtReal, f be Function of X,ExtREAL st
(for x be Element of X holds f.x = er * chi(A,X).x)
holds (er = +infty implies f = Xchi(A,X)) &
(er = -infty implies f = -Xchi(A,X)) &
(er <> +infty & er <> -infty implies
ex r be Real st r = er & f = r(#)chi(A,X));
theorem :: MEASUR11:63
for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL,
A be Element of S st f is_measurable_on A & A c= dom f holds
-f is_measurable_on A;
registration
let X be non empty set, f be without-infty PartFunc of X,ExtREAL;
cluster -f -> without+infty;
end;
registration
let X be non empty set, f be without+infty PartFunc of X,ExtREAL;
cluster -f -> without-infty;
end;
definition
let X be non empty set;
let f1,f2 be without+infty PartFunc of X,ExtREAL;
redefine func f1+f2 -> without+infty PartFunc of X,ExtREAL;
end;
definition
let X be non empty set;
let f1,f2 be without-infty PartFunc of X,ExtREAL;
redefine func f1+f2 -> without-infty PartFunc of X,ExtREAL;
end;
definition
let X be non empty set;
let f1 be without+infty PartFunc of X,ExtREAL;
let f2 be without-infty PartFunc of X,ExtREAL;
redefine func f1-f2 -> without+infty PartFunc of X,ExtREAL;
end;
definition
let X be non empty set;
let f1 be without-infty PartFunc of X,ExtREAL;
let f2 be without+infty PartFunc of X,ExtREAL;
redefine func f1-f2 -> without-infty PartFunc of X,ExtREAL;
end;
theorem :: MEASUR11:64
for X be non empty set, f,g be PartFunc of X,ExtREAL
holds -(f+g) = (-f) + (-g) & -(f-g) = (-f) + g
& -(f-g) = g - f & -(-f+g) = f - g & -(-f+g) = f + (-g);
theorem :: MEASUR11:65
for X be non empty set, S be SigmaField of X,
f,g be without+infty PartFunc of X,ExtREAL, A be Element of S st
f is_measurable_on A & g is_measurable_on A & A c= dom (f+g) holds
f+g is_measurable_on A;
theorem :: MEASUR11:66
for X be non empty set, S be SigmaField of X, A be Element of S,
f be without+infty PartFunc of X,ExtREAL,
g be without-infty PartFunc of X,ExtREAL
st f is_measurable_on A & g is_measurable_on A & A c= dom(f-g) holds
f-g is_measurable_on A;
theorem :: MEASUR11:67
for X be non empty set, S be SigmaField of X, A be Element of S,
f be without-infty PartFunc of X,ExtREAL,
g be without+infty PartFunc of X,ExtREAL
st f is_measurable_on A & g is_measurable_on A & A c= dom(f-g) holds
f-g is_measurable_on A;
theorem :: MEASUR11:68
for X be non empty set, S be SigmaField of X, P be Element of S,
F be summable FinSequence of Funcs(X,ExtREAL)
st (for n be Nat st n in dom F holds F/.n is_measurable_on P) holds
for n be Nat st n in dom F holds (Partial_Sums F)/.n is_measurable_on P;
begin :: Some properties of integral
theorem :: MEASUR11:69
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2,
x be Element of X1, y be Element of X2
st E = [:A,B:] holds
Integral(M2,ProjMap1(chi(E,[:X1,X2:]),x))
= M2.(Measurable-X-section(E,x)) * chi(A,X1).x
& Integral(M1,ProjMap2(chi(E,[:X1,X2:]),y))
= M1.(Measurable-Y-section(E,y)) * chi(B,X2).y;
theorem :: MEASUR11:70
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
E be Element of sigma measurable_rectangles(S1,S2)
st E in Field_generated_by measurable_rectangles(S1,S2)
ex f be disjoint_valued FinSequence of measurable_rectangles(S1,S2),
A be FinSequence of S1, B be FinSequence of S2 st
len f = len A & len f = len B & E = Union f
& (for n be Nat st n in dom f holds proj1(f.n) = A.n & proj2(f.n) = B.n)
& (for n be Nat, x,y be set st n in dom f & x in X1 & y in X2 holds
chi(f.n,[:X1,X2:]).(x,y) = chi(A.n,X1).x * chi(B.n,X2).y);
theorem :: MEASUR11:71
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2),
x be Element of X1, y be Element of X2,
U be Element of S1, V be Element of S2
holds
M1.(Measurable-Y-section(E,y) /\ U)
= Integral(M1,ProjMap2(chi(E /\ [:U,X2:],[:X1,X2:]),y))
& M2.(Measurable-X-section(E,x) /\ V)
= Integral(M2,ProjMap1(chi(E /\ [:X1,V:],[:X1,X2:]),x));
theorem :: MEASUR11:72
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2),
x be Element of X1, y be Element of X2
holds
M1.(Measurable-Y-section(E,y)) = Integral(M1,ProjMap2(chi(E,[:X1,X2:]),y))
& M2.(Measurable-X-section(E,x)) = Integral(M2,ProjMap1(chi(E,[:X1,X2:]),x));
theorem :: MEASUR11:73
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2,
f be disjoint_valued FinSequence of measurable_rectangles(S1,S2),
x be Element of X1, n be Nat,
En be Element of sigma measurable_rectangles(S1,S2),
An be Element of S1, Bn be Element of S2
st n in dom f & f.n = En & En = [:An,Bn:] holds
Integral(M2,ProjMap1(chi(f.n,[:X1,X2:]),x))
= M2.(Measurable-X-section(En,x)) * chi(An,X1).x;
theorem :: MEASUR11:74
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
E be Element of sigma measurable_rectangles(S1,S2)
st E in Field_generated_by measurable_rectangles(S1,S2) & E <> {}
ex f be disjoint_valued FinSequence of measurable_rectangles(S1,S2),
A be FinSequence of S1, B be FinSequence of S2,
Xf be summable FinSequence of Funcs([:X1,X2:],ExtREAL) st
E = Union f & len f in dom f & len f = len A & len f = len B
& len f = len Xf
& ( for n be Nat st n in dom f holds f.n = [:A.n,B.n:] )
& ( for n be Nat st n in dom Xf holds Xf.n = chi(f.n,[:X1,X2:]) )
& (Partial_Sums Xf).(len Xf) = chi(E,[:X1,X2:])
& ( for n be Nat, x,y be set st n in dom Xf & x in X1 & y in X2
holds (Xf.n).(x,y) = chi(A.n,X1).x * chi(B.n,X2).y )
& ( for x be Element of X1 holds
ProjMap1(chi(E,[:X1,X2:]),x) = ProjMap1(((Partial_Sums Xf)/.(len Xf)),x) )
& ( for y be Element of X2 holds
ProjMap2(chi(E,[:X1,X2:]),y) = ProjMap2(((Partial_Sums Xf)/.(len Xf)),y) )
;
theorem :: MEASUR11:75
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
F be FinSequence of measurable_rectangles(S1,S2) holds
Union F in sigma measurable_rectangles(S1,S2);
theorem :: MEASUR11:76
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2)
st E in Field_generated_by measurable_rectangles(S1,S2) & E <> {}
ex F be disjoint_valued FinSequence of measurable_rectangles(S1,S2),
A be FinSequence of S1, B be FinSequence of S2,
C be summable FinSequence of Funcs([:X1,X2:],ExtREAL),
I be summable FinSequence of Funcs(X1,ExtREAL),
J be summable FinSequence of Funcs(X2,ExtREAL)
st
E = Union F & len F in dom F & len F = len A & len F = len B
& len F = len C & len F = len I
& len F = len J
& ( for n be Nat st n in dom C holds C.n = chi(F.n,[:X1,X2:]) )
& (Partial_Sums C)/.(len C) = chi(E,[:X1,X2:])
& ( for x be Element of X1, n be Nat st n in dom I holds
(I.n).x = Integral(M2,ProjMap1((C/.n),x)) )
& ( for n be Nat, P be Element of S1 st n in dom I holds
I/.n is_measurable_on P )
& ( for x be Element of X1 holds
Integral(M2,ProjMap1(((Partial_Sums C)/.(len C)),x))
= ((Partial_Sums I)/.(len I)).x)
& ( for y be Element of X2, n be Nat st n in dom J holds
(J.n).y = Integral(M1,ProjMap2((C/.n),y)) )
& ( for n be Nat, P be Element of S2 st n in dom J holds
J/.n is_measurable_on P )
& ( for y be Element of X2 holds
Integral(M1,ProjMap2(((Partial_Sums C)/.(len C)),y))
= ((Partial_Sums J)/.(len J)).y);
definition
let X1,X2 be non empty set;
let S1 be SigmaField of X1, S2 be SigmaField of X2;
let F be Set_Sequence of sigma measurable_rectangles(S1,S2);
let n be Nat;
redefine func F.n -> Element of sigma measurable_rectangles(S1,S2);
end;
definition
let X1,X2 be non empty set;
let S1 be SigmaField of X1, S2 be SigmaField of X2;
let F be Function of [:NAT,sigma measurable_rectangles(S1,S2):],
sigma measurable_rectangles(S1,S2);
let n be Element of NAT, E be Element of sigma measurable_rectangles(S1,S2);
redefine func F.(n,E) -> Element of sigma measurable_rectangles(S1,S2);
end;
theorem :: MEASUR11:77
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2),
V be Element of S2
st E in Field_generated_by measurable_rectangles(S1,S2)
ex F be Function of X1,ExtREAL st
( for x be Element of X1 holds
F.x = M2.(Measurable-X-section(E,x) /\ V))
& (for P be Element of S1 holds F is_measurable_on P);
theorem :: MEASUR11:78
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2),
V be Element of S1
st E in Field_generated_by measurable_rectangles(S1,S2)
ex F be Function of X2,ExtREAL st
( for x be Element of X2 holds
F.x = M1.(Measurable-Y-section(E,x) /\ V))
& (for P be Element of S2 holds F is_measurable_on P);
theorem :: MEASUR11:79
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2)
st
E in Field_generated_by measurable_rectangles(S1,S2)
holds
(for B be Element of S2 holds
E in {E where E is Element of sigma measurable_rectangles(S1,S2) :
(ex F be Function of X1,ExtREAL st
(for x be Element of X1 holds
F.x = M2.(Measurable-X-section(E,x) /\ B))
& (for V be Element of S1 holds F is_measurable_on V))} );
theorem :: MEASUR11:80
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1,
E be Element of sigma measurable_rectangles(S1,S2)
st
E in Field_generated_by measurable_rectangles(S1,S2) holds
(for B be Element of S1 holds
E in {E where E is Element of sigma measurable_rectangles(S1,S2) :
(ex F be Function of X2,ExtREAL st
(for x be Element of X2 holds
F.x = M1.(Measurable-Y-section(E,x) /\ B))
& (for V be Element of S2 holds F is_measurable_on V))} );
theorem :: MEASUR11:81
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2, B be Element of S2 holds
Field_generated_by measurable_rectangles(S1,S2)
c= {E where E is Element of sigma measurable_rectangles(S1,S2) :
(ex F be Function of X1,ExtREAL st
(for x be Element of X1 holds
F.x = M2.(Measurable-X-section(E,x) /\ B))
& (for V be Element of S1 holds F is_measurable_on V))};
theorem :: MEASUR11:82
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, B be Element of S1 holds
Field_generated_by measurable_rectangles(S1,S2)
c= {E where E is Element of sigma measurable_rectangles(S1,S2) :
(ex F be Function of X2,ExtREAL st
(for y be Element of X2 holds
F.y = M1.(Measurable-Y-section(E,y) /\ B))
& (for V be Element of S2 holds F is_measurable_on V))};
begin :: Sigma finite measure
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
attr M is sigma_finite means
:: MEASUR11:def 12
ex E be Set_Sequence of S st
(for n be Nat holds M.(E.n) < +infty) & Union E = X;
end;
theorem :: MEASUR11:83
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S
holds
M is sigma_finite
iff
ex F be Set_Sequence of S st
F is non-descending & (for n be Nat holds M.(F.n) < +infty)
& lim F = X;
theorem :: MEASUR11:84
for X be set, S be semialgebra_of_sets of X,
P be pre-Measure of S, M be induced_Measure of S,P holds
M = (C_Meas M)|(Field_generated_by S);
begin :: Fubini's theorem on measure
theorem :: MEASUR11:85
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2, B be Element of S2
st M2.B < +infty holds
{E where E is Element of sigma measurable_rectangles(S1,S2) :
(ex F be Function of X1,ExtREAL st
(for x be Element of X1 holds
F.x = M2.(Measurable-X-section(E,x) /\ B))
& (for V be Element of S1 holds F is_measurable_on V))}
is MonotoneClass of [:X1,X2:];
theorem :: MEASUR11:86
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, B be Element of S1
st M1.B < +infty holds
{E where E is Element of sigma measurable_rectangles(S1,S2) :
(ex F be Function of X2,ExtREAL st
(for y be Element of X2 holds
F.y = M1.(Measurable-Y-section(E,y) /\ B))
& (for V be Element of S2 holds F is_measurable_on V))}
is MonotoneClass of [:X1,X2:];
theorem :: MEASUR11:87
for X be non empty set, F be Field_Subset of X, L be SetSequence of X
st rng L is MonotoneClass of X & F c= rng L
holds sigma F = monotoneclass F & sigma F c= rng L;
theorem :: MEASUR11:88
for X be non empty set, F be Field_Subset of X, K be Subset-Family of X
st K is MonotoneClass of X & F c= K
holds sigma F = monotoneclass F & sigma F c= K;
theorem :: MEASUR11:89
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2, B be Element of S2
st M2.B < +infty holds
sigma measurable_rectangles(S1,S2)
c= {E where E is Element of sigma measurable_rectangles(S1,S2):
(ex F be Function of X1,ExtREAL st
(for x be Element of X1 holds
F.x = M2.(Measurable-X-section(E,x) /\ B))
& (for V be Element of S1 holds F is_measurable_on V))};
theorem :: MEASUR11:90
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, B be Element of S1
st M1.B < +infty holds
sigma measurable_rectangles(S1,S2)
c= {E where E is Element of sigma measurable_rectangles(S1,S2) :
(ex F be Function of X2,ExtREAL st
(for y be Element of X2 holds
F.y = M1.(Measurable-Y-section(E,y) /\ B))
& (for V be Element of S2 holds F is_measurable_on V))};
theorem :: MEASUR11:91
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2, E be Element of sigma measurable_rectangles(S1,S2)
st M2 is sigma_finite
holds
(ex F be Function of X1,ExtREAL st
(for x be Element of X1 holds
F.x = M2.(Measurable-X-section(E,x)))
& (for V be Element of S1 holds F is_measurable_on V));
theorem :: MEASUR11:92
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, E be Element of sigma measurable_rectangles(S1,S2)
st M1 is sigma_finite
holds
(ex F be Function of X2,ExtREAL st
(for y be Element of X2 holds
F.y = M1.(Measurable-Y-section(E,y)))
& (for V be Element of S2 holds F is_measurable_on V));
definition
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2);
assume M2 is sigma_finite;
func Y-vol(E,M2) -> nonnegative Function of X1,ExtREAL means
:: MEASUR11:def 13
(for x be Element of X1 holds it.x = M2.(Measurable-X-section(E,x)))
& (for V be Element of S1 holds it is_measurable_on V);
end;
definition
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1,
E be Element of sigma measurable_rectangles(S1,S2);
assume M1 is sigma_finite;
func X-vol(E,M1) -> nonnegative Function of X2,ExtREAL means
:: MEASUR11:def 14
(for y be Element of X2 holds it.y = M1.(Measurable-Y-section(E,y)))
& (for V be Element of S2 holds it is_measurable_on V);
end;
theorem :: MEASUR11:93
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2,
E1,E2 be Element of sigma measurable_rectangles(S1,S2)
st M2 is sigma_finite & E1 misses E2 holds
Y-vol(E1 \/ E2,M2) = Y-vol(E1,M2) + Y-vol(E2,M2);
theorem :: MEASUR11:94
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1,
E1,E2 be Element of sigma measurable_rectangles(S1,S2)
st M1 is sigma_finite & E1 misses E2 holds
X-vol(E1 \/ E2,M1) = X-vol(E1,M1) + X-vol(E2,M1);
theorem :: MEASUR11:95
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E1,E2 be Element of sigma measurable_rectangles(S1,S2)
st M2 is sigma_finite & E1 misses E2 holds
Integral(M1,Y-vol(E1 \/ E2,M2))
= Integral(M1,Y-vol(E1,M2)) + Integral(M1,Y-vol(E2,M2));
theorem :: MEASUR11:96
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E1,E2 be Element of sigma measurable_rectangles(S1,S2)
st M1 is sigma_finite & E1 misses E2 holds
Integral(M2,X-vol(E1 \/ E2,M1))
= Integral(M2,X-vol(E1,M1)) + Integral(M2,X-vol(E2,M1));
theorem :: MEASUR11:97
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st E = [:A,B:] & M2 is sigma_finite holds
(M2.B = +infty implies Y-vol(E,M2) = Xchi(A,X1))
& (M2.B <> +infty implies
ex r be Real st r = M2.B & Y-vol(E,M2) = r(#)chi(A,X1));
theorem :: MEASUR11:98
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st E = [:A,B:] & M1 is sigma_finite holds
(M1.A = +infty implies X-vol(E,M1) = Xchi(B,X2))
& (M1.A <> +infty implies
ex r be Real st r = M1.A & X-vol(E,M1) = r(#)chi(B,X2));
theorem :: MEASUR11:99
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
A be Element of S, r be Real st r >= 0 holds
Integral(M,r(#)chi(A,X)) = r * M.A;
theorem :: MEASUR11:100
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
F be FinSequence of sigma measurable_rectangles(S1,S2),
n be Nat
st M2 is sigma_finite
& F is FinSequence of measurable_rectangles(S1,S2) holds
product_sigma_Measure(M1,M2).(F.n) = Integral(M1,Y-vol(F.n,M2));
theorem :: MEASUR11:101
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
F be FinSequence of sigma measurable_rectangles(S1,S2),
n be Nat
st M1 is sigma_finite
& F is FinSequence of measurable_rectangles(S1,S2)
holds
product_sigma_Measure(M1,M2).(F.n) = Integral(M2,X-vol(F.n,M1));
theorem :: MEASUR11:102
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
F be disjoint_valued FinSequence of sigma measurable_rectangles(S1,S2),
n be Nat
st M2 is sigma_finite
& F is FinSequence of measurable_rectangles(S1,S2)
holds
product_sigma_Measure(M1,M2).(Union F) = Integral(M1,Y-vol(Union F,M2));
theorem :: MEASUR11:103
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
F be disjoint_valued FinSequence of sigma measurable_rectangles(S1,S2),
n be Nat
st M1 is sigma_finite
& F is FinSequence of measurable_rectangles(S1,S2)
holds
product_sigma_Measure(M1,M2).(Union F) = Integral(M2,X-vol(Union F,M1));
theorem :: MEASUR11:104
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2)
st
E in Field_generated_by measurable_rectangles(S1,S2) & M2 is sigma_finite
holds
for V be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2 st
V = [:A,B:] holds
E in {E where E is Element of sigma measurable_rectangles(S1,S2) :
Integral(M1,(Y-vol(E/\V,M2))) = (product_sigma_Measure(M1,M2)).(E/\V)};
theorem :: MEASUR11:105
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2)
st
E in Field_generated_by measurable_rectangles(S1,S2) & M1 is sigma_finite
holds
for V be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2 st
V = [:A,B:] holds
E in {E where E is Element of sigma measurable_rectangles(S1,S2) :
Integral(M2,(X-vol(E/\V,M1))) = (product_sigma_Measure(M1,M2)).(E/\V)};
theorem :: MEASUR11:106
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
V be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st M2 is sigma_finite & V = [:A,B:] holds
Field_generated_by measurable_rectangles(S1,S2)
c= {E where E is Element of sigma measurable_rectangles(S1,S2) :
Integral(M1,(Y-vol(E/\V,M2))) = (product_sigma_Measure(M1,M2)).(E/\V)};
theorem :: MEASUR11:107
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
V be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st M1 is sigma_finite & V = [:A,B:] holds
Field_generated_by measurable_rectangles(S1,S2)
c= {E where E is Element of sigma measurable_rectangles(S1,S2) :
Integral(M2,(X-vol(E/\V,M1))) = (product_sigma_Measure(M1,M2)).(E/\V)};
theorem :: MEASUR11:108
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2,
E,V be Element of sigma measurable_rectangles(S1,S2),
P be Set_Sequence of sigma measurable_rectangles(S1,S2),
x be Element of X1
st P is non-descending & lim P = E holds
ex K be SetSequence of S2 st
K is non-descending
& (for n be Nat holds K.n
= Measurable-X-section(P.n,x) /\ Measurable-X-section(V,x))
& lim K = Measurable-X-section(E,x) /\ Measurable-X-section(V,x);
theorem :: MEASUR11:109
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1,
E,V be Element of sigma measurable_rectangles(S1,S2),
P be Set_Sequence of sigma measurable_rectangles(S1,S2),
y be Element of X2
st P is non-descending & lim P = E
holds
ex K be SetSequence of S1 st
K is non-descending
& (for n be Nat holds K.n
= Measurable-Y-section(P.n,y) /\ Measurable-Y-section(V,y))
& lim K = Measurable-Y-section(E,y) /\ Measurable-Y-section(V,y);
theorem :: MEASUR11:110
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M2 be sigma_Measure of S2,
E,V be Element of sigma measurable_rectangles(S1,S2),
P be Set_Sequence of sigma measurable_rectangles(S1,S2),
x be Element of X1
st P is non-ascending & lim P = E holds
ex K be SetSequence of S2 st
K is non-ascending
& (for n be Nat holds K.n
= Measurable-X-section(P.n,x) /\ Measurable-X-section(V,x))
& lim K = Measurable-X-section(E,x) /\ Measurable-X-section(V,x);
theorem :: MEASUR11:111
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1,
E,V be Element of sigma measurable_rectangles(S1,S2),
P be Set_Sequence of sigma measurable_rectangles(S1,S2),
y be Element of X2
st P is non-ascending & lim P = E holds
ex K be SetSequence of S1 st
K is non-ascending
& (for n be Nat holds K.n
= Measurable-Y-section(P.n,y) /\ Measurable-Y-section(V,y))
& lim K = Measurable-Y-section(E,y) /\ Measurable-Y-section(V,y);
theorem :: MEASUR11:112
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
V be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st
M2 is sigma_finite & V = [:A,B:] & product_sigma_Measure(M1,M2).V < +infty &
M2.B < +infty
holds
{E where E is Element of sigma measurable_rectangles(S1,S2) :
Integral(M1,(Y-vol(E/\V,M2))) = (product_sigma_Measure(M1,M2)).(E/\V)}
is MonotoneClass of [:X1,X2:];
theorem :: MEASUR11:113
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
V be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st
M1 is sigma_finite & V = [:A,B:] & product_sigma_Measure(M1,M2).V < +infty &
M1.A < +infty
holds
{E where E is Element of sigma measurable_rectangles(S1,S2) :
Integral(M2,(X-vol(E/\V,M1))) = (product_sigma_Measure(M1,M2)).(E/\V)}
is MonotoneClass of [:X1,X2:];
theorem :: MEASUR11:114
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
V be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st M2 is sigma_finite & V = [:A,B:]
& product_sigma_Measure(M1,M2).V < +infty & M2.B < +infty holds
sigma measurable_rectangles(S1,S2)
c= {E where E is Element of sigma measurable_rectangles(S1,S2) :
Integral(M1,(Y-vol(E/\V,M2))) = (product_sigma_Measure(M1,M2)).(E/\V)};
theorem :: MEASUR11:115
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
V be Element of sigma measurable_rectangles(S1,S2),
A be Element of S1, B be Element of S2
st M1 is sigma_finite & V = [:A,B:]
& product_sigma_Measure(M1,M2).V < +infty & M1.A < +infty holds
sigma measurable_rectangles(S1,S2)
c= {E where E is Element of sigma measurable_rectangles(S1,S2) :
Integral(M2,(X-vol(E/\V,M1))) = (product_sigma_Measure(M1,M2)).(E/\V)};
theorem :: MEASUR11:116
for X,Y be set, A be SetSequence of X, B be SetSequence of Y,
C be SetSequence of [:X,Y:] st A is non-descending & B is non-descending &
(for n be Nat holds C.n = [:A.n,B.n:]) holds
C is non-descending & C is convergent & Union C = [:Union A,Union B:];
::$N Fubini's theorem
theorem :: MEASUR11:117
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2)
st M1 is sigma_finite & M2 is sigma_finite
holds Integral(M1,(Y-vol(E,M2))) = (product_sigma_Measure(M1,M2)).E;
::$N Fubini's theorem
theorem :: MEASUR11:118
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
E be Element of sigma measurable_rectangles(S1,S2)
st M1 is sigma_finite & M2 is sigma_finite
holds Integral(M2,(X-vol(E,M1))) = (product_sigma_Measure(M1,M2)).E;