Documentation

Lean 4 Proof

theorem scale_scope_monotone_in_gamma
    (γ₁ γ₂ ρ : ℝ) (hγ1 : 1 < γ₁) (hγ2 : γ₁ < γ₂) (hρ : ρ < 1) :
    scaleScopeCrossPartialSign γ₁ ρ < scaleScopeCrossPartialSign γ₂ ρ := by
  simp only [scaleScopeCrossPartialSign]
  have h1ρ : 0 < 1 - ρ := by linarith
  have : γ₁ * (γ₁ - 1) < γ₂ * (γ₂ - 1) := by nlinarith
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:272

Module Section

## IRS and Firm Scope

In the same file