:: Probability on Finite Set and Real Valued Random Variables
::  by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received March 17, 2009
:: Copyright (c) 2009-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, REAL_1,
      INTEGRA5, TARSKI, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0, MEASURE6,
      MESFUNC5, FUNCT_3, VALUED_1, MESFUNC1, ARYTM_1, SUPINF_2, MESFUNC2,
      FINSEQ_1, NAT_1, CARD_3, CARD_1, MESFUNC3, INTEGRA1, ZFMISC_1, XXREAL_2,
      VALUED_0, RPR_1, FINSET_1, UPROOTS, RFUNCT_3, PROB_4, COMPLEX1, EQREL_1,
      SEQ_2, ORDINAL2, POWER, RANDOM_1, BSPACE, FUNCT_7, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FINSET_1, CARD_1,
      NUMBERS, XXREAL_3, XREAL_0, XXREAL_0, XCMPLX_0, COMPLEX1, XXREAL_2,
      FUNCT_1, REAL_1, SUPINF_2, RELSET_1, PARTFUN1, VALUED_1, FINSEQ_1,
      RFUNCT_3, NAT_1, FUNCT_2, SEQ_2, RPR_1, PROB_1, PROB_4, MEASURE1,
      EXTREAL1, MESFUNC1, MESFUNC3, MEASURE6, MESFUNC5, MESFUNC6, MESFUNC2,
      RVSUM_1, UPROOTS, MESFUN6C;
 constructors REAL_1, RPR_1, NAT_3, EXTREAL1, POWER, RVSUM_1, MESFUNC6,
      MESFUNC3, MESFUNC5, MEASURE6, MESFUNC2, BINOP_2, INTEGRA2, PROB_4,
      SUPINF_1, UPROOTS, MESFUN6C, MESFUNC1, DOMAIN_1, RELSET_1, COMSEQ_2,
      FUNCT_7;
 registrations SUBSET_1, NAT_1, XREAL_0, XXREAL_0, MEMBERED, ORDINAL1,
      FINSEQ_1, MEASURE1, FUNCT_2, RELAT_1, SEQ_4, FINSET_1, NUMBERS, XCMPLX_0,
      VALUED_0, VALUED_1, RELSET_1, JORDAN5A, XXREAL_3;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

theorem :: RANDOM_1:1
  for X be non empty set, S be SigmaField of X, M be sigma_Measure
  of S, f be PartFunc of X,ExtREAL, E be Element of S, a be Real st f
is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in
  E holds a <= f.x) holds (a qua ExtReal)*(M.E) <= Integral(M,f|E);

theorem :: RANDOM_1:2
  for X be non empty set, S be SigmaField of X, M be sigma_Measure
  of S, f be PartFunc of X,REAL, E be Element of S, a be Real st f
is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in
  E holds a <= f.x) holds (a qua ExtReal)*M.E <= Integral(M,f|E);

theorem :: RANDOM_1:3
  for X be non empty set, S be SigmaField of X, M be sigma_Measure
  of S, f be PartFunc of X,ExtREAL, E be Element of S, a be Real st f
is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in
  E holds f.x <= a) holds Integral(M,f|E) <= (a qua ExtReal)*M.E;

theorem :: RANDOM_1:4
  for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,REAL, E be Element of S, a be Real st f is_integrable_on M &
  E c= dom f & M.E < +infty & (for x be Element of X st x in E holds f.x <= a)
  holds Integral(M,f|E) <=(a qua ExtReal)*M.E;

begin :: Trivial SigmaField and Probability on Finite set

reserve Omega for non empty set;
reserve r for Real;
reserve Sigma for SigmaField of Omega;
reserve P for Probability of Sigma;
reserve E for finite non empty set;

notation
  let E be non empty set;
  synonym Trivial-SigmaField (E) for bool E;
end;

definition
  let E be non empty set;
  redefine func Trivial-SigmaField (E) -> SigmaField of E;
end;

theorem :: RANDOM_1:5
  for Omega be non empty finite set, f be PartFunc of Omega,REAL holds
ex F be Finite_Sep_Sequence of Trivial-SigmaField (Omega), s being FinSequence
of (dom f) st dom f = union (rng F) & dom F = dom (s) & s is one-to-one & rng s
= dom f & len s = card (dom f) & (for k be Nat st k in dom F holds F.k={s.k} )
  & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y
  in F.n holds f.x = f.y;

theorem :: RANDOM_1:6
  for Omega be non empty finite set, f be PartFunc of Omega,REAL
  holds f is_simple_func_in Trivial-SigmaField (Omega) & dom f is Element of
  Trivial-SigmaField (Omega);

theorem :: RANDOM_1:7
  for Omega be non empty finite set, M being sigma_Measure of
