Theory Arrow_Debreu_Model
section ‹ Arrow-Debreu model ›
theory Arrow_Debreu_Model
imports
"../Preferences"
"../Preferences"
"../Utility_Functions"
"../Argmax"
Consumers
Common
begin
locale pre_arrow_debreu_model =
fixes production_sets :: "'f ⇒ ('a::ordered_euclidean_space) set"
fixes consumption_set :: "'a set"
fixes agents :: "'i set"
fixes firms :: "'f set"
fixes ℰ :: "'i ⇒ 'a" (‹ℰ[_]›)
fixes Pref :: "'i ⇒ 'a relation" (‹Pr[_]›)
fixes U :: "'i ⇒ 'a ⇒ real" (‹U[_]›)
fixes Θ :: "'i ⇒ 'f ⇒ real" (‹Θ[_,_]›)
assumes cons_set_props: "arrow_debreu_consum_set consumption_set"
assumes agent_props: "i ∈ agents ⟹ eucl_ordinal_utility consumption_set (Pr[i]) (U[i])"
assumes firms_comp_owned: "j ∈ firms ⟹ (∑i∈agents. Θ[i,j]) = 1"
assumes finite_nonepty_agents: "finite agents" and "agents ≠ {}"
sublocale pre_arrow_debreu_model ⊆ pareto_ordering agents U
.
context pre_arrow_debreu_model
begin
text ‹ Calculate wealth of individual i in context of Private Ownership economy. ›
context
begin
private abbreviation poe_wealth
where
"poe_wealth P i Y ≡ P ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (P ∙ Y j))"
subsection ‹ Feasiblity ›
private abbreviation feasible
where
"feasible X Y ≡ feasible_private_ownership agents firms ℰ consumption_set production_sets X Y"
private abbreviation calculate_value
where
"calculate_value P x ≡ P ∙ x"
subsection ‹ Profit maximisation ›
text ‹ In a production economy (which this is) we need to specify profit maximisation. ›
definition profit_maximisation
where
"profit_maximisation P S = arg_max_set (λx. P ∙ x) S"
subsection ‹ Competitive Equilibirium ›
text ‹ Competitive equilibrium in context of production economy with private ownership.
This includes the profit maximisation condition. ›
definition competitive_equilibrium
where
"competitive_equilibrium P X Y ⟷ feasible X Y ∧
(∀j ∈ firms. (Y j) ∈ profit_maximisation P (production_sets j)) ∧
(∀i ∈ agents. (X i) ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y)))"
lemma competitive_equilibriumD [dest]:
assumes "competitive_equilibrium P X Y"
shows "feasible X Y ∧
(∀j ∈ firms. (Y j) ∈ profit_maximisation P (production_sets j)) ∧
(∀i ∈ agents. (X i) ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y)))"
using assms by (simp add: competitive_equilibrium_def)
lemma compet_max_profit:
assumes "j ∈ firms"
assumes "competitive_equilibrium P X Y"
shows "Y j ∈ profit_maximisation P (production_sets j)"
using assms(1) assms(2) by blast
subsection ‹ Pareto Optimality ›
definition pareto_optimal
where
"pareto_optimal X Y ⟷
(feasible X Y ∧
(∄X' Y'. feasible X' Y' ∧ X' ≻Pareto X))"
lemma pareto_optimalI[intro]:
assumes "feasible X Y"
and "∄X' Y'. feasible X' Y' ∧ X' ≻Pareto X"
shows "pareto_optimal X Y"
using pareto_optimal_def assms(1) assms(2) by blast
lemma pareto_optimalD[dest]:
assumes "pareto_optimal X Y"
shows "feasible X Y" and "∄X' Y'. feasible X' Y' ∧ X' ≻Pareto X"
using pareto_optimal_def assms by auto
lemma util_fun_def_holds:
assumes "i ∈ agents"
and "x ∈ consumption_set"
and "y ∈ consumption_set"
shows "x ≽[Pr[i]] y ⟷ U[i] x ≥ U[i] y"
proof
assume "x ≽[Pr[i]] y"
show "U[i] x ≥ U[i] y"
by (meson ‹x ≽[Pr[i]] y› agent_props assms eucl_ordinal_utility_def ordinal_utility_def)
next
assume "U[i] x ≥ U[i] y"
have "eucl_ordinal_utility consumption_set (Pr[i]) (U[i])"
by (simp add: agent_props assms)
then show "x ≽[Pr[i]] y"
by (meson ‹U[i] y ≤ U[i] x› assms(2) assms(3) eucl_ordinal_utility_def ordinal_utility.util_def_conf)
qed
lemma base_pref_is_ord_eucl_rpr: "i ∈ agents ⟹ rational_preference consumption_set Pr[i]"
using agent_props ord_eucl_utility_imp_rpr real_vector_rpr.have_rpr by blast
lemma prof_max_ge_all_in_pset:
assumes "j ∈ firms"
assumes "Y j ∈ profit_maximisation P (production_sets j)"
shows "∀y ∈ production_sets j. P ∙ Y j ≥ P ∙ y"
using all_leq assms(2) profit_maximisation_def by fastforce
subsection ‹ Lemmas for final result ›
text ‹ Strictly preferred bundles are strictly more expensive. ›
lemma all_prefered_are_more_expensive:
assumes i_agt: "i ∈ agents"
assumes equil: "competitive_equilibrium P 𝒳 𝒴"
assumes "z ∈ consumption_set"
assumes "(U i) z > (U i) (𝒳 i)"
shows "z ∙ P > P ∙ (𝒳 i)"
proof (rule ccontr)
assume neg_as : "¬(z ∙ P > P ∙ (𝒳 i))"
have xp_leq : "z ∙ P ≤ P ∙ (𝒳 i)"
using ‹¬z ∙ P > P ∙ (𝒳 i)› by auto
have x_in_argmax: "(𝒳 i) ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (poe_wealth P i 𝒴))"
using equil i_agt by blast
hence x_in: "𝒳 i ∈ (budget_constraint (calculate_value P) consumption_set (poe_wealth P i 𝒴))"
using argmax_sol_in_s [of "(𝒳 i)" "U[i]" "budget_constraint (calculate_value P) consumption_set (poe_wealth P i 𝒴)"]
by blast
hence z_in_budget: "z ∈ (budget_constraint (calculate_value P) consumption_set (poe_wealth P i 𝒴))"
proof -
have z_leq_endow: "P ∙ z ≤ P ∙ (𝒳 i)"
by (metis xp_leq inner_commute)
have z_in_cons: "z ∈ consumption_set"
using assms by auto
then show ?thesis
using x_in budget_constraint_def z_leq_endow
proof -
have "∀r. P ∙ 𝒳 i ≤ r ⟶ P ∙ z ≤ r"
using z_leq_endow by linarith
then show ?thesis
using budget_constraint_def x_in z_in_cons
by (simp add: budget_constraint_def)
qed
qed
have nex_prop: "∄e. e ∈ (budget_constraint (calculate_value P) consumption_set (poe_wealth P i 𝒴)) ∧
U[i] e > U[i] (𝒳 i)"
using no_better_in_s[of "𝒳 i" "U[i]"
"budget_constraint (calculate_value P) consumption_set (poe_wealth P i 𝒴)"] x_in_argmax by blast
have "z ∈ budget_constraint (calculate_value P) consumption_set (poe_wealth P i 𝒴) ∧ U[i] z > U[i] (𝒳 i)"
using assms z_in_budget by blast
thus False using nex_prop
by blast
qed
text ‹ Given local non-satiation, argmax will use the entire budget. ›
lemma am_utilises_entire_bgt:
assumes i_agts: "i ∈ agents"
assumes lns : "local_nonsatiation consumption_set Pr[i]"
assumes argmax_sol : "X ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y))"
shows "P ∙ X = P ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (P ∙ Y j))"
proof -
let ?wlt = "P ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (P ∙ Y j))"
let ?bc = "budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y)"
have xin: "X ∈ budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y)"
using argmax_sol_in_s [of "X" "U[i]" ?bc] argmax_sol by blast
hence is_leq: "X ∙ P ≤ (poe_wealth P i Y)"
by (metis (mono_tags, lifting) budget_constraint_def
inner_commute mem_Collect_eq)
have not_less: "¬X ∙ P < (poe_wealth P i Y)"
proof
assume neg: "X ∙ P < (poe_wealth P i Y)"
have bgt_leq: "∀x∈ ?bc. U[i] X ≥ U[i] x"
using leq_all_in_sol [of "X" "U[i]" "?bc"]
all_leq [of "X" "U[i]" "?bc"]
argmax_sol by blast
define s_low where
"s_low = {x . P ∙ x < ?wlt}"
have "∃e > 0. ball X e ⊆ s_low"
proof -
have x_in_budget: "P ∙ X < ?wlt"
by (metis inner_commute neg)
have s_low_open: "open s_low"
using open_halfspace_lt s_low_def by blast
then show ?thesis
using s_low_open open_contains_ball_eq
s_low_def x_in_budget by blast
qed
obtain e where
"e > 0" and e: "ball X e ⊆ s_low"
using ‹∃e>0. ball X e ⊆ s_low› by blast
obtain y where
y_props: "y ∈ ball X e" "y ≻[Pref i] X"
using ‹0 < e› xin assms(2) budget_constraint_def
by (metis (no_types, lifting) lns_alt_def2 mem_Collect_eq)
have "y ∈ budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y)"
proof -
have "y ∈ s_low"
using ‹y ∈ ball X e› e by blast
moreover have "y ∈ consumption_set"
by (meson agent_props eucl_ordinal_utility_def i_agts ordinal_utility_def y_props(2))
moreover have "P ∙ y ≤ poe_wealth P i Y"
using calculation(1) s_low_def by auto
ultimately show ?thesis
by (simp add: budget_constraint_def)
qed
then show False
using bgt_leq i_agts y_props(2) util_fun_def_holds xin budget_constraint_def
by (metis (no_types, lifting) mem_Collect_eq)
qed
then show ?thesis
by (metis inner_commute is_leq
less_eq_real_def)
qed
corollary x_equil_x_ext_budget:
assumes i_agt: "i ∈ agents"
assumes lns : "local_nonsatiation consumption_set Pr[i]"
assumes equilibrium : "competitive_equilibrium P X Y"
shows "P ∙ X i = P ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (P ∙ Y j))"
proof -
have "X i ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y))"
using equilibrium i_agt by blast
then show ?thesis
using am_utilises_entire_bgt i_agt lns by blast
qed
lemma same_price_in_argmax :
assumes i_agt: "i ∈ agents"
assumes lns : "local_nonsatiation consumption_set Pr[i]"
assumes "x ∈ arg_max_set (U[i]) (budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y))"
assumes "y ∈ arg_max_set (U[i]) (budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y))"
shows "(P ∙ x) = (P ∙ y)"
using am_utilises_entire_bgt assms lns
by (metis (no_types) am_utilises_entire_bgt assms(3) assms(4) i_agt lns)
text ‹ Greater or equal utility implies greater or equal value. ›
lemma utility_ge_price_ge :
assumes agts: "i ∈ agents"
assumes lns : "local_nonsatiation consumption_set Pr[i]"
assumes equil: "competitive_equilibrium P X Y"
assumes geq: "U[i] z ≥ U[i] (X i)"
and "z ∈ consumption_set"
shows "P ∙ z ≥ P ∙ (X i)"
proof -
let ?bc = "(budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y))"
have not_in : "z ∉ arg_max_set (U[i]) ?bc ⟹
P ∙ z > (P ∙ ℰ[i]) + (∑j∈(firms). (Θ[i,j] *⇩R (P ∙ Y j)))"
proof-
assume "z ∉ arg_max_set (U[i]) ?bc"
moreover have "X i ∈ arg_max_set (U[i]) ?bc"
using competitive_equilibriumD assms pareto_optimal_def
by auto
ultimately have "z ∉ budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y)"
by (meson geq leq_all_in_sol)
then show ?thesis
using budget_constraint_def assms
by (simp add: budget_constraint_def)
qed
have x_in_argmax: "(X i) ∈ arg_max_set U[i] ?bc"
using agts equil by blast
hence x_in_budget: "(X i) ∈ ?bc"
using argmax_sol_in_s [of "(X i)" "U[i]" "?bc"] by blast
have "U[i] z = U[i] (X i) ⟹ P ∙ z ≥ P ∙ (X i)"
proof(rule contrapos_pp)
assume con_neg: "¬ P ∙ z ≥ P ∙ (X i)"
then have "P ∙ z < P ∙ (X i)"
by linarith
then have z_in_argmax: "z ∈ arg_max_set U[i] ?bc"
proof -
have "P ∙(X i) = P ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (P ∙ Y j))"
using agts am_utilises_entire_bgt lns x_in_argmax by blast
then show ?thesis
by (metis (no_types) con_neg less_eq_real_def not_in)
qed
have z_budget_utilisation: "P ∙ z = P ∙ (X i)"
by (metis (no_types) agts am_utilises_entire_bgt lns x_in_argmax z_in_argmax)
have "P ∙ (X i) = P ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (P ∙ Y j))"
using agts am_utilises_entire_bgt lns x_in_argmax by blast
show "¬ U[i] z = U[i] (X i)"
using z_budget_utilisation con_neg by linarith
qed
thus ?thesis
by (metis (no_types) agts am_utilises_entire_bgt eq_iff eucl_less_le_not_le lns not_in x_in_argmax)
qed
lemma commutativity_sums_over_funs:
fixes X :: "'x set"
fixes Y :: "'y set"
shows "(∑i∈X. ∑j∈Y. (f i j *⇩R C ∙ g j)) = (∑j∈Y.∑i∈X. (f i j *⇩R C ∙ g j))"
using Groups_Big.comm_monoid_add_class.sum.swap by auto
lemma assoc_fun_over_sum:
fixes X :: "'x set"
fixes Y :: "'y set"
shows "(∑j∈Y. ∑i∈X. f i j *⇩R C ∙ g j) = (∑j∈Y. (∑i∈X. f i j) *⇩R C ∙ g j)"
by (simp add: inner_sum_left scaleR_left.sum)
text ‹ Walras' law in context of production economy with private ownership.
That is, in an equilibrium demand equals supply. ›
lemma walras_law:
assumes "⋀i. i∈agents ⟹ local_nonsatiation consumption_set Pr[i]"
assumes "(∀i ∈ agents. (X i) ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (poe_wealth P i Y)))"
shows "P ∙ (∑i∈agents. (X i)) = P ∙ ((∑i∈agents. ℰ[i]) + (∑j∈firms. Y j))"
proof -
have value_equal: "P ∙ (∑i∈agents. (X i)) = P ∙ (∑i∈agents. ℰ[i]) + (∑i∈agents. ∑f∈firms. Θ[i,f] *⇩R (P ∙ Y f))"
proof -
have all_exhaust_bgt: "∀i∈agents. P ∙ (X i) = P ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (P ∙ (Y j)))"
using assms am_utilises_entire_bgt by blast
then show ?thesis
by (simp add:all_exhaust_bgt inner_sum_right sum.distrib)
qed
have eq_1: "(∑i∈agents. ∑j∈firms. (Θ[i,j] *⇩R P ∙ Y j)) = (∑j∈firms. ∑i∈agents. (Θ[i,j] *⇩R P ∙ Y j))"
using commutativity_sums_over_funs [of Θ P Y firms agents] by blast
hence eq_2: "P ∙ (∑i∈agents. X i) = P ∙ (∑i∈agents. ℰ[i]) + (∑j∈firms. ∑i∈agents. Θ[i,j] *⇩R P ∙ Y j)"
using value_equal by auto
also have eq_3: "...= P ∙ (∑i∈agents. ℰ[i]) + (∑j∈firms. (∑i∈agents. Θ[i,j]) *⇩R P ∙ Y j)"
using assoc_fun_over_sum[of "Θ" P Y agents firms] by auto
also have eq_4: "... = P ∙ (∑i∈agents. ℰ[i]) + (∑f∈firms. P ∙ Y f)"
using firms_comp_owned by auto
have comp_wise_inner: "P ∙ (∑i∈agents. X i) - (P ∙ (∑i∈agents. ℰ[i])) - (∑f∈firms. P ∙ Y f) = 0"
using eq_1 eq_2 eq_3 eq_4 by linarith
then show ?thesis
by (simp add: inner_right_distrib inner_sum_right)
qed
lemma walras_law_in_compeq:
assumes "⋀i. i∈agents ⟹ local_nonsatiation consumption_set Pr[i]"
assumes "competitive_equilibrium P X Y"
shows "P ∙ ((∑i∈agents. (X i)) - (∑i∈agents. ℰ[i]) - (∑j∈firms. Y j)) = 0"
proof-
have "P ∙ (∑i∈agents. (X i)) = P ∙ ((∑i∈agents. ℰ[i]) + (∑j∈firms. Y j))"
using assms(1) assms(2) walras_law by auto
then show ?thesis
by (simp add: inner_diff_right inner_right_distrib)
qed
subsection ‹ First Welfare Theorem ›
text ‹ Proof of First Welfare Theorem in context of production economy with private ownership. ›
theorem first_welfare_theorem_priv_own:
assumes "⋀i. i ∈ agents ⟹ local_nonsatiation consumption_set Pr[i]"
and "Price > 0"
assumes "competitive_equilibrium Price 𝒳 𝒴"
shows "pareto_optimal 𝒳 𝒴"
proof (rule ccontr)
assume neg_as: "¬ pareto_optimal 𝒳 𝒴"
have equili_feasible : "feasible 𝒳 𝒴"
using assms by (simp add: competitive_equilibrium_def)
obtain X' Y' where
xprime_pareto: "feasible X' Y' ∧
(∀i ∈ agents. U[i] (X' i) ≥ U[i] (𝒳 i)) ∧
(∃i ∈ agents. U[i] (X' i) > U[i] (𝒳 i))"
using equili_feasible pareto_optimal_def
pareto_dominating_def neg_as by auto
have is_feasible: "feasible X' Y'"
using xprime_pareto by blast
have xprime_leq_y: "∀i ∈ agents. (Price ∙ (X' i) ≥
(Price ∙ ℰ[i]) + (∑j∈(firms). Θ[i,j] *⇩R (Price ∙ 𝒴 j)))"
proof
fix i
assume as: "i ∈ agents"
have xprime_cons: "X' i ∈ consumption_set"
using feasible_private_ownershipD as is_feasible by blast
have x_leq_xprime: "U[i] (X' i) ≥ U[i] (𝒳 i)"
using ‹i ∈ agents› xprime_pareto by blast
have lns_pref: "local_nonsatiation consumption_set Pr[i]"
using as assms by blast
hence xprime_ge_x: "Price ∙ (X' i) ≥ Price ∙ (𝒳 i)"
using x_leq_xprime xprime_cons as assms utility_ge_price_ge by blast
then show "Price ∙ (X' i) ≥ (Price ∙ ℰ[i]) + (∑j∈(firms). Θ[i,j] *⇩R (Price ∙ 𝒴 j))"
using xprime_ge_x ‹i ∈ agents› lns_pref assms x_equil_x_ext_budget by fastforce
qed
have ex_greater_value : "∃i ∈ agents. Price ∙ (X' i) > Price ∙ (𝒳 i)"
proof(rule ccontr)
assume cpos : "¬(∃i ∈ agents. Price ∙ (X' i) > Price ∙ (𝒳 i))"
obtain i where
obt_witness : "i ∈ agents" "(U[i]) (X' i) > U[i] (𝒳 i)"
using xprime_pareto by blast
show False
by (metis all_prefered_are_more_expensive assms(3) cpos
feasible_private_ownershipD(2) inner_commute xprime_pareto)
qed
have dom_g : "Price ∙ (∑i∈agents. X' i) > Price ∙ (∑i∈agents. (𝒳 i))" (is "_ > _ ∙ ?x_sum")
proof-
have "(∑i∈agents. Price ∙ X' i) > (∑i∈agents. Price ∙ (𝒳 i))"
by (metis (mono_tags, lifting) xprime_leq_y assms(1,3) ex_greater_value
finite_nonepty_agents sum_strict_mono_ex1 x_equil_x_ext_budget)
thus "Price ∙ (∑i∈agents. X' i) > Price ∙ ?x_sum"
by (simp add: inner_sum_right)
qed
let ?y_sum = "(∑j∈firms. 𝒴 j)"
have equili_walras_law: "Price ∙ ?x_sum =
(∑i∈agents. Price ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (Price ∙ 𝒴 j)))" (is "_ = ?ws")
proof-
have "∀i∈agents. Price ∙ 𝒳 i = Price ∙ ℰ[i] + (∑j∈firms. Θ[i,j] *⇩R (Price ∙ 𝒴 j))"
by (metis (no_types, lifting) assms(1,3) x_equil_x_ext_budget)
then show ?thesis
by (simp add: inner_sum_right)
qed
also have remove_firm_pct: "... = Price ∙ (∑i∈agents. ℰ[i]) + (Price ∙ ?y_sum)"
proof-
have equals_inner_price:"0 = Price ∙ (?x_sum - ((∑i∈agents. ℰ i) + ?y_sum))"
by (metis (no_types) diff_diff_add assms(1,3) walras_law_in_compeq)
have "Price ∙ ?x_sum = Price ∙ ((∑i∈agents. ℰ i) + ?y_sum)"
by (metis (no_types) equals_inner_price inner_diff_right right_minus_eq)
then show ?thesis
by (simp add: equili_walras_law inner_right_distrib)
qed
have xp_l_yp: "(∑i∈agents. X' i) ≤ (∑i∈agents. ℰ[i]) + (∑f∈firms. Y' f)"
using feasible_private_ownership_def is_feasible by blast
hence yprime_sgr_y: "Price ∙ (∑i∈agents. ℰ[i]) + Price ∙ (∑f∈firms. Y' f) > ?ws"
proof -
have "Price ∙ (∑i∈agents. X' i) ≤ Price ∙ ((∑i∈agents. ℰ[i]) + (∑j∈firms. Y' j))"
by (metis xp_l_yp atLeastAtMost_iff inner_commute
interval_inner_leI(2) less_imp_le order_refl assms(2))
hence "?ws < Price ∙ ((∑i∈agents. ℰ i) + (∑j∈firms. Y' j))"
using dom_g equili_walras_law by linarith
then show ?thesis
by (simp add: inner_right_distrib)
qed
have Y_is_optimum: "∀j∈firms. ∀y ∈ production_sets j. Price ∙ 𝒴 j ≥ Price ∙ y"
using assms prof_max_ge_all_in_pset by blast
have yprime_in_prod_set: "∀j ∈ firms. Y' j ∈ production_sets j"
using feasible_private_ownershipD xprime_pareto by fastforce
hence "∀j ∈ firms. ∀y ∈ production_sets j. Price ∙ 𝒴 j ≥ Price ∙ y"
using Y_is_optimum by blast
hence Y_ge_yprime: "∀j ∈ firms. Price ∙ 𝒴 j ≥ Price ∙ Y' j"
using yprime_in_prod_set by blast
hence yprime_p_leq_Y: "Price ∙ (∑f∈firms. Y' f) ≤ Price ∙ ?y_sum"
by (simp add: Y_ge_yprime inner_sum_right sum_mono)
then show False
using remove_firm_pct yprime_sgr_y by linarith
qed
text ‹ Equilibrium cannot be Pareto dominated. ›
lemma equilibria_dom_eachother:
assumes "⋀i. i ∈ agents ⟹ local_nonsatiation consumption_set Pr[i]"
and "Price > 0"
assumes equil: "competitive_equilibrium Price 𝒳 𝒴"
shows "∄X' Y'. competitive_equilibrium P X' Y' ∧ X' ≻Pareto 𝒳"
proof -
have "pareto_optimal 𝒳 𝒴"
by (meson equil first_welfare_theorem_priv_own assms)
hence "∄X' Y'. feasible X' Y' ∧ X' ≻Pareto 𝒳"
using pareto_optimal_def by blast
thus ?thesis
by auto
qed
text ‹ Using monotonicity instead of local non-satiation proves the First Welfare Theorem. ›
corollary first_welfare_thm_monotone:
assumes "∀M ∈ carrier. (∀x > M. x ∈ carrier)"
assumes "⋀i. i ∈ agents ⟹ monotone_preference consumption_set Pr[i]"
and "Price > 0"
assumes "competitive_equilibrium Price 𝒳 𝒴"
shows "pareto_optimal 𝒳 𝒴"
by (meson arrow_debreu_consum_set_def assms cons_set_props first_welfare_theorem_priv_own unbounded_above_mono_imp_lns)
end
end
end