Leibniz' Project
Utility is a kind of index of satisfaction: it is a number such that, the higher it is, the more satisfied you are. Then the social utility is the sum of all individual utilities and constitutes a kind of global index of satisfaction.
The present article states that, essentially, if everyone is assigned the same (standard) utility, pure communism is the (single) redistribution which maximizes the social utility.
One relies on this article.
Throughout this page, let \(I\) be the finite set of individuals (with \(N\) as the number of individuals) and \(gs \in \mathbb R\) is governement spending.
variable {Individual : Type} variable {eqInd : DecidableEq Individual} variable {Society : Fintype Individual}
The more money you receive, the more you are satisfied: utility increases with money.
\(\mathbf{Definition}\)
The utility function \(u: \mathbb R \to
\mathbb R\) is said to increase with money if it is
monotone.
def increases_with_money (utility : MonetaryValue -> ℝ) : Prop := Monotone utility
You are more satisfied to get an extra euro when you already have only one euro than when you have 1000€.
\(\mathbf{Definition}\)
The utility function \(u: \mathbb R \to
\mathbb R\) is said to (resp. strictly) satisfy the law of
diminishing marginal utility if \(u''\) is (resp. strictly)
concave on \({\mathbb R}^+\).
def law_diminishing_marginal_utility (utility : MonetaryValue -> ℝ) : Prop := ConcaveOn ℝ (Set.Ici (0 : ℝ)) utility def law_diminishing_marginal_utility_strict (utility : MonetaryValue -> ℝ) : Prop := StrictConcaveOn ℝ (Set.Ici (0 : ℝ)) utility
The social utility is just of all individual utilities.
\(\mathbf{Definition}\)
Let \(u: \mathbb R \to \mathbb
R\) be a utility function and \(r
: I \to \mathbb R\) be a profile of retributions given to
individuals.
The social utility of \(u\) on
\(r\) is \(\sum_{i \in I} u(r(i))\).
def (utility : MonetaryValue -> ℝ) (retr : Individual -> ℝ) : ℝ := ∑ i, utility (retr i)
Pure communism is essentially the single redistribution maximizing the social utility.
\(\mathbf{Proposition}\)
Let \(u: \mathbb R \to \mathbb
R\) be a utility function satisfying the law of diminishing
marginal utility.
Let \(r : {\mathbb R}^I \to {\mathbb
R}^I\) be a redistribution and \(c \in {\mathbb R}^I\) be a
retribution profile, such that all indivdual retributions are
nonnegative (this hypothesis is here only in order to be able to
apply the law of diminishing marginal utility which regards only
positive retributions).
Then the social utility on \(r(c)\) is less or equal to the social
utility with pure communism instead of \(r\).
\(\mathbf{proof:}\)
The social utility on \(r(c)\) is
\(su = \sum_{i \in I}
u(r(c)(i))\).
\(u\) being concave, by Jensen’s
inequality, \[u(\frac {\sum_{i \in I}
r(c)(i)} N) \ge \frac {\sum_{i \in I} u(r(c)(i))} N\] So
that \[su \le N \times u(\frac {\sum_{i
\in I} r(c)(i)} N)\] By the equilibrium of accounts, \(\sum_{i \in I} r(c)(i) = \sum_{i \in I} c(i)
- gs\), so \[su \le N \times
u(\frac {(\sum_{i \in I} c(i)) - gs} N)\] The right hand
side of the inequality above is the social utility which would
have occurred in pure communism.
■
\(\mathbf{Proposition}\)
Let \(u: \mathbb R \to \mathbb
R\) be a utility function strictly satisfying the law of
diminishing marginal utility.
Let \(r : {\mathbb R}^I \to {\mathbb
R}^I\) be a redistribution and \(c \in {\mathbb R}^I\) be a
retribution profile, such that all indivdual retributions are
nonnegative.
If the social utility on \(r(c)\)
equals to the social utility with pure communism instead of \(r\) (that is if it is maximal), then
\(r\) coincides with pure
communism on \(c\).
\(\mathbf{proof:}\)
If \(r\) does not coincide with
pure communism, there would two individual retributions. So that,
\(u\) being strictly concave, by
the strict version of Jensen’s inequality, \[u(\frac {\sum_{i \in I} r(c)(i)} N) \gt
\frac {\sum_{i \in I} u(r(c)(i))} N\] So that \[\sum_{i \in I} u(r(c)(i)) \lt N \times
u(\frac {\sum_{i \in I} r(c)(i)} N)\] By the equilibrium of
accounts, \(\sum_{i \in I} r(c)(i) =
\sum_{i \in I} c(i) - gs\), so \[\sum_{i \in I} u(r(c)(i)) \lt N \times
u(\frac {(\sum_{i \in I} c(i)) - gs} N)\] Therefore the
social utility on \(r(c)\)
(left-hand side of the inequality above) does not equal the social
utility with pure communism instead of \(r\) (right-hand side of the
inequality above).
■
theorem {government_spending : MonetaryValue} {utility : MonetaryValue -> ℝ} {cont : Individual -> MonetaryValue} {redi : @Redistribution Individual Society government_spending} (inh : Fintype.card Individual ≠ 0) (ldmu : law_diminishing_marginal_utility utility) (rpos : ∀ i, 0 ≤ redi.val cont i) : @social_utility Individual Society utility (redi.val cont) ≤ @social_utility Individual Society utility ( @pure_communism Individual Society government_spending cont ) := by unfold social_utility pure_communism total_value rw [Finset.sum_const] unfold law_diminishing_marginal_utility at ldmu let weight := fun _ : Individual => (1 : ℝ) / ↑(Fintype.card Individual) have h0 : ∀ i, 0 ≤ weight i := by unfold weight intro i exact Nat.one_div_cast_nonneg (Fintype.card Individual) have inh' : (Fintype.card Individual : ℝ) ≠ 0 := by exact Nat.cast_ne_zero.mpr inh have h1 : ∑ i, weight i = 1 := by unfold weight rw [Finset.sum_const] simp rw [Lean.Grind.Field.mul_inv_cancel] exact inh' have jens : ( ∑ i, weight i * utility (redi.val cont i) ≤ utility (∑ i, weight i * (redi.val cont i)) ) := by apply ldmu.le_map_sum · intro i iin unfold weight simp · unfold weight rw [Finset.sum_const] simp rw [Lean.Grind.Field.mul_inv_cancel] exact inh' · intro i iin specialize (rpos i) simp exact rpos unfold weight at jens rw [sum_reals_mult_constant] at jens have equi := redi.property cont unfold accounts_at_equilibirum total_value at equi have equl : ∑ i, cont i - government_spending = ∑ i, redi.val cont i := by exact sub_eq_iff_eq_add.mpr (id (Eq.symm equi)) rw [equl] have mulc : ( ∑ i, redi.val cont i / ↑(Fintype.card Individual) = ∑ i, 1 / ↑(Fintype.card Individual) * redi.val cont i ) := by apply Fintype.sum_congr intro i field rw [<- mulc] at jens have nneg : 0 ≤ (Fintype.card Individual : ℝ) := by exact Nat.cast_nonneg' (Fintype.card Individual) apply Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_left at jens specialize (jens nneg) rw [<- mul_assoc] at jens simp at jens rw [Lean.Grind.Field.mul_inv_cancel] at jens · rw [one_mul] at jens simp rw [sum_reals_div_constant] at jens · exact jens · exact Nat.cast_ne_zero.mpr inh · exact Nat.cast_ne_zero.mpr inh theorem {government_spending : MonetaryValue} {utility : MonetaryValue -> ℝ} {cont : Individual -> MonetaryValue} {redi : @Redistribution Individual Society government_spending} (inh : Fintype.card Individual ≠ 0) (ldmu : law_diminishing_marginal_utility_strict utility) (rpos : ∀ i, 0 ≤ redi.val cont i) : @social_utility Individual Society utility (redi.val cont) = @social_utility Individual Society utility ( @pure_communism Individual Society government_spending cont ) → redi.val cont = @pure_communism Individual Society government_spending cont := by intro eqsu unfold social_utility pure_communism total_value at eqsu rw [Finset.sum_const] at eqsu let weight := fun _ : Individual => (1 : ℝ) / ↑(Fintype.card Individual) have equi := redi.property cont unfold total_value at equi have h0 : ∀ i, 0 < weight i := by unfold weight intro i exact Nat.one_div_cast_pos inh have inh' : (Fintype.card Individual : ℝ) ≠ 0 := by exact Nat.cast_ne_zero.mpr inh have h1 : ∑ i, weight i = 1 := by unfold weight rw [Finset.sum_const] simp rw [Lean.Grind.Field.mul_inv_cancel] exact inh' by_contra nerd have jens : ( ∑ i, weight i * utility (redi.val cont i) < utility (∑ i, weight i * (redi.val cont i)) ) := by apply ldmu.lt_map_sum · intro i iin unfold weight simp exact Nat.zero_lt_of_ne_zero inh · unfold weight rw [Finset.sum_const] simp rw [Lean.Grind.Field.mul_inv_cancel] exact inh' · intro i iin specialize (rpos i) simp exact rpos · contrapose nerd rw [not_exists] at nerd simp at nerd unfold pure_communism total_value apply funext intro i specialize (nerd i) have sumc : ( ∑ j, redi.val cont j = ↑(Fintype.card Individual) * redi.val cont i ) := by rw [Fintype.sum_congr (fun j => redi.val cont j) (fun _ => redi.val cont i)] · rw [Finset.sum_const] simp · intro k rw [nerd] rw [<- equi] simp rw [sumc] rw [mul_comm] rw [mul_div_assoc] rw [div_self] · simp · exact inh' unfold weight at jens rw [sum_reals_mult_constant] at jens rw [sum_reals_mult_constant] at jens rw [eqsu] at jens simp at jens rw [<- mul_assoc] at jens rw [Lean.Grind.Field.inv_mul_cancel] at jens · rw [<- equi] at jens simp at jens rw [mul_comm] at jens rw [div_eq_mul_inv] at jens simp at jens · exact inh'
