Theory First_Welfare_Theorem.Utility_Functions

(* License: LGPL *)
(*
Author: Julian Parsert <julian.parsert@gmail.com>
Author: Cezary Kaliszyk
*)


section ‹ Utility Functions ›

text ‹ Utility functions and results involving them. ›

theory Utility_Functions
  imports
    Preferences
begin


subsection "Ordinal utility functions"

text ‹ Ordinal utility function locale ›

locale ordinal_utility =
  fixes carrier :: "'a set"
  fixes relation :: "'a relation"
  fixes u :: "'a ⇒ real"
  assumes util_def[iff]: "x ∈ carrier ⟹ y ∈ carrier ⟹ x ≽[relation] y ⟷ u x ≥ u y"
  assumes not_outside: "x ≽[relation] y ⟹ x ∈ carrier"
    and "x ≽[relation] y ⟹ y ∈ carrier"
begin

lemma util_def_conf: "x ∈ carrier ⟹ y ∈ carrier ⟹ u x ≥ u y ⟷ x ≽[relation] y"
  using util_def by blast

lemma relation_subset_crossp:
  "relation ⊆ carrier × carrier"
proof
  fix x
  assume "x ∈ relation"
  have "∀(a,b) ∈ relation. a ∈ carrier ∧ b ∈ carrier"
    by (metis (no_types, lifting) case_prod_conv ordinal_utility_axioms ordinal_utility_def surj_pair)
  then show "x ∈ carrier × carrier"
    using ‹x ∈ relation› by auto
qed

text ‹ Utility function implies totality of relation ›
lemma util_imp_total: "total_on carrier relation"
proof
  fix x and y
  assume x_inc: "x ∈ carrier" and y_inc : "y ∈ carrier"
  have fst : "u x ≥ u y ∨ u y ≥ u x"
    using util_def by auto
  then show  "x ≽[relation] y ∨ y ≽[relation] x"
    by (simp add: x_inc y_inc)
qed

lemma x_y_in_carrier: "x ≽[relation] y ⟹ x ∈ carrier ∧ y ∈ carrier"
  by (meson ordinal_utility_axioms ordinal_utility_def)

text ‹ Utility function implies transitivity of relation. ›

lemma util_imp_trans: "trans relation"
proof (rule transI)
  fix x and y and z
  assume x_y: "x ≽[relation] y"
  assume y_z: "y ≽[relation] z"
  have x_ge_y: "x ≽[relation] y"
    using x_y by auto
  then have x_y: "u x ≥ u y"
    by (meson x_y_in_carrier ordinal_utility_axioms util_def x_y)
  have "u y ≥ u z"
    by (meson y_z ordinal_utility_axioms ordinal_utility_def)
  have "x ∈ carrier"
    using x_y_in_carrier[of x y] x_ge_y  by simp
  then have "u x ≥ u z"
    using ‹u z ≤ u y› order_trans x_y by blast
  hence "x ≽[relation] z"
    by (meson ‹x ∈ carrier› ordinal_utility_axioms ordinal_utility_def y_z)
  then show "x ≽[relation] z" .
qed

lemma util_imp_refl: "refl_on carrier relation"
  by (simp add: refl_on_def relation_subset_crossp)

lemma affine_trans_is_u:
  shows "∀α>0. (∀β. ordinal_utility  carrier relation (λx. u(x)*α + β))"
proof (rule allI, rule impI, rule allI)
  fix α::real and β
  assume *:"α > 0"
  show "ordinal_utility carrier relation (λx. u x * α + β)"
  proof (subst ordinal_utility_def, rule conjI, goal_cases)
    case 1
    then show ?case
      by (metis * add.commute add_le_cancel_left not_le mult_less_cancel_right_pos util_def_conf)
  next
    case 2
    then show ?case 
      by (meson refl_on_domain util_imp_refl)
  qed
qed

text ‹ This utility function definition is ordinal.
        Hence they are only unique up to a monotone transformation. ›

lemma ordinality_of_utility_function :
  fixes f :: "real ⇒ real"
  assumes monot: "monotone (>) (>) f"
  shows "(f ∘ u) x > (f ∘ u) y ⟷ u x > u y"
proof -
  let ?func = "(λx. f(u x))"
  have "∀m n . u m ≥ u n ⟷ ?func m ≥ ?func n"
    by (metis le_less monot monotone_def not_less)
  hence "u x > u y ⟷ ?func x > ?func y"
    using not_le by blast
  thus ?thesis  by auto
qed

