Theory Exchange_Economy

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


theory Exchange_Economy
  imports
    "../Preferences"
    "../Utility_Functions"
    "../Argmax"
    Consumers
    Common
begin

section ‹ Exchange Economy ›

text ‹ Define the exchange economy model ›

locale exchange_economy =
  fixes consumption_set :: "('a::ordered_euclidean_space) set"
  fixes agents :: "'i set"
  fixes ℰ :: "'i ⇒ 'a"
  fixes Pref :: "'i ⇒ 'a relation"
  fixes U :: "'i ⇒ 'a ⇒ real"
  assumes cons_set_props: "pre_arrow_debreu_consumption_set consumption_set"
  assumes agent_props: "i ∈ agents ⟹ eucl_ordinal_utility consumption_set (Pref i) (U i)"
  assumes finite_agents: "finite agents" and "agents ≠ {}"

sublocale exchange_economy ⊆ pareto_ordering agents U
  .                                 

context exchange_economy
begin

context 
begin

notation U ("U[_]")
notation Pref ("Pr[_]")
notation ℰ ("ℰ[_]")

lemma base_pref_is_ord_eucl_rpr: "i ∈ agents ⟹ rational_preference consumption_set Pr[i]"
  by (meson exchange_economy.agent_props exchange_economy_axioms
      ord_eucl_utility_imp_rpr real_vector_rpr.have_rpr)

private abbreviation calculate_value 
  where
    "calculate_value P x ≡ P ∙ x"

subsection ‹ Feasibility ›

definition feasible_allocation
  where
    "feasible_allocation A E ⟷
      (∑i∈agents. A i) ≤ (∑i∈agents. E i)"


subsection ‹ Pareto optimality ›

