Theory Arrow_Debreu_Model

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


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  (iagents. Θ[i,j]) = 1"
  assumes finite_nonepty_agents: "finite agents" and "agents  {}"

sublocale pre_arrow_debreu_model  pareto_ordering agents U
  .

(*sublocale pre_arrow_debreu_model ⊆ exchange_economy consumption_set agents ℰ Pref U Price
  by (metis exchange_economy.intro pre_arrow_debreu_model_axioms pre_arrow_debreu_model_def)
*)

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] + (jfirms. Θ[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] + (jfirms. Θ[i,j] *R (P  Y j))"
proof -
  let ?wlt = "P  ℰ[i] + (jfirms. Θ[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] + (jfirms. Θ[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] + (jfirms. Θ[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] + (jfirms. Θ[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 "(iX. jY. (f i j *R C  g j)) = (jY.iX. (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 "(jY. iX. f i j *R C  g j) = (jY. (iX. 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. iagents  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  (iagents. (X i)) = P  ((iagents. ℰ[i]) + (jfirms. Y j))"
proof -
  have value_equal: "P  (iagents. (X i)) = P  (iagents. ℰ[i]) + (iagents. ffirms. Θ[i,f] *R (P  Y f))"
  proof -
    have all_exhaust_bgt: "iagents. P  (X i) = P  ℰ[i] + (jfirms. Θ[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: "(iagents. jfirms. (Θ[i,j] *R P  Y j)) = (jfirms. iagents. (Θ[i,j] *R P  Y j))"
    using commutativity_sums_over_funs [of Θ P Y firms agents] by blast
  hence eq_2: "P  (iagents. X i) = P  (iagents. ℰ[i]) + (jfirms. iagents. Θ[i,j] *R P  Y j)"
    using value_equal by auto
  also  have eq_3: "...= P  (iagents. ℰ[i]) + (jfirms. (iagents. Θ[i,j]) *R P   Y j)"
    using assoc_fun_over_sum[of "Θ" P Y agents firms] by auto
  also have eq_4: "... = P  (iagents. ℰ[i]) + (ffirms. P   Y f)"
    using firms_comp_owned by auto
  have comp_wise_inner: "P   (iagents. X i) - (P  (iagents. ℰ[i])) - (ffirms. 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. iagents  local_nonsatiation consumption_set Pr[i]"
  assumes "competitive_equilibrium P X Y"
  shows "P  ((iagents. (X i)) - (iagents. ℰ[i]) - (jfirms. Y j)) = 0"
proof-
  have "P  (iagents. (X i)) = P  ((iagents. ℰ[i]) + (jfirms. 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  (iagents. X' i) > Price  (iagents. (𝒳 i))" (is "_ > _  ?x_sum")
  proof-
    have "(iagents. Price  X' i) > (iagents. 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  (iagents. X' i) > Price  ?x_sum"
      by (simp add: inner_sum_right)
  qed
  let ?y_sum = "(jfirms. 𝒴 j)"
  have equili_walras_law: "Price  ?x_sum =
    (iagents. Price  ℰ[i] + (jfirms. Θ[i,j] *R (Price  𝒴 j)))" (is "_ = ?ws")
  proof-
    have "iagents. Price  𝒳 i = Price  ℰ[i] + (jfirms. Θ[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  (iagents. ℰ[i]) + (Price  ?y_sum)"
  proof-
    have equals_inner_price:"0 = Price  (?x_sum - ((iagents.  i) + ?y_sum))"
      by (metis (no_types) diff_diff_add assms(1,3) walras_law_in_compeq)
    have "Price  ?x_sum = Price  ((iagents.  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: "(iagents. X' i)  (iagents. ℰ[i]) + (ffirms. Y' f)"
    using feasible_private_ownership_def is_feasible by blast
  hence yprime_sgr_y: "Price  (iagents. ℰ[i]) + Price  (ffirms. Y' f) > ?ws"
  proof -
    have "Price  (iagents. X' i)  Price  ((iagents. ℰ[i]) + (jfirms. 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  ((iagents.  i) + (jfirms. Y' j))"
      using dom_g equili_walras_law by linarith
    then show ?thesis
      by (simp add: inner_right_distrib)
  qed
  have Y_is_optimum: "jfirms. 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  (ffirms. 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