Leibniz' Project
Home
A definition of capitalism and communism in terms of redistribution of wealth

Presentation

Taxation permits to redistribute wealth between individuals in a society, drawing off the government’s operating costs.
With wealth being represented as money (that is as a number):
- in pure capitalism, there is no operating cost and the redistribution just retributes every individual up to its contribution
- in pure capitalism with operating costs equally divided between individuals (everyone pays the same tax), the redistribution retributes every individual up to its contribution, minus its share in the costs
- purely ccommunist redistribution equally retributes every individual, whatever its contribution

Throughout this page, let \(I\) be the finite set of individuals (with \(N \gt 0\) as the number of individuals).
Contributions by individuals are represented by their monetary value, which is a real number (potentially negative, in case of vandalism for example). So are retributions to individuals, and government spending.

	
		variable {Individual : Type}
variable {eqInd : DecidableEq Individual}
variable {Society : Fintype Individual}

open Finset BigOperators Equiv

@[reducible]
def MonetaryValue : Type := ℝ

Redistribution

In a society people work, contributing to the community up to a magnitude typically defined by the law of supply and demand. Then the society redistributes the produced wealth (under the form of money in our model), minus its operating costs.

\(\mathbf{Definition}\)
Being given government spending \(gs \in \mathbb R\), a profile of contributions made by every individual \(c \in {\mathbb R}^I\), a redistribution function returns a retribution \(r \in {\mathbb R}^I\), which is the money given back to every individual, with the constraint of accounts at equilibrium: \(\sum_{i \in I} c(i) = gs + \sum_{i \in I} r(i)\).

	
		def total_value (dist : Individual -> MonetaryValue) : MonetaryValue :=
  ∑ i : Individual, dist i

def accounts_at_equilibirum (government_spending : MonetaryValue)
(redi : (Individual -> MonetaryValue) -> (Individual -> MonetaryValue)) :
Prop :=
  ∀ (dist : Individual -> MonetaryValue),
    @total_value Individual Society (redi dist) + government_spending =
    @total_value Individual Society dist

@[reducible]
def Redistribution (government_spending : MonetaryValue) : Type :=
  {
    redi : (Individual -> MonetaryValue) -> (Individual -> MonetaryValue) //
    @accounts_at_equilibirum Individual Society government_spending redi
  }

Capitalism and communism

Pure capitalism retributes every individual up to his contribution, minus its share in (potential) operating costs, provided everyone is taxed up to the same amount.

\(\mathbf{Definition}\)
Pure capitalism is the redistribution defined by \[\begin{align*} {\mathbb R}^I &\to {\mathbb R}^I\\ c &\mapsto c \end{align*}\] Pure capitalism with government spending \(gs \in \mathbb R\) is the redistribution defined by \[\begin{align*} {\mathbb R}^I &\to {\mathbb R}^I\\ c &\mapsto \left({i \in I} \mapsto c(i) - \frac {gs} N\right) \end{align*}\] Setting \(gs\) to \(0\) makes these two definitions coincide.

	
		def pure_capitalism :
(Individual -> MonetaryValue) -> (Individual -> MonetaryValue) :=
  id

noncomputable def pure_capitalism_costs_equally_divided
(government_spending : MonetaryValue) :
(Individual -> MonetaryValue) -> (Individual -> MonetaryValue) :=
  fun (cont : Individual -> MonetaryValue) => fun i =>
  cont i - government_spending / Fintype.card Individual

lemma pure_capitalism_costs_equally_divided_0 :
@pure_capitalism_costs_equally_divided Individual Society 0 =
@pure_capitalism Individual := by
  unfold pure_capitalism_costs_equally_divided pure_capitalism
  apply funext
  simp

lemma pure_capitalism_costs_equally_divided_at_equilibirum
(inh : Fintype.card Individual ≠ 0) (government_spending : MonetaryValue) :
@accounts_at_equilibirum Individual Society government_spending (
  @pure_capitalism_costs_equally_divided Individual Society government_spending
) := by
  unfold pure_capitalism_costs_equally_divided accounts_at_equilibirum
  intro dist
  unfold total_value
  simp
  rw [mul_comm]
  rw [division_def]
  rw [mul_assoc]
  rw [inv_mul_cancel₀]
  · simp
  · exact Nat.cast_ne_zero.mpr inh

