:: FINANCE1 semantic presentation begin notationlet "a", "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; synonym :::"halfline_fin"::: "(" "a" "," "r" ")" for :::"[.":::"a" "," "r":::".[":::; end; definitionlet "a", "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"halfline_fin"::: redefine func :::"halfline_fin"::: "(" "a" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: FINANCE1:1 (Bool "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "k")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "k")) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: FINANCE1:2 (Bool "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "k")) ($#k2_rcomp_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "k")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) ; definitionlet "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"half_open_sets"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"SetSequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: FINANCE1:def 1 (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_finance1 :::"halfline_fin"::: ) "(" "a" "," (Set "(" "b" ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_finance1 :::"halfline_fin"::: ) "(" "a" "," (Set "(" "b" ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"half_open_sets"::: FINANCE1:def 1 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_finance1 :::"half_open_sets"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_finance1 :::"halfline_fin"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_finance1 :::"halfline_fin"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" )) ")" ) ")" ) ")" ))); definitionmode :::"pricefunction"::: -> ($#m1_subset_1 :::"Real_Sequence":::) means :: FINANCE1:def 2 (Bool "(" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"pricefunction"::: FINANCE1:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b1")) "is" ($#m1_finance1 :::"pricefunction"::: ) ) "iff" (Bool "(" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" )); notationlet "phi", "jpi" be ($#m1_subset_1 :::"Real_Sequence":::); synonym :::"ElementsOfBuyPortfolio"::: "(" "phi" "," "jpi" ")" for "phi" :::"(#)"::: "jpi"; end; definitionlet "phi", "jpi" be ($#m1_subset_1 :::"Real_Sequence":::); :: original: :::"ElementsOfBuyPortfolio"::: redefine func :::"ElementsOfBuyPortfolio"::: "(" "phi" "," "jpi" ")" -> ($#m1_subset_1 :::"Real_Sequence":::); end; definitionlet "d" be ($#m1_hidden :::"Nat":::); let "phi", "jpi" be ($#m1_subset_1 :::"Real_Sequence":::); func :::"BuyPortfolioExt"::: "(" "phi" "," "jpi" "," "d" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: FINANCE1:def 3 (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k3_finance1 :::"ElementsOfBuyPortfolio"::: ) "(" "phi" "," "jpi" ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) "d"); func :::"BuyPortfolio"::: "(" "phi" "," "jpi" "," "d" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: FINANCE1:def 4 (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set "(" ($#k3_finance1 :::"ElementsOfBuyPortfolio"::: ) "(" "phi" "," "jpi" ")" ")" ) ($#k10_nat_1 :::"^\"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" "d" ($#k10_binop_2 :::"-"::: ) (Num 1) ")" )); end; :: deftheorem defines :::"BuyPortfolioExt"::: FINANCE1:def 3 : (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "phi")) "," (Set (Var "jpi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set ($#k4_finance1 :::"BuyPortfolioExt"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k3_finance1 :::"ElementsOfBuyPortfolio"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")))))); :: deftheorem defines :::"BuyPortfolio"::: FINANCE1:def 4 : (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "phi")) "," (Set (Var "jpi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set ($#k5_finance1 :::"BuyPortfolio"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set "(" ($#k3_finance1 :::"ElementsOfBuyPortfolio"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) ")" ")" ) ($#k10_nat_1 :::"^\"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "d")) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ))))); definitionlet "Omega", "Omega2" be ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "Sigma2" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega2")); let "X" be ($#m1_hidden :::"Function":::); pred "X" :::"is_random_variable_on"::: "Sigma" "," "Sigma2" means :: FINANCE1:def 5 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "Sigma2" "holds" (Bool "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element"::: ) "of" "Omega" : (Bool (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "x"))) "}" "is" ($#m2_subset_1 :::"Element"::: ) "of" "Sigma")); end; :: deftheorem defines :::"is_random_variable_on"::: FINANCE1:def 5 : (Bool "for" (Set (Var "Omega")) "," (Set (Var "Omega2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "Sigma2")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega2")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_finance1 :::"is_random_variable_on"::: ) (Set (Var "Sigma")) "," (Set (Var "Sigma2"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma2")) "holds" (Bool "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "x"))) "}" "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma")))) ")" ))))); definitionlet "Omega", "Omega2" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F2" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega2")); func :::"set_of_random_variables_on"::: "(" "F" "," "F2" ")" -> ($#m1_hidden :::"set"::: ) equals :: FINANCE1:def 6 "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" "Omega" "," "Omega2" : (Bool (Set (Var "f")) ($#r1_finance1 :::"is_random_variable_on"::: ) "F" "," "F2") "}" ; end; :: deftheorem defines :::"set_of_random_variables_on"::: FINANCE1:def 6 : (Bool "for" (Set (Var "Omega")) "," (Set (Var "Omega2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega2")) "holds" (Bool (Set ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Var "F")) "," (Set (Var "F2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set (Var "Omega2")) : (Bool (Set (Var "f")) ($#r1_finance1 :::"is_random_variable_on"::: ) (Set (Var "F")) "," (Set (Var "F2"))) "}" )))); registrationlet "Omega", "Omega2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F2" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega2")); cluster (Set ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" "F" "," "F2" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "Omega", "Omega2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F2" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega2")); let "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "X")) ($#r1_hidden :::"="::: ) (Set ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Const "F")) "," (Set (Const "F2")) ")" )) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); func :::"Change_Element_to_Func"::: "(" "F" "," "F2" "," "k" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Omega" "," "Omega2" equals :: FINANCE1:def 7 "k"; end; :: deftheorem defines :::"Change_Element_to_Func"::: FINANCE1:def 7 : (Bool "for" (Set (Var "Omega")) "," (Set (Var "Omega2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega2")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Var "F")) "," (Set (Var "F2")) ")" ))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k7_finance1 :::"Change_Element_to_Func"::: ) "(" (Set (Var "F")) "," (Set (Var "F2")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "k")))))))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); func :::"ElementsOfPortfolioValueProb_fut"::: "(" "F" "," "k" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Omega" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: FINANCE1:def 8 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Omega" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_finance1 :::"Change_Element_to_Func"::: ) "(" "F" "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) "," "k" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))))); end; :: deftheorem defines :::"ElementsOfPortfolioValueProb_fut"::: FINANCE1:def 8 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_finance1 :::"ElementsOfPortfolioValueProb_fut"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" )) "iff" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) "holds" (Bool (Set (Set (Var "b5")) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_finance1 :::"Change_Element_to_Func"::: ) "(" (Set (Var "F")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) "," (Set (Var "k")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))))) ")" )))))); definitionlet "p" be ($#m1_hidden :::"Nat":::); let "Omega", "Omega2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F2" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega2")); let "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "X")) ($#r1_hidden :::"="::: ) (Set ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Const "F")) "," (Set (Const "F2")) ")" )) ; let "G" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Const "X")); func :::"Element_Of"::: "(" "F" "," "F2" "," "G" "," "p" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Omega" "," "Omega2" equals :: FINANCE1:def 9 (Set "G" ($#k1_funct_1 :::"."::: ) "p"); end; :: deftheorem defines :::"Element_Of"::: FINANCE1:def 9 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Omega")) "," (Set (Var "Omega2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega2")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Var "F")) "," (Set (Var "F2")) ")" ))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) "holds" (Bool (Set ($#k9_finance1 :::"Element_Of"::: ) "(" (Set (Var "F")) "," (Set (Var "F2")) "," (Set (Var "G")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "p")))))))))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "Omega")); let "G" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Const "X")); let "phi" be ($#m1_subset_1 :::"Real_Sequence":::); func :::"ElementsOfPortfolioValue_fut"::: "(" "phi" "," "F" "," "w" "," "G" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: FINANCE1:def 10 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_finance1 :::"ElementsOfPortfolioValueProb_fut"::: ) "(" "F" "," (Set "(" "G" ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) "w" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" "phi" ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"ElementsOfPortfolioValue_fut"::: FINANCE1:def 10 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) (Bool "for" (Set (Var "phi")) "," (Set (Var "b7")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k10_finance1 :::"ElementsOfPortfolioValue_fut"::: ) "(" (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "w")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b7")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_finance1 :::"ElementsOfPortfolioValueProb_fut"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "w")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "phi")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))))); definitionlet "d" be ($#m1_hidden :::"Nat":::); let "phi" be ($#m1_subset_1 :::"Real_Sequence":::); let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Const "X")); let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "Omega")); func :::"PortfolioValueFutExt"::: "(" "d" "," "phi" "," "F" "," "G" "," "w" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: FINANCE1:def 11 (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k10_finance1 :::"ElementsOfPortfolioValue_fut"::: ) "(" "phi" "," "F" "," "w" "," "G" ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) "d"); func :::"PortfolioValueFut"::: "(" "d" "," "phi" "," "F" "," "G" "," "w" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: FINANCE1:def 12 (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set "(" ($#k10_finance1 :::"ElementsOfPortfolioValue_fut"::: ) "(" "phi" "," "F" "," "w" "," "G" ")" ")" ) ($#k10_nat_1 :::"^\"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" "d" ($#k10_binop_2 :::"-"::: ) (Num 1) ")" )); end; :: deftheorem defines :::"PortfolioValueFutExt"::: FINANCE1:def 11 : (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k11_finance1 :::"PortfolioValueFutExt"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k10_finance1 :::"ElementsOfPortfolioValue_fut"::: ) "(" (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "w")) "," (Set (Var "G")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))))))))))); :: deftheorem defines :::"PortfolioValueFut"::: FINANCE1:def 12 : (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k12_finance1 :::"PortfolioValueFut"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set "(" ($#k10_finance1 :::"ElementsOfPortfolioValue_fut"::: ) "(" (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "w")) "," (Set (Var "G")) ")" ")" ) ($#k10_nat_1 :::"^\"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "d")) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" )))))))))); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ); end; theorem :: FINANCE1:3 (Bool "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "k")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) )) & (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "k")) ($#k2_rcomp_1 :::".["::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) )) ")" )) ; theorem :: FINANCE1:4 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "k2")) "," (Set (Var "k1")) ($#k3_rcomp_1 :::".["::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ))) ; theorem :: FINANCE1:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k2_finance1 :::"half_open_sets"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ))) ; theorem :: FINANCE1:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k2_finance1 :::"half_open_sets"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: FINANCE1:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set "(" ($#k2_finance1 :::"half_open_sets"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) )))) ; theorem :: FINANCE1:8 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "k2")) "," (Set (Var "k1")) ($#k1_rcomp_1 :::".]"::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ))) ; theorem :: FINANCE1:9 (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 "X")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_finance1 :::"is_random_variable_on"::: ) (Set (Var "Sigma")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) "}" "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma"))) & (Bool "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) "}" "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k2")))) "holds" (Bool "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool "(" (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w")))) & (Bool (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k2"))) ")" ) "}" "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma"))) ")" ) & (Bool "(" "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2")))) "holds" (Bool "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool "(" (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w")))) & (Bool (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2"))) ")" ) "}" "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma"))) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k11_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "X")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" ) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k14_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "X")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) "}" ) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k10_relat_1 :::"eq_dom"::: ) "(" (Set (Var "X")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "}" ) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k10_relat_1 :::"eq_dom"::: ) "(" (Set (Var "X")) "," (Set (Var "r")) ")" ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma"))) ")" ) ")" )))) ; theorem :: FINANCE1:10 (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 "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "Omega")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "s"))) ($#r1_finance1 :::"is_random_variable_on"::: ) (Set (Var "Sigma")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ))))) ; theorem :: FINANCE1:11 (Bool "for" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "jpi")) "being" ($#m1_finance1 :::"pricefunction"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_finance1 :::"BuyPortfolioExt"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "phi")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k5_finance1 :::"BuyPortfolio"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ")" )))))) ; theorem :: FINANCE1:12 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Var "F")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) ")" ")" ) "st" (Bool (Bool (Set ($#k9_finance1 :::"Element_Of"::: ) "(" (Set (Var "F")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) "," (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "Omega")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" )))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k11_finance1 :::"PortfolioValueFutExt"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "phi")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k12_finance1 :::"PortfolioValueFut"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ")" )))))))))) ; theorem :: FINANCE1:13 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k19_binop_2 :::"-"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "jpi")) "being" ($#m1_finance1 :::"pricefunction"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Var "F")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) ")" ")" ) "st" (Bool (Bool (Set ($#k9_finance1 :::"Element_Of"::: ) "(" (Set (Var "F")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) "," (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "Omega")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" )))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set ($#k4_finance1 :::"BuyPortfolioExt"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k11_finance1 :::"PortfolioValueFutExt"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k12_finance1 :::"PortfolioValueFut"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k5_finance1 :::"BuyPortfolio"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ")" ) ")" ))))))))))) ; theorem :: FINANCE1:14 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k19_binop_2 :::"-"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "jpi")) "being" ($#m1_finance1 :::"pricefunction"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Var "F")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) ")" ")" ) "st" (Bool (Bool (Set ($#k9_finance1 :::"Element_Of"::: ) "(" (Set (Var "F")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) "," (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "Omega")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ))) & (Bool (Set ($#k4_finance1 :::"BuyPortfolioExt"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set ($#k11_finance1 :::"PortfolioValueFutExt"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ($#r1_tarski :::"c="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set ($#k12_finance1 :::"PortfolioValueFut"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k5_finance1 :::"BuyPortfolio"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ")" ))) "}" ) & (Bool "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set ($#k11_finance1 :::"PortfolioValueFutExt"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ($#r1_tarski :::"c="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set ($#k12_finance1 :::"PortfolioValueFut"::: ) "(" (Set (Var "d")) "," (Set (Var "phi")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k5_finance1 :::"BuyPortfolio"::: ) "(" (Set (Var "phi")) "," (Set (Var "jpi")) "," (Set (Var "d")) ")" ")" ))) "}" ) ")" )))))))) ; theorem :: FINANCE1:15 (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_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_finance1 :::"is_random_variable_on"::: ) (Set (Var "Sigma")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set ($#k4_prob_1 :::"[#]"::: ) (Set (Var "Sigma")))) & (Bool (Set (Var "f")) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma"))) ")" )))) ; theorem :: FINANCE1:16 (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")) "holds" (Bool (Set ($#k6_finance1 :::"set_of_random_variables_on"::: ) "(" (Set (Var "Sigma")) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) (Set (Var "Sigma")))))) ;