:: Probability on Finite Set and Real Valued Random Variables :: by Hiroyuki Okazaki and Yasunari Shidama :: :: Received March 17, 2009 :: Copyright (c) 2009-2018 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_measurable_on X; 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 definition let Omega,Sigma; mode Real-Valued-Random-Variable of Sigma -> Function of Omega,REAL means :: RANDOM_1:def 2 it is_measurable_on [#]Sigma; 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 3 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 4 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;