:: Measurability of Extended Real Valued Functions
::  by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 6, 2000
:: Copyright (c) 2000-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, SUBSET_1, PARTFUN1, PROB_1, FUNCT_1, RAT_1,
      REAL_1, NAT_1, VALUED_0, RELAT_1, COMPLEX1, ARYTM_3, XXREAL_0, TARSKI,
      VALUED_1, ARYTM_1, MESFUNC1, SUPINF_2, RFUNCT_3, CARD_1, FUNCT_3, PROB_2,
      FINSEQ_1, FUNCOP_1, MEASURE1, SUPINF_1, ORDINAL4, MESFUNC2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3, XCMPLX_0,
      XREAL_0, VALUED_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      NAT_1, WELLORD2, RAT_1, FINSEQ_1, PROB_1, XXREAL_0, SUPINF_1, FUNCOP_1,
      SUPINF_2, FUNCT_3, PROB_2, MEASURE1, MEASURE2, MEASURE3, MEASURE6,
      EXTREAL1, MESFUNC1;
 constructors PARTFUN1, WELLORD2, FUNCT_3, FUNCOP_1, REAL_1, NAT_1, RAT_1,
      FINSEQ_1, PROB_2, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1, SUPINF_1,
      RELSET_1, BINOP_2, NUMBERS;
 registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, RAT_1, MEMBERED,
      FINSEQ_1, MEASURE1, VALUED_0, FUNCT_2, CARD_1, XXREAL_3;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin  :: Finite Valued Function ::

reserve X for non empty set;
reserve e for set;
reserve x for Element of X;
reserve f,g for PartFunc of X,ExtREAL;
reserve S for SigmaField of X;
reserve F for Function of RAT,S;
reserve p,q for Rational;
reserve r for Real;
reserve n,m for Nat;
reserve A,B for Element of S;

definition
  let X, f;
  redefine attr f is real-valued means
:: MESFUNC2:def 1

  for x st x in dom f holds |. f.x .| < +infty;
end;

