:: Fubini's Theorem
::  by Noboru Endou
:: 
:: Received March 11, 2019
:: Copyright (c) 2019-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,
      REAL_1, FUNCT_1, XBOOLE_0, TARSKI, ZFMISC_1, PROB_1, SUPINF_2, VALUED_0,
      PARTFUN1, MEASURE1, MESFUNC5, MESFUNC1, MEASUR10, FUNCT_3, MEASUR11,
      COMPLEX1, MESFUN12, RFUNCT_3, INTEGRA5, MESFUN13, MEASURE6, LPSPACE1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XXREAL_3, XXREAL_0, XREAL_0,
      NUMBERS, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, PARTFUN1, PROB_1, SUPINF_2,
      MEASURE1, MESFUNC1, MESFUNC2, MESFUNC5, EXTREAL1, MEASUR10, MEASUR11,
      MESFUN12, MESFUNC6, LPSPACE1;
 constructors EXTREAL1, SUPINF_1, MESFUNC2, MEASUR11, MESFUN12, MESFUNC6,
      LPSPACE1;
 registrations ORDINAL1, XBOOLE_0, RELAT_1, SUBSET_1, XXREAL_0, XREAL_0, NAT_1,
      NUMBERS, VALUED_0, RELSET_1, MEASURE1, XXREAL_3, MESFUNC7;
 requirements BOOLE, SUBSET, NUMERALS, REAL;


begin :: Preliminaries

reserve X for set;

theorem :: MESFUN13:1
  for A being Subset of X, f being X-defined Relation holds
    f|A` = f|(dom f \ A);

theorem :: MESFUN13:2
for f being PartFunc of X,ExtREAL holds
 great_eq_dom(f,+infty) = eq_dom(f,+infty);

theorem :: MESFUN13:3
for f being PartFunc of X,ExtREAL holds
 less_eq_dom(f,-infty) = eq_dom(f,-infty);

theorem :: MESFUN13:4
for f being PartFunc of X,ExtREAL, er being ExtReal
 holds great_eq_dom(f,er) misses less_dom(f,er);

theorem :: MESFUN13:5
for f being PartFunc of X,ExtREAL holds
 dom f = eq_dom(f,-infty) \/ (great_dom(f,-infty) /\ less_dom(f,+infty))
         \/ eq_dom(f,+infty);

reserve X,X1,X2 for non empty set;

theorem :: MESFUN13:6
for f being PartFunc of X,ExtREAL, x being Element of X
holds (max+f).x <= (|.f.|).x & (max-f).x <= (|.f.|).x;

theorem :: MESFUN13:7
for f being PartFunc of [:X1,X2:],ExtREAL,
    x being Element of X1, y being Element of X2
holds ProjPMap1(|.f.|,x) = |.ProjPMap1(f,x).|
    & ProjPMap2(|.f.|,y) = |.ProjPMap2(f,y).|;

begin :: Markov's inequality and Misc.

reserve S for SigmaField of X;
reserve S1 for SigmaField of X1;
reserve S2 for SigmaField of X2;
reserve M for sigma_Measure of S;
reserve M1 for sigma_Measure of S1;
reserve M2 for sigma_Measure of S2;

registration
  let X be non empty set, S be SigmaField of X, E be Element of S;
  cluster E-measurable for PartFunc of X,ExtREAL;
end;

theorem :: MESFUN13:8
for E being Element of S, f be E-measurable PartFunc of X,ExtREAL
 st dom f = E holds eq_dom(f,+infty) in S & eq_dom(f,-infty) in S;

theorem :: MESFUN13:9
for E being Element of sigma measurable_rectangles(S1,S2),
 f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite & dom f = E
holds Integral(M1,Integral2(M2,|.f.|)) = Integral(Prod_Measure(M1,M2),|.f.|)
    & Integral(M2,Integral1(M1,|.f.|)) = Integral(Prod_Measure(M1,M2),|.f.|);

theorem :: MESFUN13:10
for E being Element of sigma measurable_rectangles(S1,S2),
 f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite & E = dom f
holds f is_integrable_on Prod_Measure(M1,M2)
        iff Integral(M2,Integral1(M1,|.f.|)) < +infty;

theorem :: MESFUN13:11
for E being Element of sigma measurable_rectangles(S1,S2),
 f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite & E = dom f
holds f is_integrable_on Prod_Measure(M1,M2)
        iff Integral(M1,Integral2(M2,|.f.|)) < +infty;

theorem :: MESFUN13:12
for E being Element of sigma measurable_rectangles(S1,S2),
 U being Element of S1, f be E-measurable PartFunc of [:X1,X2:],ExtREAL
st M2 is sigma_finite & E = dom f
holds Integral2(M2,|.f.|) is U-measurable;

theorem :: MESFUN13:13
for E being Element of sigma measurable_rectangles(S1,S2),
 V being Element of S2, f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & E = dom f
holds Integral1(M1,|.f.|) is V-measurable;

theorem :: MESFUN13:14
for f being PartFunc of [:X1,X2:],ExtREAL
st M2 is sigma_finite & f is_integrable_on Prod_Measure(M1,M2)
holds
  Integral(M1,max+(Integral2(M2,|.f.|))) = Integral(M1,Integral2(M2,|.f.|))
& Integral(M1,max-(Integral2(M2,|.f.|))) = 0;

theorem :: MESFUN13:15
for f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite
 & f is_integrable_on Prod_Measure(M1,M2) holds
  Integral(M2,max+(Integral1(M1,|.f.|))) = Integral(M2,Integral1(M1,|.f.|))
& Integral(M2,max-(Integral1(M1,|.f.|))) = 0;

::$N Markov's inequality
theorem :: MESFUN13:16  :: extension of RANDOM_1:36
for E being Element of S, f being E-measurable PartFunc of X,ExtREAL,
er being ExtReal st dom f = E & f is nonnegative & er >= 0
holds er*M.(great_eq_dom(f,er)) <= Integral(M,f);

begin :: Fubini's Theorem

theorem :: MESFUN13:17
for f,g being PartFunc of X,ExtREAL
 st f is_integrable_on M & g is_integrable_on M
 holds Integral(M,f+g)
         = Integral(M,f|(dom f /\ dom g)) + Integral(M,g|(dom f /\ dom g))
     & Integral(M,f-g)
         = Integral(M,f|(dom f /\ dom g)) - Integral(M,g|(dom f /\ dom g));

theorem :: MESFUN13:18
for f being PartFunc of X,ExtREAL holds f is_integrable_on M iff
    max+f is_integrable_on M & max-f is_integrable_on M;

theorem :: MESFUN13:19
for A,B being Element of S, f being PartFunc of X,ExtREAL
st B c= A & f|A is B-measurable holds f is B-measurable;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
  f be PartFunc of X,ExtREAL;
  pred f is_a.e.integrable_on M means
:: MESFUN13:def 1
  ex A be Element of S st M.A = 0 & A c= dom f & f|A` is_integrable_on M;
