Documentation

Lean 4 Proof

theorem scale_scope_complementarity {γ ρ : ℝ} (hγ : 1 < γ) (hρ : ρ < 1) :
    0 < scaleScopeCrossPartialSign γ ρ := by
  simp only [scaleScopeCrossPartialSign]
  apply mul_pos
  · apply mul_pos <;> linarith
  · linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/IRS.lean:120

Module Section

Increasing returns to scale results (Paper 1, Section 11):

In the same file