Theory Neumann_Morgenstern_Utility_Theorem

(* License: LGPL *)
(* Author: Julian Parsert *)


theory Neumann_Morgenstern_Utility_Theorem
  imports
    "HOL-Probability.Probability"
    "First_Welfare_Theorem.Utility_Functions"
    Lotteries
begin


section ‹ Properties of Preferences ›

subsection ‹ Independent Preferences›

text ‹ Independence is sometimes called substitution ›


text ‹ Notice how r is "added" to the right of mix-pmf and the element to the left q/p changes ›
definition independent_vnm
  where
    "independent_vnm C P =
    (∀p ∈ C. ∀q ∈ C. ∀r ∈ C. ∀(α::real) ∈ {0<..1}. p ≽[P] q ⟷ mix_pmf α p r ≽[P] mix_pmf α q r)"

lemma independent_vnmI1:
  assumes "(∀p ∈ C. ∀q ∈ C. ∀r ∈ C. ∀α ∈ {0<..1}. p ≽[P] q ⟷ mix_pmf α p r ≽[P] mix_pmf α q r)"
  shows "independent_vnm C P"
  using assms independent_vnm_def by blast

lemma independent_vnmI2:
  assumes "⋀p q r α. p ∈ C ⟹ q ∈ C ⟹ r ∈ C ⟹ α ∈ {0<..1} ⟹ p ≽[P] q ⟷ mix_pmf α p r ≽[P] mix_pmf α q r"
  shows "independent_vnm C P"
  by (rule independent_vnmI1, standard, standard, standard, 
      standard, simp add: assms) (meson assms greaterThanAtMost_iff)

lemma independent_vnm_alt_def:
  shows "independent_vnm C P ⟷ (∀p ∈ C. ∀q ∈ C. ∀r ∈ C. ∀α ∈ {0<..<1}. 
  p ≽[P] q ⟷ mix_pmf α p r ≽[P] mix_pmf α q r)" (is "?L ⟷ ?R")
proof (rule iffI)
  assume a: "?R"
  have "independent_vnm C P" 
    by(rule independent_vnmI2, simp add: a) (metis a greaterThanLessThan_iff 
        linorder_neqE_linordered_idom not_le pmf_mix_1)
  then show "?L" by auto
qed (simp add: independent_vnm_def)

lemma independece_dest_alt: 
  assumes "independent_vnm C P"
  shows "(∀p ∈ C. ∀q ∈ C. ∀r ∈ C. ∀(α::real) ∈ {0<..1}. p ≽[P] q ⟷ mix_pmf α p r ≽[P] mix_pmf α q r)"
proof (standard, standard, standard, standard)
  fix p q r α
  assume as1: "p ∈ C" 
  assume as2: "q ∈ C"
  assume as3: "r ∈ C"
  assume as4: "(α::real) ∈ {0<..1}"
  then show "p ≽[P] q = mix_pmf α p r ≽[P] mix_pmf α q r"
    using as1 as2 as3 assms(1) independent_vnm_def by blast
qed

lemma independent_vnmD1:
  assumes "independent_vnm C P"
  shows "(∀p ∈ C. ∀q ∈ C. ∀r ∈ C. ∀α ∈ {0<..1}. p ≽[P] q ⟷ mix_pmf α p r ≽[P] mix_pmf α q r)"
  using assms independent_vnm_def by blast

lemma independent_vnmD2:
  fixes p q r α
  assumes "α ∈ {0<..1}"
    and "p ∈ C"
    and "q ∈ C"
    and "r ∈ C"
  assumes "independent_vnm C P"
  assumes "p ≽[P] q"
  shows "mix_pmf α p r ≽[P] mix_pmf α q r"
  using assms independece_dest_alt  by blast

lemma independent_vnmD3:
  fixes p q r α
  assumes "α ∈ {0<..1}"
    and "p ∈ C"
    and "q ∈ C"
    and "r ∈ C"
  assumes "independent_vnm C P" 
  assumes "mix_pmf α p r ≽[P] mix_pmf α q r"
  shows "p ≽[P] q"
  using assms independece_dest_alt by blast

lemma independent_vnmD4:
  assumes "independent_vnm C P"
  assumes "refl_on C P"
  assumes "p ∈ C" 
    and "q ∈ C" 
    and "r ∈ C"
    and "α ∈ {0..1}" 
    and "p ≽[P] q" 
  shows "mix_pmf α p r ≽[P] mix_pmf α q r"
  using assms
  by (cases "α = 0 ∨ α ∈ {0<..1}",metis assms(1,2,3,4) 
      independece_dest_alt pmf_mix_0 refl_onD, auto)

lemma approx_indep_ge:
  assumes "x ≈[ℛ] y"
  assumes "α ∈ {0..(1::real)}"
  assumes rpr: "rational_preference (lotteries_on outcomes) ℛ"
    and ind: "independent_vnm (lotteries_on outcomes) ℛ"
  shows "∀r ∈ lotteries_on outcomes. (mix_pmf α y r) ≽[ℛ] (mix_pmf α x r)"
proof
  fix r
  assume a: "r ∈ lotteries_on outcomes" (is "r ∈ ?lo")
  have clct: "y ≽[ℛ] x ∧ independent_vnm ?lo ℛ ∧ y ∈ ?lo ∧ x ∈ ?lo ∧ r ∈ ?lo"
    by (meson  a assms(1) assms(2) atLeastAtMost_iff greaterThanAtMost_iff 
        ind preference_def rational_preference_def rpr)
  then have in_lo: "mix_pmf α y r ∈ ?lo" "(mix_pmf α x r) ∈ ?lo"
    by (metis  assms(2) atLeastAtMost_iff greaterThanLessThan_iff
        less_eq_real_def mix_pmf_in_lotteries pmf_mix_0 pmf_mix_1 a)+
  have "0 = α ∨ 0 < α"
    using assms by auto
  then show "mix_pmf α y r ≽[ℛ] mix_pmf α x r"
    using in_lo(2) rational_preference.compl rpr
    by (auto,blast) (meson assms(2) atLeastAtMost_iff clct
        greaterThanAtMost_iff independent_vnmD2)
qed

lemma approx_imp_approx_ind:
  assumes "x ≈[ℛ] y"
  assumes "α ∈ {0..(1::real)}"
  assumes rpr: "rational_preference (lotteries_on outcomes) ℛ"
    and ind: "independent_vnm (lotteries_on outcomes) ℛ"
  shows "∀r ∈ lotteries_on outcomes. (mix_pmf α y r) ≈[ℛ] (mix_pmf α x r)"
  using approx_indep_ge assms(1) assms(2) ind rpr by blast

lemma geq_imp_mix_geq_right:
  assumes "x ≽[ℛ] y"
  assumes rpr: "rational_preference (lotteries_on outcomes) ℛ"
  assumes ind: "independent_vnm (lotteries_on outcomes) ℛ"
  assumes "α ∈ {0..(1::real)}"
  shows "(mix_pmf α x y) ≽[ℛ] y"
proof -
  have xy_p: "x ∈ (lotteries_on outcomes)" "y ∈ (lotteries_on outcomes)"
    by (meson assms(1) preference.not_outside rational_preference_def rpr)
      (meson assms(1) preference_def rational_preference_def rpr)
  have "(mix_pmf α x y) ∈ (lotteries_on outcomes)" (is "?mpf ∈ ?lot")
    using mix_pmf_in_lotteries [of x outcomes y α] xy_p assms(2)
    by (meson approx_indep_ge assms(4) ind preference.not_outside 
        rational_preference.compl rational_preference_def)
  have all: "∀r ∈ ?lot. (mix_pmf α x r) ≽[ℛ] (mix_pmf α y r)"
    by (metis assms assms(2) atLeastAtMost_iff greaterThanAtMost_iff independece_dest_alt 
        less_eq_real_def pmf_mix_0 rational_preference.compl rpr ind xy_p)
  thus ?thesis      
    by (metis all assms(4) set_pmf_mix_eq xy_p(2))
qed

lemma geq_imp_mix_geq_left:
  assumes "x ≽[ℛ] y"
  assumes rpr: "rational_preference (lotteries_on outcomes) ℛ"
  assumes ind: "independent_vnm (lotteries_on outcomes) ℛ"
  assumes "α ∈ {0..(1::real)}"
  shows "(mix_pmf α y x) ≽[ℛ] y"
proof -
  define β where
    b: "β = 1 - α"
  have "β ∈ {0..1}"
    using assms(4) b by auto
  then have "mix_pmf β x y ≽[ℛ] y" 
    using geq_imp_mix_geq_right[OF assms] assms(1) geq_imp_mix_geq_right ind rpr by blast
  moreover have "mix_pmf β x y = mix_pmf α y x"
    by (metis assms(4) b pmf_inverse_switch_eqals)
  ultimately show ?thesis 
    by simp
qed

lemma sg_imp_mix_sg:
  assumes "x ≻[ℛ] y"
  assumes rpr: "rational_preference (lotteries_on outcomes) ℛ"
  assumes ind: "independent_vnm (lotteries_on outcomes) ℛ"
  assumes "α ∈ {0<..(1::real)}"
  shows "(mix_pmf α x y) ≻[ℛ] y"
