Theory Expected_Utility

(* License: LGPL *)

theory Expected_Utility
imports
  Neumann_Morgenstern_Utility_Theorem
begin

section ‹ Definition of vNM-utility function ›

text ‹ We define a version of the vNM Utility function using the locale mechanism. 
       Currently this definition and system U have no proven relation yet. ›

text ‹ Important: u is actually not the von Neuman Utility Function, 
       but a Bernoulli Utility Function. The Expected value p 
       given u is the von Neumann Utility Function. ›

locale vNM_utility =
  fixes outcomes :: "'a set"
  fixes relation :: "'a pmf relation"
  fixes u :: "'a ⇒ real"
  assumes "relation ⊆ (lotteries_on outcomes × lotteries_on outcomes)"
  assumes "⋀p q.  p ∈ lotteries_on outcomes ⟹ 
                  q ∈ lotteries_on outcomes ⟹ 
        p ≽[relation] q ⟷ measure_pmf.expectation p u ≥ measure_pmf.expectation q u"
begin

lemma vNM_utilityD:
  shows "relation ⊆ (lotteries_on outcomes × lotteries_on outcomes)"
    and "p ∈ lotteries_on outcomes ⟹ q ∈ lotteries_on outcomes ⟹ 
    p ≽[relation] q ⟷ measure_pmf.expectation p u ≥ measure_pmf.expectation q u"
  using vNM_utility_axioms vNM_utility_def by (blast+)

lemma not_outside:
  assumes "p ≽[relation] q"
  shows "p ∈ lotteries_on outcomes"
    and "q ∈ lotteries_on outcomes"
proof (goal_cases)
  case 1
  then show ?case
    by (meson assms contra_subsetD mem_Sigma_iff vNM_utility_axioms vNM_utility_def)
next
  case 2
  then show ?case
    by (metis assms mem_Sigma_iff subsetCE vNM_utility_axioms vNM_utility_def)
qed

lemma utility_ge:
  assumes "p ≽[relation] q"
  shows "measure_pmf.expectation p u ≥ measure_pmf.expectation q u"
  using assms vNM_utility_axioms vNM_utility_def
  by (metis (no_types, lifting) not_outside(1) not_outside(2))

end (* vNM_Utility *)

sublocale vNM_utility ⊆ ordinal_utility "(lotteries_on outcomes)" relation "(λp. measure_pmf.expectation p u)"
proof (standard, goal_cases)
  case (2 x y)
  then show ?case
    using not_outside(1) by blast
next
  case (3 x y)
  then show ?case 
    by (auto simp add: not_outside(2))
qed (metis (mono_tags, lifting) vNM_utility_axioms vNM_utility_def)

context vNM_utility
begin

lemma strict_preference_iff_strict_utility:
 assumes "p ∈ lotteries_on outcomes" 
 assumes "q ∈ lotteries_on outcomes"
 shows "p ≻[relation] q ⟷ measure_pmf.expectation p u > measure_pmf.expectation q u"
  by (meson assms(1) assms(2) less_eq_real_def not_le util_def)

lemma pos_distrib_left:
  assumes "c > 0"
  shows "(∑z∈outcomes. pmf q z * (c * u z)) = c * (∑z∈outcomes. pmf q z * (u z))"
proof -
  have "(∑z∈outcomes. pmf q z * (c * u z)) = (∑z∈outcomes. pmf q z * c * u z)"
    by (simp add: ab_semigroup_mult_class.mult_ac(1))
  also have "... = (∑z∈outcomes. c * pmf q z *  u z)"
    by (simp add: mult.commute)
  also have "... = c * (∑z∈outcomes. pmf q z *  u z)"
    by (simp add: ab_semigroup_mult_class.mult_ac(1) sum_distrib_left)
  finally show ?thesis .
qed

lemma sum_pmf_util_commute:
  "(∑a∈outcomes. pmf p a * u a) = (∑a∈outcomes. u a * pmf p a)"
  by (simp add: mult.commute)



section ‹ Finite outcomes ›
context
  assumes fnt: "finite outcomes"
begin

lemma sum_equals_pmf_expectation:
  assumes "p ∈ lotteries_on outcomes"
  shows"(∑z∈outcomes. (pmf p z) * (u z)) = measure_pmf.expectation p u"
