Documentation

Lean 4 Proof

theorem surplus_loss_nonneg {ρ H : ℝ} {J : ℕ} (hρ : ρ < 1) (hH : 1 / (J : ℝ) ≤ H) :
    0 ≤ surplusLoss ρ H J := by
  simp only [surplusLoss]
  exact mul_nonneg (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:56

Module Section

CES Inequality Decomposition

In the same file