Documentation

Lean 4 Proof

theorem lower_rho_compresses_shares {ρ₁ ρ₂ : ℝ} {r : ℝ}
    (h12 : ρ₁ < ρ₂) (hr : 1 < r) :
    r ^ ρ₁ < r ^ ρ₂ :=
  rpow_lt_rpow_of_exponent_lt (by linarith) h12

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:332

Module Section

## CES Inequality Measures

In the same file