:: Integral of Real-valued Measurable Function
::  by Yasunari Shidama and Noboru Endou
::
:: Received October 27, 2006
:: Copyright (c) 2006-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, XBOOLE_0, PROB_1, FUNCT_1, PARTFUN1, SUBSET_1, REAL_1,
      NAT_1, COMPLEX1, MEASURE6, RELAT_1, MEASURE1, MESFUNC2, TARSKI, FINSEQ_1,
      XXREAL_0, ARYTM_3, ARYTM_1, VALUED_0, MESFUNC1, SETFAM_1, VALUED_1,
      RAT_1, RFUNCT_3, SUPINF_2, CARD_1, SUPINF_1, MESFUNC5, MESFUNC3, INT_1,
      ZFMISC_1, INTEGRA5, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3,
      XCMPLX_0, DOMAIN_1, XREAL_0, REAL_1, RAT_1, NAT_1, NAT_D, FUNCT_1,
      RELSET_1, PARTFUN1, FINSEQ_1, VALUED_1, SUPINF_2, COMPLEX1, XXREAL_0,
      VALUED_0, RFUNCT_3, MEASURE6, FUNCT_2, SUPINF_1, MEASURE1, EXTREAL1,
      MESFUNC1, MESFUNC2, MESFUNC3, SETFAM_1, PROB_1, MESFUNC5;
 constructors DOMAIN_1, REAL_1, SQUARE_1, NAT_D, MEASURE3, MEASURE6, EXTREAL1,
      MESFUNC1, BINARITH, MESFUNC2, MESFUNC3, MESFUNC5, SUPINF_1, RELSET_1,
      ABSVALUE, RFUNCT_3, FUNCT_4, SEQFUNC;
 registrations SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, RAT_1, MEMBERED,
      MEASURE1, VALUED_0, ORDINAL1, XXREAL_3;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: The Measurability of Real-valued Functions

reserve X for non empty set,
  Y for set,
  S for SigmaField of X,
  F for sequence of S,
  f,g for PartFunc of X,REAL,
  A,B for Element of S,
  r,s for Real,
  a for Real,
  n for Nat;

theorem :: MESFUNC6:1
  |. R_EAL f .| = R_EAL abs f;

theorem :: MESFUNC6:2
  for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, r be Real
 st dom f in S & (for x be object st x  in dom f holds f.x = r)
  holds f is_simple_func_in S;

theorem :: MESFUNC6:3
  for x be set holds x in less_dom(f,a) iff x in dom f &
   ex y being Real st y=f.x & y < a;

theorem :: MESFUNC6:4
  for x be set holds x in less_eq_dom(f,a) iff x in dom f &
   ex y being Real st y=f.x & y <= a;

theorem :: MESFUNC6:5
  for x be set holds x in great_dom(f,r) iff x in dom f &
  ex y being Real st y=f.x & r < y;

theorem :: MESFUNC6:6
  for x be set holds x in great_eq_dom(f,r) iff x in dom f &
  ex y being Real st y=f.x & r <= y;

theorem :: MESFUNC6:7
  for x be set holds x in eq_dom(f,r) iff x in dom f &
   ex y being Real st y=f.x & r= y;

theorem :: MESFUNC6:8
  (for n holds F.n = Y /\ great_dom(f,r-1/(n+1))) implies Y /\
  great_eq_dom(f,r) = meet rng F;

theorem :: MESFUNC6:9
  (for n holds F.n = Y /\ less_dom(f,(r+1/(n+1)))) implies Y /\
  less_eq_dom(f,r) = meet rng F;

theorem :: MESFUNC6:10
  (for n holds F.n = Y /\ less_eq_dom(f,r-1/(n+1))) implies Y /\
  less_dom(f,r) = union rng F;

theorem :: MESFUNC6:11
  (for n holds F.n = Y /\ great_eq_dom(f,r+1/(n+1))) implies Y /\
  great_dom(f,r) = union rng F;

definition
  let X be non empty set;
  let S be SigmaField of X;
  let A be Element of S;
  let f be PartFunc of X,REAL;
  attr f is A-measurable means
