Documentation

Lean 4 Proof

theorem jensen_gap_nonneg {ρ : ℝ} (hρ₀ : 0 < ρ) (hρ₁ : ρ ≤ 1)
    {x : Fin J → ℝ} (hx : ∀ j, 0 ≤ x j) (hJ : 0 < J) :
    0 ≤ ((1 / ↑J : ℝ) * ∑ j : Fin J, x j) ^ ρ -
        (1 / ↑J : ℝ) * ∑ j : Fin J, (x j) ^ ρ := by
  linarith [jensen_ces_concave hρ₀ hρ₁ hx hJ]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:564

Module Section

Economics extensions for CES formalization:

In the same file