Theory First_Welfare_Theorem.Preferences
section ‹Preference Relations›
text ‹ Preferences modeled as a set of pairs ›
theory Preferences
imports
"HOL-Analysis.Multivariate_Analysis"
Syntax
begin
subsection ‹Basic Preference Relation›
text ‹ Basic preference relation locale with carrier and relation modeled as a set of pairs. ›
locale preference =
fixes carrier :: "'a set"
fixes relation :: "'a relation"
assumes not_outside: "(x,y) ∈ relation ⟹ x ∈ carrier"
and "(x,y) ∈ relation ⟹ y ∈ carrier"
assumes trans_refl: "preorder_on carrier relation"
context preference
begin
no_notation eqpoll (infixl "≈" 50)
abbreviation geq ("_ ≽ _" [51,51] 60)
where
"x ≽ y ≡ x ≽[relation] y"
abbreviation str_gr ("_ ≻ _" [51,51] 60)
where
"x ≻ y ≡ x ≽ y ∧ ¬y ≽ x"
abbreviation indiff ("_ ≈ _" [51,51] 60)
where
"x ≈ y ≡ x ≽ y ∧ y ≽ x"
lemma reflexivity: "refl_on carrier relation"
using preorder_on_def trans_refl by blast
lemma transitivity: "trans relation"
using preorder_on_def trans_refl by auto
lemma indiff_trans [simp]: "x ≈ y ⟹ y ≈ z ⟹ x ≈ z"
by (meson transE transitivity)
end
subsubsection ‹ Contour sets ›
definition at_least_as_good :: "'a ⇒ 'a set ⇒ 'a relation ⇒ 'a set"
where
"at_least_as_good x B P = {y ∈ B. y ≽[P] x }"
definition no_better_than :: "'a ⇒ 'a set ⇒ 'a relation ⇒ 'a set"
where
"no_better_than x B P = {y ∈ B. x ≽[P] y}"
definition as_good_as :: "'a ⇒ 'a set ⇒ 'a relation ⇒ 'a set"
where
"as_good_as x B P = {y ∈ B. x ≈[P] y}"
lemma at_lst_asgd_ge:
assumes "x ∈ at_least_as_good y B Pr"
shows "x ≽[Pr] y"
using assms at_least_as_good_def by fastforce
lemma strict_contour_is_diff:
"{a ∈ B. a ≻[Pr] y} = at_least_as_good y B Pr - as_good_as y B Pr"
by(auto simp add: at_least_as_good_def as_good_as_def)
lemma strict_countour_def [simp]:
"(at_least_as_good y B Pr) - as_good_as y B Pr = {x ∈ B. x ≻[Pr] y}"
by (simp add: as_good_as_def at_least_as_good_def strict_contour_is_diff)
lemma at_least_as_goodD [dest]:
assumes "z ∈ at_least_as_good y B Pr"
shows "z ≽[Pr] y"
using assms at_least_as_good_def by fastforce
subsection ‹Rational Preference Relation›
text ‹ Rational preferences add totality to the basic preferences. ›
locale rational_preference = preference +
assumes total: "total_on carrier relation"
begin
lemma compl: "∀x ∈ carrier . ∀y∈ carrier . x ≽ y ∨ y ≽ x"
by (metis refl_onD reflexivity total total_on_def)
lemma strict_not_refl_weak [iff]: "x ∈ carrier ∧ y ∈ carrier ⟹ ¬ (y ≽ x) ⟷ x ≻ y"
by (metis refl_onD reflexivity total total_on_def)
lemma strict_trans [simp]: "x ≻ y ⟹ y ≻ z ⟹ x ≻ z"
by (meson transE transitivity)
lemma completeD [dest]: "x ∈ carrier ⟹ y ∈ carrier ⟹ x ≠ y ⟹ x ≽ y ∨ y ≽ x"
by blast
lemma pref_in_at_least_as:
assumes "x ≽ y"
shows "x ∈ at_least_as_good y carrier relation"
by (metis (no_types, lifting) CollectI assms
at_least_as_good_def preference.not_outside preference_axioms)
lemma worse_in_no_better:
assumes "x ≽ y"
shows "y ∈ no_better_than y carrier relation"
by (metis (no_types, lifting) CollectI assms no_better_than_def
preference_axioms preference_def strict_not_refl_weak)
lemma strict_is_neg_transitive :
assumes "x ∈ carrier ∧ y ∈ carrier ∧ z ∈ carrier"
shows "x ≻ y ⟹ x ≻ z ∨ z ≻ y"
by (meson assms compl transE transitivity)
lemma weak_is_transitive:
assumes "x ∈ carrier ∧ y ∈ carrier ∧ z ∈ carrier"
shows "x ≽ y ⟹ y ≽ z ⟹ x ≽ z"
by (meson transD transitivity)
lemma no_better_than_nonepty:
assumes "carrier ≠ {}"
shows "⋀x. x ∈ carrier ⟹ (no_better_than x carrier relation) ≠ {}"
by (metis (no_types, lifting) empty_iff mem_Collect_eq
no_better_than_def refl_onD reflexivity)
lemma no_better_subset_pref :
assumes "x ≽ y"
shows "no_better_than y carrier relation ⊆ no_better_than x carrier relation"
proof
fix a
assume "a ∈ no_better_than y carrier relation"
then show "a ∈ no_better_than x carrier relation"
by (metis (no_types, lifting) assms mem_Collect_eq no_better_than_def transE transitivity)
qed
lemma no_better_thansubset_rel :
assumes "x ∈ carrier" and "y ∈ carrier"
assumes "no_better_than y carrier relation ⊆ no_better_than x carrier relation"
shows "x ≽ y"
proof -
have "{a ∈ carrier. y ≽ a} ⊆ {a ∈ carrier. x ≽ a}"
by (metis (no_types) assms(3) no_better_than_def)
then show ?thesis
by (metis (mono_tags, lifting) Collect_mono_iff assms(2) compl)
qed
lemma nbt_nest :
shows "(no_better_than y carrier relation ⊆ no_better_than x carrier relation) ∨
(no_better_than x carrier relation ⊆ no_better_than y carrier relation)"
by (metis (no_types, lifting) CollectD compl no_better_subset_pref no_better_than_def not_outside subsetI)
lemma at_lst_asgd_not_ge:
assumes "carrier ≠ {}"
assumes "x ∈ carrier" and "y ∈ carrier"
assumes "x ∉ at_least_as_good y carrier relation"
shows "¬ x ≽ y"
by (metis (no_types, lifting) CollectI assms(2) assms(4) at_least_as_good_def)
lemma as_good_as_sameIff[iff]:
"z ∈ as_good_as y carrier relation ⟷ z ≽ y ∧ y ≽ z"
by (metis (no_types, lifting) as_good_as_def mem_Collect_eq not_outside)
lemma same_at_least_as_equal:
assumes "z ≈ y"
shows "at_least_as_good z carrier relation =
at_least_as_good y carrier relation" (is "?az = ?ay")
proof
have "z ∈ carrier ∧ y ∈ carrier"
by (meson assms refl_onD2 reflexivity)
moreover have "∀x ∈ carrier. x ≽ z ⟶ x ≽ y"
by (meson assms transD transitivity)
ultimately show "?az ⊆ ?ay"
by (metis at_lst_asgd_ge at_lst_asgd_not_ge
equals0D not_outside subsetI)
next
have "z ∈ carrier ∧ y ∈ carrier"
by (meson assms refl_onD2 reflexivity)
moreover have "∀x ∈ carrier. x ≽ y ⟶ x ≽ z"
by (meson assms transD transitivity)
ultimately show "?ay ⊆ ?az"
by (metis at_lst_asgd_ge at_lst_asgd_not_ge
equals0D not_outside subsetI)
qed
lemma as_good_asIff [iff]:
"x ∈ as_good_as y carrier relation ⟷ x ≈[relation] y"
by blast
lemma nbt_subset:
assumes "finite carrier"
assumes "x ∈ carrier" and "y ∈ carrier"
shows "no_better_than x carrier relation ⊆ no_better_than x carrier relation ∨
no_better_than x carrier relation ⊆ no_better_than x carrier relation"
by auto
lemma fnt_carrier_fnt_rel: "finite carrier ⟹ finite relation"
by (metis finite_SigmaI refl_on_def reflexivity rev_finite_subset)
lemma nbt_subset_carrier:
assumes "x ∈ carrier"
shows "no_better_than x carrier relation ⊆ carrier"
using no_better_than_def by fastforce
lemma xy_in_eachothers_nbt:
assumes "x ∈ carrier" "y ∈ carrier"
shows "x ∈ no_better_than y carrier relation ∨
y ∈ no_better_than x carrier relation"
by (meson assms(1) assms(2) contra_subsetD nbt_nest refl_onD reflexivity worse_in_no_better)
lemma same_nbt_same_pref:
assumes "x ∈ carrier" "y ∈ carrier"
shows "x ∈ no_better_than y carrier relation ∧
y ∈ no_better_than x carrier relation ⟷ x ≈ y"
by (metis (mono_tags, lifting) CollectD contra_subsetD no_better_subset_pref
no_better_than_def worse_in_no_better)
lemma indifferent_imp_weak_pref:
assumes "x ≈ y"
shows" x ≽ y" "y ≽ x"
by (simp add: assms)+
subsection ‹ Finite carrier›
context
assumes "finite carrier"
begin
lemma fnt_carrier_fnt_nbt:
shows "∀x∈carrier. finite (no_better_than x carrier relation)"
proof
fix x
assume "x ∈ carrier"
then show "finite (no_better_than x carrier relation)"
using finite_subset nbt_subset_carrier ‹finite carrier› by blast
qed
lemma nbt_subset_imp_card_leq:
assumes "x ∈ carrier" and "y ∈ carrier"
shows "no_better_than x carrier relation ⊆ no_better_than y carrier relation ⟷
card (no_better_than x carrier relation) ≤ card (no_better_than y carrier relation)"
(is "?nbt ⟷ ?card")
proof
assume "?nbt"
then show "?card"
by (simp add: assms(2) card_mono fnt_carrier_fnt_nbt)
next
assume "?card"
then show "?nbt"
by (metis assms(1) card_seteq fnt_carrier_fnt_nbt nbt_nest)
qed
lemma card_leq_pref:
assumes "x ∈ carrier" and "y ∈ carrier"
shows "card (no_better_than x carrier relation) ≤ card (no_better_than y carrier relation)
⟷ y ≽ x"
proof (rule iffI, goal_cases)
case 1
then show ?case
using assms(1) assms(2) nbt_subset_imp_card_leq no_better_thansubset_rel by presburger
next
case 2
then show ?case
using assms(1) assms(2) nbt_subset_imp_card_leq no_better_subset_pref by blast
qed
lemma finite_ne_remove_induct:
assumes "finite B" "B ≠ {}"
"⋀A. finite A ⟹ A ⊆ B ⟹ A ≠ {} ⟹
(⋀x. x ∈ A ⟹ A - {x} ≠ {} ⟹ P (A - {x})) ⟹ P A"
shows "P B"
by (metis assms finite_remove_induct[where P = "λF. F = {} ∨ P F" for P])
lemma finite_nempty_preorder_has_max:
assumes "finite B" "B ≠ {}" "refl_on B R" "trans R" "total_on B R"
shows "∃x ∈ B. ∀y ∈ B. (x, y) ∈ R"
using assms(1) subset_refl[of B] assms(2)
proof (induct B rule: finite_subset_induct)
case (insert x F)
then show ?case using assms(3-)
by (cases "F = {}") (auto simp: refl_onD total_on_def, metis refl_onD2 transE)
qed auto
lemma finite_nempty_preorder_has_min:
assumes "finite B" "B ≠ {}" "refl_on B R" "trans R" "total_on B R"
shows "∃x ∈ B. ∀y ∈ B. (y, x) ∈ R"
using assms(1) subset_refl[of B] assms(2)
proof (induct B rule: finite_subset_induct)
case (insert x F)
then show ?case using assms(3-)
by (cases "F = {}") (auto simp: refl_onD total_on_def, metis refl_onD2 transE)
qed auto
lemma finite_nonempty_carrier_has_maximum:
assumes "carrier ≠ {}"
shows "∃e ∈ carrier. ∀m ∈ carrier. e ≽[relation] m"
using finite_nempty_preorder_has_max[of carrier relation] assms
‹finite carrier› reflexivity total transitivity by blast
lemma finite_nonempty_carrier_has_minimum:
assumes "carrier ≠ {}"
shows "∃e ∈ carrier. ∀m ∈ carrier. m ≽[relation] e"
using finite_nempty_preorder_has_min[of carrier relation] assms
‹finite carrier› reflexivity total transitivity by blast
end
lemma all_carrier_ex_sub_rel:
"∀c ⊆ carrier. ∃r ⊆ relation. rational_preference c r"
proof (standard,standard)
fix c
assume c_in: "c ⊆ carrier"
define r' where
"r' = {(x,y) ∈ relation. x ∈ c ∧ y ∈ c}"
have r'_sub: "r' ⊆ c × c"
using r'_def by blast
have "∀x ∈ c. x ≽[r'] x"
by (metis (no_types, lifting) CollectI c_in case_prodI compl r'_def subsetCE)
then have refl: "refl_on c r'"
by (meson r'_sub refl_onI)
have trans: "trans r'"
proof
fix x y z
assume a1: "x ≽[r'] y"
assume a2: "y ≽[r'] z"
show " x ≽[r'] z"
by (metis (mono_tags, lifting) CollectD CollectI a1 a2 case_prodD case_prodI r'_def transE transitivity)
qed
have total: "total_on c r'"
proof (standard)
fix x y
assume a1:"x ∈ c"
assume a2: "y ∈ c"
assume a3: "x ≠ y"
show "x ≽[r'] y ∨ y ≽[r'] x "
by (metis (no_types, lifting) CollectI a1 a2 c_in case_prodI compl r'_def subset_iff)
qed
have "rational_preference c r'"
by (meson local.refl local.trans preference.intro preorder_on_def rational_preference.intro
rational_preference_axioms.intro refl_on_domain total)
thus "∃r⊆relation. rational_preference c r"
by (metis (no_types, lifting) CollectD case_prodD r'_def subrelI)
qed
end
subsection ‹ Local Non-Satiation ›
text ‹ Defining local non-satiation. ›
definition local_nonsatiation
where
"local_nonsatiation B P ⟷
(∀x∈B. ∀e>0. ∃y∈B. norm (y - x) ≤ e ∧ y ≻[P] x)"
text ‹ Alternate definitions and intro/dest rules with them ›
lemma lns_alt_def1 [iff] :
shows "local_nonsatiation B P ⟷ (∀x ∈ B. ∀e>0. (∃y ∈ B. dist y x ≤ e ∧ y ≻[P] x))"
by(simp add : dist_norm local_nonsatiation_def)
lemma lns_normI [intro]:
assumes "⋀x e. x ∈ B ⟹ e > 0 ⟹ (∃y∈B. norm (y - x) ≤ e ∧ y ≻[P] x)"
shows "local_nonsatiation B P"
by (simp add: assms dist_norm)
lemma lns_distI [intro]:
assumes "⋀x e. x ∈ B ⟹ e > 0 ⟹ (∃y∈B. (dist y x) ≤ e ∧ y ≻[P] x)"
shows "local_nonsatiation B P"
by (meson lns_alt_def1 assms)
lemma lns_alt_def2 [iff]:
"local_nonsatiation B P ⟷ (∀x∈B. ∀e>0. (∃y. y ∈ (ball x e) ∧ y ∈ B ∧ y ≻[P] x))"
proof
assume "local_nonsatiation B P"
then show "∀x∈B. ∀e>0. ∃x'. x' ∈ ball x e ∧ x' ∈ B ∧ x' ≻[P] x"
by (auto simp add : ball_def) (metis dense le_less_trans dist_commute)
next
assume "∀x∈B. ∀e>0. ∃y. y ∈ ball x e ∧ y ∈ B ∧ y ≻[P] x"
then show "local_nonsatiation B P"
by (metis (no_types, lifting) ball_def dist_commute
less_le_not_le lns_alt_def1 mem_Collect_eq)
qed
lemma lns_normD [dest]:
assumes "local_nonsatiation B P"
shows "∀x ∈ B. ∀e>0. ∃y ∈ B. (norm (y - x) ≤ e ∧ y ≻[P] x)"
by (meson assms local_nonsatiation_def)
subsection ‹ Convex preferences ›
definition weak_convex_pref :: "('a::real_vector) relation ⇒ bool"
where
"weak_convex_pref Pr ⟷ (∀x y. x ≽[Pr] y ⟶
(∀α β. α + β = 1 ∧ α > 0 ∧ β > 0 ⟶ α *⇩R x + β *⇩R y ≽[Pr] y))"
definition convex_pref :: "('a::real_vector) relation ⇒ bool"
where
"convex_pref Pr ⟷ (∀x y. x ≻[Pr] y ⟶
(∀α. 1 > α ∧ α > 0 ⟶ α *⇩R x + (1-α) *⇩R y ≻[Pr] y))"
definition strict_convex_pref :: "('a::real_vector) relation ⇒ bool"
where
"strict_convex_pref Pr ⟷ (∀x y. x ≽[Pr] y ∧ x ≠ y ⟶
(∀α. 1 > α ∧ α > 0 ⟶ α *⇩R x + (1-α) *⇩R y ≻[Pr] y))"
lemma convex_ge_imp_conved:
assumes "∀x y. x ≽[Pr] y ⟶ (∀α β. α + β = 1 ∧ α ≥ 0 ∧ β ≥ 0 ⟶ α *⇩R x + β *⇩R y ≽[Pr] y)"
shows "weak_convex_pref Pr"
by (simp add: assms weak_convex_pref_def)
lemma weak_convexI [intro]:
assumes "⋀x y α β. x ≽[Pr] y ⟹ α + β = 1 ⟹ 0 < α ⟹ 0 < β ⟹ α *⇩R x + β *⇩R y ≽[Pr] y"
shows "weak_convex_pref Pr"
by (simp add: assms weak_convex_pref_def)
lemma weak_convexD [dest]:
assumes "weak_convex_pref Pr" and "x ≽[Pr] y" and "0 < u" and "0 < v" and "u + v = 1"
shows "u *⇩R x + v *⇩R y ≽[Pr] y"
using assms weak_convex_pref_def by blast
subsection ‹ Real Vector Preferences ›
text ‹ Preference relations on real vector type class. ›
locale real_vector_rpr = rational_preference carrier relation
for carrier :: "'a::real_vector set"
and relation :: "'a relation"
sublocale real_vector_rpr ⊆ rational_preference carrier relation
by (simp add: rational_preference_axioms)
context real_vector_rpr
begin
lemma have_rpr: "rational_preference carrier relation"
by (simp add: rational_preference_axioms)
text ‹ Multiple convexity alternate definitions intro/dest rules. ›
lemma weak_convex1D [dest]:
assumes "weak_convex_pref relation" and "x ≽[relation] y" and "0 ≤ u" and "0 ≤ v" and "u + v = 1"
shows "u *⇩R x + v *⇩R y ≽[relation] y"
proof-
have u_0: "u = 0 ⟶ u *⇩R x + v *⇩R y ≽[relation] y"
proof
assume u_0: "u = 0"
have "v = 1"
using assms(5) u_0 by auto
then have "?thesis"
by (metis add.left_neutral assms(2) preference.reflexivity preference_axioms
real_vector.scale_zero_left refl_onD2 scaleR_one strict_not_refl_weak)
thus "u *⇩R x + v *⇩R y ≽[relation] y "
using u_0 by blast
qed
have "u ≠ 0 ∧ u ≠ 1 ⟶ u *⇩R x + v *⇩R y ≽[relation] y"
by (metis add_cancel_right_right antisym_conv not_le assms weak_convexD )
then show ?thesis
by (metis u_0 assms(2,5) add_cancel_right_right real_vector.scale_zero_left scaleR_one)
qed
lemma weak_convex1I [intro] :
assumes "∀x. convex (at_least_as_good x carrier relation)"
shows "weak_convex_pref relation"
proof (rule weak_convexI)
fix x and y and α β :: real
assume assum : "x ≽[relation] y"
assume reals: "0 < α" "0 < β" " α + β = 1"
then have "x ∈ carrier"
by (meson assum preference.not_outside rational_preference.axioms(1) have_rpr)
have "y ∈ carrier"
by (meson assum refl_onD2 reflexivity)
then have y_in_upper_cont: "y ∈ (at_least_as_good y carrier relation)"
using assms rational_preference.at_lst_asgd_not_ge
rational_preference.compl by (metis empty_iff have_rpr)
then have "x ∈ (at_least_as_good y carrier relation)"
using assum pref_in_at_least_as by blast
moreover have "0 ≤ β" and "0 ≤ α"
using reals by (auto)
ultimately show "(α *⇩R x + β *⇩R y) ≽[relation] y"
by (meson assms(1) at_least_as_goodD convexD reals(3) y_in_upper_cont)
qed
text ‹ Definition of convexity in "Handbook of Social Choice and Welfare"\<^cite>‹"arrow2010handbook"›. ›
lemma convex_def_alt:
assumes "rational_preference carrier relation"
assumes "weak_convex_pref relation"
shows "(∀x ∈ carrier. convex (at_least_as_good x carrier relation))"
proof
fix x
assume x_in: "x ∈ carrier"
show "convex (at_least_as_good x carrier relation)" (is "convex ?x")
proof (rule convexI)
fix a b :: "'a" and α :: "real" and β :: "real"
assume a_in: "a ∈ ?x"
assume b_in: "b ∈ ?x"
assume reals: " 0 ≤ α" "0 ≤ β" "α + β = 1"
have a_g_x: "a ≽[relation] x"
using a_in by blast
have b_g_x: "b ≽[relation] x"
using b_in by blast
have "a ≽[relation] b ∨ b ≽[relation] a"
by (meson a_in at_least_as_goodD b_in preference.not_outside
rational_preference.compl rational_preference_def assms(1))
then show "α *⇩R a + β *⇩R b ∈ ?x"
proof(rule disjE)
assume "a ≽[relation] b"
then have "α *⇩R a + β *⇩R b ≽[relation] b"
using assms reals by blast
then have "α *⇩R a + β *⇩R b ≽[relation] x"
by (meson b_g_x assms(1) preference.not_outside x_in
rational_preference.strict_is_neg_transitive
rational_preference.strict_not_refl_weak rational_preference_def)
then show ?thesis
by (metis (no_types, lifting) CollectI assms(1)
at_least_as_good_def preference_def rational_preference_def)
next
assume as: "b ≽[relation] a"
then have "α *⇩R a + β *⇩R b ≽[relation] a"
by (metis add.commute assms(2) reals weak_convex1D)
have "α *⇩R a + β *⇩R b ≽[relation] a"
by (metis as add.commute assms(2)
reals(1,2,3) weak_convex1D)
then have "α *⇩R a + β *⇩R b ≽[relation] x"
by (meson a_g_x assms(1) preference.indiff_trans x_in
preference.not_outside rational_preference.axioms(1)
rational_preference.strict_is_neg_transitive )
then show ?thesis
using pref_in_at_least_as by blast
qed
qed
qed
lemma convex_imp_convex_str_upper_cnt:
assumes "∀x ∈ carrier. convex (at_least_as_good x carrier relation)"
shows "convex (at_least_as_good x carrier relation - as_good_as x carrier relation)"
(is "convex ( ?a - ?b)")
proof (rule convexI)
fix a y u v
assume as_a: "a ∈ ?a - ?b"
assume as_y: "y ∈ ?a - ?b"
assume reals: "0 ≤ (u::real)" "0 ≤ v" "u + v = 1"
have cvx: "weak_convex_pref relation "
by (meson assms at_least_as_goodD convexI have_rpr
preference_def rational_preference.axioms(1) weak_convex1I)
then have a_g_x: "a ≻[relation] x"
using as_a by blast
then have y_gt_x: "y ≻[relation] x"
using as_y by blast
show "u *⇩R a + v *⇩R y ∈ ?a - ?b"
proof
show "u *⇩R a + v *⇩R y ∈ ?a"
by (metis DiffD1 a_g_x as_a as_y assms convexD reals have_rpr
preference_def rational_preference.axioms(1))
next
have "a ≽[relation] y ∨ y ≽[relation] a"
by (meson a_g_x y_gt_x assms(1) preference.not_outside have_rpr
rational_preference.axioms(1) rational_preference.strict_not_refl_weak)
then show "u *⇩R a + v *⇩R y ∉ ?b"
proof
assume "a ≽[relation] y"
then have "u *⇩R a + v *⇩R y ≽[relation] y"
using cvx assms(1) reals by blast
then have "u *⇩R a + v *⇩R y ≻[relation] x"
using y_gt_x by (meson assms(1) rational_preference.axioms(1) have_rpr
rational_preference.strict_is_neg_transitive preference_def)
then show "u *⇩R a + v *⇩R y ∉ as_good_as x carrier relation"
by blast
next
assume "y ≽[relation] a"
then have "u *⇩R a + v *⇩R y ≽[relation] a"
using cvx assms(1) reals by (metis add.commute weak_convex1D)
then have "u *⇩R a + v *⇩R y ≻[relation] x"
by (meson a_g_x assms(1) rational_preference.strict_is_neg_transitive
rational_preference.axioms(1) preference_def have_rpr)
then show "u *⇩R a + v *⇩R y ∉ ?b"
by blast
qed
qed
qed
end
subsubsection ‹ Monotone preferences ›
definition weak_monotone_prefs :: "'a set ⇒ ('a::ord) relation ⇒ bool"
where
"weak_monotone_prefs B P ⟷ (∀x ∈ B. ∀y ∈ B. x ≥ y ⟶ x ≽[P]y)"
definition monotone_preference :: "'a set ⇒ ('a::ord) relation ⇒ bool"
where
"monotone_preference B P ⟷ (∀x ∈ B. ∀y ∈ B. x > y ⟶ x ≻[P] y)"
text ‹ Given a carrier set that is unbounded above (not the "standard" mathematical definition),
monotonicity implies local non-satiation. ›
lemma unbounded_above_mono_imp_lns:
assumes "∀M ∈ carrier. (∀x > M. x ∈ carrier)"
assumes mono: "monotone_preference (carrier:: 'a::ordered_euclidean_space set) relation"
shows "local_nonsatiation carrier relation"
proof(rule lns_distI)
fix x and e::"real"
assume x_in: "x ∈ carrier"
assume gz : "e > 0"
show "∃y∈carrier. dist y x ≤ e ∧ y ≽[relation] x ∧ (x, y) ∉ relation"
proof-
obtain v :: real where
v:"v < e" "0 < v" using gz dense by blast
obtain i where
i:"(i::'a) ∈ Basis" by fastforce
define y where
y_value : "y = x + v *⇩R i"
have ge:"y ≥ x"
using y_value i unfolding y_value
by (simp add: v(2) zero_le_scaleR_iff)
have "y ≠ x"
using y_value i unfolding y_value
using v(2) by auto
hence y_str_g_x : "y > x"
using ge by auto
have y_in: "y ∈ carrier"
using assms(1) x_in y_str_g_x by blast
then have y_pref_x : "y ≻[relation] x"
using y_str_g_x x_in mono monotone_preference_def by blast
hence " norm (y - x) ≤ e"
using ‹0 < v› y_value y_value i v by auto
hence dist_less_e : "dist y x ≤ e"
by (simp add: dist_norm)
thus ?thesis
using y_pref_x dist_less_e y_in by blast
qed
qed
end