theorem :: MESFUNC2:1
  f = 1(#)f;

theorem :: MESFUNC2:2
  f is real-valued or g is real-valued implies
  dom (f+g) = dom f /\ dom g & dom (f-g) = dom f /\ dom g;

theorem :: MESFUNC2:3
  for f,g,F,r,A st f is real-valued & g is real-valued &
  (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);

begin  :: Measurability of f+g and f-g ::

theorem :: MESFUNC2:4
  ex F being sequence of RAT st F is one-to-one & dom F = NAT & rng F = RAT;

theorem :: MESFUNC2:5
  for X,Y,Z be non empty set, F be Function of X,Z st X,Y are_equipotent holds
  ex G be Function of Y,Z st rng F = rng G;

theorem :: MESFUNC2:6
  for S,f,g,A st f is A-measurable & g is A-measurable holds
  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 :: MESFUNC2:7
  for f,g,A st f is real-valued & g is real-valued & f is A-measurable &
  g is A-measurable holds f+g is A-measurable;

theorem :: MESFUNC2:8
  for C being non empty set, f1,f2 being PartFunc of C,ExtREAL holds
  f1 - f2 = f1 + (-f2);

theorem :: MESFUNC2:9
  for C being non empty set, f being PartFunc of C,ExtREAL holds -f = (-1)(#)f;

theorem :: MESFUNC2:10
  for C being non empty set, f being PartFunc of C,ExtREAL, r be Real
  st f is real-valued holds r(#)f is real-valued;

theorem :: MESFUNC2:11
  for f,g,A st f is real-valued & g is real-valued & f is A-measurable &
  g is A-measurable & A c= dom g holds f-g is A-measurable;

begin  ::definitions of extended real valued functions max+(f) and max-(f) ::
       :: and their basic properties                                       ::

definition
  let C be non empty set, f be PartFunc of C,ExtREAL;
  func max+(f) -> PartFunc of C,ExtREAL means
:: MESFUNC2:def 2

  dom it = dom f &
  for x be Element of C st x in dom it holds it.x = max(f.x,0.);
  func max-(f) -> PartFunc of C,ExtREAL means
:: MESFUNC2:def 3

  dom it = dom f &
  for x be Element of C st x in dom it holds it.x = max(-(f.x),0.);
end;

theorem :: MESFUNC2:12
  for C being non empty set, f being PartFunc of C,ExtREAL,
  x being Element of C holds 0. <= (max+(f)).x;

theorem :: MESFUNC2:13
  for C being non empty set, f being PartFunc of C,ExtREAL,
  x being Element of C holds 0. <= (max-(f)).x;

theorem :: MESFUNC2:14
  for C being non empty set, f being PartFunc of C,ExtREAL holds
  max-(f) = max+(-f);

theorem :: MESFUNC2:15
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
  st 0. < max+(f).x holds max-(f).x = 0.;

theorem :: MESFUNC2:16
  for C being non empty set, f being PartFunc of C,ExtREAL,
  x being Element of C st 0. < max-(f).x holds max+(f).x = 0.;

theorem :: MESFUNC2:17
  for C being non empty set, f being PartFunc of C,ExtREAL holds
  dom f = dom (max+(f)-max-(f)) & dom f = dom (max+(f)+max-(f));

theorem :: MESFUNC2:18
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
  holds
  (max+(f).x = f.x or max+(f).x = 0.) & (max-(f).x = -(f.x) or max-(f).x = 0.);

theorem :: MESFUNC2:19
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
  st max+(f).x = f.x holds max-(f).x = 0.;

theorem :: MESFUNC2:20
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
  st x in dom f & max+(f).x = 0. holds max-(f).x = -(f.x);

theorem :: MESFUNC2:21
  for C being non empty set, f being PartFunc of C,ExtREAL,
  x being Element of C st max-(f).x = -(f.x) holds max+(f).x = 0.;

theorem :: MESFUNC2:22
  for C being non empty set, f being PartFunc of C,ExtREAL,
  x being Element of C st x in dom f & max-(f).x = 0. holds max+(f).x = f.x;

theorem :: MESFUNC2:23
  for C being non empty set, f being PartFunc of C,ExtREAL holds
  f = max+(f) - max-(f);

theorem :: MESFUNC2:24
  for C being non empty set, f being PartFunc of C,ExtREAL holds
  |.f.| = max+(f) + max-(f);

begin  :: Measurability of max+(f), max-(f) and |.f.|

theorem :: MESFUNC2:25
  f is A-measurable implies max+(f) is A-measurable;

theorem :: MESFUNC2:26
  f is A-measurable & A c= dom f implies max-(f) is A-measurable;

theorem :: MESFUNC2:27
  for f,A st f is A-measurable & A c= dom f holds |.f.| is A-measurable;

begin

definition
  let A,X be set;
  redefine func chi(A,X) -> PartFunc of X,ExtREAL;
end;

theorem :: MESFUNC2:28
  chi(A,X) is real-valued;

theorem :: MESFUNC2:29
  chi(A,X) is B-measurable;

begin  :: Definition and measurability of simple function

registration
  let X be set;
  let S be SigmaField of X;
  cluster disjoint_valued for FinSequence of S;
end;

definition
  let X be set;
  let S be SigmaField of X;
  mode Finite_Sep_Sequence of S is disjoint_valued FinSequence of S;
end;

theorem :: MESFUNC2:30
  for F being Function st F is Finite_Sep_Sequence of S holds
  ex G being Sep_Sequence of S st union rng F = union rng G &
  (for n st n in dom F holds F.n = G.n) &
  for m st not m in dom F holds G.m = {};

theorem :: MESFUNC2:31
  for F being Function st F is Finite_Sep_Sequence of S holds union rng F in S;

definition
  let X be non empty set;
  let S be SigmaField of X;
  let f be PartFunc of X,ExtREAL;
  pred f is_simple_func_in S means
:: MESFUNC2:def 4
  f is real-valued &
  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 :: MESFUNC2:32
  f is real-valued implies rng f is Subset of REAL;

theorem :: MESFUNC2:33
  for F being Relation st F is Finite_Sep_Sequence of S holds
  F|(Seg n) is Finite_Sep_Sequence of S;

theorem :: MESFUNC2:34
  f is_simple_func_in S implies f is A-measurable;