proof -
  have xy_p: "x ∈ (lotteries_on outcomes)" "y ∈ (lotteries_on outcomes)"
    by (meson assms(1) preference.not_outside rational_preference_def rpr)
      (meson assms(1) preference_def rational_preference_def rpr)
  have "(mix_pmf α x y) ∈ (lotteries_on outcomes)" (is "?mpf ∈ ?lot")
    using mix_pmf_in_lotteries [of x outcomes y α] xy_p assms(2)
    using assms(4) by fastforce
  have all: "∀r ∈ ?lot. (mix_pmf α x r) ≽[ℛ] (mix_pmf α y r)"
    by (metis assms(1,3,4)  independece_dest_alt ind xy_p)
  have "(mix_pmf α x y) ≽[ℛ] y"
    by (metis all assms(4) atLeastAtMost_iff greaterThanAtMost_iff 
        less_eq_real_def set_pmf_mix_eq xy_p(2))
  have all2: "∀r ∈ ?lot. (mix_pmf α x r) ≻[ℛ] (mix_pmf α y r)"
    using assms(1) assms(4) ind independece_dest_alt xy_p(1) xy_p(2) by blast
  then show ?thesis 
    by (metis assms(4) atLeastAtMost_iff greaterThanAtMost_iff 
        less_eq_real_def set_pmf_mix_eq xy_p(2))
qed



subsection ‹ Continuity ›

text ‹ Continuity is sometimes called Archimedean Axiom›
definition continuous_vnm
  where
    "continuous_vnm C P = (∀p ∈ C. ∀q ∈ C. ∀r ∈ C. p ≽[P] q ∧ q ≽[P] r ⟶ 
    (∃α ∈ {0..1}. (mix_pmf α p r) ≈[P] q))"

lemma continuous_vnmD:
  assumes "continuous_vnm C P"
  shows "(∀p ∈ C. ∀q ∈ C. ∀r ∈ C. p ≽[P] q ∧ q ≽[P] r ⟶
    (∃α ∈ {0..1}. (mix_pmf α p r) ≈[P] q))"
  using continuous_vnm_def assms by blast

lemma continuous_vnmI:
  assumes "⋀p q r. p ∈ C ⟹ q ∈ C ⟹ r ∈ C ⟹ p ≽[P] q ∧ q ≽[P] r ⟹ 
    ∃α ∈ {0..1}. (mix_pmf α p r) ≈[P] q"
  shows "continuous_vnm C P"
  by (simp add: assms continuous_vnm_def)

lemma mix_in_lot:
  assumes "x ∈ lotteries_on outcomes"
    and "y ∈ lotteries_on outcomes"
    and "α ∈ {0..1}"
  shows "(mix_pmf α x y) ∈ lotteries_on outcomes"
  using assms(1) assms(2) assms(3) less_eq_real_def mix_pmf_in_lotteries by fastforce


lemma non_unique_continuous_unfolding:
  assumes cnt: "continuous_vnm (lotteries_on outcomes) ℛ"
  assumes "rational_preference (lotteries_on outcomes) ℛ"
  assumes "p ≽[ℛ] q"
    and "q ≽[ℛ] r"
    and "p ≻[ℛ] r"
  shows "∃α ∈ {0..1}. q ≈[ℛ] mix_pmf α p r"
  using assms(1) assms(2) cnt continuous_vnmD assms
proof -
  have "∀p q. p∈ (lotteries_on outcomes) ∧ q ∈ (lotteries_on outcomes) ⟷ p ≽[ℛ] q ∨ q ≽[ℛ] p"
    using assms rational_preference.compl[of "lotteries_on outcomes" ℛ]
    by (metis (no_types, opaque_lifting) preference_def rational_preference_def)
  then show ?thesis
    using continuous_vnmD[OF assms(1)] by (metis assms(3) assms(4))
qed


section ‹ System U start, as per vNM›

text ‹ These are the first two assumptions which we use to derive the first results.
       We assume rationality and independence. In this system U the von-Neumann-Morgenstern 
        Utility Theorem is proven. ›
context
  fixes outcomes :: "'a set"
  fixes ℛ
  assumes rpr: "rational_preference (lotteries_on outcomes) ℛ"
  assumes ind: "independent_vnm (lotteries_on outcomes) ℛ"
begin

abbreviation "𝒫 ≡ lotteries_on outcomes"

lemma relation_in_carrier:
  "x ≽[ℛ] y ⟹ x ∈ 𝒫 ∧ y ∈ 𝒫"
  by (meson preference_def rational_preference_def rpr)

lemma mix_pmf_preferred_independence:
  assumes "r ∈ 𝒫"
    and "α ∈ {0..1}"
  assumes "p ≽[ℛ] q"
  shows "mix_pmf α p r ≽[ℛ] mix_pmf α q r"
  using ind by (metis relation_in_carrier antisym_conv1 assms atLeastAtMost_iff 
      greaterThanAtMost_iff independece_dest_alt pmf_mix_0 
      rational_preference.no_better_thansubset_rel rpr subsetI)

lemma mix_pmf_strict_preferred_independence:
  assumes "r ∈ 𝒫"
    and "α ∈ {0<..1}"
  assumes "p ≻[ℛ] q"
  shows "mix_pmf α p r ≻[ℛ] mix_pmf α q r"
  by (meson assms(1) assms(2) assms(3) ind independent_vnmD2 
      independent_vnmD3 relation_in_carrier)

lemma mix_pmf_preferred_independence_rev:
  assumes "p ∈ 𝒫"
    and "q ∈ 𝒫"
    and "r ∈ 𝒫"
    and "α ∈ {0<..1}"
  assumes "mix_pmf α p r ≽[ℛ] mix_pmf α q r"
  shows "p ≽[ℛ] q"
proof -
  have "mix_pmf α p r ∈ 𝒫"
    using assms mix_in_lot relation_in_carrier by blast
  moreover have "mix_pmf α q r ∈ 𝒫"
    using assms mix_in_lot assms(2) relation_in_carrier by blast
  ultimately show ?thesis 
    using ind independent_vnmD3[of α p 𝒫 q r ℛ] assms by blast
qed

lemma x_sg_y_sg_mpmf_right:
  assumes "x ≻[ℛ] y"
  assumes "b ∈ {0<..(1::real)}"
  shows "x ≻[ℛ] mix_pmf b y x"
proof -
  consider "b = 1" | "b ≠ 1"
    by blast
  then show ?thesis 
  proof (cases)
    case 2
    have sg: "(mix_pmf b x y) ≻[ℛ] y"
      using assms(1) assms(2) assms ind rpr sg_imp_mix_sg "2" by fastforce
    have "mix_pmf b x y ∈ 𝒫"
      by (meson sg preference_def rational_preference_def rpr)
    have "mix_pmf b x x ∈ 𝒫"
      using relation_in_carrier assms(2) mix_in_lot assms by fastforce
    have "b ∈ {0<..<1}"
      using "2" assms(2)  by auto
    have "mix_pmf b x x ≻[ℛ] mix_pmf b y x"
      using mix_pmf_preferred_independence[of x b] assms
      by (meson ‹b ∈ {0<..<1}› greaterThanAtMost_iff greaterThanLessThan_iff ind 
          independece_dest_alt less_eq_real_def preference_def 
          rational_preference.axioms(1) relation_in_carrier rpr)
    then show ?thesis
      using mix_pmf_preferred_independence
      by (metis assms(2) atLeastAtMost_iff greaterThanAtMost_iff less_eq_real_def set_pmf_mix_eq)
  qed (simp add: assms(1))
qed

lemma neumann_3B_b:
  assumes "u ≻[ℛ] v"
  assumes "α ∈ {0<..<1}"
  shows "u ≻[ℛ] mix_pmf α u v"
proof -
  have *: "preorder_on 𝒫 ℛ ∧ rational_preference_axioms 𝒫 ℛ"
    by (metis (no_types) preference_def rational_preference_def rpr)
  have "1 - α ∈ {0<..1}"
    using assms(2) by auto
  then show ?thesis
    using * assms by (metis atLeastAtMost_iff greaterThanLessThan_iff 
        less_eq_real_def pmf_inverse_switch_eqals x_sg_y_sg_mpmf_right)
qed

lemma neumann_3B_b_non_strict:
  assumes "u ≽[ℛ] v"
  assumes "α ∈ {0..1}"
  shows "u ≽[ℛ] mix_pmf α u v"
proof -
  have f2: "mix_pmf α (u::'a pmf) v = mix_pmf (1 - α) v u"
    using pmf_inverse_switch_eqals assms(2) by auto
  have "1 - α ∈ {0..1}"
    using assms(2) by force
  then show ?thesis
    using f2 relation_in_carrier 
    by (metis (no_types) assms(1) mix_pmf_preferred_independence set_pmf_mix_eq)
qed

lemma greater_mix_pmf_greater_step_1_aux: 
  assumes "v ≻[ℛ] u"
  assumes "α ∈ {0<..<(1::real)}"
    and "β ∈ {0<..<(1::real)}"
  assumes "β > α"
  shows "(mix_pmf β v u) ≻[ℛ] (mix_pmf α v u)"