proof -
  have fnt: "finite outcomes"
    by (simp add: vNM_utilityD(1) fnt)
  have "measure_pmf.expectation p u = (∑a∈outcomes. pmf p a * u a)"
    using support_in_outcomes assms fnt integral_measure_pmf_real
      sum_pmf_util_commute by fastforce
  then show ?thesis
    using real_scaleR_def by presburger
qed

lemma expected_utility_weak_preference:
  assumes "p ∈ lotteries_on outcomes" 
    and "q ∈ lotteries_on outcomes"
  shows   "p ≽[relation] q ⟷ (∑z∈outcomes. (pmf p z) * (u z)) ≥ (∑z∈outcomes. (pmf q z) * (u z))"
  using sum_equals_pmf_expectation[of p, OF assms(1)] 
        sum_equals_pmf_expectation[of q, OF assms(2)]
   vNM_utility_def assms(1) assms(2) util_def_conf by presburger

lemma diff_leq_zero_weak_preference:
  assumes "p ∈ lotteries_on outcomes"
    and "q ∈ lotteries_on outcomes"
  shows "p ≽ q ⟷ ((∑a∈outcomes. pmf q a * u a) - (∑a∈outcomes. pmf p a * u a) ≤ 0)"
  using assms(1) assms(2) diff_le_0_iff_le
  by (metis (mono_tags, lifting) expected_utility_weak_preference)

lemma expected_utility_strict_preference:
  assumes "p ∈ lotteries_on outcomes" 
    and "q ∈ lotteries_on outcomes"
  shows   "p ≻[relation] q ⟷ measure_pmf.expectation p u > measure_pmf.expectation q u"
  using assms expected_utility_weak_preference less_eq_real_def not_le
  by (metis (no_types, lifting) util_def_conf)

lemma scale_pos_left: 
  assumes "c > 0" 
  shows "vNM_utility outcomes relation (λx. c * u x)"
proof(standard, goal_cases)
  case 1
  then show ?case
    using vNM_utility_axioms vNM_utility_def by blast
