Documentation

Lean 4 Proof

theorem complements_favor_scarce {ρ r : ℝ}
    (hρ : ρ < 0) (hr : 1 < r) :
    r ^ ρ < 1 := by
  rw [← rpow_zero r]
  exact rpow_lt_rpow_of_exponent_lt (by linarith) hρ

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:102

Module Section

CES Inequality Decomposition

In the same file