Theory Utility_Functions

theory Utility_Functions
imports
  Complex_Main
  "HOL-Probability.Probability"
  Lotteries
  Preference_Profiles
begin

subsection ‹Definition of von Neumann--Morgenstern utility functions›

locale vnm_utility = finite_total_preorder_on +
  fixes u :: "'a ⇒ real"
  assumes utility_le_iff: "x ∈ carrier ⟹ y ∈ carrier ⟹ u x ≤ u y ⟷ x ≼[le] y"
begin

lemma utility_le: "x ≼[le] y ⟹ u x ≤ u y"
  using not_outside[of x y] utility_le_iff by simp

lemma utility_less_iff:
  "x ∈ carrier ⟹ y ∈ carrier ⟹ u x < u y ⟷ x ≺[le] y"
  using utility_le_iff[of x y] utility_le_iff[of y x]
  by (auto simp: strongly_preferred_def)

lemma utility_less: "x ≺[le] y ⟹ u x < u y"
  using not_outside[of x y] utility_less_iff by (simp add: strongly_preferred_def)

text ‹
  The following lemma allows us to compute the expected utility by summing
  over all indifference classes, using the fact that alternatives in the same
  indifference class must have the same utility.
›
lemma expected_utility_weak_ranking:
  assumes "p ∈ lotteries_on carrier"
  shows   "measure_pmf.expectation p u =
             (∑A←weak_ranking le. u (SOME x. x ∈ A) * measure_pmf.prob p A)"
proof -
  from assms have "measure_pmf.expectation p u = (∑a∈carrier. u a * pmf p a)"
    by (subst integral_measure_pmf[OF finite_carrier])
       (auto simp: lotteries_on_def ac_simps)
  also have carrier: "carrier = ⋃(set (weak_ranking le))" by (simp add: weak_ranking_Union)
  also from carrier have finite: "finite A" if "A ∈ set (weak_ranking le)" for A
    using that by (blast intro!: finite_subset[OF _ finite_carrier, of A])
  hence "(∑a∈⋃(set (weak_ranking le)). u a * pmf p a) =
           (∑A←weak_ranking le. ∑a∈A. u a * pmf p a)" (is "_ = sum_list ?xs")
    using weak_ranking_total_preorder
    by (subst sum.Union_disjoint)
       (auto simp: is_weak_ranking_iff disjoint_def sum.distinct_set_conv_list)
  also have "?xs  = map (λA. ∑a∈A. u (SOME a. a∈A) * pmf p a) (weak_ranking le)"
  proof (intro map_cong HOL.refl sum.cong)
    fix x A assume x: "x ∈ A" and A: "A ∈ set (weak_ranking le)"
    have "(SOME x. x ∈ A) ∈ A" by (rule someI_ex) (insert x, blast)
    from weak_ranking_eqclass1[OF A x this] weak_ranking_eqclass1[OF A this x] x this A
      have "u x = u (SOME x. x ∈ A)"
      by (intro antisym; subst utility_le_iff) (auto simp: carrier)
    thus "u x * pmf p x = u (SOME x. x ∈ A) * pmf p x" by simp
  qed
  also have "… = map (λA. u (SOME a. a ∈ A) * measure_pmf.prob p A) (weak_ranking le)"
    using finite by (intro map_cong HOL.refl)
                    (auto simp: sum_distrib_left measure_measure_pmf_finite)
  finally show ?thesis .
qed

lemma scaled: "c > 0 ⟹ vnm_utility carrier le (λx. c * u x)"
  by unfold_locales (insert utility_le_iff, auto)

lemma add_right:
  assumes "⋀x y. le x y ⟹ f x ≤ f y"
  shows   "vnm_utility carrier le (λx. u x + f x)"
proof
  fix x y assume xy: "x ∈ carrier" "y ∈ carrier"
  from assms[of x y] utility_le_iff[OF xy] assms[of y x] utility_le_iff[OF xy(2,1)]
    show "(u x + f x ≤ u y + f y) = le x y" by auto
qed

lemma add_left:
  "(⋀x y. le x y ⟹ f x ≤ f y) ⟹ vnm_utility carrier le (λx. f x + u x)"
  by (subst add.commute) (rule add_right)

text ‹
  Given a consistent utility function, any function that assigns equal values to
  equivalent alternatives can be added to it (scaled with a sufficiently small @{term "ε"}),
  again yielding a consistent utility function.
›
lemma add_epsilon:
  assumes A: "⋀x y. le x y ⟹ le y x ⟹ f x = f y"
  shows "∃ε>0. vnm_utility carrier le (λx. u x + ε * f x)"
proof -
  let ?A = "{(u y - u x) / (f x - f y) |x y. x ≺[le] y ∧ f x > f y}"
  have "?A = (λ(x,y). (u y - u x) / (f x - f y)) ` {(x,y) |x y. x ≺[le] y ∧ f x > f y}" by auto
  also have "finite {(x,y) |x y. x ≺[le] y ∧ f x > f y}"
    by (rule finite_subset[of _ "carrier × carrier"])
       (insert not_outside, auto simp: strongly_preferred_def)
  hence "finite ((λ(x,y). (u y - u x) / (f x - f y)) ` {(x,y) |x y. x ≺[le] y ∧ f x > f y})"
    by simp
  finally have finite: "finite ?A" .

  define ε where "ε = Min (insert 1 ?A) / 2"
  from finite have "Min (insert 1 ?A) > 0"
    by (auto intro!: divide_pos_pos simp: utility_less)
  hence ε: "ε > 0" unfolding ε_def by simp

  have mono: "u x + ε * f x < u y + ε * f y" if xy: "x ≺[le] y" for x y
  proof (cases "f x > f y")
    assume less: "f x > f y"
    from ε have "ε < Min (insert 1 ?A)" unfolding ε_def by linarith
    also from less xy finite have "Min (insert 1 ?A) ≤ (u y - u x) / (f x - f y)" unfolding ε_def
      by (intro Min_le) auto
    finally show ?thesis using less by (simp add: field_simps)
  next
    assume "¬f x > f y"
    with utility_less[OF xy] ε show ?thesis
      by (simp add: algebra_simps not_less add_less_le_mono)
  qed
  have eq: "u x + ε * f x = u y + ε * f y" if xy: "x ≼[le] y" "y ≼[le] x" for x y
    using xy[THEN utility_le] A[OF xy] by simp
  have "vnm_utility carrier le (λx. u x + ε * f x)"
  proof
    fix x y assume xy: "x ∈ carrier" "y ∈ carrier"
    show "(u x + ε * f x ≤ u y + ε * f y) ⟷ le x y"
      using total[OF xy] mono[of x y] mono[of y x] eq[of x y]
      by (cases "le x y"; cases "le y x") (auto simp: strongly_preferred_def)
  qed
  from ε this show ?thesis by blast
qed

lemma diff_epsilon:
  assumes "⋀x y. le x y ⟹ le y x ⟹ f x = f y"
  shows "∃ε>0. vnm_utility carrier le (λx. u x - ε * f x)"
proof -
  from assms have "∃ε>0. vnm_utility carrier le (λx. u x + ε * -f x)"
    by (intro add_epsilon) (subst neg_equal_iff_equal)
  thus ?thesis by simp
qed

end

end