noncomputable def pure_capitalism_costs_equally_divided_Redistribution
(inh : Fintype.card Individual ≠ 0) (government_spending : MonetaryValue) :
@Redistribution Individual Society government_spending :=
  ⟨ pure_capitalism_costs_equally_divided government_spending,
    pure_capitalism_costs_equally_divided_at_equilibirum inh government_spending ⟩

def pure_capitalism_Redistribution (inh : Fintype.card Individual ≠ 0) :
@Redistribution Individual Society 0 :=
  ⟨
    pure_capitalism,
    pure_capitalism_costs_equally_divided_0 ▸
    pure_capitalism_costs_equally_divided_at_equilibirum inh 0
  ⟩

Pure communism retributes every individual the same amount, regardless of its contribution.

\(\mathbf{Definition}\)
Pure communism is the redistribution defined by \[\begin{align*} {\mathbb R}^I &\to {\mathbb R}^I\\ c &\mapsto \left({i_0 \in I} \mapsto \frac {(\sum_{i \in I} c(i)) - gs} N\right) \end{align*}\]

	
		noncomputable def pure_communism (government_spending : MonetaryValue) :
(Individual -> MonetaryValue) -> (Individual -> MonetaryValue) :=
  fun (cont : Individual -> MonetaryValue) => fun _ =>
  (@total_value Individual Society cont - government_spending) /
  (Fintype.card Individual : MonetaryValue)