proof -
  define t where
    t: "t = mix_pmf β v u"
  obtain γ where
    g: "α = β * γ"
    by (metis assms(2) assms(4) greaterThanLessThan_iff 
        mult.commute nonzero_eq_divide_eq not_less_iff_gr_or_eq)
  have g1: "γ > 0 ∧ γ < 1"
    by (metis (full_types) assms(2) assms(4) g greaterThanLessThan_iff 
        less_trans mult.right_neutral mult_less_cancel_left_pos not_le 
        sgn_le_0_iff sgn_pos zero_le_one zero_le_sgn_iff zero_less_mult_iff)
  have t_in: "mix_pmf β v u ∈ 𝒫"
    by (meson assms(1) assms(3) mix_pmf_in_lotteries preference_def rational_preference_def rpr)
  have "v ≻[ℛ] mix_pmf (1 - β) v u"
    using x_sg_y_sg_mpmf_right[of u v "1-β"] assms
    by (metis atLeastAtMost_iff greaterThanAtMost_iff greaterThanLessThan_iff 
        less_eq_real_def pmf_inverse_switch_eqals x_sg_y_sg_mpmf_right)
  have "t ≻[ℛ] u"
    using assms(1) assms(3) ind rpr sg_imp_mix_sg t by fastforce
  hence t_s: "t ≻[ℛ] (mix_pmf γ t u)" 
  proof -
    have "(mix_pmf γ t u) ∈ 𝒫"
      by (metis assms(1) assms(3) atLeastAtMost_iff g1 mix_in_lot mix_pmf_in_lotteries 
          not_less order.asym preference_def rational_preference_def rpr t)
    have "t ≻[ℛ] mix_pmf γ (mix_pmf β v u) u"
      using neumann_3B_b[of t u γ] assms t g1
      by (meson greaterThanAtMost_iff greaterThanLessThan_iff 
          ind less_eq_real_def rpr sg_imp_mix_sg)
    thus ?thesis
      using t by blast
  qed
  from product_mix_pmf_prob_distrib[of _ β v u] assms
  have "mix_pmf β v u ≻[ℛ] mix_pmf α v u"
    by (metis t_s atLeastAtMost_iff g g1 greaterThanLessThan_iff less_eq_real_def mult.commute t)
  then show ?thesis by blast
qed

section ‹ This lemma is in called step 1 in literature. 
In Von Neumann and Morgenstern's book this is A:A (albeit more general) ›

lemma step_1_most_general:
  assumes "x ≻[ℛ] y"
  assumes "α ∈ {0..(1::real)}"
    and "β ∈ {0..(1::real)}"
  assumes "α > β"
  shows "(mix_pmf α x y) ≻[ℛ] (mix_pmf β x y)"
proof -
  consider (ex) "α = 1 ∧ β = 0" | (m) "α ≠ 1 ∨ β ≠ 0"
    by blast
  then show ?thesis
  proof (cases)
    case m
    consider  "β = 0" |  "β ≠ 0"
      by blast
    then show ?thesis
    proof (cases)
      case 1
      then show ?thesis
        using assms(1) assms(2) assms(4) ind rpr sg_imp_mix_sg by fastforce
    next
      case 2
      let ?d = "(β/α)"
      have sg: "(mix_pmf α x y) ≻[ℛ] y"
        using assms(1) assms(2) assms(3) assms(4) ind rpr sg_imp_mix_sg by fastforce
      have a: "α > 0"
        using assms(3) assms(4) by auto
      then have div_in: "?d ∈ {0<..1}"
        using assms(3) assms(4) 2 by auto
      have mx_p: "(mix_pmf α x y) ∈ 𝒫"
        by (meson sg preference_def rational_preference_def rpr)
      have y_P: "y ∈ 𝒫"
        by (meson assms(1) preference_def rational_preference_def rpr)
      hence "(mix_pmf ?d (mix_pmf α x y) y) ∈ 𝒫"
        using div_in mx_p by (simp add: mix_in_lot)
      have " mix_pmf β (mix_pmf α x y) y ≻[ℛ] y"
        using sg_imp_mix_sg[of "(mix_pmf α x y)" y ℛ outcomes β] sg div_in rpr ind
          a assms(2) "2" assms(3) by auto
      have al1: "∀r ∈ 𝒫. (mix_pmf α x r) ≻[ℛ] (mix_pmf α y r)"
        by (meson a assms(1) assms(2) atLeastAtMost_iff greaterThanAtMost_iff ind 
            independece_dest_alt preference.not_outside rational_preference_def rpr y_P)
      then show ?thesis 
        using greater_mix_pmf_greater_step_1_aux assms
        by (metis a div_in divide_less_eq_1_pos greaterThanAtMost_iff 
            greaterThanLessThan_iff mix_pmf_comp_with_dif_equiv neumann_3B_b sg)
    qed 
  qed (simp add: assms(1))
qed


text ‹ Kreps refers to this lemma as 5.6 c. 
       The lemma after that is also significant.›
lemma approx_remains_after_same_comp:
  assumes "p ≈[ℛ] q"
    and "r ∈ 𝒫"
    and "α ∈ {0..1}"
  shows "mix_pmf α p r ≈[ℛ] mix_pmf α q r"
  using approx_indep_ge assms(1) assms(2) assms(3) ind rpr by blast

text ‹ This lemma is the symmetric version of the previous lemma. 
       This lemma is never mentioned in literature anywhere. 
       Even though it looks trivial now, due to the asymmetric nature of the 
       independence axiom, it is not so trivial, and definitely worth mentioning. ›
lemma approx_remains_after_same_comp_left:
  assumes "p ≈[ℛ] q"
    and "r ∈ 𝒫"
    and "α ∈ {0..1}"
  shows "mix_pmf α r p ≈[ℛ] mix_pmf α r q"
proof -
  have 1: "α ≤ 1 ∧ α ≥ 0" "1 - α ∈ {0..1}"
    using assms(3) by auto+
  have fst: "mix_pmf α r p ≈[ℛ] mix_pmf (1-α) p r"
    using assms  by (metis mix_in_lot pmf_inverse_switch_eqals 
    rational_preference.compl relation_in_carrier rpr)
  moreover have "mix_pmf α r p ≈[ℛ] mix_pmf α r q"
    using approx_remains_after_same_comp[of _ _ _ α] pmf_inverse_switch_eqals[of α p q] 1 
      pmf_inverse_switch_eqals rpr mix_pmf_preferred_independence[of _ α _ _]
    by (metis assms(1) assms(2) assms(3) mix_pmf_preferred_independence)
  thus ?thesis
    by blast
qed

lemma mix_of_preferred_is_preferred:
  assumes "p ≽[ℛ] w"
  assumes "q ≽[ℛ] w"
  assumes "α ∈ {0..1}"
  shows "mix_pmf α p q ≽[ℛ] w"
proof -
  consider "p ≽[ℛ] q" | "q ≽[ℛ] p"
    using rpr assms(1) assms(2) rational_preference.compl relation_in_carrier by blast
  then show ?thesis
  proof (cases)
    case 1
    have "mix_pmf α p q ≽[ℛ] q"
      using "1" assms(3) geq_imp_mix_geq_right ind rpr by blast
    moreover have "q ≽[ℛ] w" 
      using assms by auto
    ultimately show ?thesis using rpr preference.transitivity[of 𝒫 ℛ]
      by (meson rational_preference_def transE)
  next
    case 2
    have "mix_pmf α p q ≽[ℛ] p"      
      using "2" assms geq_imp_mix_geq_left ind rpr by blast
    moreover have "p ≽[ℛ] w" 
      using assms by auto
    ultimately show ?thesis using rpr preference.transitivity[of 𝒫 ℛ]
      by (meson rational_preference_def transE)
  qed
qed

lemma mix_of_not_preferred_is_not_preferred:
  assumes "w ≽[ℛ] p"
  assumes "w ≽[ℛ] q"
  assumes "α ∈ {0..1}"
  shows "w ≽[ℛ] mix_pmf α p q"
proof -
  consider "p ≽[ℛ] q" | "q ≽[ℛ] p"
    using rpr assms(1) assms(2) rational_preference.compl relation_in_carrier by blast
  then show ?thesis
  proof (cases)
    case 1
    moreover have "p ≽[ℛ] mix_pmf α p q"
      using assms(3) neumann_3B_b_non_strict calculation by blast
    moreover show ?thesis
      using rpr preference.transitivity[of 𝒫 ℛ]
      by (meson assms(1) calculation(2) rational_preference_def transE)
  next
    case 2
    moreover have "q ≽[ℛ] mix_pmf α p q"
      using assms(3) neumann_3B_b_non_strict calculation
      by (metis mix_pmf_preferred_independence relation_in_carrier set_pmf_mix_eq)
    moreover show ?thesis
      using rpr preference.transitivity[of 𝒫 ℛ]
      by (meson assms(2) calculation(2) rational_preference_def transE)
  qed
qed

private definition degenerate_lotteries where
  "degenerate_lotteries = {x ∈ 𝒫. card (set_pmf x) = 1}"

private definition best where
  "best = {x ∈ 𝒫. (∀y ∈ 𝒫. x ≽[ℛ] y)}"

private definition worst where
  "worst = {x ∈ 𝒫. (∀y ∈ 𝒫. y ≽[ℛ] x)}"

lemma degenerate_total: 
  "∀e ∈ degenerate_lotteries. ∀m ∈ 𝒫. e ≽[ℛ] m ∨ m ≽[ℛ] e"
  using degenerate_lotteries_def rational_preference.compl rpr by fastforce

lemma degen_outcome_cardinalities:
  "card degenerate_lotteries = card outcomes"
  using card_degen_lotteries_equals_outcomes degenerate_lotteries_def by auto

lemma degenerate_lots_subset_all: "degenerate_lotteries ⊆ 𝒫"
  by (simp add: degenerate_lotteries_def)

lemma alt_definition_of_degenerate_lotteries[iff]:
  "{return_pmf x |x. x∈ outcomes} = degenerate_lotteries"
