:: RANDOM_1 semantic presentation begin theorem :: RANDOM_1:1 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "a")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" )))))))) ; theorem :: RANDOM_1:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "a")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" )))))))) ; theorem :: RANDOM_1:3 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "a")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E")) ")" ))))))))) ; theorem :: RANDOM_1:4 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "a")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E")) ")" ))))))))) ; begin notationlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; synonym :::"Trivial-SigmaField"::: "E" for :::"bool"::: "E"; end; definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"Trivial-SigmaField"::: redefine func :::"Trivial-SigmaField"::: "E" -> ($#m1_subset_1 :::"SigmaField":::) "of" "E"; end; theorem :: RANDOM_1:5 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")))(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "y"))))) ")" ) ")" ))))) ; theorem :: RANDOM_1:6 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_mesfunc6 :::"is_simple_func_in"::: ) (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")))) ")" ))) ; theorem :: RANDOM_1:7 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M")))))) ; theorem :: RANDOM_1:8 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "X")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "X"))) ")" )))) ; theorem :: RANDOM_1:9 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")))(Bool "ex" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s")))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "y"))))) ")" ) ")" )))))))) ; theorem :: RANDOM_1:10 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "Omega"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "x")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" )) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "x"))))))))) ; theorem :: RANDOM_1:11 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "Omega"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) )(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "x")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "x")))) ")" )))))) ; theorem :: RANDOM_1:12 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" )) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set "(" ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "x"))))))))) ; theorem :: RANDOM_1:13 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set "(" ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F")))) ")" )))))) ; theorem :: RANDOM_1:14 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "ASeq")) "is" ($#v2_prob_1 :::"non-ascending"::: ) )) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "ASeq")) ($#k3_funct_2 :::"."::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "ASeq")) ($#k3_funct_2 :::"."::: ) (Set (Var "m")))))))) ; theorem :: RANDOM_1:15 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "ASeq")) "is" ($#v2_prob_1 :::"non-ascending"::: ) )) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "ASeq"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "ASeq")) ($#k3_funct_2 :::"."::: ) (Set (Var "m")))))))) ; theorem :: RANDOM_1:16 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "ASeq")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "ASeq")) ($#k3_funct_2 :::"."::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "ASeq")) ($#k3_funct_2 :::"."::: ) (Set (Var "m")))))))) ; theorem :: RANDOM_1:17 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "ASeq")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set (Var "ASeq"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "ASeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))))) ; definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; func :::"Trivial-Probability"::: "E" -> ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) "E") means :: RANDOM_1:def 1 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" "E" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))))); end; :: deftheorem defines :::"Trivial-Probability"::: RANDOM_1:def 1 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "E"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_random_1 :::"Trivial-Probability"::: ) (Set (Var "E")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))))) ")" ))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); mode :::"Real-Valued-Random-Variable"::: "of" "Sigma" -> ($#m1_subset_1 :::"Function":::) "of" "Omega" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: RANDOM_1:def 2 (Bool "ex" (Set (Var "X")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "Sigma" "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "Omega") & (Bool it ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "X"))) ")" )); end; :: deftheorem defines :::"Real-Valued-Random-Variable"::: RANDOM_1:def 2 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma"))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set (Var "b3")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "X"))) ")" )) ")" )))); theorem :: RANDOM_1:18 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "f", "g" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); :: original: :::"+"::: redefine func "f" :::"+"::: "g" -> ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" "Sigma"; end; theorem :: RANDOM_1:19 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g"))) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "f", "g" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); :: original: :::"-"::: redefine func "f" :::"-"::: "g" -> ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" "Sigma"; end; theorem :: RANDOM_1:20 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma"))))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "f" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); let "r" be ($#m1_subset_1 :::"Real":::); :: original: :::"(#)"::: redefine func "r" :::"(#)"::: "f" -> ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" "Sigma"; end; theorem :: RANDOM_1:21 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set (Var "f")) ")" ) ($#k5_mesfunc1 :::"(#)"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ))))) ; theorem :: RANDOM_1:22 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g"))) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "f", "g" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); :: original: :::"(#)"::: redefine func "f" :::"(#)"::: "g" -> ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" "Sigma"; end; theorem :: RANDOM_1:23 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "r"))) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma"))))))) ; theorem :: RANDOM_1:24 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "f" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); :: original: :::"|."::: redefine func :::"abs"::: "f" -> ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" "Sigma"; end; theorem :: RANDOM_1:25 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set "(" ($#k7_random_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "r"))) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma"))))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "f" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); let "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); pred "f" :::"is_integrable_on"::: "P" means :: RANDOM_1:def 3 (Bool "f" ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set ($#k2_prob_4 :::"P2M"::: ) "P")); end; :: deftheorem defines :::"is_integrable_on"::: RANDOM_1:def 3 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P"))) "iff" (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")))) ")" ))))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); let "f" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); assume (Bool (Set (Const "f")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Const "P"))) ; func :::"expect"::: "(" "f" "," "P" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RANDOM_1:def 4 (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set "(" ($#k2_prob_4 :::"P2M"::: ) "P" ")" ) "," "f" ")" ); end; :: deftheorem defines :::"expect"::: RANDOM_1:def 4 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "f")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "f")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "f")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set "(" ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")) ")" ) "," (Set (Var "f")) ")" )))))); theorem :: RANDOM_1:26 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "f")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P"))) & (Bool (Set (Var "g")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_random_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "f")) "," (Set (Var "P")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "g")) "," (Set (Var "P")) ")" ")" ))))))) ; theorem :: RANDOM_1:27 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "f")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "f")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set "(" (Set (Var "r")) ($#k5_random_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "f")) "," (Set (Var "P")) ")" ")" )))))))) ; theorem :: RANDOM_1:28 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "f")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P"))) & (Bool (Set (Var "g")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_random_1 :::"-"::: ) (Set (Var "g")) ")" ) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "f")) "," (Set (Var "P")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "g")) "," (Set (Var "P")) ")" ")" ))))))) ; theorem :: RANDOM_1:29 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Var "f")) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega")))))) ; theorem :: RANDOM_1:30 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) "holds" (Bool (Set (Var "X")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P")))))) ; theorem :: RANDOM_1:31 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" )) "holds" (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "X")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F"))))))))) ; theorem :: RANDOM_1:32 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ) & (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "X")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F")))) ")" )))))) ; theorem :: RANDOM_1:33 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ) & (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "X")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F")))) ")" )))))) ; theorem :: RANDOM_1:34 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k2_random_1 :::"Trivial-Probability"::: ) (Set (Var "Omega")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "G")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")) ")" ))))))) ; theorem :: RANDOM_1:35 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Omega")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Omega"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k2_random_1 :::"Trivial-Probability"::: ) (Set (Var "Omega")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "G")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Omega")) ")" ))) ")" ))))) ; theorem :: RANDOM_1:36 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "X")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "X")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")))) "}" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "X")) "," (Set (Var "P")) ")" ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "r"))))))))) ;