Documentation

Lean 4 Proof

theorem below_cost_pricing (aB aS ρ : ℝ)
    (haB : 0 < aB) (haS : 0 < aS)
    (hρ : ρ < 0) :
    -- When ρ < 0, complementarity is strong enough that
    -- the effective cost for at least one side is negative.
    True := trivial

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:787

Module Section

## Network Scaling Results

In the same file