Documentation

Lean 4 Proof

theorem powerMean_mono {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₂ : 0 < ρ₂)
    (hle : ρ₁ ≤ ρ₂) (hρ₁ne : ρ₁ ≠ 0) (hρ₂ne : ρ₂ ≠ 0)
    {x : Fin J → ℝ} (hx : ∀ j, 0 < x j)
    (hJ : 0 < J) :
    powerMean J ρ₁ hρ₁ne x ≤ powerMean J ρ₂ hρ₂ne x := by
  rcases eq_or_lt_of_le hle with heq | hlt
  · subst heq; exact le_refl _
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJr
  -- Weights w_i = 1/J summing to 1
  set w : Fin J → ℝ := fun _ => (1 : ℝ) / ↑J with hw_def
  have hw_nn : ∀ i ∈ Finset.univ, 0 ≤ w i := fun _ _ => by positivity
  have hw_sum : ∑ i ∈ Finset.univ, w i = 1 := by
    simp [w, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    exact div_self hJne
  have hp : 1 ≤ ρ₂ / ρ₁ := by rwa [le_div_iff₀ hρ₁, one_mul]
  -- Apply arith_mean_le_rpow_mean with z_i = x_i^{rho1}, p = rho2/rho1
  have step := Real.arith_mean_le_rpow_mean Finset.univ w (fun j => (x j) ^ ρ₁)
    hw_nn hw_sum (fun i _ => rpow_nonneg (le_of_lt (hx i)) ρ₁) hp
  -- Simplify (x_i^{rho1})^{rho2/rho1} = x_i^{rho2}
  have hrw : ∀ j ∈ Finset.univ, w j * ((x j) ^ ρ₁) ^ (ρ₂ / ρ₁) = w j * (x j) ^ ρ₂ := by
    intro j _; congr 1
    rw [← rpow_mul (le_of_lt (hx j)), mul_div_cancel₀ ρ₂ (ne_of_gt hρ₁)]
  rw [Finset.sum_congr rfl hrw] at step
  -- Simplify 1/(rho2/rho1) = rho1/rho2
  have h_inv : (1 : ℝ) / (ρ₂ / ρ₁) = ρ₁ / ρ₂ := by field_simp
  rw [h_inv] at step
  -- step : (1/J) Sum x_i^{rho1} le ((1/J) Sum x_i^{rho2})^{rho1/rho2}
  -- Convert weighted sums to (1/J) * Sum form
  have hw_rw : ∀ (ρ : ℝ), ∑ i ∈ Finset.univ, w i * (x i) ^ ρ =
      (1 / ↑J) * ∑ i : Fin J, (x i) ^ ρ := by
    intro ρ; simp [w, Finset.mul_sum]
  rw [hw_rw ρ₁, hw_rw ρ₂] at step
  -- Raise to 1/rho1: A^{1/rho1} le (B^{rho1/rho2})^{1/rho1} = B^{1/rho2}
  simp only [powerMean]
  have h1ρ₁ : (0 : ℝ) < 1 / ρ₁ := div_pos one_pos hρ₁
  have hA_nn : 0 ≤ (1 / ↑J) * ∑ i : Fin J, (x i) ^ ρ₁ :=
    mul_nonneg (div_nonneg one_pos.le (Nat.cast_nonneg J))
      (Finset.sum_nonneg (fun j _ => rpow_nonneg (le_of_lt (hx j)) ρ₁))
  have hB_nn : 0 ≤ (1 / ↑J) * ∑ i : Fin J, (x i) ^ ρ₂ :=
    mul_nonneg (div_nonneg one_pos.le (Nat.cast_nonneg J))
      (Finset.sum_nonneg (fun j _ => rpow_nonneg (le_of_lt (hx j)) ρ₂))
  -- From step and rpow_le_rpow: A^{1/rho1} le (B^{rho1/rho2})^{1/rho1}
  have key := rpow_le_rpow hA_nn step (le_of_lt h1ρ₁)
  -- Simplify RHS: (B^{rho1/rho2})^{1/rho1} = B^{(rho1/rho2)*(1/rho1)} = B^{1/rho2}
  rw [← rpow_mul hB_nn] at key
  have hexp : ρ₁ / ρ₂ * (1 / ρ₁) = 1 / ρ₂ := by field_simp
  rwa [hexp] at key

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:436

Module Section

Economics extensions for CES formalization:

In the same file