:: Random Variables and Product of Probability Spaces
::  by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 1, 2012
:: Copyright (c) 2012-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, MEASURE1, PARTFUN1, SUBSET_1, TARSKI,
      RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0, XXREAL_1, LOPBAN_1, FUNCT_2, DIST_1,
      MSSUBFAM, VALUED_0, MESFUNC1, SUPINF_2, FINSEQ_1, NAT_1, CARD_3, CARD_1,
      ZFMISC_1, RPR_1, FINSET_1, PROB_4, EQREL_1, RANDOM_1, RANDOM_2, RANDOM_3,
      FUNCOP_1, FINANCE1, PBOOLE, REAL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PBOOLE, ENUMSET1,
      FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_1, NAT_1, XREAL_0,
      VALUED_0, FINSEQ_1, RPR_1, SUPINF_2, PROB_1, PROB_2, MEASURE1, MEASURE6,
      MESFUNC1, PROB_4, MESFUNC6, RANDOM_1, DIST_1, RANDOM_2, FINANCE1;
 constructors REAL_1, RPR_1, MESFUNC6, MESFUNC3, DIST_1, MEASURE6, INTEGRA2,
      PROB_4, MESFUNC1, RELSET_1, COMSEQ_2, RANDOM_2, FINANCE1, ENUMSET1;
 registrations XBOOLE_0, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, ORDINAL1,
      MEASURE1, FUNCOP_1, FINANCE1, VALUED_0, FINSEQ_1, FUNCT_2, RELAT_1,
      FINSET_1, NUMBERS, PROB_1, PARTFUN1, RELSET_1, CARD_1, PBOOLE, PRE_CIRC;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Random Variables

reserve Omega, Omega1, Omega2 for non empty set;
reserve Sigma for SigmaField of Omega;
reserve S1 for SigmaField of Omega1;
reserve S2 for SigmaField of Omega2;

theorem :: RANDOM_3:1
  for B being non empty set, f being Function holds
  f " (union B)
  = union the set of all f "Y where Y is Element of B;

theorem :: RANDOM_3:2
  for f be Function of Omega1,Omega2,
  B be SetSequence of Omega2,
  D be SetSequence of Omega1
  st for n be Element of NAT holds D.n = f "(B.n) holds
  f"(Union B) = Union D;

theorem :: RANDOM_3:3
  for f be Function of Omega1,Omega2,
  B be SetSequence of Omega2,
  D be SetSequence of Omega1
  st for n be Element of NAT holds D.n = f "(B.n) holds
  f"(Intersection B) = Intersection D;

theorem :: RANDOM_3:4
  for F being Function of Omega,REAL,
  r being Real
  st F is Real-Valued-Random-Variable of Sigma
  holds F"(].-infty,r.[) in Sigma;