Trivial-SigmaField (Omega), f be PartFunc of Omega,REAL st dom f <> {} & M.(dom
  f) < +infty holds f is_integrable_on M;

theorem :: RANDOM_1:8
  for Omega be non empty finite set, f be PartFunc of Omega,REAL
  ex X be Element of Trivial-SigmaField (Omega) st
    dom f = X & f is X-measurable;

theorem :: RANDOM_1:9
  for Omega be non empty finite set, M being sigma_Measure of
Trivial-SigmaField (Omega), f be Function of Omega,REAL, x being FinSequence of
ExtREAL, s being FinSequence of (Omega) st s is one-to-one & rng s = Omega ex F
  be Finite_Sep_Sequence of Trivial-SigmaField (Omega), a being FinSequence of
  REAL st dom f = union (rng F) & dom a = dom s & dom F = dom s & (for k be Nat
  st k in dom F holds F.k={s.k} ) & for n being Nat for x,y being Element of
  Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y;

theorem :: RANDOM_1:10
  for Omega be non empty finite set, M being sigma_Measure of
Trivial-SigmaField (Omega), f be Function of Omega,REAL, x being FinSequence of
  ExtREAL, s being FinSequence of (Omega) st M.Omega < +infty & len x = card (
Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being
Nat st n in dom x
   holds x.n =  (f.(s.n) qua ExtReal) * M.{s.n})
  holds Integral(M,f) = Sum x;

theorem :: RANDOM_1:11
  for Omega be non empty finite set, M being sigma_Measure of
  Trivial-SigmaField (Omega), f be Function of Omega,REAL st M.Omega < +infty
holds ex x being FinSequence of ExtREAL, s being FinSequence of (Omega) st len
  x = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (
for n being Nat st n in dom x
  holds x.n = (f.(s.n) qua ExtReal) * M.{s.n}) & Integral
  (M,f) = Sum x;

theorem :: RANDOM_1:12
  for Omega be non empty finite set, P be Probability of
  Trivial-SigmaField (Omega), f be Function of Omega,REAL, x be FinSequence of
REAL, s be FinSequence of Omega st len x = card (Omega) & s is one-to-one & rng
s = Omega & len s = card (Omega) & (for n being Nat st n in dom x holds x.n = f
  .(s.n) * P.{s.n}) holds Integral(P2M(P),f) =Sum x;

theorem :: RANDOM_1:13
  for Omega be non empty finite set, P be Probability of
  Trivial-SigmaField (Omega), f be Function of Omega,REAL holds ex F being
  FinSequence of REAL, s being FinSequence of Omega st len F = card (Omega) & s
is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in
  dom F holds F.n = f.(s.n) * P.{s.n}) & Integral(P2M(P),f) = Sum F;

theorem :: RANDOM_1:14
  for E be finite non empty set, ASeq being SetSequence of E st
  ASeq is non-ascending
  ex N be Nat st for m be Nat
  st N<=m holds ASeq.N = ASeq.m;

theorem :: RANDOM_1:15
  for E be finite non empty set, ASeq being SetSequence of E st
  ASeq is non-ascending
    ex N be Nat st for m be Nat
  st N<=m holds Intersection ASeq = ASeq.m;

theorem :: RANDOM_1:16
  for E be finite non empty set, ASeq being SetSequence of E st
ASeq is non-descending
 ex N be Nat st for m be Nat st N <= m holds ASeq.N = ASeq.m;

theorem :: RANDOM_1:17
  for E be finite non empty set, ASeq being SetSequence of E st ASeq is
  non-descending holds ex N be Nat st for m be Nat st N<=m holds Union ASeq =
  ASeq.m;

definition
  let E;
  func Trivial-Probability (E) -> Probability of Trivial-SigmaField (E) means
:: RANDOM_1:def 1

  for A be Event of E holds it.A = prob(A);
end;

:: Real-Valued-Random-Variable