corollary utility_prefs_corresp :
  fixes f :: "real ⇒ real"
  assumes monotonicity : "monotone (>) (>) f"
  shows "∀x∈carrier. ∀y∈carrier. (x,y) ∈ relation ⟷ (f ∘ u) x ≥ (f ∘ u) y"
  by (meson monotonicity not_less ordinality_of_utility_function util_def_conf)

corollary monotone_comp_is_utility:
  fixes f :: "real ⇒ real"
  assumes monot: "monotone (>) (>) f"
  shows "ordinal_utility carrier relation (f ∘ u)"
proof (rule ordinal_utility.intro, goal_cases)
case (1 x y)
  then show ?case
    using monot utility_prefs_corresp by blast
next
  case (2 x y)
  then show ?case
    using not_outside by blast
next
  case (3 x y)
  then show ?case
    using x_y_in_carrier by blast
qed

lemma ordinal_utility_left:
  assumes "x ≽[relation] y"
  shows "u x ≥ u y"
  using assms x_y_in_carrier by blast

lemma add_right:
  assumes "⋀x y. x ≽[relation] y ⟹ f x ≥ f y"
  shows   "ordinal_utility carrier relation (λx. u x + f x)"
proof (rule ordinal_utility.intro, goal_cases)
  case (1 x y)
  assume xy: "x ∈ carrier" "y ∈ carrier"
  then show ?case
  proof -
    have "u x ≤ u y ⟶ (∃r. ((x, y) ∉ relation ∧ ¬ r ≤ u x + f x) ∧ r ≤ u y + f y) ∨ u y ≤ u x"
      by (metis (no_types) add_le_cancel_left add_le_cancel_right assms util_def xy(1) xy(2))
    moreover show ?thesis
      by (meson add_mono assms calculation le_cases order_trans util_def xy(1) xy(2))
  qed
next
  case (2 x y)
  then show ?case
    using not_outside by blast
next
  case (3 x y)
  then show ?case
    using x_y_in_carrier by blast
qed

lemma add_left:
  assumes "⋀x y. x ≽[relation] y ⟹ f x ≥ f y"
  shows "ordinal_utility carrier relation (λx. f x + u x)"
proof -
  have "ordinal_utility carrier relation (λx. u x + f x)"
    by (simp add: add_right assms)
  thus ?thesis using Groups.ab_semigroup_add_class.add.commute
    by (simp add: add.commute)
qed


lemma ordinal_utility_scale_transl:
  assumes "(c::real) > 0"
  shows "ordinal_utility carrier relation (λx. c * (u x) + d)"
proof -
  have "monotone (>) (>) (λx. c * x + d)" (is "monotone (>) (>) ?fn" )
    by (simp add: assms monotone_def)
  with monotone_comp_is_utility have "ordinal_utility carrier relation (?fn ∘ u)"
    by blast
  moreover have "?fn ∘ u =  (λx. c * (u x) + d)"
    by auto
  finally show ?thesis
    by auto
qed

lemma strict_prefernce_iff_strict_utility:
  assumes "x ∈ carrier"
  assumes "y ∈ carrier"
  shows "x ≻[relation] y ⟷ u x > u y"
  by (meson assms(1) assms(2) less_eq_real_def not_less util_def)

end

text ‹ A utility function implies a rational preference relation.
      Hence a utility function contains exactly the same amount of information as a RPR ›

sublocale ordinal_utility ⊆ rational_preference carrier relation
proof
  fix x and y
  assume xy: "x ≽[relation] y"
  then show "x ∈ carrier"
    and "y ∈ carrier"
    using not_outside by (simp)
      (meson xy refl_onD2 util_imp_refl)
next
  show "preorder_on carrier relation"
  proof-
    have "trans relation" using util_imp_trans by auto
    then have "preorder_on carrier relation"
      by (simp add: preorder_on_def util_imp_refl)
    then show ?thesis .
  qed
next
  show "total_on carrier relation"
    by (simp add: util_imp_total)
qed


text ‹ Given a finite carrier set. We can guarantee that given a rational preference
       relation, there must also exist a utility function representing this relation.
       Construction of witness roughly follows from.›

theorem fnt_carrier_exists_util_fun:
  assumes "finite carrier"
  assumes "rational_preference carrier relation"
  shows "∃u. ordinal_utility carrier relation u"