next
  case (2 p q)
  have "q ∈ lotteries_on outcomes" and "p ∈ lotteries_on outcomes"
    using "2"(2) by (simp add: fnt "2"(1))+
  then have *: "p ≽ q = (measure_pmf.expectation q u ≤ measure_pmf.expectation p u)"
    using expected_utility_weak_preference[of p q] assms by blast
  have dist_c: "(∑z∈outcomes. (pmf q z) * (c * u z)) = c * (∑z∈outcomes. (pmf q z) * (u z))"
    using pos_distrib_left[of c q] assms by blast
  have dist_c': "(∑z∈outcomes. (pmf p z) * (c * u z)) = c * (∑z∈outcomes. (pmf p z) * (u z))"
    using pos_distrib_left[of c p] assms by blast
  have "p ≽ q ⟷ ((∑z∈outcomes. (pmf q z) * (c * u z)) ≤ (∑z∈outcomes. (pmf p z) * (c * u z)))"
  proof (rule iffI)
    assume "p ≽ q"
    then have "(∑z∈outcomes. pmf q z * (u z)) ≤ (∑z∈outcomes. pmf p z * (u z))" 
      using utility_ge
      using "2"(1) "2"(2) sum_equals_pmf_expectation by presburger
    then show "(∑z∈outcomes. pmf q z * (c * u z)) ≤ (∑z∈outcomes. pmf p z * (c * u z))" 
      using dist_c dist_c'
      by (simp add: assms)
  next
    assume "(∑z∈outcomes. pmf q z * (c * u z)) ≤ (∑z∈outcomes. pmf p z * (c * u z))"
    then have "(∑z∈outcomes. pmf q z * (u z)) ≤ (∑z∈outcomes. pmf p z * (u z))"
      using "2"(1) mult_le_cancel_left_pos assms by (simp add: dist_c dist_c')
    then show "p ≽ q"
      using "2"(2) assms "2"(1) by (simp add: * sum_equals_pmf_expectation)
  qed
  then show ?case
    by (simp add: "*" assms)
qed

lemma strict_alt_def:
  assumes "p ∈ lotteries_on outcomes" 
    and "q ∈ lotteries_on outcomes"
  shows "p ≻[relation] q ⟷ 
            (∑z∈outcomes. (pmf p z) * (u z)) > (∑z∈outcomes. (pmf q z) * (u z))"
  using sum_equals_pmf_expectation[of p, OF assms(1)] assms(1) assms(2)
    sum_equals_pmf_expectation[of q, OF assms(2)] strict_prefernce_iff_strict_utility
  by presburger

lemma strict_alt_def_utility_g:
  assumes "p ≻[relation] q"
  shows "(∑z∈outcomes. (pmf p z) * (u z)) > (∑z∈outcomes. (pmf q z) * (u z))"
  using assms not_outside(1) not_outside(2) strict_alt_def
  by meson

end (* finite outcomes *)

end (* Definition of vNM Utility Function as locale *)

lemma vnm_utility_is_ordinal_utility:
  assumes "vNM_utility outcomes relation u"
  shows "ordinal_utility (lotteries_on outcomes) relation (λp. measure_pmf.expectation p u)"
proof (standard, goal_cases)
  case (1 x y)
  then show ?case
    using assms vNM_utility_def by blast
next
  case (2 x y)
  then show ?case 
    using assms vNM_utility.not_outside(1) by blast
next
  case (3 x y)
  then show ?case 
    using assms vNM_utility.not_outside(2) by blast
qed

lemma vnm_utility_imp_reational_prefs:
  assumes "vNM_utility outcomes relation u"
  shows "rational_preference (lotteries_on outcomes) relation"
proof (standard,goal_cases)
  case (1 x y)
  then show ?case
    using assms vNM_utility.not_outside(1) by blast
next
  case (2 x y)
  then show ?case
    using assms vNM_utility.not_outside(2) by blast
next
  case 3
  have t: "trans relation"
    using assms ordinal_utility.util_imp_trans vnm_utility_is_ordinal_utility by blast
  have "refl_on (lotteries_on outcomes) relation"
    by (meson assms order_refl refl_on_def vNM_utility_def)
  then show ?case
    using preorder_on_def t by blast
next
  case 4
  have "total_on (lotteries_on outcomes) relation"
    using ordinal_utility.util_imp_total[of "lotteries_on outcomes" 
        relation "(λp. (∑z∈outcomes. (pmf p z) * (u z)))"]
      assms vnm_utility_is_ordinal_utility
    using ordinal_utility.util_imp_total by blast
  then show ?case
    by simp
qed

theorem expected_utilty_theorem_form_vnm_utility:
  assumes fnt: "finite outcomes" and "outcomes ≠ {}"
  shows "rational_preference (lotteries_on outcomes) ℛ ∧ 
         independent_vnm (lotteries_on outcomes) ℛ ∧ 
         continuous_vnm (lotteries_on outcomes) ℛ ⟷ 
         (∃u. vNM_utility outcomes ℛ u)"
proof
  assume "rational_preference (𝒫 outcomes) ℛ ∧ independent_vnm (𝒫 outcomes) ℛ ∧ continuous_vnm (𝒫 outcomes) ℛ"
  with Von_Neumann_Morgenstern_Utility_Theorem[of outcomes ℛ, OF assms] have
  "(∃u. ordinal_utility (𝒫 outcomes) ℛ (λx. measure_pmf.expectation x u))" using assms by blast
  then obtain u where
    u: "ordinal_utility (𝒫 outcomes) ℛ (λx. measure_pmf.expectation x u)"
    by auto
  have "vNM_utility outcomes ℛ u"
  proof (standard, goal_cases)
    case 1
    then show ?case
      using u ordinal_utility.relation_subset_crossp by blast
  next
    case (2 p q)
    then show ?case
      using assms(2) expected_value_is_utility_function fnt u by blast
  qed
  then show "∃u. vNM_utility outcomes ℛ u" 
    by blast
next
  assume a: "∃u. vNM_utility outcomes ℛ u"
  then have "rational_preference (𝒫 outcomes) ℛ"
    using vnm_utility_imp_reational_prefs by auto
  moreover have "independent_vnm (𝒫 outcomes) ℛ"
    using a by (meson assms(2) fnt vNM_utility_implies_independence vnm_utility_is_ordinal_utility)
  moreover have "continuous_vnm (𝒫 outcomes) ℛ"
    using a by (meson assms(2) fnt vNM_utilty_implies_continuity vnm_utility_is_ordinal_utility)
  ultimately show "rational_preference (𝒫 outcomes) ℛ ∧ independent_vnm (𝒫 outcomes) ℛ ∧ continuous_vnm (𝒫 outcomes) ℛ"
    by auto
qed

end