Theory Stochastic_Dominance
section ‹Stochastic Dominance›
theory Stochastic_Dominance
imports
Complex_Main
"HOL-Probability.Probability"
Lotteries
Preference_Profiles
Utility_Functions
begin
subsection ‹Definition of Stochastic Dominance›
text ‹
This is the definition of stochastic dominance. It lifts a preference relation
on alternatives to the stochastic dominance ordering on lotteries.
›
definition SD :: "'alt relation ⇒ 'alt lottery relation" where
"p ≽[SD(R)] q ⟷ p ∈ lotteries_on {x. R x x} ∧ q ∈ lotteries_on {x. R x x} ∧
(∀x. R x x ⟶ measure_pmf.prob p {y. y ≽[R] x} ≥
measure_pmf.prob q {y. y ≽[R] x})"
lemma SD_empty [simp]: "SD (λ_ _. False) = (λ_ _. False)"
by (auto simp: fun_eq_iff SD_def lotteries_on_def set_pmf_not_empty)
text ‹
Stochastic dominance over any relation is a preorder.
›
lemma SD_refl: "p ≼[SD(R)] p ⟷ p ∈ lotteries_on {x. R x x}"
by (simp add: SD_def)
lemma SD_trans [simp, trans]: "p ≼[SD(R)] q ⟹ q ≼[SD(R)] r ⟹ p ≼[SD(R)] r"
unfolding SD_def by (auto intro: order.trans)
lemma SD_is_preorder: "preorder_on (lotteries_on {x. R x x}) (SD R)"
by unfold_locales (auto simp: SD_def intro: order.trans)
context preorder_on
begin
lemma SD_preorder:
"p ≽[SD(le)] q ⟷ p ∈ lotteries_on carrier ∧ q ∈ lotteries_on carrier ∧
(∀x∈carrier. measure_pmf.prob p (preferred_alts le x) ≥
measure_pmf.prob q (preferred_alts le x))"
by (simp add: SD_def preferred_alts_def carrier_eq)
lemma SD_preorderI [intro?]:
assumes "p ∈ lotteries_on carrier" "q ∈ lotteries_on carrier"
assumes "⋀x. x ∈ carrier ⟹
measure_pmf.prob p (preferred_alts le x) ≥ measure_pmf.prob q (preferred_alts le x)"
shows "p ≽[SD(le)] q"
using assms by (simp add: SD_preorder)
lemma SD_preorderD:
assumes "p ≽[SD(le)] q"
shows "p ∈ lotteries_on carrier" "q ∈ lotteries_on carrier"
and "⋀x. x ∈ carrier ⟹
measure_pmf.prob p (preferred_alts le x) ≥ measure_pmf.prob q (preferred_alts le x)"
using assms unfolding SD_preorder by simp_all
lemma SD_refl' [simp]: "p ≼[SD(le)] p ⟷ p ∈ lotteries_on carrier"
by (simp add: SD_def carrier_eq)
lemma SD_is_preorder': "preorder_on (lotteries_on carrier) (SD(le))"
using SD_is_preorder[of le] by (simp add: carrier_eq)
lemma SD_singleton_left:
assumes "x ∈ carrier" "q ∈ lotteries_on carrier"
shows "return_pmf x ≼[SD(le)] q ⟷ (∀y∈set_pmf q. x ≼[le] y)"
proof
assume SD: "return_pmf x ≼[SD(le)] q"
from assms SD_preorderD(3)[OF SD, of x]
have "measure_pmf.prob (return_pmf x) (preferred_alts le x) ≤
measure_pmf.prob q (preferred_alts le x)" by simp
also from assms have "measure_pmf.prob (return_pmf x) (preferred_alts le x) = 1"
by (simp add: indicator_def)
finally have "AE y in q. y ≽[le] x"
by (simp add: measure_pmf.measure_ge_1_iff measure_pmf.prob_eq_1 preferred_alts_def)
thus "∀y∈set_pmf q. y ≽[le] x" by (simp add: AE_measure_pmf_iff)
next
assume A: "∀y∈set_pmf q. x ≼[le] y"
show "return_pmf x ≼[SD(le)] q"
proof (rule SD_preorderI)
fix y assume y: "y ∈ carrier"
show "measure_pmf.prob (return_pmf x) (preferred_alts le y)
≤ measure_pmf.prob q (preferred_alts le y)"
proof (cases "y ≼[le] x")
case True
from True A have "measure_pmf.prob q (preferred_alts le y) = 1"
by (auto simp: AE_measure_pmf_iff measure_pmf.prob_eq_1 preferred_alts_def intro: trans)
thus ?thesis by simp
qed (simp_all add: preferred_alts_def indicator_def measure_nonneg)
qed (insert assms, simp_all add: lotteries_on_def)
qed
lemma SD_singleton_right:
assumes x: "x ∈ carrier" and q: "q ∈ lotteries_on carrier"
shows "q ≼[SD(le)] return_pmf x ⟷ (∀y∈set_pmf q. y ≼[le] x)"
proof safe
fix y assume SD: "q ≼[SD(le)] return_pmf x" and y: "y ∈ set_pmf q"
from y assms have [simp]: "y ∈ carrier" by (auto simp: lotteries_on_def)
from y have "0 < measure_pmf.prob q (preferred_alts le y)"
by (rule measure_pmf_posI) simp_all
also have "… ≤ measure_pmf.prob (return_pmf x) (preferred_alts le y)"
by (rule SD_preorderD(3)[OF SD]) simp_all
finally show "y ≼[le] x"
by (auto simp: indicator_def preferred_alts_def split: if_splits)
next
assume A: "∀y∈set_pmf q. y ≼[le] x"
show "q ≼[SD(le)] return_pmf x"
proof (rule SD_preorderI)
fix y assume y: "y ∈ carrier"
show "measure_pmf.prob q (preferred_alts le y) ≤
measure_pmf.prob (return_pmf x) (preferred_alts le y)"
proof (cases "y ≼[le] x")
case False
with A show ?thesis
by (auto simp: preferred_alts_def indicator_def measure_le_0_iff
measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: trans)
qed (simp_all add: indicator_def preferred_alts_def)
qed (insert assms, simp_all add: lotteries_on_def)
qed
lemma SD_strict_singleton_left:
assumes "x ∈ carrier" "q ∈ lotteries_on carrier"
shows "return_pmf x ≺[SD(le)] q ⟷ (∀y∈set_pmf q. x ≼[le] y) ∧ (∃y∈set_pmf q. (x ≺[le] y))"
using assms by (auto simp add: strongly_preferred_def SD_singleton_left SD_singleton_right)
lemma SD_strict_singleton_right:
assumes "x ∈ carrier" "q ∈ lotteries_on carrier"
shows "q ≺[SD(le)] return_pmf x ⟷ (∀y∈set_pmf q. y ≼[le] x) ∧ (∃y∈set_pmf q. (y ≺[le] x))"
using assms by (auto simp add: strongly_preferred_def SD_singleton_left SD_singleton_right)
lemma SD_singleton [simp]:
"x ∈ carrier ⟹ y ∈ carrier ⟹ return_pmf x ≼[SD(le)] return_pmf y ⟷ x ≼[le] y"
by (subst SD_singleton_left) (simp_all add: lotteries_on_def)
lemma SD_strict_singleton [simp]:
"x ∈ carrier ⟹ y ∈ carrier ⟹ return_pmf x ≺[SD(le)] return_pmf y ⟷ x ≺[le] y"
by (simp add: strongly_preferred_def)
end
context pref_profile_wf
begin
context
fixes i assumes i: "i ∈ agents"
begin
interpretation Ri: preorder_on alts "R i" by (simp add: i)
lemmas SD_singleton_left = Ri.SD_singleton_left
lemmas SD_singleton_right = Ri.SD_singleton_right
lemmas SD_strict_singleton_left = Ri.SD_strict_singleton_left
lemmas SD_strict_singleton_right = Ri.SD_strict_singleton_right
lemmas SD_singleton = Ri.SD_singleton
lemmas SD_strict_singleton = Ri.SD_strict_singleton
end
end
lemmas (in pref_profile_wf) [simp] = SD_singleton SD_strict_singleton
subsection ‹Stochastic Dominance for preference profiles›
context pref_profile_wf
begin
lemma SD_pref_profile:
assumes "i ∈ agents"
shows "p ≽[SD(R i)] q ⟷ p ∈ lotteries_on alts ∧ q ∈ lotteries_on alts ∧
(∀x∈alts. measure_pmf.prob p (preferred_alts (R i) x) ≥
measure_pmf.prob q (preferred_alts (R i) x))"
proof -
from assms interpret total_preorder_on alts "R i" by simp
have "preferred_alts (R i) x = {y. y ≽[R i] x}" for x using not_outside
by (auto simp: preferred_alts_def)
thus ?thesis by (simp add: SD_preorder preferred_alts_def)
qed
lemma SD_pref_profileI [intro?]:
assumes "i ∈ agents" "p ∈ lotteries_on alts" "q ∈ lotteries_on alts"
assumes "⋀x. x ∈ alts ⟹
measure_pmf.prob p (preferred_alts (R i) x) ≥
measure_pmf.prob q (preferred_alts (R i) x)"
shows "p ≽[SD(R i)] q"
using assms by (simp add: SD_pref_profile)
lemma SD_pref_profileD:
assumes "i ∈ agents" "p ≽[SD(R i)] q"
shows "p ∈ lotteries_on alts" "q ∈ lotteries_on alts"
and "⋀x. x ∈ alts ⟹
measure_pmf.prob p (preferred_alts (R i) x) ≥
measure_pmf.prob q (preferred_alts (R i) x)"
using assms by (simp_all add: SD_pref_profile)
end
subsection ‹SD efficient lotteries›
definition SD_efficient :: "('agent, 'alt) pref_profile ⇒ 'alt lottery ⇒ bool" where
SD_efficient_auxdef:
"SD_efficient R p ⟷ ¬(∃q∈lotteries_on {x. ∃i. R i x x}. q ≻[Pareto (SD ∘ R)] p)"
context pref_profile_wf
begin
sublocale SD: preorder_family agents "lotteries_on alts" "SD ∘ R" unfolding o_def
by (intro preorder_family.intro SD_is_preorder)
(simp_all add: preorder_on.SD_is_preorder' prefs_undefined')
text ‹
A lottery is considered SD-efficient if there is no other lottery such that
all agents weakly prefer the other lottery (w.r.t. stochastic dominance) and at least
one agent strongly prefers the other lottery.
›
lemma SD_efficient_def:
"SD_efficient R p ⟷ ¬(∃q∈lotteries_on alts. q ≻[Pareto (SD ∘ R)] p)"
proof -
have "SD_efficient R p ⟷ ¬(∃q∈lotteries_on {x. ∃i. R i x x}. q ≻[Pareto (SD ∘ R)] p)"
unfolding SD_efficient_auxdef ..
also from nonempty_agents obtain i where i: "i ∈ agents" by blast
with preorder_on.refl[of alts "R i"]
have "{x. ∃i. R i x x} = alts" by (auto intro!: exI[of _ i] not_outside)
finally show ?thesis .
qed
lemma SD_efficient_def':
"SD_efficient R p ⟷
¬(∃q∈lotteries_on alts. (∀i∈agents. q ≽[SD(R i)] p) ∧ (∃i∈agents. q ≻[SD(R i)] p))"
unfolding SD_efficient_def SD.Pareto_iff strongly_preferred_def [abs_def] by auto
lemma SD_inefficientI:
assumes "q ∈ lotteries_on alts" "⋀i. i ∈ agents ⟹ q ≽[SD(R i)] p"
"i ∈ agents" "q ≻[SD(R i)] p"
shows "¬SD_efficient R p"
using assms unfolding SD_efficient_def' by blast
lemma SD_inefficientI':
assumes "q ∈ lotteries_on alts" "⋀i. i ∈ agents ⟹ q ≽[SD(R i)] p"
"∃i ∈ agents. q ≻[SD(R i)] p"
shows "¬SD_efficient R p"
using assms unfolding SD_efficient_def' by blast
lemma SD_inefficientE:
assumes "¬SD_efficient R p"
obtains q i where
"q ∈ lotteries_on alts" "⋀i. i ∈ agents ⟹ q ≽[SD(R i)] p"
"i ∈ agents" "q ≻[SD(R i)] p"
using assms unfolding SD_efficient_def' by blast
lemma SD_efficientD:
assumes "SD_efficient R p" "q ∈ lotteries_on alts"
and "⋀i. i ∈ agents ⟹ q ≽[SD(R i)] p" "∃i∈agents. ¬(q ≼[SD(R i)] p)"
shows False
using assms unfolding SD_efficient_def' strongly_preferred_def by blast
lemma SD_efficient_singleton_iff:
assumes [simp]: "x ∈ alts"
shows "SD_efficient R (return_pmf x) ⟷ x ∉ pareto_losers R"
proof -
{
assume "x ∈ pareto_losers R"
then obtain y where "y ∈ alts" "x ≺[Pareto R] y"
by (rule pareto_losersE)
then have "¬SD_efficient R (return_pmf x)"
by (intro SD_inefficientI'[of "return_pmf y"]) (force simp: Pareto_strict_iff)+
} moreover {
assume "¬SD_efficient R (return_pmf x)"
from SD_inefficientE[OF this] obtain q i
where q:
"q ∈ lotteries_on alts"
"⋀i. i ∈ agents ⟹ SD (R i) (return_pmf x) q"
"i ∈ agents"
"return_pmf x ≺[SD (R i)] q"
by blast
from q obtain y where "y ∈ set_pmf q" "y ≻[R i] x"
by (auto simp: SD_strict_singleton_left)
with q have "y ≻[Pareto(R)] x"
by (fastforce simp: Pareto_strict_iff SD_singleton_left)
hence "x ∈ pareto_losers R" by simp
}
ultimately show ?thesis by blast
qed
end
subsection ‹Equivalence proof›
text ‹
We now show that a lottery is preferred w.r.t. Stochastic Dominance iff
it yields more expected utility for all compatible utility functions.
›
context finite_total_preorder_on
begin
abbreviation "is_vnm_utility ≡ vnm_utility carrier le"
lemma utility_weak_ranking_index:
"is_vnm_utility (λx. real (length (weak_ranking le) - weak_ranking_index x))"
proof
fix x y assume xy: "x ∈ carrier" "y ∈ carrier"
with this[THEN nth_weak_ranking_index(1)] this[THEN nth_weak_ranking_index(2)]
show "(real (length (weak_ranking le) - weak_ranking_index x)
≤ real (length (weak_ranking le) - weak_ranking_index y)) ⟷ le x y"
by (simp add: le_diff_iff')
qed
lemma SD_iff_expected_utilities_le:
assumes "p ∈ lotteries_on carrier" "q ∈ lotteries_on carrier"
shows "p ≼[SD(le)] q ⟷
(∀u. is_vnm_utility u ⟶ measure_pmf.expectation p u ≤ measure_pmf.expectation q u)"
proof safe
fix u assume SD: "p ≼[SD(le)] q" and is_utility: "is_vnm_utility u"
from is_utility interpret vnm_utility carrier le u .
define xs where "xs = weak_ranking le"
have le: "is_weak_ranking xs" "le = of_weak_ranking xs"
by (simp_all add: xs_def weak_ranking_total_preorder)
let ?pref = "λp x. measure_pmf.prob p {y. x ≼[le] y}" and
?pref' = "λp x. measure_pmf.prob p {y. x ≺[le] y}"
define f where "f i = (SOME x. x ∈ xs ! i)" for i
have xs_wf: "is_weak_ranking xs"
by (simp add: xs_def weak_ranking_total_preorder)
hence f: "f i ∈ xs ! i" if "i < length xs" for i
using that unfolding f_def is_weak_ranking_def
by (intro someI_ex[of "λx. x ∈ xs ! i"]) (auto simp: set_conv_nth)
have f': "f i ∈ carrier" if "i < length xs" for i
using that f weak_ranking_Union unfolding xs_def by (auto simp: set_conv_nth)
define n where "n = length xs - 1"
from assms weak_ranking_Union have carrier_nonempty: "carrier ≠ {}" and "xs ≠ []"
by (auto simp: xs_def lotteries_on_def set_pmf_not_empty)
hence n: "length xs = Suc n" and xs_nonempty: "xs ≠ []" by (auto simp add: n_def)
have SD': "?pref p (f i) ≤ ?pref q (f i)" if "i < length xs" for i
using f'[OF that] SD by (auto simp: SD_preorder preferred_alts_def)
have f_le: "le (f i) (f j) ⟷ i ≥ j" if "i < length xs" "j < length xs" for i j
using that weak_ranking_index_unique[OF xs_wf that(1) _ f]
weak_ranking_index_unique[OF xs_wf that(2) _ f]
by (auto simp add: le intro: f elim!: of_weak_ranking.cases intro!: of_weak_ranking.intros)
have "measure_pmf.expectation p u =
(∑i<n. (u (f i) - u (f (Suc i))) * ?pref p (f i)) + u (f n)"
if p: "p ∈ lotteries_on carrier" for p
proof -
from p have "measure_pmf.expectation p u =
(∑i<length xs. u (f i) * measure_pmf.prob p (xs ! i))"
by (simp add: f_def expected_utility_weak_ranking xs_def sum_list_sum_nth atLeast0LessThan)
also have "… = (∑i<length xs. u (f i) * (?pref p (f i) - ?pref' p (f i)))"
proof (intro sum.cong HOL.refl)
fix i assume i: "i ∈ {..<length xs}"
have "?pref p (f i) - ?pref' p (f i) =
measure_pmf.prob p ({y. f i ≼[le] y} - {y. f i ≺[le] y})"
by (subst measure_pmf.finite_measure_Diff [symmetric])
(auto simp: strongly_preferred_def)
also have "{y. f i ≼[le] y} - {y. f i ≺[le] y} =
{y. f i ≼[le] y ∧ y ≼[le] f i}" (is "_ = ?A")
by (auto simp: strongly_preferred_def)
also have "… = xs ! i"
proof safe
fix x assume le: "le (f i) x" "le x (f i)"
from i f show "x ∈ xs ! i"
by (intro weak_ranking_eqclass2[OF _ _ le]) (auto simp: xs_def)
next
fix x assume "x ∈ xs ! i"
from weak_ranking_eqclass1[OF _ this f] weak_ranking_eqclass1[OF _ f this] i
show "le x (f i)" "le (f i) x" by (simp_all add: xs_def)
qed
finally show "u (f i) * measure_pmf.prob p (xs ! i) =
u (f i) * (?pref p (f i) - ?pref' p (f i))" by simp
qed
also have "… = (∑i<length xs. u (f i) * ?pref p (f i)) -
(∑i<length xs. u (f i) * ?pref' p (f i))"
by (simp add: sum_subtractf ring_distribs)
also have "(∑i<length xs. u (f i) * ?pref p (f i)) =
(∑i<n. u (f i) * ?pref p (f i)) + u (f n) * ?pref p (f n)" (is "_ = ?sum")
by (simp add: n)
also have "(∑i<length xs. u (f i) * ?pref' p (f i)) =
(∑i<n. u (f (Suc i)) * ?pref' p (f (Suc i))) + u (f 0) * ?pref' p (f 0)"
unfolding n sum.lessThan_Suc_shift by simp
also have "(∑i<n. u (f (Suc i)) * ?pref' p (f (Suc i))) =
(∑i<n. u (f (Suc i)) * ?pref p (f i))"
proof (intro sum.cong HOL.refl)
fix i assume i: "i ∈ {..<n}"
have "f (Suc i) ≺[le] y ⟷ f i ≼[le] y" for y
proof (cases "y ∈ carrier")
assume "y ∈ carrier"
with weak_ranking_Union obtain j where j: "j < length xs" "y ∈ xs ! j"
by (auto simp: set_conv_nth xs_def)
with weak_ranking_eqclass1[OF _ f j(2)] weak_ranking_eqclass1[OF _ j(2) f]
have iff: "le y z ⟷ le (f j) z" "le z y ⟷ le z (f j)" for z
by (auto intro: trans simp: xs_def)
thus ?thesis using i j unfolding n_def
by (auto simp: iff f_le strongly_preferred_def)
qed (insert not_outside, auto simp: strongly_preferred_def)
thus "u (f (Suc i)) * ?pref' p (f (Suc i)) = u (f (Suc i)) * ?pref p (f i)" by simp
qed
also have "?sum - (… + u (f 0) * ?pref' p (f 0)) =
(∑i<n. (u (f i) - u (f (Suc i))) * ?pref p (f i)) -
u (f 0) * ?pref' p (f 0) + u (f n) * ?pref p (f n)"
by (simp add: ring_distribs sum_subtractf)
also have "{y. f 0 ≺[le] y} = {}"
using hd_weak_ranking[of "f 0"] xs_nonempty f not_outside
by (auto simp: hd_conv_nth xs_def strongly_preferred_def)
also have "{y. le (f n) y} = carrier"
using last_weak_ranking[of "f n"] xs_nonempty f not_outside
by (auto simp: last_conv_nth xs_def n_def)
also from p have "measure_pmf.prob p carrier = 1"
by (subst measure_pmf.prob_eq_1)
(auto simp: AE_measure_pmf_iff lotteries_on_def)
finally show ?thesis by simp
qed
from assms[THEN this] show "measure_pmf.expectation p u ≤ measure_pmf.expectation q u"
unfolding SD_preorder n_def using f'
by (auto intro!: sum_mono mult_left_mono SD' simp: utility_le_iff f_le)
next
assume "∀u. is_vnm_utility u ⟶ measure_pmf.expectation p u ≤ measure_pmf.expectation q u"
hence expected_utility_le: "measure_pmf.expectation p u ≤ measure_pmf.expectation q u"
if "is_vnm_utility u" for u using that by blast
define xs where "xs = weak_ranking le"
have le: "le = of_weak_ranking xs" and [simp]: "is_weak_ranking xs"
by (simp_all add: xs_def weak_ranking_total_preorder)
have carrier: "carrier = ⋃(set xs)"
by (simp add: xs_def weak_ranking_Union)
from assms have carrier_nonempty: "carrier ≠ {}"
by (auto simp: lotteries_on_def set_pmf_not_empty)
{
fix x assume x: "x ∈ carrier"
let ?idx = "λy. length xs - weak_ranking_index y"
have preferred_subset_carrier: "{y. le x y} ⊆ carrier"
using not_outside x by auto
have "measure_pmf.prob p {y. le x y} / real (length xs) ≤
measure_pmf.prob q {y. le x y} / real (length xs)"
proof (rule field_le_epsilon)
fix ε :: real assume ε: "ε > 0"
define u where "u y = indicator {y. y ≽[le] x} y + ε * ?idx y" for y
have is_utility: "is_vnm_utility u" unfolding u_def xs_def
proof (intro vnm_utility.add_left vnm_utility.scaled utility_weak_ranking_index)
fix y z assume "le y z"
thus "indicator {y. y ≽[le] x} y ≤ (indicator {y. y ≽[le] x} z :: real)"
by (auto intro: trans simp: indicator_def split: if_splits)
qed fact+
have "(∑y|le x y. pmf p y) ≤
(∑y|le x y. pmf p y) + ε * (∑y∈carrier. ?idx y * pmf p y)"
using ε by (auto intro!: mult_nonneg_nonneg sum_nonneg pmf_nonneg)
also from expected_utility_le is_utility have
"measure_pmf.expectation p u ≤ measure_pmf.expectation q u" .
with assms
have "(∑a∈carrier. u a * pmf p a) ≤ (∑a∈carrier. u a * pmf q a)"
by (subst (asm) (1 2) integral_measure_pmf[OF finite_carrier])
(auto simp: lotteries_on_def set_pmf_eq ac_simps)
hence "(∑y|le x y. pmf p y) + ε * (∑y∈carrier. ?idx y * pmf p y) ≤
(∑y|le x y. pmf q y) + ε * (∑y∈carrier. ?idx y * pmf q y)"
using x preferred_subset_carrier not_outside
by (simp add: u_def sum.distrib finite_carrier algebra_simps sum_distrib_left Int_absorb1 cong: rev_conj_cong)
also have "(∑y∈carrier. ?idx y * pmf q y) ≤ (∑y∈carrier. length xs * pmf q y)"
by (intro sum_mono mult_right_mono) (simp_all add: pmf_nonneg)
also have "… = measure_pmf.expectation q (λ_. length xs)"
using assms by (subst integral_measure_pmf[OF finite_carrier])
(auto simp: lotteries_on_def set_pmf_eq ac_simps)
also have "… = length xs" by simp
also have "(∑y | le x y. pmf p y) = measure_pmf.prob p {y. le x y}"
using finite_subset[OF preferred_subset_carrier finite_carrier]
by (simp add: measure_measure_pmf_finite)
also have "(∑y | le x y. pmf q y) = measure_pmf.prob q {y. le x y}"
using finite_subset[OF preferred_subset_carrier finite_carrier]
by (simp add: measure_measure_pmf_finite)
finally show "measure_pmf.prob p {y. le x y} / length xs ≤
measure_pmf.prob q {y. le x y} / length xs + ε"
using ε by (simp add: divide_simps)
qed
moreover from carrier_nonempty carrier have "xs ≠ []" by auto
ultimately have "measure_pmf.prob p {y. le x y} ≤
measure_pmf.prob q {y. le x y}"
by (simp add: field_simps)
}
with assms show "p ≼[SD(le)] q" unfolding SD_preorder preferred_alts_def by blast
qed
lemma not_strict_SD_iff:
assumes "p ∈ lotteries_on carrier" "q ∈ lotteries_on carrier"
shows "¬(p ≺[SD(le)] q) ⟷
(∃u. is_vnm_utility u ∧ measure_pmf.expectation q u ≤ measure_pmf.expectation p u)"
proof
let ?E = "measure_pmf.expectation :: 'a pmf ⇒ _ ⇒ real"
assume "∃u. is_vnm_utility u ∧ ?E p u ≥ ?E q u"
then obtain u where u: "is_vnm_utility u" "?E p u ≥ ?E q u" by blast
interpret u: vnm_utility carrier le u by fact
show "¬ p ≺[SD le] q"
proof
assume less: "p ≺[SD le] q"
with assms have pq: "?E p u ≤ ?E q u" if "is_vnm_utility u" for u
using that by (auto simp: SD_iff_expected_utilities_le strongly_preferred_def)
with u have u_eq: "?E p u = ?E q u" by (intro antisym) simp_all
from less assms obtain u' where u': "is_vnm_utility u'" "?E p u' < ?E q u'"
by (auto simp: SD_iff_expected_utilities_le strongly_preferred_def not_le)
interpret u': vnm_utility carrier le u' by fact
have "∃ε>0. is_vnm_utility (λx. u x - ε * u' x)"
by (intro u.diff_epsilon antisym u'.utility_le)
then obtain ε where ε: "ε > 0" "is_vnm_utility (λx. u x - ε * u' x)" by auto
define u'' where "u'' x = u x - ε * u' x" for x
interpret u'': vnm_utility carrier le u'' unfolding u''_def by fact
have exp_u'': "?E p u'' = ?E p u - ε * ?E p u'" if "p ∈ lotteries_on carrier" for p using that
by (subst (1 2 3) integral_measure_pmf[of carrier])
(auto simp: lotteries_on_def u''_def algebra_simps sum_subtractf sum_distrib_left)
from assms ε have "?E p u'' > ?E q u''"
by (simp_all add: exp_u'' algebra_simps u_eq u')
with pq[OF u''.vnm_utility_axioms] show False by simp
qed
qed (insert assms utility_weak_ranking_index,
auto simp: strongly_preferred_def SD_iff_expected_utilities_le not_le not_less intro: antisym)
lemma strict_SD_iff:
assumes "p ∈ lotteries_on carrier" "q ∈ lotteries_on carrier"
shows "(p ≺[SD(le)] q) ⟷
(∀u. is_vnm_utility u ⟶ measure_pmf.expectation p u < measure_pmf.expectation q u)"
using not_strict_SD_iff[OF assms] by auto
end
end