lemma pure_communism_at_equilibirum (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
@accounts_at_equilibirum Individual Society government_spending (
  @pure_communism Individual Society government_spending
) := by
  unfold pure_communism accounts_at_equilibirum total_value
  intro dist
  simp
  rw [mul_div_cancel_of_imp']
  · simp
  · intro emp
    exfalso
    apply inh
    exact Nat.cast_eq_zero.mp emp

noncomputable def pure_communism_Redistribution (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
@Redistribution Individual Society government_spending :=
  ⟨ pure_communism government_spending,
    pure_communism_at_equilibirum inh government_spending ⟩

Egalitarian redistribution

A redistribution is egalitarian if the retribution to every individual doesn’t depend on who the individual is. Everyone receives equal treatment.

\(\mathbf{Definition}\)
The redistribution \(r: {\mathbb R}^I \to {\mathbb R}^I\) is said egalitarian if \[\forall σ \in S_I, c \in {\mathbb R}^I, {r(c)}_σ = r(c_σ)\] (where \(S_I\) denotes the set of permutations on \(I\) and \(d_σ(i) = d(σ(i))\) \(\forall d \in {\mathbb R}^I, σ \in S_I\)).

	
		def is_egalitarian {government_spending : MonetaryValue}
(redi : @Redistribution Individual Society government_spending) :
Prop :=
  ∀ (σ : Perm Individual) (cont : Individual -> MonetaryValue),
    PermutationsActingOnFunctions (redi.val cont) σ =
    redi.val (PermutationsActingOnFunctions cont σ)

As in pure capitalisms everyone is retributed depending solely on its contribution, they are egalitarian.

\(\mathbf{Lemma}\)
Pure capitalisms are egalitarian.

\(\mathbf{proof:}\)
\(\forall σ \in S_I, c \in {\mathbb R}^I, {r(c)}_σ = i \mapsto r(c)(σ(i)) = i \mapsto c(σ(i)) - \frac {gs} N = i \mapsto r(c(σ(i))) = r(c_σ)\).
■

	
		lemma capitalism_is_egalitarian (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
@is_egalitarian Individual Society government_spending (
  pure_capitalism_costs_equally_divided_Redistribution inh government_spending
 ) := by
  tauto

Pure communism is unsurprisingly egalitarian as well.

\(\mathbf{Lemma}\)
Pure communism is egalitarian.

\(\mathbf{proof:}\)
\(\forall σ \in S_I, c \in {\mathbb R}^I, {r(c)}_σ = \frac {(\sum_{i \in I} c(i)) - gs} N = r(c_σ)\).
■

	
		lemma communism_is_egalitarian (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
@is_egalitarian Individual Society government_spending (
  pure_communism_Redistribution inh government_spending
) := by
  unfold is_egalitarian pure_communism_Redistribution
  simp
  unfold pure_communism PermutationsActingOnFunctions total_value
  intro σ cont
  apply funext
  intro ind
  refine (div_eq_div_iff ?_ ?_).mpr ?_
  · exact Nat.cast_ne_zero.mpr inh
  · exact Nat.cast_ne_zero.mpr inh
  · refine (mul_left_inj' ?_).mpr ?_
    · exact Nat.cast_ne_zero.mpr inh
    · simp
      rw [<- sum_reals_perm]
      tauto

Work incentive

An individual is encouraged to work if increasing its contribution increases its retribution as well.

\(\mathbf{Definition}\)
The redistribution \(r: {\mathbb R}^I \to {\mathbb R}^I\) is said to encourage the work if \[\forall c \in {\mathbb R}^I, i \in I, c' \in {\mathbb R} \text{ such that } c(i) < c', r(c)(i) < r(c_{i \leftarrow c'})(i)\] (where \(c_{i \leftarrow c'}\) denotes the profile of contributions \(c\) in which \(i\)’s contribution is replaced with \(c'\)).

	
		def encourages_work {government_spending : MonetaryValue}
(redi : @Redistribution Individual Society government_spending) :
Prop :=
  ∀ (cont : Individual -> MonetaryValue) (m : MonetaryValue)
  (i : Individual),
    cont i < m →
    redi.val cont i < redi.val (replace cont i m) i

Pure capitalisms encourage the work as increasing one’s contribution increases one’s retribution up to the same amount.

\(\mathbf{Lemma}\)
Pure capitalisms encourage the work.

\(\mathbf{proof:}\)
\(\forall c \in {\mathbb R}^I, i \in I, c' \in {\mathbb R} \text{ such that } c(i) < c', r(c)(i) = c(i) - \frac {gs} N < c' - \frac {gs} N = r(c_{i \leftarrow c'})(i)\).
■

	
		lemma capitalism_encourages_work (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
@encourages_work Individual eqInd Society government_spending (
  pure_capitalism_costs_equally_divided_Redistribution inh government_spending
 ) := by
  unfold encourages_work pure_capitalism_costs_equally_divided_Redistribution
  unfold pure_capitalism_costs_equally_divided
  intro cont m i ltim
  simp
  rewrite [replace_changes]
  exact ltim

Pure communism encourages the work but the reward is divided by the number of individuals.

\(\mathbf{Lemma}\)
Pure communism encourages the work.

\(\mathbf{proof:}\)
\(\forall c \in {\mathbb R}^I, i \in I, c' \in {\mathbb R} \text{ such that } c(i) < c', r(c)(i) = \frac {(\sum_{j \in I} c(j)) - gs} N < \frac {(\sum_{j \ne i \in I} c(j)) + c' - gs} N = r(c_{i \leftarrow c'})(i)\).
■

	
		lemma communism_encourages_work (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
@encourages_work Individual eqInd Society government_spending (
  pure_communism_Redistribution inh government_spending
) := by
  unfold encourages_work pure_communism_Redistribution
  intro cont m j ltjm
  simp
  unfold pure_communism total_value
  have inh' : 0 < ↑(Fintype.card Individual) := by
    exact Nat.zero_lt_of_ne_zero inh
  have smp :
      (∑ i, replace cont j m i) / ↑(Fintype.card Individual) * ↑(Fintype.card Individual) =
      ∑ i, replace cont j m i := by
    refine div_mul_cancel₀ (∑ i, replace cont j m i) ?_
    refine Ne.symm (ne_of_lt ?_)
    exact Nat.cast_pos'.mpr inh'
  refine (div_lt_div_iff_of_pos_right ?_).mpr ?_
  · exact Nat.cast_pos'.mpr inh'
  · simp
    rw [<- sub_pos]
    rw [<- sum_reals_sub]
    refine (sum_pos_iff_of_nonneg ?_).mpr ?_
    · intro i iu
      rcases eq : decide (i = j) with true|false
      · rw [replace_unchanges]
        · simp
        · exact Ne.symm (not_eq_of_beq_eq_false eq)
      · have eqij : i = j := by
          exact of_decide_eq_true eq
        rw [eqij]
        rw [replace_changes]
        have lejm : cont j <= m := by
          exact Std.le_of_lt ltjm
        exact sub_nonneg_of_le lejm
    · exists j
      simp
      rw [replace_changes]
      exact ltjm

The work incentive of an individual between two contributions is the difference between the corresponding retributions.

\(\mathbf{Definition}\)
Let \(r: {\mathbb R}^I \to {\mathbb R}^I\) be a redistribution.
Let \(i \in I\) be an individual.
Let \(q, q' \in {\mathbb R}\) be quantities (representing individual contributions) such that \(q \lt q'\).
Let \(c \in {\mathbb R}^I\) be a contribution profile.
The work incentive between contributions \(q\) and \(q'\) for \(i\) is defined as \[r(c_{i \leftarrow q'})(i) - r(c_{i \leftarrow q})(i)\]

	
		def work_incentive_between {c1 c2 : MonetaryValue} {government_spending : MonetaryValue}
(redi : @Redistribution Individual Society government_spending) (i : Individual)
(cont : Individual -> MonetaryValue) :
MonetaryValue :=
  redi.val (replace cont i c2) i - redi.val (replace cont i c1) i

\(\mathbf{Definition}\)
Let \(r: {\mathbb R}^I \to {\mathbb R}^I\) be a redistribution.
Let \(i \in I\) be an individual.
Let \(q \in {\mathbb R}\) be a quantity (representing an individual contribution).
Let \(c \in {\mathbb R}^I\) be a contribution profile.
The instantaneous work incentive at contribution \(q\) for \(i\) is defined as \[\frac {\mathrm{d} r(c_{i \leftarrow q})(i)} {\mathrm{d} q}\] It may not exist, in case the function is not differentiable.

	
		def retribution_function {government_spending : MonetaryValue}
(redi : @Redistribution Individual Society government_spending)
(i : Individual) (cont : Individual -> MonetaryValue) :
MonetaryValue -> MonetaryValue :=
  fun c => redi.val (replace cont i c) i

@[reducible]
noncomputable def instantaneous_work_incentive {government_spending : MonetaryValue}
(i : Individual) (c0 : MonetaryValue)
(redi : @Redistribution Individual Society government_spending)
(cont : Individual -> MonetaryValue) :
MonetaryValue :=
  deriv (
    @retribution_function Individual eqInd Society government_spending redi i cont
  ) c0

In pure capitalisms the work incentive between two contributions is just the difference between them.

\(\mathbf{Lemma}\)
In pure capitalisms the work incentive between contributions \(q\) and \(q'\) for whatever individual is \(q' - q\).

\(\mathbf{proof:}\)
\((q' - \frac {gs} N) - (q - \frac {gs} N) = q' - q\).
■

	
		lemma work_incentive_capitalism_between (government_spending : MonetaryValue)
(i : Individual) (c c' : MonetaryValue) (cont : Individual -> MonetaryValue) :
(
  @work_incentive_between Individual eqInd Society c c' government_spending
  (pure_capitalism_costs_equally_divided_Redistribution (
    inhabited_implies_nonnull_card i
  ) government_spending) i cont
) = c' - c := by
  unfold pure_capitalism_costs_equally_divided_Redistribution
  unfold work_incentive_between pure_capitalism_costs_equally_divided
  simp
  rw [replace_changes]
  rw [replace_changes]

\(\mathbf{Lemma}\)
In pure capitalisms the instantaneous work incentive is the function constant at \(1\).

\(\mathbf{proof:}\)
\(\frac {\mathrm{d} r(c_{i \leftarrow q})(i)} {\mathrm{d} q} = \frac {\mathrm{d} (q - \frac {gs} N)} {\mathrm{d} q} = 1\).
■

	
		lemma instantaneous_work_incentive_capitalism {government_spending : MonetaryValue}
(i : Individual) (c0 : MonetaryValue) (cont : Individual -> MonetaryValue) :
@instantaneous_work_incentive Individual eqInd Society government_spending i c0 (
  pure_capitalism_costs_equally_divided_Redistribution (
    inhabited_implies_nonnull_card i
  ) government_spending
) cont = 1 := by
  unfold pure_capitalism_costs_equally_divided_Redistribution
  unfold instantaneous_work_incentive pure_capitalism_costs_equally_divided
  unfold retribution_function replace
  simp

In pure communism the work incentive between two contributions is the difference between them divided by the number of individuals (the benefit of the extra work provided is split among individuals).

\(\mathbf{Lemma}\)
In pure communism the work incentive between contributions \(q\) and \(q'\) for whatever individual is \(\frac {q' - q} N\).

\(\mathbf{proof:}\)
\(r(c_{i \leftarrow q'})(i) - r(c_{i \leftarrow q})(i)\)
\(= \frac {q' + (\sum_{j \ne i \in I} c(j)) - gs} N - \frac {q + (\sum_{j \ne i \in I} c(j)) - gs} N\)
\(= \frac {(q' + (\sum_{j \ne i \in I} c(j)) - gs) - (q + (\sum_{j \ne i \in I} c(j)) - gs)} N\)
\(= \frac {q' - q} N\)
■

	
		lemma work_incentive_communism_between (government_spending : MonetaryValue)
(i : Individual) (c c' : MonetaryValue) (cont : Individual -> MonetaryValue) :
(
  @work_incentive_between Individual eqInd Society c c' government_spending
  (pure_communism_Redistribution (
    inhabited_implies_nonnull_card i
  ) government_spending) i cont
) = (c' - c) / Fintype.card Individual := by
  unfold pure_communism_Redistribution work_incentive_between
  simp
  unfold pure_communism total_value
  have inh : Fintype.card Individual ≠ 0 := by
    apply inhabited_implies_nonnull_card
    exact i
  have divdist :
      (∑ i_1, replace cont i c' i_1 - government_spending) / ↑(Fintype.card Individual) -
      (∑ i_1, replace cont i c i_1 - government_spending) / ↑(Fintype.card Individual) =
      (∑ i_1, replace cont i c' i_1 - ∑ i_1, replace cont i c i_1) /
      ↑(Fintype.card Individual) := by
    rw [sub_div]
    rw [sub_div]
    simp
    exact
      div_sub_div_same (∑ i_1, replace cont i c' i_1) (∑ i_1, replace cont i c i_1)
      ↑(Fintype.card Individual)
  rw [divdist]
  refine (div_left_inj' ?_).mpr ?_
  · exact Nat.cast_ne_zero.mpr inh
  · rw [<- sum_reals_sub]
    have smc :
        (fun j => replace cont i c' j - replace cont i c j) =
        (fun j => if j = i then c' - c else 0) := by
      apply funext
      intro j
      rcases eq : decide (j = i) with true|false
      · rw [replace_unchanges]
        · rw [replace_unchanges]
          · simp
            intro eqij
            rw [eqij] at eq
            simp at eq
          · exact Ne.symm (not_eq_of_beq_eq_false eq)
        · exact Ne.symm (not_eq_of_beq_eq_false eq)
      · have eqij : j = i := by
          exact of_decide_eq_true eq
        rw [eqij]
        rw [replace_changes]
        rw [replace_changes]
        simp
    have eqsum :
        ∑ i_1, (replace cont i c' i_1 - replace cont i c i_1) =
        ∑ i_1, if i_1 = i then c' - c else 0 := by
      exact
        Fintype.sum_congr (fun a ↦ replace cont i c' a - replace cont i c a)
          (fun a ↦ if a = i then c' - c else 0) (congrFun smc)
    rw [eqsum]
    exact Fintype.sum_ite_eq' i fun j ↦ c' - c

\(\mathbf{Lemma}\)
In pure communism the instantaneous work incentive is the function constant at \(\frac 1 N\).

\(\mathbf{proof:}\)
\(\frac {\mathrm{d} r(c_{i \leftarrow q})(i)} {\mathrm{d} q} = \frac {\mathrm{d} (\frac {q + (\sum_{j \ne i \in I} c(j)) - gs} N)} {\mathrm{d} q} = \frac 1 N\).
■

	
		lemma instantaneous_work_incentive_communism {government_spending : MonetaryValue}
{i : Individual} {c0 : MonetaryValue} {cont : Individual -> MonetaryValue}
(_ : DifferentiableAt ℝ (
  @retribution_function Individual eqInd Society government_spending (
    pure_communism_Redistribution (
      inhabited_implies_nonnull_card i
    ) government_spending
  ) i cont
) c0) :
@instantaneous_work_incentive Individual eqInd Society government_spending i c0 (
  pure_communism_Redistribution (
    inhabited_implies_nonnull_card i
  ) government_spending
) cont = 1  / Fintype.card Individual := by
  unfold pure_communism_Redistribution instantaneous_work_incentive pure_communism
  unfold retribution_function replace total_value
  simp
  have distr : (
    deriv (fun c ↦ (∑ x, if x = i then c else cont x) / ↑(Fintype.card Individual)) c0 =
    deriv (fun c ↦ (∑ x, if x = i then c else cont x)) c0 / ↑(Fintype.card Individual)
  ) := by
    simpa [div_eq_mul_inv] using (
      deriv_const_mul
      ((Fintype.card Individual : ℝ)⁻¹)
      (fun c ↦ ∑ x, if x = i then c else cont x)
      c0
    ).symm
  rw [<- distr]
  have derd : (
    deriv (fun c ↦ (∑ x, if x = i then c else cont x) / ↑(Fintype.card Individual)) c0 =
    deriv (fun c ↦ (∑ x, if x = i then c else cont x)) c0  / ↑(Fintype.card Individual)
  ) := by
    simpa using (
      deriv_const_div
      (fun c ↦ ∑ x, if x = i then c else cont x)
      (↑(Fintype.card Individual))
      c0
    )
  rw [derd]
  have sumf : (
    (fun c ↦ ∑ x, if x = i then c else cont x) =
    ∑ x, (fun c ↦ if x = i then c else cont x)
  ) := by
    exact Eq.symm (sum_fn univ fun c c_1 ↦ if c = i then c_1 else cont c)
  rw [sumf]
  rw [deriv_sum]
  rotate_left
  · intro j ju
    rcases eq : decide (j = i) with true|false
    · have casne : (fun c ↦ if j = i then c else cont j) = fun c => cont j := by
        apply funext
        intro mv
        refine ite_cond_eq_false mv (cont j) ?_
        exact eq_false_of_decide eq
      rw [casne]
      simp
    · have eqij : j = i := by
        exact of_decide_eq_true eq
      rw [eqij]
      simp
  · rw [div_eq_mul_inv]
    have inh : Fintype.card Individual ≠ 0 := by
      exact inhabited_implies_nonnull_card i
    refine (mul_inv_eq_iff_eq_mul₀ ?_).mpr ?_
    · exact Nat.cast_ne_zero.mpr inh
    · have mul1 : (
        (@Nat.cast MonetaryValue Real.instNatCast (Fintype.card Individual))⁻¹ *
        @Nat.cast MonetaryValue Real.instNatCast (Fintype.card Individual) = 1
      ) := by
        refine inv_mul_cancel₀ ?_
        exact Nat.cast_ne_zero.mpr inh
      rw [mul1]
      have all0 : (
        ∀ (j : Individual), j ≠ i →
        deriv (fun c ↦ if j = i then c else cont j) c0 = 0
      ) := by
        intro j neij
        have casne : (fun c ↦ if j = i then c else cont j) = fun c => cont j := by
          apply funext
          intro mv
          refine ite_cond_eq_false mv (cont j) ?_
          exact eq_false neij
        rw [casne]
        simp
      rw [Fintype.sum_eq_single i all0]
      simp

Currency change

A currency change is just the multiplication of all amounts by a multiplier. This happened for example to countries having joined the euro area.

\(\mathbf{Definition}\)
Subject to a currency change of multiplier \(k \gt 0\), a redistribution \(r: {\mathbb R}^I \to {\mathbb R}^I\) beconmes: \[\begin{align*} {\mathbb R}^I &\to {\mathbb R}^I\\ c &\mapsto k \times r(\frac c k) \end{align*}\]

	
		def currency_change {k : MonetaryValue} (_ : 0 < k)  (mv : MonetaryValue) :
MonetaryValue :=
  mv * k

noncomputable def currency_change_inverse {k : MonetaryValue} (_ : 0 < k)
(mv : MonetaryValue) :
MonetaryValue :=
  mv / k

lemma inverse_currency_change {k : MonetaryValue} (pos : 0 < k) :
Inverse (@currency_change k pos) (@currency_change_inverse k pos) := by
  unfold currency_change currency_change_inverse Inverse
  apply And.intro
  · intro x
    simp
    field_simp
  · intro x
    simp
    field_simp

def currency_change_distribution {k : MonetaryValue} (pos : 0 < k)
(dist : Individual -> MonetaryValue) :
Individual -> MonetaryValue :=
  fun i => currency_change pos (dist i)

noncomputable def currency_change_distribution_inverse {k : MonetaryValue}
(pos : 0 < k) (dist : Individual -> MonetaryValue) :
Individual -> MonetaryValue :=
  fun i => currency_change_inverse pos (dist i)

lemma inverse_currency_change_distribution {k : MonetaryValue} (pos : 0 < k) :
Inverse (@currency_change_distribution Individual k pos) (
  currency_change_distribution_inverse pos
) := by
  unfold currency_change_distribution currency_change_distribution_inverse Inverse
  apply And.intro
  · intro dist
    simp
    apply funext
    intro i
    rw [(inverse_currency_change pos).left]
  · intro dist
    simp
    apply funext
    intro i
    rw [(inverse_currency_change pos).right]

noncomputable def currency_change_redistribution {k : MonetaryValue} (pos : 0 < k)
(redi : (Individual -> MonetaryValue) -> (Individual -> MonetaryValue)) :
(Individual -> MonetaryValue) -> (Individual -> MonetaryValue) :=
  fun cont => currency_change_distribution pos (redi (
    currency_change_distribution_inverse pos cont
  ))

lemma currency_change_at_equilibrium {k : MonetaryValue}
{government_spending : MonetaryValue}
{redi : (Individual -> MonetaryValue) -> (Individual -> MonetaryValue)}
(pos : 0 < k)
(equi : @accounts_at_equilibirum Individual Society government_spending redi) :
@accounts_at_equilibirum Individual Society (government_spending * k) (
  currency_change_redistribution pos redi
) := by
  unfold accounts_at_equilibirum currency_change_redistribution
  intro dist
  unfold total_value currency_change_distribution
  unfold currency_change currency_change_distribution_inverse
  have distr : (
    ∑ i, (redi (fun i ↦ currency_change_inverse pos (dist i)) i * k) =
    (∑ i, redi (fun i ↦ currency_change_inverse pos (dist i)) i) * k
  ) := by
    exact Eq.symm (sum_mul univ (redi fun i ↦ currency_change_inverse pos (dist i)) k)
  rw [distr]
  unfold currency_change_inverse
  unfold accounts_at_equilibirum at equi
  specialize (equi (currency_change_distribution_inverse pos dist))
  unfold total_value currency_change_distribution_inverse at equi
  unfold currency_change_inverse at equi
  have mulk :(
    (∑ i, redi (fun i ↦ dist i / k) i + government_spending) * k =
    (∑ i, dist i / k) * k
  ) := by
    exact (mul_right_cancel_iff_of_pos pos).mpr equi
  rw [add_mul] at mulk
  rw [mulk]
  rw [mul_comm]
  rw [Finset.mul_sum]
  refine Eq.symm (Fintype.sum_congr dist (fun a ↦ k * (dist a / k)) ?_)
  intro i
  rw [mul_comm]
  rw [division_def]
  rw [mul_assoc]
  have invk : k⁻¹ * k = 1 := by
    refine inv_mul_cancel₀ ?_
    exact Ne.symm (Std.ne_of_lt pos)
  rw [invk]
  simp

noncomputable def change_currency_Redistribution {k : MonetaryValue}
{government_spending : MonetaryValue}
(redi : @Redistribution Individual Society government_spending)
(pos : 0 < k) :
@Redistribution Individual Society (government_spending * k) :=
  ⟨ currency_change_redistribution pos redi,
    currency_change_at_equilibrium pos redi.property ⟩

Fairness

A fair redistribution will retribute more to an individual who contributes more. Pure capitalisms are oviously fair. For pure communism, it is not so as everyone earns the same whatever the work done.

\(\mathbf{Definition}\)
The redistribution \(r: {\mathbb R}^I \to {\mathbb R}^I\) is said fair if \(\forall c \in {\mathbb R}^I, i, j \in I, c(i) \le c(j) \Rightarrow r(i) \le r(j)\) And it is said strictly fair if \(\forall c \in {\mathbb R}^I, i, j \in I, c(i) \lt c(j) \Rightarrow r(i) \lt r(j)\)

	
		def is_fair {government_spending : MonetaryValue}
(redi : @Redistribution Individual Society government_spending) :
Prop :=
  ∀ (cont : Individual -> MonetaryValue) (i j : Individual),
    cont i <= cont j ->
    redi.val cont i <= redi.val cont j

def is_strictly_fair {government_spending : MonetaryValue}
(redi : @Redistribution Individual Society government_spending) :
Prop :=
  ∀ (cont : Individual -> MonetaryValue) (i j : Individual),
    cont i < cont j ->
    redi.val cont i < redi.val cont j

\(\mathbf{Lemma}\)
Pure capitalisms are fair and strictly fair.

\(\mathbf{proof:}\)
As \(r(i) = c(i) - \frac {gs} N\), the two implications are obvious.
■

	
		lemma capitalism_is_fair (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
@is_fair Individual Society government_spending (
  pure_capitalism_costs_equally_divided_Redistribution inh government_spending
) := by
  unfold is_fair pure_capitalism_costs_equally_divided_Redistribution
  intro cont i j
  simp
  unfold pure_capitalism_costs_equally_divided
  intro conc
  exact tsub_le_tsub_right conc (government_spending / ↑(Fintype.card Individual))

lemma capitalism_is_strictly_fair (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
@is_strictly_fair Individual Society government_spending (
  pure_capitalism_costs_equally_divided_Redistribution inh government_spending
) := by
  unfold is_strictly_fair pure_capitalism_costs_equally_divided_Redistribution
  intro cont i j
  simp
  unfold pure_capitalism_costs_equally_divided
  intro conc
  exact sub_lt_sub_right conc (government_spending / ↑(Fintype.card Individual))

\(\mathbf{Lemma}\)
Pure communism is fair but not strictly fair (if there are at least two individuals).

\(\mathbf{proof:}\)
\(\forall i, j \in I, r(i) = r(j)\) which makes the first implication true.
But it is not true that \(r(i) \lt r(j)\) when \(c(i) \lt c(j)\).
■

	
		lemma communism_is_fair (inh : Fintype.card Individual ≠ 0)
(government_spending : MonetaryValue) :
is_fair (pure_communism_Redistribution inh government_spending) := by
  unfold is_fair pure_communism_Redistribution
  intro cont i j
  simp
  unfold pure_communism
  intro leij
  simp

lemma communism_not_strictly_fair {i j : Individual} [DecidableEq Individual]
(government_spending : MonetaryValue) (neij : j ≠ i) :
¬ @is_strictly_fair Individual Society government_spending (
  pure_communism_Redistribution (inhabited_implies_nonnull_card i) government_spending
) := by
  unfold is_strictly_fair pure_communism_Redistribution
  intro sf
  specialize (sf (fun i_1 : Individual => if i_1 = i then (1 : ℝ) else (0 : ℝ)) j i)
  have eqii : (if i = i then (1 : ℝ) else 0) = 1 := by
    exact if_pos rfl
  rw [eqii] at sf
  have ji10 : (if j = i then (1 : ℝ) else 0) = 0 := by
    exact if_neg neij
  rw [ji10] at sf
  simp at sf
  unfold pure_communism at sf
  simp at sf
The proofs' code is currently in . To switch to , click on the following icon:
You can contribute via github
Contact: webmaster@leibnizproject.com