Documentation

Lean 4 Proof

def surplusLoss (ρ H : ℝ) (J : ℕ) : ℝ := (1 - ρ) * (H - 1 / J)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Inequality.lean:45

Module Section

CES Inequality Decomposition

In the same file