definition pareto_optimal_endow
  where
    "pareto_optimal_endow X E ⟷
              (feasible_allocation X E ∧
              (∄X'. feasible_allocation X' E ∧ X' ≻Pareto X))"


subsection ‹Competitive Equilibrium in Exchange Economy ›

text ‹ Competitive Equilibirum or Walrasian Equilibrium definition. ›

definition comp_equilib_endow
  where
    "comp_equilib_endow P X E ≡
      feasible_allocation X E ∧
      (∀i ∈ agents. X i ∈ arg_max_set U[i]
        (budget_constraint (calculate_value P) consumption_set (P ∙ E i)))"


subsection ‹ Lemmas for final result ›

lemma utility_function_def[iff]:
  assumes "i ∈ agents"
  shows "U[i] x ≥ U[i] y ⟷ x ≽[Pr[i]] y"
proof
  have "ordinal_utility consumption_set (Pref i) (U[i])"
    using agent_props assms eucl_ordinal_utility_def by auto
  then show " U[i] y ≤  U[i] x ⟹ x ≽[Pref i] y"
    by (meson UNIV_I cons_set_props ordinal_utility.util_def_conf
        pre_arrow_debreu_consumption_set_def)
next
  show "x ≽[Pref i] y ⟹ U[i] y ≤ U[i] x"
    by (meson agent_props assms ordinal_utility_def eucl_ordinal_utility_def)
qed

lemma budget_constraint_is_feasible:
  assumes "i ∈ agents"
  assumes "X ∈ (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
  shows "P ∙ X ≤ P ∙ ℰ[i]"
  using budget_constraint_def assms
  by (simp add: budget_constraint_def)

lemma arg_max_set_therefore_no_better :
  assumes "i ∈ agents"
  assumes "x ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
  shows "U[i] y > U[i] x ⟶ y ∉ budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"
  by (meson no_better_in_s assms)

text ‹ Since we need no restriction on the consumption set for the First Welfare Theorem ›

lemma consumption_set_member: "∀x. x ∈ consumption_set"
proof -
  have "⋀(x::'a). x ∈ consumption_set"
    using cons_set_props pre_arrow_debreu_consumption_set_def
    by (simp add: pre_arrow_debreu_consumption_set_def)
  thus ?thesis
    by blast
qed

text ‹ Under the assumption of Local non-satiation, agents will utilise their entire budget. ›

lemma argmax_entire_budget :
  assumes "i ∈ agents"
  assumes "local_nonsatiation consumption_set Pr[i]"
  assumes "X ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
  shows "P ∙ X = P ∙ ℰ[i]"
proof -
  have leq : "(P ∙ X) ≤ (P ∙ ℰ[i])"
  proof-
    have "X ∈ budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"
      using argmax_sol_in_s[of X "U[i]" "budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"]
        assms by auto
    thus ?thesis
      using assms(1) budget_constraint_is_feasible by blast
  qed
  have not_less: "¬(P ∙ X < P ∙ ℰ[i])"
  proof
    assume cpos: "(P ∙ X) < (P ∙ ℰ[i])"
    define lesS where "lesS = {x. P ∙ x < P ∙ ℰ[i]}"
    obtain e where
      e: "0 < e" "ball X e ⊆ lesS"
      by (metis cpos lesS_def mem_Collect_eq
          open_contains_ball_eq open_halfspace_lt)
    obtain Y where
      Y: "Y ≻[Pref i] X " "Y ∈ ball X e"
      using e consumption_set_member assms by blast
    have "Y ∈ consumption_set"
      using consumption_set_member by blast
    hence "Y ∈ budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"
      using budget_constraint_def e lesS_def
        less_eq_real_def Y  by fastforce
    thus False
      by (meson assms Y all_leq utility_function_def)
  qed
  show ?thesis
    using leq not_less by auto
qed

text ‹ All bundles that would be strictly preferred to any argmax result, are more expensive. ›

lemma pref_more_expensive:
  assumes "i ∈ agents"
  assumes "x ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
  assumes "U[i] y > U[i] x"
  shows "y ∙ P > P ∙ ℰ[i]"
proof (rule ccontr)
  assume cpos :  "¬(y ∙ P > P ∙ ℰ[i])"
  then have xp_leq : "y ∙ P ≤ P ∙  ℰ[i]"
    by auto
  hence "x ∈ budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"
    using argmax_sol_in_s[of x " U[i]" "budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"]
      assms by auto
  hence xp_in: "y ∈ budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"
  proof -
    have "P ∙ y ≤ P ∙ ℰ[i]"
      by (metis xp_leq inner_commute)
    then show ?thesis
      using consumption_set_member by (simp add: budget_constraint_def)
  qed
  hence "y ≻[Pref i] x"
    using arg_max_set_therefore_no_better assms by blast
  hence "y ≻[Pref i] x ∧ y ∈ budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"
    using xp_in by blast
  hence "x ∉ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
    by (meson assms exchange_economy.arg_max_set_therefore_no_better
        exchange_economy_axioms)
  then show False
    using assms(2) by auto
qed

text ‹ Greater or equal utility implies greater or equal price. ›

lemma same_util_is_equal_or_more_expensive:
  assumes "i ∈ agents"
  assumes "local_nonsatiation consumption_set Pr[i]"
  assumes "x ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
  assumes "U[i] y ≥ U[i] x"
  shows "y ∙ P ≥ P ∙ ℰ[i]"
proof-
  have not_in: "y ∉ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))
    ⟹ y ∙ P > P ∙ ℰ[i]"
  proof-
    assume "y ∉ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
    then have "y ∉ budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i])"
      by (meson assms leq_all_in_sol assms)
    then show ?thesis
      by (simp add: budget_constraint_def inner_commute
          consumption_set_member)
  qed
  show ?thesis
    by (metis argmax_entire_budget not_in assms(1,2,3)
        dual_order.order_iff_strict inner_commute)
qed

lemma all_in_argmax_same_price:
  assumes "i ∈ agents"
  assumes "local_nonsatiation consumption_set Pr[i]"
  assumes "x ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
    and  "y ∈ arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P ∙ ℰ[i]))"
  shows "P ∙ x = P ∙ y"
  using argmax_entire_budget assms(1) assms(2) assms(3) assms(4) by presburger

text ‹ All rationally acting agents (which is every agent by assumption)
        will not decrease his utility ›
lemma individual_rationalism :
  assumes "comp_equilib_endow P X ℰ"
  shows "∀i ∈ agents. X i ≽[Pref i] ℰ[i]"
  by (metis pref_more_expensive comp_equilib_endow_def assms
      inner_commute less_irrefl not_le utility_function_def)

lemma walras_law_per_agent :
  assumes "⋀i. i ∈ agents ⟹ local_nonsatiation consumption_set Pr[i]"
  assumes "comp_equilib_endow P X ℰ"
  shows "∀i ∈ agents. P ∙ X i = P ∙ ℰ[i]"
  by (meson argmax_entire_budget comp_equilib_endow_def assms)

text ‹ Walras Law holds in our Exchange Economy model. It states that in an equilibrium,
       demand equals supply ›

lemma walras_law:
  assumes "⋀i. i ∈ agents ⟹ local_nonsatiation consumption_set Pr[i]"
  assumes "comp_equilib_endow P X ℰ"
  shows "(∑i∈agents. P ∙ (X i)) - (∑i∈agents. P ∙ ℰ[i]) = 0"
  using assms walras_law_per_agent by auto

lemma inner_with_ge_0: "(P::(real, 'n::finite) vec) > 0 ⟹ A ≥ B ⟹  P ∙ A ≥ P ∙ B"
  by (metis dual_order.order_iff_strict inner_commute
      interval_inner_leI(2) ord_class.atLeastAtMost_iff)

subsection ‹ First Welfare Theorem in Exchange Economy ›

text ‹ We prove the first welfare theorem in our Exchange Economy model. ›

theorem first_welfare_theorem_exchange:
  assumes lns : "⋀i. i ∈ agents ⟹ local_nonsatiation consumption_set Pr[i]"
    and price_cond: "Price > 0"
  assumes equilibrium : "comp_equilib_endow Price 𝒳 ℰ"
  shows "pareto_optimal_endow 𝒳 ℰ"
proof (rule ccontr)
  assume neg_ass : "¬ pareto_optimal_endow 𝒳 ℰ"
  have equili_feasible : "feasible_allocation 𝒳 ℰ"
    using comp_equilib_endow_def equilibrium
    by (simp add: comp_equilib_endow_def)
  have price_g_zero : "Price > 0"
    by (simp add: price_cond)
  obtain Y where
    xprime_pareto: "feasible_allocation Y ℰ ∧
            (∀i ∈ agents. U[i] (Y i) ≥ U[i] (𝒳 i)) ∧
            (∃i ∈ agents. U[i] (Y i) > U[i] (𝒳 i))"
    using equili_feasible neg_ass pareto_dominating_def
      pareto_optimal_endow_def by auto
  have is_feasible : "feasible_allocation Y ℰ"
    using xprime_pareto by blast
  have all_great_eq_value : "∀i ∈ agents. Price ∙ (Y i) ≥ Price ∙ (𝒳 i)"
  proof
    fix i
    assume "i ∈ agents"
    show "Price ∙ (Y i) ≥ Price ∙ (𝒳 i)"
    proof -
      have x_in_agmx : "(𝒳 i) ∈ arg_max_set U[i] (budget_constraint (calculate_value Price) consumption_set (Price ∙ ℰ[i]))"
        by (meson ‹i ∈ agents› comp_equilib_endow_def equilibrium)
      have "( U[i]) (𝒳 i) - U[i] (Y i) ≤ 0"
        using ‹i ∈ agents› xprime_pareto by auto
      hence "Price ∙ (𝒳 i) - Price ∙ (Y i) ≤ 0"
        by (metis ‹i ∈ agents› argmax_entire_budget diff_le_0_iff_le x_in_agmx
            inner_commute lns same_util_is_equal_or_more_expensive)
      then show ?thesis
        by auto
    qed
  qed
  have ex_greater_value : "∃i ∈ agents. Price ∙ (Y i) > Price ∙ (𝒳 i)"
  proof (rule ccontr)
    assume a1 : "¬(∃i ∈ agents. Price ∙ (Y i) > Price ∙ (𝒳 i))"
    obtain i where
      obt_witness : "i ∈ agents" "U[i] (Y i) > ( U[i]) (𝒳 i)"
      using xprime_pareto by blast
    have "Price ∙ Y i ≠ Price ∙ 𝒳 i"
    proof -
      have "Price ∙ Y i > Price ∙ ℰ i"
        by (metis pref_more_expensive comp_equilib_endow_def
            equilibrium inner_commute obt_witness(1) obt_witness(2))
      have "Price ∙ ℰ i = Price ∙ 𝒳 i"
        using equilibrium lns obt_witness(1) walras_law_per_agent by auto
      then show ?thesis
        using ‹Price ∙ ℰ i < Price ∙ Y i› by linarith
    qed
    then show False
      using a1 all_great_eq_value obt_witness(1) by fastforce
  qed
  have dominating_more_exp : "Price ∙ (∑i∈agents. Y i) > Price ∙ (∑i∈agents. 𝒳 i)"
  proof -
    have mp_rule : "(∑i∈agents. Price ∙ Y i) > (∑i∈agents. Price ∙ 𝒳 i) ⟹ ?thesis"
      by (simp add: inner_sum_right)
    have "(∑i∈agents. Price ∙ Y i) > (∑i∈agents. Price ∙ 𝒳 i)"
      by (simp add: all_great_eq_value finite_agents ex_greater_value sum_strict_mono_ex1)
    thus "Price ∙ (∑i∈agents. Y i) > Price ∙ (∑i∈agents. 𝒳 i)"
      using mp_rule by blast
  qed
  have equili_walras_law : "Price ∙ (∑i∈agents. 𝒳 i) = Price ∙ (∑i∈agents. ℰ[i])"
    by (metis (mono_tags) eq_iff_diff_eq_0 equilibrium
        inner_sum_right lns walras_law)
  have dominating_feasible : "Price ∙ (∑i∈agents. 𝒳 i) ≥ Price ∙ (∑i∈agents. Y i)"
    by (metis atLeastAtMost_iff dual_order.order_iff_strict equili_walras_law
        feasible_allocation_def inner_commute interval_inner_leI(1) is_feasible price_g_zero)
  show False
    using dominating_more_exp equili_walras_law dominating_feasible
    by linarith
qed


text ‹ Monotone preferences can be used instead of local non-satiation.
       Many textbooks etc. do not introduce the concept of
       local non-satiation and use monotonicity instead. ›

corollary first_welfare_exch_thm_monot:
  assumes "∀M ∈ carrier. (∀x > M. x ∈ carrier)"
  assumes "⋀i. i ∈ agents ⟹ monotone_preference consumption_set Pr[i]"
  and price_cond: "Price > 0"
  assumes "comp_equilib_endow Price 𝒳 ℰ"
  shows "pareto_optimal_endow 𝒳 ℰ"
  by (meson assms exchange_economy.consumption_set_member
      first_welfare_theorem_exchange exchange_economy_axioms unbounded_above_mono_imp_lns)

end

end

end