registration
  let Omega,Sigma;
  cluster ([#]Sigma)-measurable for Function of Omega,REAL;
end;

definition
  let Omega,Sigma;
  mode Real-Valued-Random-Variable of Sigma is
       ([#]Sigma)-measurable Function of Omega,REAL;
end;

reserve f,g for Real-Valued-Random-Variable of Sigma;

theorem :: RANDOM_1:18
  f+g is Real-Valued-Random-Variable of Sigma;

definition
  let Omega,Sigma,f,g;
  redefine func f + g -> Real-Valued-Random-Variable of Sigma;
end;

theorem :: RANDOM_1:19
  f-g is Real-Valued-Random-Variable of Sigma;

definition
  let Omega,Sigma,f,g;
  redefine func f-g -> Real-Valued-Random-Variable of Sigma;
end;

theorem :: RANDOM_1:20
  for r be Real holds r(#)f is Real-Valued-Random-Variable of Sigma;

definition
  let Omega,Sigma,f;
  let r be Real;
  redefine func r(#)f -> Real-Valued-Random-Variable of Sigma;
end;

theorem :: RANDOM_1:21
  for f,g be PartFunc of Omega,REAL holds (R_EAL f)(#)(R_EAL g) = R_EAL (f(#)g)
;

theorem :: RANDOM_1:22
  f(#)g is Real-Valued-Random-Variable of Sigma;

definition
  let Omega,Sigma,f,g;
  redefine func f(#)g -> Real-Valued-Random-Variable of Sigma;
end;

theorem :: RANDOM_1:23
  for r be Real st 0 <= r & f is nonnegative holds (f
  to_power r) is Real-Valued-Random-Variable of Sigma;

theorem :: RANDOM_1:24
  abs f is Real-Valued-Random-Variable of Sigma;

definition
  let Omega,Sigma,f;
  redefine func abs f -> Real-Valued-Random-Variable of Sigma;
end;

theorem :: RANDOM_1:25
  for r be Real st 0 <= r holds (abs(f) to_power r) is
  Real-Valued-Random-Variable of Sigma;

:: Definition of the Expectations

definition
  let Omega,Sigma,f,P;
  pred f is_integrable_on P means
:: RANDOM_1:def 2
  f is_integrable_on P2M(P);
end;

definition
  let Omega,Sigma,P;
  let f be Real-Valued-Random-Variable of Sigma;
  assume
 f is_integrable_on P;
  func expect (f,P) -> Real equals
:: RANDOM_1:def 3
  Integral(P2M(P),f);
end;

theorem :: RANDOM_1:26
  f is_integrable_on P & g is_integrable_on P implies expect (f+g,
  P) = expect (f,P) + expect (g,P);

theorem :: RANDOM_1:27
 for r being Real holds
  f is_integrable_on P implies expect (r(#)f,P) = r* expect (f,P);

theorem :: RANDOM_1:28
  f is_integrable_on P & g is_integrable_on P implies expect (f-g,P) =
  expect (f,P) - expect (g,P);

theorem :: RANDOM_1:29
  for Omega be non empty finite set, f be Function of Omega,REAL holds
  f is Real-Valued-Random-Variable of Trivial-SigmaField (Omega);

theorem :: RANDOM_1:30
  for Omega be non empty finite set, P be Probability of
  Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of
  Trivial-SigmaField (Omega) holds X is_integrable_on P;

theorem :: RANDOM_1:31
  for Omega be non empty finite set, P be Probability of
  Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of
Trivial-SigmaField (Omega), F being FinSequence of REAL, s being FinSequence of
Omega st len F = card (Omega) & s is one-to-one & rng s = Omega & len s = card
  (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) holds
  expect(X,P) = Sum F;

theorem :: RANDOM_1:32
  for Omega be non empty finite set, P be Probability of
  Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of
Trivial-SigmaField (Omega) ex F being FinSequence of REAL, s being FinSequence
  of Omega st len F = card (Omega) & s is one-to-one & rng s = Omega & len s =
card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) &
  expect(X,P) = Sum F;

theorem :: RANDOM_1:33
  for Omega be non empty finite set, P be Probability of
  Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of
Trivial-SigmaField (Omega) ex F being FinSequence of REAL, s being FinSequence
  of Omega st len F = card (Omega) & s is one-to-one & rng s = Omega & len s =
card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) &
  expect(X,P) = Sum F;

theorem :: RANDOM_1:34
  for Omega be non empty finite set, X be Real-Valued-Random-Variable of
Trivial-SigmaField (Omega), G being FinSequence of REAL, s being FinSequence of
Omega st len G = card (Omega) & s is one-to-one & rng s = Omega & len s = card
(Omega) & (for n being Nat st n in dom G holds G.n = X.(s.n) ) holds expect(X,
  Trivial-Probability (Omega)) = (Sum G) / card (Omega);

theorem :: RANDOM_1:35
  for Omega be non empty finite set, X be Real-Valued-Random-Variable of
  Trivial-SigmaField (Omega)
 ex G being FinSequence of REAL, s being FinSequence of Omega
  st len G = card (Omega) & s is one-to-one & rng s = Omega
& len s = card (Omega) &
(for n being Nat st n in dom G holds G.n = X.(s.n) ) &
  expect(X,Trivial-Probability (Omega)) = (Sum G) / card (Omega);

:: Markov's Theorem

theorem :: RANDOM_1:36
  for X be Real-Valued-Random-Variable of Sigma st 0 < r &
  X is nonnegative & X is_integrable_on P holds
  P.({t where t is Element of Omega : r <= X.t }) <= expect (X,P)/r;