end;

theorem :: MESFUN13:20
for f being PartFunc of X,ExtREAL
 st f is_a.e.integrable_on M holds dom f in S;

theorem :: MESFUN13:21
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
  f is_a.e.integrable_on M;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
  f be PartFunc of X,ExtREAL;
  pred f is_a.e.finite M means
:: MESFUN13:def 2
  ex A be Element of S st M.A = 0 & A c= dom f & f|A` is PartFunc of X,REAL;
end;

theorem :: MESFUN13:22
for E being Element of S, f being E-measurable PartFunc of X,ExtREAL
st dom f = E holds
 f is_a.e.finite M iff M.(eq_dom(f,+infty) \/ eq_dom(f,-infty)) = 0;

theorem :: MESFUN13:23
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
  M.(eq_dom(f,+infty)) = 0 & M.(eq_dom(f,-infty)) = 0 & f is_a.e.finite M
& for r being Real st r > 0 holds M.(great_eq_dom(|.f.|,r)) < +infty;

theorem :: MESFUN13:24
for f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
 & f is_integrable_on Prod_Measure(M1,M2)
 holds Integral1(M1,max+f) is_integrable_on M2
     & Integral2(M2,max+f) is_integrable_on M1
     & Integral1(M1,max-f) is_integrable_on M2
     & Integral2(M2,max-f) is_integrable_on M1
     & Integral1(M1,|.f.|) is_integrable_on M2
     & Integral2(M2,|.f.|) is_integrable_on M1;

theorem :: MESFUN13:25
for E being Element of S, f being E-measurable PartFunc of X,ExtREAL
  st dom f c= E & f is_a.e.integrable_on M holds f is_integrable_on M;

theorem :: MESFUN13:26
for A being Element of S, f being PartFunc of X,ExtREAL st
  M.A = 0 & A c= dom f & f|A` is_integrable_on M holds
  ex g be PartFunc of X,ExtREAL st dom g = dom f &
    f|A` = g|A` & g is_integrable_on M & Integral(M,f|A`) = Integral(M,g);

theorem :: MESFUN13:27
for f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
 & f is_integrable_on Prod_Measure(M1,M2)
holds
    Integral(Prod_Measure(M1,M2),f)
     = Integral(M2,Integral1(M1,max+f)) - Integral(M2,Integral1(M1,max-f))
  & Integral(Prod_Measure(M1,M2),f)
     = Integral(M1,Integral2(M2,max+f)) - Integral(M1,Integral2(M2,max-f));

theorem :: MESFUN13:28
for E being Element of sigma measurable_rectangles(S1,S2), y be Element of X2
holds
  ( M1.Measurable-Y-section(E,y) <> 0
     implies Integral1(M1,Xchi(E,[:X1,X2:])).y = +infty ) &
  ( M1.Measurable-Y-section(E,y) = 0
     implies Integral1(M1,Xchi(E,[:X1,X2:])).y = 0 );

theorem :: MESFUN13:29
for E being Element of sigma measurable_rectangles(S1,S2), x be Element of X1
holds
  ( M2.Measurable-X-section(E,x) <> 0
     implies Integral2(M2,Xchi(E,[:X1,X2:])).x = +infty ) &
  ( M2.Measurable-X-section(E,x) = 0
     implies Integral2(M2,Xchi(E,[:X1,X2:])).x = 0 );

::$N Fubini`s theorem
theorem :: MESFUN13:30
for X1,X2 being non empty set, S1 being SigmaField of X1,
S2 being SigmaField of X2, M1 being sigma_Measure of S1,
M2 being sigma_Measure of S2, f being PartFunc of [:X1,X2:],ExtREAL,
SX1 being Element of S1
st M1 is sigma_finite & M2 is sigma_finite
 & f is_integrable_on Prod_Measure(M1,M2) & X1 = SX1
holds
  ex U be Element of S1 st M1.U = 0
    & (for x being Element of X1 st x in U` holds
          ProjPMap1(f,x) is_integrable_on M2)
    & Integral2(M2,|.f.|)|U` is PartFunc of X1,REAL
    & Integral2(M2,f) is (SX1\U)-measurable
    & Integral2(M2,f)|U` is_integrable_on M1
    & Integral2(M2,f)|U` in L1_Functions M1
    & (ex g be Function of X1,ExtREAL st
         g is_integrable_on M1 & g|U` = Integral2(M2,f)|U`
       & Integral(Prod_Measure(M1,M2),f) = Integral(M1,g));

theorem :: MESFUN13:31
for X1,X2 being non empty set, S1 being SigmaField of X1,
S2 being SigmaField of X2, M1 being sigma_Measure of S1,
M2 being sigma_Measure of S2, f being PartFunc of [:X1,X2:],ExtREAL,
SX2 being Element of S2
st M1 is sigma_finite & M2 is sigma_finite
 & f is_integrable_on Prod_Measure(M1,M2) & X2 = SX2
holds
  ex V be Element of S2 st M2.V = 0
    & (for y being Element of X2 st y in V` holds
          ProjPMap2(f,y) is_integrable_on M1)
    & Integral1(M1,|.f.|)|V` is PartFunc of X2,REAL
    & Integral1(M1,f) is (SX2\V)-measurable
    & Integral1(M1,f)|V` is_integrable_on M2
    & Integral1(M1,f)|V` in L1_Functions M2
    & (ex g be Function of X2,ExtREAL st
         g is_integrable_on M2 & g|V` = Integral1(M1,f)|V`
       & Integral(Prod_Measure(M1,M2),f) = Integral(M2,g));

theorem :: MESFUN13:32
for X1,X2 being non empty set, S1 being SigmaField of X1,
S2 being SigmaField of X2, M1 being sigma_Measure of S1,
M2 being sigma_Measure of S2, f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
 & f is_integrable_on Prod_Measure(M1,M2)
 & (for x being Element of X1 holds Integral2(M2,|.f.|).x < +infty)
holds
      (for x being Element of X1 holds ProjPMap1(f,x) is_integrable_on M2)
    & (for U being Element of S1 holds Integral2(M2,f) is U-measurable)
    & Integral2(M2,f) is_integrable_on M1
    & Integral(Prod_Measure(M1,M2),f) = Integral(M1,Integral2(M2,f))
    & Integral2(M2,f) in L1_Functions M1;

theorem :: MESFUN13:33
for X1,X2 being non empty set, S1 being SigmaField of X1,
S2 being SigmaField of X2, M1 being sigma_Measure of S1,
M2 being sigma_Measure of S2, f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
 & f is_integrable_on Prod_Measure(M1,M2)
 & (for y being Element of X2 holds Integral1(M1,|.f.|).y < +infty)
holds
      (for y being Element of X2 holds ProjPMap2(f,y) is_integrable_on M1)
    & (for V being Element of S2 holds Integral1(M1,f) is V-measurable)
    & Integral1(M1,f) is_integrable_on M2
    & Integral(Prod_Measure(M1,M2),f) = Integral(M2,Integral1(M1,f))
    & Integral1(M1,f) in L1_Functions M2;