Documentation

Lean 4 Proof

theorem substitutability_dampens_inequality {ρ r : ℝ}
    (hρ_lt : ρ < 1) (hr : 1 < r) :
    r ^ ρ < r := by
  conv_rhs => rw [← rpow_one r]
  exact rpow_lt_rpow_of_exponent_lt (by linarith) hρ_lt

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:86

Module Section

CES Inequality Decomposition

In the same file