Documentation

Lean 4 Proof

theorem income_ratio_from_ces {a_i a_j x_i x_j ρ : ℝ} :
    incomeRatio a_i a_j x_i x_j ρ = (a_i / a_j) * (x_i / x_j) ^ ρ := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:70

Module Section

CES Inequality Decomposition

In the same file