:: Fubini's Theorem on Measure :: by Noboru Endou :: :: Received February 23, 2017 :: Copyright (c) 2017-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, 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, ORDINAL1, 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 notation let R be Relation, x be set; synonym X-section(R,x) for Im(R,x); end; notation let R be Relation, y be set; synonym Y-section(R,y) for Coim(R,y); end; definition let X,Y be set, E be Subset of [:X,Y:], x be set; redefine 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,Y be set, E be Subset of [:X,Y:], y be set; redefine 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,Y,p be set, E1,E2 be Subset of [:X,Y:] st E1 c= E2 holds X-section(E1,p) c= X-section(E2,p); theorem :: MEASUR11:21 for X,Y,p be set, E1,E2 be Subset of [:X,Y:] 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 A-measurable & A c= dom f holds -f is A-measurable; 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 A-measurable & g is A-measurable & A c= dom (f+g) holds f+g is A-measurable; 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 A-measurable & g is A-measurable & A c= dom(f-g) holds f-g is A-measurable; 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 A-measurable & g is A-measurable & A c= dom(f-g) holds f-g is A-measurable; 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 P-measurable) holds for n be Nat st n in dom F holds (Partial_Sums F)/.n is P-measurable; 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 P-measurable) & ( 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 P-measurable) & ( 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 P-measurable); 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 P-measurable); 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 V-measurable))} ); 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 V-measurable))} ); 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 V-measurable))}; 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 V-measurable))}; 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 V-measurable))} 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 V-measurable))} 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 V-measurable))}; 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 V-measurable))}; 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 V-measurable)); 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 V-measurable)); 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 V-measurable); 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 V-measurable); 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;