:: MESFUNC6:def 1
  R_EAL f is A-measurable;
end;

theorem :: MESFUNC6:12
  f is A-measurable iff for r being Real holds A /\
  less_dom(f,r) in S;

theorem :: MESFUNC6:13
  A c= dom f implies (f is A-measurable iff for r being Real
 holds A /\ great_eq_dom(f,r) in S);

theorem :: MESFUNC6:14
  f is A-measurable iff for r being Real holds A /\
  less_eq_dom(f,r) in S;

theorem :: MESFUNC6:15
  A c= dom f implies (f is A-measurable iff for r being Real
  holds A /\ great_dom(f,r) in S );

theorem :: MESFUNC6:16
  B c= A & f is A-measurable implies f is B-measurable;

theorem :: MESFUNC6:17
  f is A-measurable & f is B-measurable implies f is (A\/B)-measurable;

theorem :: MESFUNC6:18
  f is A-measurable & A c= dom f implies A /\ great_dom(f,r) /\
  less_dom(f,s) in S;

theorem :: MESFUNC6:19
  f is A-measurable & g is A-measurable & A c= dom g implies A /\
  less_dom(f,r) /\ great_dom(g,r) in S;

theorem :: MESFUNC6:20
  R_EAL(r(#)f)=r(#)R_EAL f;

theorem :: MESFUNC6:21
  f is A-measurable & A c= dom f implies r(#)f is A-measurable;

begin :: The Measurability of $f+g$ and $f-g$ for Real-valued Functions $f,g$

reserve X for non empty set,
  S for SigmaField of X,
  f,g for PartFunc of X,REAL,
  A for Element of S,
  r for Real,
  p for Rational;

theorem :: MESFUNC6:22
  R_EAL f is real-valued;

theorem :: MESFUNC6:23
  R_EAL(f+g)=R_EAL f + R_EAL g & R_EAL(f-g)=R_EAL f - R_EAL g &
  dom(R_EAL(f+g))= dom(R_EAL f) /\ dom(R_EAL g) & dom(R_EAL(f-g))= dom(R_EAL f)
  /\ dom(R_EAL g) & dom(R_EAL(f+g))= dom f /\ dom g & dom(R_EAL(f-g))= dom f /\
  dom g;

theorem :: MESFUNC6:24
  for F be Function of RAT,S st (for p holds F.p = (A/\less_dom(f,p)) /\
  (A/\less_dom(g,r-p))) holds A /\ less_dom(f+g,r) = union rng F;

theorem :: MESFUNC6:25
  f is A-measurable & g is A-measurable implies ex F being
Function of RAT,S st for p being Rational holds F.p = (A /\ less_dom(f,p)) /\ (
  A /\ less_dom(g,r-p));

theorem :: MESFUNC6:26
  f is A-measurable & g is A-measurable implies f+g is A-measurable;

theorem :: MESFUNC6:27
  R_EAL f - R_EAL g = R_EAL f + R_EAL -g;

theorem :: MESFUNC6:28
  -R_EAL f = R_EAL((-1)(#)f) & -R_EAL f = R_EAL -f;

theorem :: MESFUNC6:29
  f is A-measurable & g is A-measurable & A c= dom g implies
  f-g is A-measurable;

begin :: Basic Properties of Real-valued Functions, $\max_{+}f$ and $\max_{-}f$

reserve X for non empty set,
  f,g for PartFunc of X,REAL,
  r for Real ;

theorem :: MESFUNC6:30
  max+(R_EAL f) = max+f & max-(R_EAL f) = max-f;

theorem :: MESFUNC6:31
  for x being Element of X holds 0 <= (max+f).x;

theorem :: MESFUNC6:32
  for x being Element of X holds 0 <= (max-f).x;

theorem :: MESFUNC6:33
  max-f = max+(-f);

theorem :: MESFUNC6:34
  for x being set st x in dom f & 0 < max+f.x holds max-f.x = 0;

theorem :: MESFUNC6:35
  for x being set st x in dom f & 0 < max-f.x holds max+f.x = 0;

theorem :: MESFUNC6:36
  dom f = dom (max+f - max-f) & dom f = dom (max+f + max-f);

theorem :: MESFUNC6:37
  for x being set st x in dom f holds (max+f.x = f.x or max+f.x = 0) & (
  max-f.x = -(f.x) or max-f.x = 0);

theorem :: MESFUNC6:38
  for x being set st x in dom f & max+f.x = f.x holds max-f.x = 0;

theorem :: MESFUNC6:39
  for x being set st x in dom f & max+f.x = 0 holds max-f.x = -(f.x);

theorem :: MESFUNC6:40
  for x being set st x in dom f & max-f.x = -(f.x) holds max+f.x = 0;

theorem :: MESFUNC6:41
  for x being set st x in dom f & max-f.x = 0 holds max+f.x = f.x;

theorem :: MESFUNC6:42
  f = max+f - max-f;

theorem :: MESFUNC6:43
  |.r qua Complex.| = |. r .|;

theorem :: MESFUNC6:44
  R_EAL(abs f) =|.R_EAL f.|;

theorem :: MESFUNC6:45
  abs f = max+f + max-f;

begin :: The Measurability of $\max_{+}f, \max_{-}f$ and $|f|$

reserve X for non empty set,
  S for SigmaField of X,
  f,g for PartFunc of X,REAL,
  A for Element of S;

theorem :: MESFUNC6:46
  f is A-measurable implies max+f is A-measurable;

theorem :: MESFUNC6:47
  f is A-measurable & A c= dom f implies max-f is A-measurable;

theorem :: MESFUNC6:48
  f is A-measurable & A c= dom f implies abs f is A-measurable;

begin :: The Definition and the Measurability of a Real-valued Simple Function

reserve X for non empty set,
  Y for set,
  S for SigmaField of X,
  f,g,h for PartFunc of X,REAL,
  A for Element of S,
  r for Real;

definition
  let X,S,f;
  pred f is_simple_func_in S means
:: MESFUNC6:def 2

  ex F being Finite_Sep_Sequence of S
st (dom f = union rng F & for n being Nat,x,y being Element of X st n in dom F
  & x in F.n & y in F.n holds f.x = f.y);
end;

theorem :: MESFUNC6:49
  f is_simple_func_in S iff R_EAL f is_simple_func_in S;

theorem :: MESFUNC6:50
  f is_simple_func_in S implies f is A-measurable;

theorem :: MESFUNC6:51
  for X being set, f being PartFunc of X,REAL holds f is
  nonnegative iff for x being object holds 0 <= f.x;

theorem :: MESFUNC6:52
  for X being set, f being PartFunc of X,REAL st for x being object
  st x in dom f holds 0 <= f.x holds f is nonnegative;

theorem :: MESFUNC6:53
  for X being set, f being PartFunc of X,REAL holds f is nonpositive iff
  for x being set holds f.x <= 0;

theorem :: MESFUNC6:54
  (for x being object st x in dom f holds f.x <= 0) implies f is nonpositive;

theorem :: MESFUNC6:55
  f is nonnegative implies f|Y is nonnegative;

theorem :: MESFUNC6:56
  f is nonnegative & g is nonnegative implies f+g is nonnegative;

theorem :: MESFUNC6:57
  f is nonnegative implies (0 <= r implies r(#)f is nonnegative) & (r <=
  0 implies r(#)f is nonpositive);

theorem :: MESFUNC6:58
  (for x be set st x in dom f /\ dom g holds g.x <= f.x) implies f
  -g is nonnegative;

theorem :: MESFUNC6:59
  f is nonnegative & g is nonnegative & h is nonnegative implies f+g+h
  is nonnegative;

theorem :: MESFUNC6:60
  for x be object st x in dom(f+g+h) holds (f+g+h).x=f.x+g.x+h.x;

theorem :: MESFUNC6:61
  max+f is nonnegative & max-f is nonnegative;

theorem :: MESFUNC6:62
  dom(max+(f+g) + max-f) = dom f /\ dom g & dom(max-(f+g) + max+f)
= dom f /\ dom g & dom(max+(f+g) + max-f + max-g) = dom f /\ dom g & dom(max-(f
+g) + max+f + max+g) = dom f /\ dom g & max+(f+g) + max-f is nonnegative & max-
  (f+g) + max+f is nonnegative;

theorem :: MESFUNC6:63
  max+(f+g) + max-f + max-g = max-(f+g) + max+f + max+g;

theorem :: MESFUNC6:64
  0 <= r implies max+(r(#)f) = r(#)max+f & max-(r(#)f) = r(#)max-f;

theorem :: MESFUNC6:65
  0 <= r implies max+((-r)(#)f) = r(#)max-f & max-((-r)(#)f) = r(#)max+f;

theorem :: MESFUNC6:66
  max+(f|Y)=max+f|Y & max-(f|Y)=max-f|Y;

theorem :: MESFUNC6:67
  Y c= dom(f+g) implies dom((f+g)|Y) =Y & dom(f|Y+g|Y)=Y & (f+g)|Y = f|Y +g|Y;

theorem :: MESFUNC6:68
  eq_dom(f,r) = f"{r};

begin :: Lemmas for a Real-valued Measurable Function and a Simple Function

reserve X for non empty set,
  S for SigmaField of X,
  f,g for PartFunc of X,REAL ,
  A,B for Element of S,
  r,s for Real;

theorem :: MESFUNC6:69
  f is A-measurable & A c= dom f implies A /\ great_eq_dom(f,r) /\
  less_dom(f,s) in S;

theorem :: MESFUNC6:70
  f is_simple_func_in S implies f|A is_simple_func_in S;

theorem :: MESFUNC6:71
  f is_simple_func_in S implies dom f is Element of S;

theorem :: MESFUNC6:72
  f is_simple_func_in S & g is_simple_func_in S implies f+g is_simple_func_in S
;

theorem :: MESFUNC6:73
  f is_simple_func_in S implies r(#)f is_simple_func_in S;

theorem :: MESFUNC6:74
  (for x be set st x in dom(f-g) holds g.x <= f.x) implies f-g is nonnegative;

theorem :: MESFUNC6:75
  ex f be PartFunc of X,REAL st f is_simple_func_in S & dom f = A & for
  x be object st x in A holds f.x=r;

theorem :: MESFUNC6:76
  f is B-measurable & A = dom f /\ B implies f|B is A-measurable;

theorem :: MESFUNC6:77
  A c= dom f & f is A-measurable & g is A-measurable implies max+(
  f+g) + max-f is A-measurable;

theorem :: MESFUNC6:78
  A c= dom f /\ dom g & f is A-measurable & g is A-measurable
  implies max-(f+g) + max+f is A-measurable;

theorem :: MESFUNC6:79
  dom f in S & dom g in S implies dom(f+g) in S;

theorem :: MESFUNC6:80
  dom f = A implies (f is B-measurable iff f is (A/\B)-measurable);

theorem :: MESFUNC6:81
  ( ex A be Element of S st dom f = A ) implies for c be Real, B be
  Element of S st f is B-measurable holds c(#)f is B-measurable;

begin :: The Integral of a Real-valued Function

reserve X for non empty set,
  S for SigmaField of X,
  M for sigma_Measure of S,
  f,g for PartFunc of X,REAL,
  r for Real,
  E,A,B for Element of S;

definition
  let X be non empty set;
  let S be SigmaField of X;
  let M be sigma_Measure of S;
  let f be PartFunc of X,REAL;
  func Integral(M,f) -> Element of ExtREAL equals
:: MESFUNC6:def 3
  Integral(M,R_EAL f);
end;

theorem :: MESFUNC6:82
  (ex A be Element of S st A = dom f & f is A-measurable) & f
  is nonnegative implies Integral(M,f) = integral+(M,R_EAL f);

theorem :: MESFUNC6:83
  f is_simple_func_in S & f is nonnegative implies Integral(M,f) =
  integral+(M,R_EAL f) & Integral(M,f) = integral'(M,R_EAL f);

theorem :: MESFUNC6:84
  (ex A be Element of S st A = dom f & f is A-measurable) & f is
  nonnegative implies 0 <= Integral(M,f);

theorem :: MESFUNC6:85
  (ex E be Element of S st E = dom f & f is E-measurable) & f is
  nonnegative & A misses B implies Integral(M,f|(A\/B)) = Integral(M,f|A)+
  Integral(M,f|B);

theorem :: MESFUNC6:86
  (ex E be Element of S st E = dom f & f is E-measurable) & f is
  nonnegative implies 0<= Integral(M,f|A);

theorem :: MESFUNC6:87
  (ex E be Element of S st E = dom f & f is E-measurable ) & f is
  nonnegative & A c= B implies Integral(M,f|A) <= Integral(M,f|B);

theorem :: MESFUNC6:88
  (ex E be Element of S st E = dom f & f is E-measurable) & M.A = 0
  implies Integral(M,f|A)=0;

theorem :: MESFUNC6:89
  E = dom f & f is E-measurable & M.A =0 implies Integral(M,f|(E\A))
  = Integral(M,f);

definition
  let X be non empty set;
  let S be SigmaField of X;
  let M be sigma_Measure of S;
  let f be PartFunc of X,REAL;
  pred f is_integrable_on M means
:: MESFUNC6:def 4

  R_EAL f is_integrable_on M;
end;

theorem :: MESFUNC6:90
  f is_integrable_on M implies -infty < Integral(M,f) & Integral(M,f) < +infty;

theorem :: MESFUNC6:91
  f is_integrable_on M implies f|A is_integrable_on M;

theorem :: MESFUNC6:92
  f is_integrable_on M & A misses B implies Integral(M,f|(A\/B)) =
  Integral(M,f|A) + Integral(M,f|B);

theorem :: MESFUNC6:93
  f is_integrable_on M & B = (dom f)\A implies f|A is_integrable_on M &
  Integral(M,f) = Integral(M,f|A)+Integral(M,f|B);

theorem :: MESFUNC6:94
  (ex A be Element of S st A = dom f & f is A-measurable ) implies (f
  is_integrable_on M iff abs f is_integrable_on M);

theorem :: MESFUNC6:95
  f is_integrable_on M implies |. Integral(M,f).| <= Integral(M,abs f);

theorem :: MESFUNC6:96
  ( ex A be Element of S st A = dom f & f is A-measurable ) & dom f =
dom g & g is_integrable_on M & ( for x be Element of X st x in dom f holds
  |.f.x qua Complex.| <= g.x ) implies
  f is_integrable_on M & Integral(M,abs f) <= Integral(M,g);

theorem :: MESFUNC6:97
  dom f in S & 0 <= r & (for x be object st x in dom f holds f.x = r)
  implies Integral(M,f) = r * M.(dom f);

theorem :: MESFUNC6:98
  f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is
  nonnegative implies f+g is_integrable_on M;

theorem :: MESFUNC6:99
  f is_integrable_on M & g is_integrable_on M implies dom (f+g) in S;

theorem :: MESFUNC6:100
  f is_integrable_on M & g is_integrable_on M implies f+g is_integrable_on M;

theorem :: MESFUNC6:101
  f is_integrable_on M & g is_integrable_on M implies ex E be Element of
  S st E = dom f /\ dom g & Integral(M,f+g)=Integral(M,f|E)+Integral(M,g|E);

theorem :: MESFUNC6:102
  f is_integrable_on M implies r(#)f is_integrable_on M & Integral(M,r
  (#)f) = r * Integral(M,f);

definition
  let X be non empty set;
  let S be SigmaField of X;
  let M be sigma_Measure of S;
  let f be PartFunc of X,REAL;
  let B be Element of S;
  func Integral_on(M,B,f) -> Element of ExtREAL equals
:: MESFUNC6:def 5
  Integral(M,f|B);
end;

theorem :: MESFUNC6:103
  f is_integrable_on M & g is_integrable_on M & B c= dom(f+g) implies f+
g is_integrable_on M & Integral_on(M,B,f+g) = Integral_on(M,B,f) + Integral_on(
  M,B,g);

theorem :: MESFUNC6:104
  f is_integrable_on M implies f|B is_integrable_on M & Integral_on(M,B,
  r(#)f) = r * Integral_on(M,B,f);