proof-
  define f where
    f: "f = (λx. card (no_better_than x carrier relation))"
  have "ordinal_utility carrier relation f"
  proof
    fix x y
    assume x_c: "x ∈ carrier"
    assume y_c: "y ∈ carrier"
    show "x ≽[relation] y ⟷ (real (f y) ≤ real (f x))"
    proof
      assume asm: "x ≽[relation] y"
      define yn where
        yn: "yn = no_better_than y carrier relation"
      define xn where
        xn: "xn = no_better_than x carrier relation"
      then have "yn ⊆ xn"
        by (simp add: asm yn assms(2) rational_preference.no_better_subset_pref)
      then have "card yn ≤ card xn"
        by (simp add: x_c y_c asm assms(1) assms(2) rational_preference.card_leq_pref xn yn)
      then show "(real (f y) ≤ real (f x))"
        using  f xn yn by simp
    next
      assume "real (f y) ≤ real (f x)"
      then show "x ≽[relation] y"
        using assms(1) assms(2) f rational_preference.card_leq_pref x_c y_c by fastforce
    qed
  next
    fix x y
    assume asm: "x ≽[relation] y"
    show "x ∈ carrier"
      by (meson asm assms(2) preference.not_outside rational_preference.axioms(1))
    show "y ∈ carrier"
      by (meson asm assms(2) preference_def rational_preference_def)
  qed
  then show ?thesis
    by blast
qed

corollary obt_u_fnt_carrier:
  assumes "finite carrier"
  assumes "rational_preference carrier relation"
  obtains u where "ordinal_utility carrier relation u"
  using assms(1) assms(2) fnt_carrier_exists_util_fun by blast

theorem ordinal_util_imp_rat_prefs:
  assumes "ordinal_utility carrier relation u"
  shows "rational_preference carrier relation"
  by (metis (full_types) assms order_on_defs(1) ordinal_utility.util_imp_refl 
      ordinal_utility.util_imp_total ordinal_utility.util_imp_trans ordinal_utility_def 
      preference.intro rational_preference.intro rational_preference_axioms_def)

subsection ‹ Utility function on  Euclidean Space ›

locale eucl_ordinal_utility = ordinal_utility carrier relation u
  for carrier :: "('a::euclidean_space) set"
  and relation :: "'a relation"
  and u :: "'a ⇒ real"

sublocale eucl_ordinal_utility ⊆ rational_preference carrier relation
  using rational_preference_axioms by blast


lemma ord_eucl_utility_imp_rpr: "eucl_ordinal_utility s rel u ⟶ real_vector_rpr s rel"
  using eucl_ordinal_utility.axioms ordinal_util_imp_rat_prefs real_vector_rpr.intro by blast

context eucl_ordinal_utility
begin

text ‹ Local non-satiation on utility functions ›

lemma lns_pref_lns_util [iff]:
  "local_nonsatiation carrier relation ⟷
  (∀x∈carrier. ∀e > 0. ∃y∈carrier.
  norm (y - x) ≤ e ∧ u y > u x)" (is "_ ⟷ ?alt")
proof
  assume lns: "local_nonsatiation carrier relation"
  have "∀a b. a ≻ b ⟶ u a > u b"
    by (metis less_eq_real_def util_def x_y_in_carrier)
  then show "?alt"
    by (meson lns local_nonsatiation_def)
next
  assume lns: "?alt"
  show "local_nonsatiation carrier relation"
  proof(rule lns_normI)
    fix x and e::real
    assume x_in: "x ∈ carrier"
    assume e: "e > 0"
    have "∀x ∈ carrier. ∀e>0. ∃y∈carrier. norm (y - x) ≤ e ∧ y ≻ x"
      by (meson less_eq_real_def linorder_not_less lns util_def)
    have "∃y∈carrier. norm (y - x) ≤ e ∧ u y > u x"
      using e x_in lns by blast
    then show "∃y∈carrier. norm (y - x) ≤ e ∧ y ≻ x"
      by (meson compl not_less util_def x_in)
  qed
qed

end

lemma finite_carrier_rpr_iff_u:
  assumes "finite carrier"
    and "(relation::'a relation) ⊆ carrier × carrier"
  shows "rational_preference carrier relation ⟷ (∃u. ordinal_utility carrier relation u)"
proof
  assume "rational_preference carrier relation" 
  then show "∃u. ordinal_utility carrier relation u"
    by (simp add: assms(1) fnt_carrier_exists_util_fun)
next
  assume "∃u. ordinal_utility carrier relation u"
  then show "rational_preference carrier relation" 
    by (metis (full_types) order_on_defs(1) ordinal_utility.util_imp_refl 
        ordinal_utility.util_imp_total ordinal_utility.util_imp_trans ordinal_utility_def 
        preference.intro rational_preference_axioms_def rational_preference_def)
qed


end