theorem :: RANDOM_3:5
  for F being Function of Omega,REAL st
  F is Real-Valued-Random-Variable of Sigma holds
  { x where x is Element of Borel_Sets : F"x is Element of Sigma }
  is SigmaField of REAL;

theorem :: RANDOM_3:6
  for f being Function of Omega,REAL
  st f is Real-Valued-Random-Variable of Sigma holds
  { x where x is Element of Borel_Sets : f"x is Element of Sigma }
  = Borel_Sets;

theorem :: RANDOM_3:7
  for f being Function of Omega,REAL holds
  f is (Sigma,Borel_Sets)-random_variable-like iff
  f is Real-Valued-Random-Variable of Sigma;

theorem :: RANDOM_3:8
  for f being Function of Omega,REAL holds
  set_of_random_variables_on (Sigma,Borel_Sets) =
  Real-Valued-Random-Variables-Set Sigma;

definition
::$CD
end;

registration
  let Omega1, Omega2, S1, S2;
  cluster (S1,S2)-random_variable-like for Function of Omega1, Omega2;
end;

definition
  let Omega1, Omega2, S1, S2;
  mode random_variable of S1,S2 is
    (S1,S2)-random_variable-like Function of Omega1, Omega2;
end;

theorem :: RANDOM_3:9
  for f being Function of Omega,REAL holds
  f is random_variable of Sigma, Borel_Sets iff
  f is Real-Valued-Random-Variable of Sigma;

definition
  let F be Function;
  attr F is random_variable_family-like means
:: RANDOM_3:def 2
  for x be set st x in dom F
  ex Omega1, Omega2 be non empty set,
  S1 be SigmaField of Omega1, S2 be SigmaField of Omega2,
  f be random_variable of S1,S2 st F.x = f;
end;

registration
  cluster random_variable_family-like for Function;
end;

definition
  mode random_variable_family is random_variable_family-like Function;
end;

reserve F for random_variable of S1,S2;

definition
  let Y be non empty set;
  let S be SigmaField of Y;
  let F be Function;
  attr F is S-Measure_valued means
:: RANDOM_3:def 3
  for x be set st x in dom F ex M being sigma_Measure of S st F.x = M;
end;

registration
  let Y be non empty set;
  let S be SigmaField of Y;
  cluster S-Measure_valued for Function;
end;

definition
  let Y be non empty set;
  let S be SigmaField of Y;
  let F be Function;
  attr F is S-Probability_valued means
:: RANDOM_3:def 4
  for x be set st x in dom F ex P be Probability of S st F.x = P;
end;

registration
  let Y be non empty set;
  let S be SigmaField of Y;
  cluster S-Probability_valued for Function;
end;

registration
  let X,Y be non empty set;
  let S be SigmaField of Y;
  cluster X-defined for S-Probability_valued Function;
end;

registration
  let X, Y be non empty set;
  let S be SigmaField of Y;
  cluster total for X-defined S-Probability_valued Function;
end;

registration
  let Y be non empty set, S be SigmaField of Y;
  cluster S-Probability_valued -> S-Measure_valued for Function;
end;

definition
  let Y be non empty set;
  let S be SigmaField of Y;
  let F be Function;
  attr F is S-Random-Variable-Family means
:: RANDOM_3:def 5
  for x be set st x in dom F
  ex Z be Real-Valued-Random-Variable of S st F.x = Z;
end;

registration
  let Y be non empty set;
  let S be SigmaField of Y;
  cluster S-Random-Variable-Family for Function;
end;

theorem :: RANDOM_3:10
  for y being Element of S2 st y <> {} holds
  {z where z is Element of Omega1: F.z is Element of y} = F"y;

theorem :: RANDOM_3:11
  for F be random_variable of S1,S2 holds
  {x where x is Subset of Omega1 : ex y be Element of S2 st x =F"y } c= S1 &
  {x where x is Subset of Omega1 : ex y be Element of S2 st x =F"y }
  is SigmaField of Omega1;

definition
  let Omega1,Omega2,S1,S2;
  let M be Measure of S1,
  F be random_variable of S1,S2;
  func image_measure(F,M) -> Measure of S2 means
:: RANDOM_3:def 6
  for y be Element of S2 holds it.y = M.(F"y);
end;

registration
  let Omega1,Omega2,S1,S2;
  let M be sigma_Measure of S1,
      F be random_variable of S1,S2;
  cluster image_measure(F,M) -> sigma-additive;
end;

theorem :: RANDOM_3:12
  for P being Probability of S1,
  F being random_variable of S1,S2 holds
  (image_measure(F,P2M(P))).Omega2 = 1;

definition
  let Omega1,Omega2,S1,S2;
  let P be Probability of S1,
  F be random_variable of S1,S2;
  func probability(F,P) -> Probability of S2 equals
:: RANDOM_3:def 7
  M2P(image_measure(F,P2M(P)));
end;

theorem :: RANDOM_3:13
  for P being Probability of S1,
  F being random_variable of S1,S2 holds
  probability(F,P) = image_measure(F,P2M(P));

theorem :: RANDOM_3:14
  for P being Probability of S1,
  F be random_variable of S1,S2 holds
  for y be set st y in S2 holds (probability(F,P)).y = P.(F"y);

theorem :: RANDOM_3:15
  for F be Function of Omega1, Omega2
  holds F is random_variable of
  Trivial-SigmaField Omega1, Trivial-SigmaField Omega2;

theorem :: RANDOM_3:16
  for S be non empty set,
  F be non empty FinSequence of S holds
  F is random_variable of
  Trivial-SigmaField (Seg len F),Trivial-SigmaField (S);

theorem :: RANDOM_3:17
  for V,S be finite non empty set,
  G be random_variable of Trivial-SigmaField (V),Trivial-SigmaField (S)
  holds
  for y be set st y in Trivial-SigmaField (S) holds
  (probability(G,Trivial-Probability V)).y = card(G"y)/card(V);

theorem :: RANDOM_3:18
  for S be finite non empty set,
  s be non empty FinSequence of S
  holds
  ex G be random_variable of
  Trivial-SigmaField (Seg len s),Trivial-SigmaField (S)
  st G = s &
 for  x be set st x in S
  holds
  (probability(G,Trivial-Probability (Seg len s))).{x}
  = FDprobability (x,s);

begin :: Product of Probability Spaces

registration
  let D be non-empty ManySortedSet of NAT;
  let n be Nat;
  cluster D.n -> non empty;
end;

definition
  let S, F be ManySortedSet of NAT;
  attr F is S -SigmaField_sequence-like means
:: RANDOM_3:def 8
  for n be Nat holds F.n is SigmaField of S.n;
end;

registration
  let S be ManySortedSet of NAT;
  cluster S-SigmaField_sequence-like for ManySortedSet of NAT;
end;

definition
  let D be ManySortedSet of NAT;
  mode SigmaField_sequence of D is
    D-SigmaField_sequence-like ManySortedSet of NAT;
end;

definition
  let D be ManySortedSet of NAT;
  let S be SigmaField_sequence of D;
  let n be Nat;
  redefine func S.n -> SigmaField of D.n;
end;

definition
  let D be non-empty ManySortedSet of NAT;
  let S be SigmaField_sequence of D;
  let M be ManySortedSet of NAT;
  attr M is S-Probability_sequence-like means
:: RANDOM_3:def 9
  for n be Nat holds M.n is Probability of S.n;
end;

registration
  let D be non-empty ManySortedSet of NAT;
  let S be SigmaField_sequence of D;
  cluster S-Probability_sequence-like for ManySortedSet of NAT;
end;

definition
  let D be non-empty ManySortedSet of NAT;
  let S be SigmaField_sequence of D;
  mode Probability_sequence of S is
    S-Probability_sequence-like ManySortedSet of NAT;
end;

definition
  let D be non-empty ManySortedSet of NAT;
  let S be SigmaField_sequence of D;
  let P be Probability_sequence of S;
  let n be Nat;
  redefine func P.n -> Probability of (S.n);
end;

definition
  let D be ManySortedSet of NAT;
  func Product_dom(D) -> ManySortedSet of NAT means
:: RANDOM_3:def 10
  it.0 = D.0 & for i be Nat holds it.(i+1) = [:it.i, D.(i+1) :];
end;

theorem :: RANDOM_3:19
  for D be ManySortedSet of NAT holds
  (Product_dom(D)).0 = D.0 &
  (Product_dom(D)).1 = [:D.0,D.1:] &
  (Product_dom(D)).2 = [:D.0,D.1,D.2:] &
  (Product_dom(D)).3 = [:D.0,D.1,D.2,D.3:];

registration
  let D be non-empty ManySortedSet of NAT;
  cluster Product_dom(D) -> non-empty;
end;

registration
  let D be finite-yielding ManySortedSet of NAT;
  cluster Product_dom(D) -> finite-yielding;
end;

definition
  let Omega,Sigma;
  let P be set;
  assume  P is Probability of Sigma;
  func modetrans(P,Sigma) -> Probability of Sigma equals
:: RANDOM_3:def 11

  P;
end;

definition
  let D be finite-yielding non-empty ManySortedSet of NAT;
  func Trivial-SigmaField_sequence(D) -> SigmaField_sequence of D means
:: RANDOM_3:def 12

  for n be Nat holds it.n = Trivial-SigmaField (D.n);
end;

definition
  let D be finite-yielding non-empty ManySortedSet of NAT;
  let P be Probability_sequence of Trivial-SigmaField_sequence(D);
  let n be Nat;
  redefine func P.n -> Probability of Trivial-SigmaField(D.n);
end;

definition
  let D be finite-yielding non-empty ManySortedSet of NAT;
  let P be Probability_sequence of Trivial-SigmaField_sequence(D);
  func Product-Probability(P,D) -> ManySortedSet of NAT means
:: RANDOM_3:def 13
  it.0 = P.0 & for i be Nat holds
  it.(i+1) = Product-Probability
  ( (Product_dom(D)).i,D.(i+1),
  modetrans(it.i,Trivial-SigmaField ((Product_dom(D)).i)), P.(i+1));
end;

theorem :: RANDOM_3:20
  for D be finite-yielding non-empty ManySortedSet of NAT,
  P be Probability_sequence of Trivial-SigmaField_sequence(D),
  n be Nat holds
  Product-Probability(P,D).n is
  Probability of Trivial-SigmaField ((Product_dom(D)).n);

theorem :: RANDOM_3:21
  for D be finite-yielding non-empty ManySortedSet of NAT,
  P be Probability_sequence of Trivial-SigmaField_sequence(D),
  n be Nat holds
  ex Pn be Probability of Trivial-SigmaField ((Product_dom(D)).n)
  st Pn = Product-Probability(P,D).n
  & Product-Probability(P,D).(n+1)
  = Product-Probability ( (Product_dom(D)).n,D.(n+1),Pn,P.(n+1));

theorem :: RANDOM_3:22
  for D be finite-yielding non-empty ManySortedSet of NAT,
  P be Probability_sequence of Trivial-SigmaField_sequence(D) holds
  Product-Probability(P,D).0 = P.0 &
  Product-Probability(P,D).1 =
  Product-Probability(D.0,D.1,P.0,P.1) &
  (ex P1 be Probability of Trivial-SigmaField ([:D.0,D.1:]) st
  P1 = Product-Probability(P,D).1 &
  Product-Probability(P,D).2 =
  Product-Probability([:D.0,D.1:],D.2,P1,P.2) ) &
  (ex P2 be Probability of Trivial-SigmaField ([:D.0,D.1,D.2:]) st
  P2 = Product-Probability(P,D).2 &
  Product-Probability(P,D).3 =
  Product-Probability([:D.0,D.1,D.2:],D.3,P2,P.3)) &
  (ex P3 be Probability of Trivial-SigmaField ([:D.0,D.1,D.2,D.3:]) st
  P3 = Product-Probability(P,D).3 &
  Product-Probability(P,D).4 =
  Product-Probability([:D.0,D.1,D.2,D.3:],D.4,P3,P.4));