Documentation

Lean 4 Proof

def incomeRatio (a_i a_j x_i x_j ρ : ℝ) : ℝ :=
  (a_i / a_j) * (x_i / x_j) ^ ρ

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Inequality.lean:38

Module Section

CES Inequality Decomposition

In the same file