proof (standard, goal_cases)
  case 1
  have "∀x ∈ {return_pmf x |x. x ∈ outcomes}. x ∈ degenerate_lotteries"
  proof
    fix x
    assume a: "x ∈ {return_pmf x |x. x ∈ outcomes}"
    then have "card (set_pmf x) = 1"
      by auto
    moreover have "set_pmf x ⊆ outcomes"
      using a set_pmf_subset_singleton by auto
    moreover have "x ∈ 𝒫"
      by (simp add: lotteries_on_def calculation)
    ultimately show "x ∈ degenerate_lotteries"
      by (simp add: degenerate_lotteries_def)
  qed
  then show ?case by blast
next
  case 2
  have "∀x ∈ degenerate_lotteries. x ∈ {return_pmf x |x. x ∈ outcomes}"
  proof
    fix x
    assume a: "x ∈ degenerate_lotteries"
    hence "card (set_pmf x) = 1"
      using degenerate_lotteries_def by blast
    moreover have "set_pmf x ⊆ outcomes"
      by (meson a degenerate_lots_subset_all subset_iff support_in_outcomes)
    moreover obtain e where "{e} = set_pmf x"
      using calculation
      by (metis card_1_singletonE)
    moreover have "e ∈ outcomes"
      using calculation(2) calculation(3) by blast
    moreover have "x = return_pmf e"
      using calculation(3) set_pmf_subset_singleton by fast
    ultimately show "x ∈ {return_pmf x |x. x ∈ outcomes}"
      by blast
  qed
  then show ?case by blast
qed

lemma best_indifferent:
  "∀x ∈ best. ∀y ∈ best. x ≈[ℛ] y"
  by (simp add: best_def)

lemma worst_indifferent:
  "∀x ∈ worst. ∀y ∈ worst. x ≈[ℛ] y"
  by (simp add: worst_def)

lemma best_worst_indiff_all_indiff:
  assumes "b ∈ best"
    and "w ∈ worst"
    and "b ≈[ℛ] w"
  shows "∀e ∈ 𝒫. e ≈[ℛ] w" "∀e ∈ 𝒫. e ≈[ℛ] b"
proof -
  show "∀e ∈ 𝒫. e ≈[ℛ] w"
  proof (standard)
    fix e 
    assume a: "e ∈ 𝒫"
    then have "b ≽[ℛ] e"
      using a best_def assms  by blast
    moreover have "e ≽[ℛ] w"
      using a assms worst_def by auto
    moreover have "b ≽[ℛ] e"
      by (simp add: calculation(1))
    moreover show "e ≈[ℛ] w"
    proof (rule ccontr)
      assume "¬ e ≈[ℛ] w"
      then consider "e ≻[ℛ] w" | "w ≻[ℛ] e"
        by (simp add: calculation(2))
      then show False 
      proof (cases)
        case 2
        then show ?thesis
          using calculation(2) by blast
      qed (meson assms(3) calculation(1) 
          rational_preference.strict_is_neg_transitive relation_in_carrier rpr)
    qed
  qed
  then show "∀e∈local.𝒫. e ≈[ℛ] b"
    using assms  by (meson rational_preference.compl 
        rational_preference.strict_is_neg_transitive relation_in_carrier rpr)
qed  

text ‹ Like Step 1 most general but with IFF. ›
lemma mix_pmf_pref_iff_more_likely [iff]: 
  assumes "b ≻[ℛ] w"
  assumes "α ∈ {0..1}"
    and "β ∈ {0..1}"
  shows "α > β ⟷ mix_pmf α b w ≻[ℛ] mix_pmf β b w" (is "?L ⟷ ?R")
  using assms step_1_most_general[of b w α β]
  by (metis linorder_neqE_linordered_idom step_1_most_general)

lemma better_worse_good_mix_preferred[iff]: 
  assumes "b ≽[ℛ] w"
  assumes "α ∈ {0..1}"
    and "β ∈ {0..1}"
  assumes "α ≥ β" 
  shows "mix_pmf α b w ≽[ℛ] mix_pmf β b w"
proof-
  have "(0::real) ≤ 1"
    by simp
  then show ?thesis
    by (metis (no_types) assms assms(1) assms(2) assms(3) atLeastAtMost_iff 
        less_eq_real_def mix_of_not_preferred_is_not_preferred 
        mix_of_preferred_is_preferred mix_pmf_preferred_independence 
        pmf_mix_0 relation_in_carrier step_1_most_general)
qed

subsection ‹ Add finiteness and non emptyness of outcomes ›
context
  assumes fnt: "finite outcomes"
  assumes nempty: "outcomes ≠ {}"
begin

lemma finite_degenerate_lotteries: 
  "finite degenerate_lotteries"
  using degen_outcome_cardinalities fnt nempty by fastforce

lemma degenerate_has_max_preferred:
  "{x ∈ degenerate_lotteries. (∀y ∈ degenerate_lotteries. x ≽[ℛ] y)} ≠ {}" (is "?l ≠ {}")
proof
  assume a: "?l = {}"
  let ?DG = "degenerate_lotteries"
  obtain R where
    R: "rational_preference ?DG R" "R ⊆ ℛ"
    using degenerate_lots_subset_all rational_preference.all_carrier_ex_sub_rel rpr by blast
  then have "∃e ∈ ?DG. ∀e' ∈ ?DG. e ≽[ℛ] e'"
    by (metis R(1) R(2) card_0_eq degen_outcome_cardinalities 
        finite_degenerate_lotteries fnt nempty subset_eq
        rational_preference.finite_nonempty_carrier_has_maximum )
  then show False
    using a by auto
qed

lemma degenerate_has_min_preferred:
  "{x ∈ degenerate_lotteries. (∀y ∈ degenerate_lotteries. y ≽[ℛ] x)} ≠ {}" (is "?l ≠ {}")
proof
  assume a: "?l = {}"
  let ?DG = "degenerate_lotteries"
  obtain R where
    R: "rational_preference ?DG R" "R ⊆ ℛ"
    using degenerate_lots_subset_all rational_preference.all_carrier_ex_sub_rel rpr by blast
  have "∃e ∈ ?DG. ∀e' ∈ ?DG. e' ≽[ℛ] e"
    by (metis R(1) R(2) card_0_eq degen_outcome_cardinalities 
        finite_degenerate_lotteries fnt nempty subset_eq
        rational_preference.finite_nonempty_carrier_has_minimum )
  then show False
    using a by auto
qed

lemma exists_best_degenerate:
  "∃x ∈ degenerate_lotteries. ∀y ∈ degenerate_lotteries. x ≽[ℛ] y"
  using degenerate_has_max_preferred by blast

lemma exists_worst_degenerate:
  "∃x ∈ degenerate_lotteries. ∀y ∈ degenerate_lotteries. y ≽[ℛ] x"
  using degenerate_has_min_preferred by blast

lemma best_degenerate_in_best_overall: 
  "∃x ∈ degenerate_lotteries. ∀y ∈ 𝒫. x ≽[ℛ] y"
