Documentation

Lean 4 Proof

theorem jensen_ces_concave {ρ : ℝ} (hρ₀ : 0 < ρ) (hρ₁ : ρ ≤ 1)
    {x : Fin J → ℝ} (hx : ∀ j, 0 ≤ x j) (hJ : 0 < J) :
    (1 / ↑J : ℝ) * ∑ j : Fin J, (x j) ^ ρ ≤
    ((1 / ↑J : ℝ) * ∑ j : Fin J, x j) ^ ρ := by
  have hconc := Real.concaveOn_rpow (le_of_lt hρ₀) hρ₁
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJr
  set w : Fin J → ℝ := fun _ => (1 : ℝ) / ↑J
  have hw_nn : ∀ j ∈ Finset.univ, 0 ≤ w j := fun _ _ => by positivity
  have hw_sum : ∑ j ∈ Finset.univ, w j = 1 := by
    simp [w, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    exact div_self hJne
  have hx_mem : ∀ j ∈ Finset.univ, x j ∈ Set.Ici (0 : ℝ) := fun j _ => Set.mem_Ici.mpr (hx j)
  have step := ConcaveOn.le_map_sum hconc hw_nn hw_sum hx_mem
  simp only [smul_eq_mul, w] at step
  rwa [← Finset.mul_sum, ← Finset.mul_sum] at step

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:545

Module Section

Economics extensions for CES formalization:

In the same file