Documentation

Lean 4 Proof

theorem powerMean_isoquant_strong_concavity_weighted (J : ℕ) (hJ : 2 ≤ J)
    (ρ : ℝ) (hρ : ρ < 1) (hρ0 : 0 < ρ)
    (x' y' : Fin J → ℝ) (hx' : ∀ j, 0 < x' j) (hy' : ∀ j, 0 < y' j)
    (hFx : powerMean J ρ (ne_of_gt hρ0) x' = 1)
    (hFy : powerMean J ρ (ne_of_gt hρ0) y' = 1)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1)
    (hmix : ∀ j, 0 < t * x' j + (1 - t) * y' j) :
    powerMean J ρ (ne_of_gt hρ0) (fun j => t * x' j + (1 - t) * y' j) - 1 ≥
      (1 - ρ) / (2 * ↑J) * t * (1 - t) *
        weightedIsoquantDistSq J ρ x' y' := by
  set hρne := ne_of_gt hρ0
  set mix := fun j => t * x' j + (1 - t) * y' j with hmix_def
  have hJpos : (0 : ℝ) < (↑J : ℝ) := Nat.cast_pos.mpr (by omega)
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  -- Extract inner sums from isoquant conditions
  -- powerMean = ((1/J) * Σ x'^ρ)^{1/ρ} = 1 means (1/J) * Σ x'^ρ = 1
  have hsum_x_pos : 0 < (1 : ℝ) / ↑J * ∑ j : Fin J, (x' j) ^ ρ := by
    apply mul_pos (div_pos one_pos hJpos)
    exact Finset.sum_pos (fun j _ => rpow_pos_of_pos (hx' j) ρ)
      ⟨⟨0, by omega⟩, Finset.mem_univ _⟩
  -- If z > 0 and z^{1/ρ} = 1, then z = (z^{1/ρ})^ρ = 1^ρ = 1
  have rpow_eq_one_iff {z : ℝ} (hz : 0 < z) (h : z ^ (1 / ρ) = 1) : z = 1 := by
    have := congr_arg (· ^ ρ) h
    simp only [one_rpow] at this
    rwa [← rpow_mul hz.le, one_div, inv_mul_cancel₀ hρne, rpow_one] at this
  have hFx_inner : (1 : ℝ) / ↑J * ∑ j : Fin J, (x' j) ^ ρ = 1 := by
    have h := hFx; simp only [powerMean] at h
    exact rpow_eq_one_iff hsum_x_pos h
  have hsum_y_pos : 0 < (1 : ℝ) / ↑J * ∑ j : Fin J, (y' j) ^ ρ := by
    apply mul_pos (div_pos one_pos hJpos)
    exact Finset.sum_pos (fun j _ => rpow_pos_of_pos (hy' j) ρ)
      ⟨⟨0, by omega⟩, Finset.mem_univ _⟩
  have hFy_inner : (1 : ℝ) / ↑J * ∑ j : Fin J, (y' j) ^ ρ = 1 := by
    have h := hFy; simp only [powerMean] at h
    exact rpow_eq_one_iff hsum_y_pos h
  -- S = (1/J)Σ (mix_j)^ρ
  set S := (1 : ℝ) / ↑J * ∑ j : Fin J, (mix j) ^ ρ with hS_def
  -- F(mix) = S^{1/ρ}
  have hFmix : powerMean J ρ hρne mix = S ^ (1 / ρ) := by
    simp only [powerMean, hS_def, hmix_def]
  -- Each component gives a concavity deficit via rpow_concavity_deficit
  have hcomp : ∀ j : Fin J,
      (mix j) ^ ρ - t * (x' j) ^ ρ - (1 - t) * (y' j) ^ ρ ≥
      ρ * (1 - ρ) / 2 * max (x' j) (y' j) ^ (ρ - 2) * t * (1 - t) *
        (x' j - y' j) ^ 2 :=
    fun j => rpow_concavity_deficit ρ (x' j) (y' j) t hρ0 hρ (hx' j) (hy' j) ht0 ht1
  -- Sum over components
  have hsum_deficit :
      (∑ j : Fin J, (mix j) ^ ρ) - t * (∑ j : Fin J, (x' j) ^ ρ) -
        (1 - t) * (∑ j : Fin J, (y' j) ^ ρ) ≥
      ρ * (1 - ρ) / 2 * t * (1 - t) *
        ∑ j : Fin J, max (x' j) (y' j) ^ (ρ - 2) * (x' j - y' j) ^ 2 := by
    have h1 : (∑ j : Fin J, (mix j) ^ ρ) - t * ∑ j : Fin J, (x' j) ^ ρ -
        (1 - t) * ∑ j : Fin J, (y' j) ^ ρ =
        ∑ j : Fin J, ((mix j) ^ ρ - t * (x' j) ^ ρ - (1 - t) * (y' j) ^ ρ) := by
      simp [Finset.mul_sum, ← Finset.sum_sub_distrib]
    have h2 : ρ * (1 - ρ) / 2 * t * (1 - t) *
        ∑ j : Fin J, max (x' j) (y' j) ^ (ρ - 2) * (x' j - y' j) ^ 2 =
        ∑ j : Fin J, (ρ * (1 - ρ) / 2 * max (x' j) (y' j) ^ (ρ - 2) * t * (1 - t) *
          (x' j - y' j) ^ 2) := by
      simp [Finset.mul_sum]; congr 1; ext j; ring
    rw [h1, h2]
    exact Finset.sum_le_sum fun j _ => hcomp j
  -- S - 1 ≥ (ρ(1-ρ)/(2J)) · t(1-t) · wdist
  have hS_deficit :
      S - 1 ≥ ρ * (1 - ρ) / (2 * ↑J) * t * (1 - t) *
        weightedIsoquantDistSq J ρ x' y' := by
    simp only [weightedIsoquantDistSq, hS_def]
    -- S - 1 = (1/J)(Σ mix^ρ - t·Σx'^ρ - (1-t)·Σy'^ρ)
    set wsum := ∑ j : Fin J, max (x' j) (y' j) ^ (ρ - 2) * (x' j - y' j) ^ 2
    have h_invJ : (0 : ℝ) < 1 / ↑J := div_pos one_pos hJpos
    -- Express 1 in terms of the sums
    have h_lhs : 1 / ↑J * ∑ j : Fin J, (mix j) ^ ρ - 1 =
        1 / ↑J * ((∑ j : Fin J, (mix j) ^ ρ) - t * ∑ j : Fin J, (x' j) ^ ρ -
          (1 - t) * ∑ j : Fin J, (y' j) ^ ρ) := by
      nlinarith [hFx_inner, hFy_inner]
    have h_rhs : ρ * (1 - ρ) / (2 * ↑J) * t * (1 - t) * wsum =
        1 / ↑J * (ρ * (1 - ρ) / 2 * t * (1 - t) * wsum) := by
      field_simp
    rw [h_lhs, h_rhs]
    exact mul_le_mul_of_nonneg_left hsum_deficit h_invJ.le
  -- S ≥ 1
  have wdist_nn : 0 ≤ weightedIsoquantDistSq J ρ x' y' := by
    apply Finset.sum_nonneg; intro j _
    exact mul_nonneg (rpow_nonneg (le_max_of_le_left (hx' j).le) _) (sq_nonneg _)
  have hS_ge1 : 1 ≤ S := by
    have h1 : (0 : ℝ) ≤ ρ * (1 - ρ) / (2 * ↑J) := by
      apply div_nonneg (mul_nonneg hρ0.le (by linarith : 0 ≤ 1 - ρ))
      exact mul_nonneg two_pos.le hJpos.le
    nlinarith [mul_nonneg h1 (mul_nonneg (mul_nonneg ht0 (by linarith : 0 ≤ 1 - t)) wdist_nn)]
  -- S^{1/ρ} - 1 ≥ (1/ρ)(S-1) by Bernoulli
  have hBern : S ^ (1 / ρ) ≥ 1 + 1 / ρ * (S - 1) :=
    bernoulli_rpow_ge_linear hρ0 hρ hS_ge1
  -- Chain the bounds
  rw [hFmix]
  calc S ^ (1 / ρ) - 1
      ≥ 1 / ρ * (S - 1) := by linarith
    _ ≥ 1 / ρ * (ρ * (1 - ρ) / (2 * ↑J) * t * (1 - t) *
        weightedIsoquantDistSq J ρ x' y') := by
        exact mul_le_mul_of_nonneg_left hS_deficit (by positivity : (0 : ℝ) ≤ 1 / ρ)
    _ = (1 - ρ) / (2 * ↑J) * t * (1 - t) *
        weightedIsoquantDistSq J ρ x' y' := by
      field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:308

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file