proof -
  obtain b where
    b: "b ∈ degenerate_lotteries" "∀y ∈ degenerate_lotteries. b ≽[ℛ] y"
    using exists_best_degenerate by blast
  have asm: "finite outcomes" "set_pmf b ⊆ outcomes"
    by (simp add: fnt) (meson b(1) degenerate_lots_subset_all subset_iff support_in_outcomes)
  obtain B where B: "set_pmf b = {B}"
    using b card_1_singletonE degenerate_lotteries_def by blast
  have deg: "∀d∈outcomes. b ≽[ℛ] return_pmf d"
    using alt_definition_of_degenerate_lotteries b(2) by blast
  define P where
    "P = (λp. p ∈ 𝒫 ⟶ return_pmf B ≽[ℛ] p)"
  have "P p" for p
  proof -
    consider "set_pmf p ⊆ outcomes" | "¬set_pmf p ⊆ outcomes"
      by blast
    then show ?thesis 
    proof (cases)
      case 1
      have "finite outcomes" "set_pmf p ⊆ outcomes"
        by (auto simp: 1 asm) 
      then show ?thesis
      proof (induct  rule: pmf_mix_induct')
        case (degenerate x)
        then show ?case
          using B P_def deg set_pmf_subset_singleton by fastforce
      qed (simp add: P_def lotteries_on_def mix_of_not_preferred_is_not_preferred
               mix_of_not_preferred_is_not_preferred[of b p q a])
    qed  (simp add: lotteries_on_def P_def)
  qed
  moreover have "∀e ∈ 𝒫. b ≽[ℛ] e"
    using calculation B P_def set_pmf_subset_singleton by fastforce
  ultimately show ?thesis
    using b degenerate_lots_subset_all by blast
qed

lemma worst_degenerate_in_worst_overall: 
  "∃x ∈ degenerate_lotteries. ∀y ∈ 𝒫. y ≽[ℛ] x"
proof -
  obtain b where
    b: "b ∈ degenerate_lotteries" "∀y ∈ degenerate_lotteries. y ≽[ℛ] b"
    using exists_worst_degenerate by blast
  have asm: "finite outcomes" "set_pmf b ⊆ outcomes"
    by (simp add: fnt) (meson b(1) degenerate_lots_subset_all subset_iff support_in_outcomes)
  obtain B where B: "set_pmf b = {B}"
    using b card_1_singletonE degenerate_lotteries_def by blast
  have deg: "∀d∈outcomes. return_pmf d ≽[ℛ] b"
    using alt_definition_of_degenerate_lotteries b(2) by blast
  define P where
    "P = (λp. p ∈ 𝒫 ⟶ p ≽[ℛ] return_pmf B)"
  have "P p" for p
  proof -
    consider "set_pmf p ⊆ outcomes" | "¬set_pmf p ⊆ outcomes"
      by blast
    then show ?thesis 
    proof (cases)
      case 1
      have "finite outcomes" "set_pmf p ⊆ outcomes"
        by (auto simp: 1 asm) 
      then show ?thesis
      proof (induct rule: pmf_mix_induct')
        case (degenerate x)
        then show ?case
          using B P_def deg set_pmf_subset_singleton by fastforce
      next
      qed (simp add: P_def lotteries_on_def mix_of_preferred_is_preferred
          mix_of_not_preferred_is_not_preferred[of b p])
    qed (simp add: lotteries_on_def P_def)
  qed
  moreover have "∀e ∈ 𝒫. e ≽[ℛ] b"
    using calculation B P_def set_pmf_subset_singleton by fastforce
  ultimately show ?thesis
    using b degenerate_lots_subset_all by blast
qed 

lemma overall_best_nonempty:
  "best ≠ {}"
  using best_def best_degenerate_in_best_overall degenerate_lots_subset_all by blast

lemma overall_worst_nonempty:
  "worst ≠ {}"
  using degenerate_lots_subset_all worst_def worst_degenerate_in_worst_overall by auto


lemma trans_approx:
  assumes "x≈[ℛ] y" 
    and " y ≈[ℛ] z" 
  shows "x ≈[ℛ] z"
  using preference.indiff_trans[of 𝒫 ℛ x y z] assms rpr rational_preference_def by blast


text ‹ First EXPLICIT use of the axiom of choice ›

private definition some_best where
  "some_best = (SOME x. x ∈ degenerate_lotteries ∧ x ∈ best)"

private definition some_worst where
  "some_worst = (SOME x. x ∈ degenerate_lotteries ∧ x ∈ worst)"

private definition my_U :: "'a pmf ⇒ real"
  where
    "my_U p = (SOME α. α∈{0..1} ∧ p ≈[ℛ] mix_pmf α some_best some_worst)"

lemma exists_best_and_degenerate: "degenerate_lotteries ∩ best ≠ {}"
  using best_def best_degenerate_in_best_overall degenerate_lots_subset_all by blast


lemma exists_worst_and_degenerate: "degenerate_lotteries ∩ worst ≠ {}"
  using worst_def worst_degenerate_in_worst_overall degenerate_lots_subset_all by blast

lemma some_best_in_best: "some_best ∈ best"
  using exists_best_and_degenerate some_best_def
  by (metis (mono_tags, lifting) Int_emptyI some_eq_ex)

lemma some_worst_in_worst: "some_worst ∈ worst"
  using exists_worst_and_degenerate some_worst_def
  by (metis (mono_tags, lifting) Int_emptyI some_eq_ex)


lemma best_always_at_least_as_good_mix:
  assumes "α ∈ {0..1}"
    and "p ∈ 𝒫"
  shows "mix_pmf α some_best p ≽[ℛ] p"
  using assms(1) assms(2) best_def mix_of_preferred_is_preferred 
    rational_preference.compl rpr some_best_in_best by fastforce

lemma geq_mix_imp_weak_pref:
  assumes "α ∈ {0..1}"
    and "β ∈ {0..1}"
  assumes "α ≥ β"
  shows "mix_pmf α some_best some_worst ≽[ℛ] mix_pmf β some_best some_worst"
  using assms(1) assms(2) assms(3) best_def some_best_in_best some_worst_in_worst worst_def by auto

lemma gamma_inverse:
  assumes "α ∈ {0<..<1}"
    and "β ∈ {0<..<1}"
  shows "(1::real) - (α - β) / (1 - β) = (1 - α) / (1 - β)"
proof - 
  have "1 - (α - β) / (1 - β) =  (1 - β)/(1 - β) - (α - β) / (1 - β)"
    using assms(2) by auto
  also have "... = (1 - β - (α - β)) / (1 - β)"
    by (metis diff_divide_distrib)
  also have "... = (1 - α) / (1 - β)"
    by simp
  finally show ?thesis .
qed

lemma all_mix_pmf_indiff_indiff_best_worst:
  assumes "l ∈ 𝒫"
  assumes "b ∈ best"
  assumes "w ∈ worst"
  assumes "b ≈[ℛ] w"
  shows "∀α ∈{0..1}. l ≈[ℛ] mix_pmf α b w"
  by (meson assms best_worst_indiff_all_indiff(1) mix_of_preferred_is_preferred
      best_worst_indiff_all_indiff(2) mix_of_not_preferred_is_not_preferred)

lemma indiff_imp_same_utility_value:
  assumes "some_best ≻[ℛ] some_worst"
  assumes "α ∈ {0..1}"
  assumes "β ∈ {0..1}"
  assumes "mix_pmf β some_best some_worst ≈[ℛ] mix_pmf α some_best some_worst"
  shows "β = α"
  using assms(1) assms(2) assms(3) assms(4) linorder_neqE_linordered_idom by blast

lemma leq_mix_imp_weak_inferior:
  assumes "some_best ≻[ℛ] some_worst"
  assumes "α ∈ {0..1}"
    and "β ∈ {0..1}"
  assumes "mix_pmf β some_best some_worst ≽[ℛ] mix_pmf α some_best some_worst"
  shows "β ≥ α"
proof -
  have *: "mix_pmf β some_best some_worst ≈[ℛ] mix_pmf α some_best some_worst ⟹ α ≤ β"
    using assms(1) assms(2) assms(3) indiff_imp_same_utility_value by blast
  consider "mix_pmf β some_best some_worst ≻[ℛ] mix_pmf α some_best some_worst" |
    "mix_pmf β some_best some_worst ≈[ℛ] mix_pmf α some_best some_worst"
    using assms(4) by blast
  then show ?thesis
    by(cases) (meson assms(2) assms(3) geq_mix_imp_weak_pref le_cases *)+
qed

lemma ge_mix_pmf_preferred:
  assumes "x ≻[ℛ] y"
  assumes "α ∈ {0..1}"
    and "β ∈ {0..1}"
  assumes "α ≥ β"
  shows "(mix_pmf α x y) ≽[ℛ] (mix_pmf β x y)"
  using assms(1) assms(2) assms(3) assms(4) by blast



subsection ‹ Add continuity to assumptions ›
context
  assumes cnt: "continuous_vnm (lotteries_on outcomes) ℛ"
begin


text ‹ In Literature this is referred to as step 2. ›
lemma step_2_unique_continuous_unfolding:
  assumes "p ≽[ℛ] q"
    and "q ≽[ℛ] r"
    and "p ≻[ℛ] r"
  shows "∃!α ∈ {0..1}. q ≈[ℛ] mix_pmf α p r"
proof (rule ccontr)
  assume neg_a: "∄!α. α ∈ {0..1} ∧ q ≈[ℛ] mix_pmf α p r"
  have "∃α ∈ {0..1}. q ≈[ℛ] mix_pmf α p r"
    using non_unique_continuous_unfolding[of outcomes ℛ p q r] 
      assms cnt rpr by blast
  then obtain α β :: real where
    a_b: "α∈{0..1}" "β ∈{0..1}" "q ≈[ℛ] mix_pmf α p r" "q ≈[ℛ] mix_pmf β p r" "α ≠ β"
    using neg_a by blast
  consider "α > β" | "β > α"
    using a_b by linarith
  then show False
  proof (cases)
    case 1
    with step_1_most_general[of p r α β] assms 
    have "mix_pmf α p r ≻[ℛ] mix_pmf β p r"
      using a_b(1) a_b(2) by blast
    then show ?thesis using a_b
      by (meson rational_preference.strict_is_neg_transitive relation_in_carrier rpr)
  next
    case 2
    with step_1_most_general[of p r β α] assms have "mix_pmf β p r ≻[ℛ]mix_pmf α p r"
      using a_b(1) a_b(2) by blast
    then show ?thesis using a_b
      by (meson rational_preference.strict_is_neg_transitive relation_in_carrier rpr)
  qed
qed

text ‹ These folowing two lemmas are referred to sometimes called step 2. ›
lemma create_unique_indiff_using_distinct_best_worst:
  assumes "l ∈ 𝒫"
  assumes "b ∈ best"
  assumes "w ∈ worst"
  assumes "b ≻[ℛ] w"
  shows "∃!α ∈{0..1}. l ≈[ℛ] mix_pmf α b w"
proof -
  have "b ≽[ℛ] l" 
    using best_def
    using assms by blast
  moreover have "l ≽[ℛ] w"
    using worst_def assms by blast
  ultimately show "∃!α∈{0..1}. l ≈[ℛ] mix_pmf α b w"
    using step_2_unique_continuous_unfolding[of b l w] assms by linarith
qed

lemma exists_element_bw_mix_is_approx:
  assumes "l ∈ 𝒫"
  assumes "b ∈ best"
  assumes "w ∈ worst"
  shows "∃α ∈{0..1}. l ≈[ℛ] mix_pmf α b w"
proof -
  consider "b ≻[ℛ] w" | "b ≈[ℛ] w"
    using assms(2) assms(3) best_def worst_def by auto
  then show ?thesis
  proof (cases)
    case 1
    then show ?thesis 
      using create_unique_indiff_using_distinct_best_worst assms by blast  
  qed (auto simp: all_mix_pmf_indiff_indiff_best_worst assms)
qed

lemma my_U_is_defined:
  assumes "p ∈ 𝒫"
  shows "my_U p ∈ {0..1}" "p ≈[ℛ] mix_pmf (my_U p) some_best some_worst"
proof -
  have "some_best ∈ best" 
    by (simp add: some_best_in_best)
  moreover have "some_worst ∈ worst"
    by (simp add: some_worst_in_worst)
  with exists_element_bw_mix_is_approx[of p "some_best" "some_worst"] calculation assms
  have e: "∃α∈{0..1}. p ≈[ℛ] mix_pmf α some_best some_worst" by blast
  then show "my_U p ∈ {0..1}"
    by (metis (mono_tags, lifting) my_U_def someI_ex)
  show "p ≈[ℛ] mix_pmf (my_U p) some_best some_worst" 
    by (metis (mono_tags, lifting) e my_U_def someI_ex)
qed 

lemma weak_pref_mix_with_my_U_weak_pref:
  assumes "p ≽[ℛ] q"
  shows "mix_pmf (my_U p) some_best some_worst ≽[ℛ] mix_pmf (my_U q) some_best some_worst"
  by (meson assms my_U_is_defined(2) relation_in_carrier rpr 
      rational_preference.weak_is_transitive)

lemma preferred_greater_my_U: 
  assumes "p ∈ 𝒫"
    and "q ∈ 𝒫"
  assumes "mix_pmf (my_U p) some_best some_worst ≻[ℛ] mix_pmf (my_U q) some_best some_worst"
  shows "my_U p > my_U q"
proof (rule ccontr)
  assume "¬ my_U p > my_U q"
  then consider "my_U p = my_U q" | "my_U p < my_U q"
    by linarith
  then show False 
  proof (cases)
    case 1
    then have "mix_pmf (my_U p) some_best some_worst ≈[ℛ] mix_pmf (my_U q) some_best some_worst"
      using assms by auto
    then show ?thesis using assms by blast
  next
    case 2
    moreover have "my_U q ∈ {0..1}"
      using assms(2) my_U_is_defined(1) by blast
    moreover have "my_U p ∈ {0..1}"
      using assms(1) my_U_is_defined(1) by blast
    moreover have "mix_pmf (my_U q) some_best some_worst ≽[ℛ] mix_pmf (my_U p) some_best some_worst"
      using calculation geq_mix_imp_weak_pref by auto
    then show ?thesis using assms by blast
  qed
qed

lemma geq_my_U_imp_weak_preference:
  assumes "p ∈ 𝒫" 
    and "q ∈ 𝒫" 
  assumes "some_best ≻[ℛ] some_worst"
  assumes "my_U p ≥ my_U q"
  shows "p ≽[ℛ] q"
proof -
  have p_q: "my_U p ∈ {0..1}" "my_U q ∈ {0..1}"
    using assms my_U_is_defined(1) by blast+
  with ge_mix_pmf_preferred[of "some_best" "some_worst" "my_U p" "my_U q"] 
    p_q assms(1) assms(3) assms(4)
  have "mix_pmf (my_U p) some_best some_worst ≽[ℛ] mix_pmf (my_U q) some_best some_worst"  by blast
  consider "my_U p = my_U q" | "my_U p > my_U q"
    using assms by linarith
  then show ?thesis
  proof (cases)
    case 2
    then show ?thesis
      by (meson assms(1) assms(2) assms(3) p_q(1) p_q(2) rational_preference.compl 
          rpr step_1_most_general weak_pref_mix_with_my_U_weak_pref)
  qed (metis assms(1) assms(2) my_U_is_defined(2) trans_approx)
qed

lemma my_U_represents_pref:
  assumes "some_best ≻[ℛ] some_worst"
  assumes "p ∈ 𝒫" 
    and "q ∈ 𝒫" 
  shows "p ≽[ℛ] q ⟷ my_U p ≥ my_U q" (is "?L ⟷ ?R")
proof -
  have p_def: "my_U p∈ {0..1}" "my_U q ∈ {0..1}"
    using assms my_U_is_defined by blast+
  show ?thesis
  proof
    assume a: ?L
    hence "mix_pmf (my_U p) some_best some_worst ≽[ℛ] mix_pmf (my_U q) some_best some_worst"
      using weak_pref_mix_with_my_U_weak_pref by auto
    then show ?R using leq_mix_imp_weak_inferior[of "my_U p" "my_U q"] p_def a
        assms(1) leq_mix_imp_weak_inferior by blast
  next 
    assume ?R
    then show ?L using geq_my_U_imp_weak_preference
      using assms(1) assms(2) assms(3) by blast
  qed
qed

lemma first_iff_u_greater_strict_preff:
  assumes "p ∈ 𝒫"
    and "q ∈ 𝒫"
  assumes "some_best ≻[ℛ] some_worst"
  shows "my_U p > my_U q ⟷ mix_pmf (my_U p) some_best some_worst ≻[ℛ] mix_pmf (my_U q) some_best some_worst"
proof
  assume a: "my_U p > my_U q"
  have "my_U p ∈ {0..1}" "my_U q ∈ {0..1}"
    using assms my_U_is_defined(1) by blast+
  then show "mix_pmf (my_U p) some_best some_worst ≻[ℛ] mix_pmf (my_U q) some_best some_worst" 
    using a assms(3) by blast
next
  assume a: "mix_pmf (my_U p) some_best some_worst ≻[ℛ] mix_pmf (my_U q) some_best some_worst"
  have "my_U p ∈ {0..1}" "my_U q ∈ {0..1}"
    using assms my_U_is_defined(1) by blast+
  then show "my_U p > my_U q "
    using preferred_greater_my_U[of p q] assms a by blast
qed

lemma second_iff_calib_mix_pref_strict_pref:
  assumes "p ∈ 𝒫"
    and "q ∈ 𝒫"
  assumes "some_best ≻[ℛ] some_worst"
  shows "mix_pmf (my_U p) some_best some_worst ≻[ℛ] mix_pmf (my_U q) some_best some_worst ⟷ p ≻[ℛ] q"
proof
  assume a: "mix_pmf (my_U p) some_best some_worst ≻[ℛ] mix_pmf (my_U q) some_best some_worst"
  have "my_U p ∈ {0..1}" "my_U q ∈ {0..1}"
    using assms my_U_is_defined(1) by blast+
  then show "p ≻[ℛ] q" 
    using a assms(3) assms(1) assms(2) geq_my_U_imp_weak_preference 
      leq_mix_imp_weak_inferior weak_pref_mix_with_my_U_weak_pref by blast
next
  assume a: "p ≻[ℛ] q"
  have "my_U p ∈ {0..1}" "my_U q ∈ {0..1}"
    using assms my_U_is_defined(1) by blast+
  then show "mix_pmf (my_U p) some_best some_worst ≻[ℛ] mix_pmf (my_U q) some_best some_worst"
    using a assms(1) assms(2) assms(3) leq_mix_imp_weak_inferior my_U_represents_pref by blast
qed

lemma my_U_is_linear_function:
  assumes "p ∈ 𝒫"
    and "q ∈ 𝒫"
    and "α ∈ {0..1}"
  assumes "some_best ≻[ℛ] some_worst" 
  shows "my_U (mix_pmf α p q) = α * my_U p + (1 - α) * my_U q"
proof - 
  define B where B: "B = some_best"
  define W where W:"W = some_worst"
  define Up where Up: "Up = my_U p"
  define Uq where Uq: "Uq = my_U q"
  have long_in: "(α * Up + (1 - α) * Uq) ∈ {0..1}"
  proof -
    have "Up ∈ {0..1}"
      using assms Up my_U_is_defined(1) by blast
    moreover have "Uq ∈ {0..1}"
      using assms Uq my_U_is_defined(1) by blast
    moreover have "α * Up ∈ {0..1}"
      using ‹Up ∈ {0..1}› assms(3) mult_le_one by auto
    moreover have "1-α ∈ {0..1}"
      using assms(3) by auto
    moreover  have "(1 - α) * Uq ∈ {0..1}"
      using mult_le_one[of "1-α" Uq] calculation(2) calculation(4) by auto
    ultimately show ?thesis
      using add_nonneg_nonneg[of "α * Up" "(1 - α) * Uq"] 
        convex_bound_le[of Up 1 Uq α "1-α"] by simp
  qed
  have fst: "p ≈[ℛ] (mix_pmf Up B W)"
    using assms my_U_is_defined[of p] B W Up by simp
  have snd: "q ≈[ℛ] (mix_pmf Uq B W)"
    using assms my_U_is_defined[of q] B W Uq by simp
  have mp_in: "(mix_pmf Up B W) ∈ 𝒫"
    using fst relation_in_carrier by blast
  have f2: "mix_pmf α p q ≈[ℛ] mix_pmf α (mix_pmf Up B W) q"
    using fst assms(2) assms(3) mix_pmf_preferred_independence by blast
  have **: "mix_pmf α (mix_pmf Up B W) (mix_pmf Uq B W) = 
            mix_pmf (α * Up + (1-α) * Uq) B W" (is "?L = ?R")
  proof -
    let ?mixPQ = "(mix_pmf (α * Up + (1 - α) * Uq) B W)"
    have "∀e∈set_pmf ?L. pmf (?L) e = pmf ?mixPQ e"
    proof 
      fix e 
      assume asm: "e ∈ set_pmf ?L"
      have i1: "pmf (?L) e = α * pmf (mix_pmf Up B W) e + 
        pmf (mix_pmf Uq B W) e - α * pmf (mix_pmf Uq B W) e" 
        using pmf_mix_deeper[of α "mix_pmf Up B W" "(mix_pmf Uq B W)" e] assms(3) by blast
      have i3: "... = α * Up * pmf B e + α * pmf W e - α * Up * pmf W e + Uq * pmf B e + 
        pmf W e - Uq * pmf W e - α * Uq * pmf B e - α * pmf W e + α * Uq * pmf W e"
        using left_diff_distrib' pmf_mix_deeper[of Up B W e] pmf_mix_deeper[of Uq B W e]
          assms Up Uq my_U_is_defined(1) by (simp add: distrib_left right_diff_distrib)
      have j4: "pmf ?mixPQ e = (α * Up + (1 - α) * Uq) * pmf B e + 
        pmf W e - (α * Up + (1 - α) * Uq) * pmf W e" 
        using pmf_mix_deeper[of "(α * Up + (1 - α) * Uq)" B W e] long_in by blast
      then show "pmf (?L) e = pmf ?mixPQ e"
        by (simp add: i1 i3 mult.commute right_diff_distrib' ring_class.ring_distribs(1))
    qed
    then show ?thesis using pmf_equiv_intro1 by blast
  qed
  have "mix_pmf α (mix_pmf Up B W) q ≈[ℛ] ?L"
    using approx_remains_after_same_comp_left assms(3) mp_in snd by blast
  hence *: "mix_pmf α p q ≈[ℛ] mix_pmf α (mix_pmf (my_U p) B W) (mix_pmf (my_U q) B W)"
    using Up Uq f2 trans_approx by blast
  have "mix_pmf α (mix_pmf (my_U p) B W) (mix_pmf (my_U q) B W) = ?R"
    using Up Uq ** by blast
  hence "my_U (mix_pmf α p q) = α * Up + (1-α) * Uq"
    by (metis * B W assms(4) indiff_imp_same_utility_value long_in 
        my_U_is_defined(1) my_U_is_defined(2) my_U_represents_pref relation_in_carrier)
  then show ?thesis
    using Up Uq by blast
qed


text ‹ Now we define a more general Utility 
       function that also takes the degenerate case into account ›
private definition general_U 
  where
    "general_U p = (if some_best ≈[ℛ] some_worst then 1 else my_U p)"

lemma general_U_is_linear_function:
  assumes "p ∈ 𝒫"
    and "q ∈ 𝒫"
    and "α ∈ {0..1}"
  shows "general_U (mix_pmf α p q) = α * (general_U p) + (1 - α) * (general_U q)"
proof -
  consider "some_best ≻[ℛ] some_worst" | "some_best ≈[ℛ] some_worst"
    using best_def some_best_in_best some_worst_in_worst worst_def by auto
  then show ?thesis
  proof (cases, goal_cases)
    case 1
    then show ?case
      using assms(1) assms(2) assms(3) general_U_def my_U_is_linear_function by auto
  next
    case 2
    then show ?case 
      using assms(1) assms(2) assms(3) general_U_def by auto
  qed
qed

lemma general_U_ordinal_Utility:
  shows "ordinal_utility 𝒫 ℛ general_U"
proof (standard, goal_cases)
  case (1 x y)
  consider (a) "some_best ≻[ℛ] some_worst" | (b) "some_best ≈[ℛ] some_worst"
    using best_def some_best_in_best some_worst_in_worst worst_def by auto
  then show ?case
  proof (cases, goal_cases)
    case a
    have "some_best ≻[ℛ] some_worst"
      using a by auto
    then show "x ≽[ℛ] y = (general_U y ≤ general_U x)"
      using 1 my_U_represents_pref[of x y] general_U_def by simp
  next
    case b
    have "general_U x = 1" "general_U y = 1"
      by (simp add: b general_U_def)+
    moreover have "x ≈[ℛ] y" using b
      by (meson "1"(1) "1"(2) best_worst_indiff_all_indiff(1) 
          some_best_in_best some_worst_in_worst trans_approx)
    ultimately show "x ≽[ℛ] y = (general_U y ≤ general_U x)"
      using general_U_def by linarith
  qed
next
  case (2 x y)
  then show ?case
    using relation_in_carrier by blast
next
  case (3 x y)
  then show ?case
    using relation_in_carrier by blast
qed

text ‹  Proof of the linearity of general-U. 
        If we consider the definition of expected utility 
        functions from Maschler, Solan, Zamir we are done. ›

theorem is_linear:
  assumes "p ∈ 𝒫"
    and "q ∈ 𝒫"
    and "α ∈ {0..1}"
  shows "∃u. u (mix_pmf α p q) = α * (u p) + (1-α) * (u q)"
proof
  let ?u = "general_U"
  consider "some_best ≻[ℛ] some_worst" | "some_best ≈[ℛ] some_worst"
    using best_def some_best_in_best some_worst_in_worst worst_def by auto
  then show "?u (mix_pmf α p q) = α * ?u p + (1 - α) * ?u q"
  proof (cases)
    case 1
    then show ?thesis
      using assms(1) assms(2) assms(3) general_U_def my_U_is_linear_function by auto
  next
    case 2
    then show ?thesis
      by (simp add: general_U_def)
  qed
qed


text ‹ Now I define a Utility function that assigns a utility to all outcomes. 
       These are only finitely many ›
private definition ocU 
  where
    "ocU p = general_U (return_pmf p)"

lemma geral_U_is_expected_value_of_ocU:
  assumes "set_pmf p ⊆ outcomes"
  shows "general_U p = measure_pmf.expectation p ocU"
  using fnt assms
proof (induct rule: pmf_mix_induct')
  case (mix p q a)
  hence "general_U (mix_pmf a p q) = a * general_U p + (1-a) * general_U q"
    using general_U_is_linear_function[of p q a] mix.hyps assms lotteries_on_def mix.hyps by auto
  also have "... = a * measure_pmf.expectation p ocU + (1-a) * measure_pmf.expectation q ocU"
    by (simp add: mix.hyps(4) mix.hyps(5))
  also have "... = measure_pmf.expectation (mix_pmf a p q) ocU"
    using general_U_is_linear_function expected_value_mix_pmf_distrib fnt infinite_super mix.hyps(1)
    by (metis fnt mix.hyps(2) mix.hyps(3))
  finally show ?case .
qed (auto simp: support_in_outcomes assms fnt integral_measure_pmf_real ocU_def)

lemma ordinal_utility_expected_value:
  "ordinal_utility 𝒫 ℛ (λx. measure_pmf.expectation x ocU)"
proof (standard, goal_cases)
  case (1 x y)
  have ocs: "set_pmf x ⊆ outcomes" "set_pmf y ⊆ outcomes"
    by (meson "1" subsetI support_in_outcomes)+
  have "x ≽[ℛ] y ⟹ (measure_pmf.expectation y ocU ≤ measure_pmf.expectation x ocU)"
  proof -
    assume "x ≽[ℛ] y"
    have "general_U x ≥ general_U y"
      by (meson ‹x ≽[ℛ] y› general_U_ordinal_Utility ordinal_utility_def)
    then show "(measure_pmf.expectation y ocU ≤ measure_pmf.expectation x ocU)"
      using geral_U_is_expected_value_of_ocU ocs by auto
  qed
  moreover have "(measure_pmf.expectation y ocU ≤ measure_pmf.expectation x ocU) ⟹ x ≽[ℛ] y"
  proof - 
    assume "(measure_pmf.expectation y ocU ≤ measure_pmf.expectation x ocU)"
    then have "general_U x ≥ general_U y"
      by (simp add:  geral_U_is_expected_value_of_ocU ocs(1) ocs(2))
    then show "x ≽[ℛ] y"
      by (meson "1"(1) "1"(2) general_U_ordinal_Utility ordinal_utility.util_def)
  qed
  ultimately show ?case 
    by blast
next
  case (2 x y)
  then show ?case
    using relation_in_carrier by blast
next
  case (3 x y)
  then show ?case
    using relation_in_carrier by auto
qed

lemma ordinal_utility_expected_value':
  "∃u. ordinal_utility 𝒫 ℛ (λx. measure_pmf.expectation x u)"
  using ordinal_utility_expected_value by blast

lemma ocU_is_expected_utility_bernoulli:
  shows "∀x ∈ 𝒫. ∀y ∈ 𝒫. x ≽[ℛ] y ⟷ 
  measure_pmf.expectation x ocU ≥ measure_pmf.expectation y ocU"
  using ordinal_utility_expected_value by (meson ordinal_utility.util_def)


end  (* continuous *)

end(* finite outcomes *)

end (* system U *)


lemma expected_value_is_utility_function:
  assumes fnt: "finite outcomes" and "outcomes ≠ {}"
  assumes "x ∈ lotteries_on outcomes" and "y ∈ lotteries_on outcomes"
  assumes "ordinal_utility (lotteries_on outcomes) ℛ (λx. measure_pmf.expectation x u)"
  shows "measure_pmf.expectation x u ≥ measure_pmf.expectation y u ⟷ x ≽[ℛ] y" (is "?L ⟷ ?R")
  using assms(3) assms(4) assms(5) ordinal_utility.util_def_conf 
    ordinal_utility.ordinal_utility_left iffI  by (metis (no_types, lifting))


lemma system_U_implies_vNM_utility:
  assumes fnt: "finite outcomes" and "outcomes ≠ {}"
  assumes rpr: "rational_preference (lotteries_on outcomes) ℛ"
  assumes ind: "independent_vnm (lotteries_on outcomes) ℛ"
  assumes cnt: "continuous_vnm (lotteries_on outcomes) ℛ"
  shows "∃u. ordinal_utility (lotteries_on outcomes) ℛ (λx. measure_pmf.expectation x u)"
  using ordinal_utility_expected_value'[of outcomes ℛ] assms by blast

lemma vNM_utility_implies_rationality:
  assumes fnt: "finite outcomes" and "outcomes ≠ {}"
  assumes "∃u. ordinal_utility (lotteries_on outcomes) ℛ (λx. measure_pmf.expectation x u)"
  shows "rational_preference (lotteries_on outcomes) ℛ"
  using assms(3) ordinal_util_imp_rat_prefs by blast

theorem vNM_utility_implies_independence:
  assumes fnt: "finite outcomes" and "outcomes ≠ {}"
  assumes "∃u. ordinal_utility (lotteries_on outcomes) ℛ (λx. measure_pmf.expectation x u)"
  shows "independent_vnm (lotteries_on outcomes) ℛ"
proof (rule independent_vnmI2)
  fix p  q r 
    and α::real
  assume a1: "p ∈ 𝒫 outcomes" 
  assume a2: "q ∈ 𝒫 outcomes" 
  assume a3: "r ∈ 𝒫 outcomes" 
  assume a4: "α ∈ {0<..1}"
  have in_lots: "mix_pmf α p r ∈ lotteries_on outcomes" "mix_pmf α q r ∈ lotteries_on outcomes" 
    using a1 a3 a4 mix_in_lot apply fastforce
    using a2 a3 a4 mix_in_lot by fastforce
  have fnts: "finite (set_pmf p)" "finite (set_pmf q)" "finite (set_pmf r)"
    using a1 a2 a3 fnt infinite_super lotteries_on_def by blast+
  obtain u where
    u: "ordinal_utility (lotteries_on outcomes) ℛ (λx. measure_pmf.expectation x u)"
    using assms by blast
  have "p ≽[ℛ] q ⟹ mix_pmf α p r ≽[ℛ] mix_pmf α q r"
  proof -
    assume "p ≽[ℛ] q"
    hence f: "measure_pmf.expectation p u ≥ measure_pmf.expectation q u"
      using u a1 a2 ordinal_utility.util_def by fastforce
    have "measure_pmf.expectation (mix_pmf α p r) u ≥ measure_pmf.expectation (mix_pmf α q r) u"
    proof -
      have "measure_pmf.expectation (mix_pmf α p r) u = 
        α * measure_pmf.expectation p u + (1 - α) * measure_pmf.expectation r u"
        using expected_value_mix_pmf_distrib[of p r α u] assms fnts a4 by fastforce
      moreover have "measure_pmf.expectation (mix_pmf α q r) u = 
        α * measure_pmf.expectation q u + (1 - α) * measure_pmf.expectation r u"
        using expected_value_mix_pmf_distrib[of q r α u] assms fnts a4 by fastforce
      ultimately show ?thesis using f using a4 by auto
    qed
    then show "mix_pmf α p r ≽[ℛ] mix_pmf α q r"
      using u ordinal_utility_expected_value' ocU_is_expected_utility_bernoulli in_lots
      by (simp add: in_lots ordinal_utility_def)
  qed
  moreover have "mix_pmf α p r ≽[ℛ] mix_pmf α q r ⟹ p ≽[ℛ] q" 
  proof -
    assume "mix_pmf α p r ≽[ℛ] mix_pmf α q r"
    hence f:"measure_pmf.expectation (mix_pmf α p r) u ≥ measure_pmf.expectation (mix_pmf α q r) u" 
      using ordinal_utility.ordinal_utility_left u by fastforce
    hence "measure_pmf.expectation p u ≥ measure_pmf.expectation q u"
    proof -
      have "measure_pmf.expectation (mix_pmf α p r) u = 
        α * measure_pmf.expectation p u + (1 - α) * measure_pmf.expectation r u"
        using expected_value_mix_pmf_distrib[of p r α u] assms fnts a4 by fastforce
      moreover have "measure_pmf.expectation (mix_pmf α q r) u = 
        α * measure_pmf.expectation q u + (1 - α) * measure_pmf.expectation r u"
        using expected_value_mix_pmf_distrib[of q r α u] assms fnts a4 by fastforce
      ultimately show ?thesis using f using a4 by auto
    qed
    then show "p ≽[ℛ] q"
      using a1 a2 ordinal_utility.util_def_conf u by fastforce
  qed
  ultimately show "p ≽[ℛ] q = mix_pmf α p r ≽[ℛ] mix_pmf α q r"
    by blast
qed

lemma exists_weight_for_equality:
  assumes "a > c" and "a ≥ b" and "b ≥ c"
  shows   "∃(e::real) ∈ {0..1}. (1-e) * a + e * c = b"
proof -
  from assms have "b ∈ closed_segment a c"
    by (simp add: closed_segment_eq_real_ivl)
  thus ?thesis by (auto simp: closed_segment_def)
qed

lemma vNM_utilty_implies_continuity:
  assumes fnt: "finite outcomes" and "outcomes ≠ {}"
  assumes "∃u. ordinal_utility (lotteries_on outcomes) ℛ (λx. measure_pmf.expectation x u)"
  shows "continuous_vnm (lotteries_on outcomes) ℛ"
proof (rule continuous_vnmI)
  fix p q r
  assume a1: "p ∈ 𝒫 outcomes" 
  assume a2: "q ∈ 𝒫 outcomes" 
  assume a3: "r ∈ 𝒫 outcomes " 
  assume a4: "p ≽[ℛ] q ∧ q ≽[ℛ] r"
  then have g: "p ≽[ℛ] r"
    by (meson assms(3) ordinal_utility.util_imp_trans transD)
  obtain u where 
    u: "ordinal_utility (lotteries_on outcomes) ℛ (λx. measure_pmf.expectation x u)"
    using assms by blast
  have geqa: "measure_pmf.expectation p u ≥ measure_pmf.expectation q u" 
    "measure_pmf.expectation q u ≥ measure_pmf.expectation r u"
    using a4 u by (meson ordinal_utility.ordinal_utility_left)+
  have fnts: "finite p" "finite q" "finite r"
    using a1 a2 a3 fnt infinite_super lotteries_on_def by auto+
  consider "p ≻[ℛ] r" | "p ≈[ℛ] r"
    using g by auto
  then show "∃α∈{0..1}. mix_pmf α p r ≈[ℛ] q"
  proof (cases)
    case 1
    define a where a: "a = measure_pmf.expectation p u"
    define b where b: "b = measure_pmf.expectation r u"
    define c where c: "c = measure_pmf.expectation q u"
    have "a > b"
      using "1" a1 a2 a3 a b ordinal_utility.util_def_conf u by force
    have "c ≤ a" "b ≤ c"
      using geqa a b c by blast+
    then obtain e ::real where
      e: "e ∈ {0..1}" "(1-e) * a + e * b = c"
      using exists_weight_for_equality[of b a c] ‹b < a› by blast
    have *:"1-e ∈ {0..1}"
      using e(1) by auto
    hence "measure_pmf.expectation (mix_pmf (1-e) p r) u = 
     (1-e) * measure_pmf.expectation p u + e * measure_pmf.expectation r u"
      using expected_value_mix_pmf_distrib[of p r "1-e" u] fnts by fastforce
    also have "... = (1-e) * a + e * b"
      using a b by auto
    also have "... = c"
      using c e by auto
    finally have f: "measure_pmf.expectation (mix_pmf (1-e) p r) u =  measure_pmf.expectation q u"
      using c by blast
    hence "mix_pmf (1-e) p r ≈[ℛ] q"
      using expected_value_is_utility_function[of outcomes "mix_pmf (1-e) p r" q ℛ u] *
    proof -
      have "mix_pmf (1 - e) p r ∈ 𝒫 outcomes"
        using ‹1 - e ∈ {0..1}› a1 a3 mix_in_lot by blast
      then show ?thesis
        using f a2 ordinal_utility.util_def u by fastforce
    qed 
    then show ?thesis
      using exists_weight_for_equality expected_value_mix_pmf_distrib * by blast
  next
    case 2
    have "r ≈[ℛ] q"
      by (meson "2" a4 assms(3) ordinal_utility.util_imp_trans transD)
    then show ?thesis  by force
  qed
qed

theorem Von_Neumann_Morgenstern_Utility_Theorem:
  assumes fnt: "finite outcomes" and "outcomes ≠ {}"
  shows "rational_preference (lotteries_on outcomes) ℛ ∧ 
         independent_vnm (lotteries_on outcomes) ℛ ∧ 
         continuous_vnm (lotteries_on outcomes) ℛ ⟷ 
   (∃u. ordinal_utility (lotteries_on outcomes) ℛ (λx. measure_pmf.expectation x u))"
  using vNM_utility_implies_independence[OF assms, of ℛ] 
    system_U_implies_vNM_utility[OF assms, of ℛ]
    vNM_utilty_implies_continuity[OF assms, of ℛ]
    ordinal_util_imp_rat_prefs[of "lotteries_on outcomes" ℛ] by auto


end