Documentation

Lean 4 Proof

theorem irs_diversity_eigenvalue_nonpos
    {J : ℕ} {ρ γ : ℝ} (hρ : ρ < 1) (hγ : 0 < γ)
    (hJ : 0 < J) {c : ℝ} (hc : 0 < c) :
    irsEigenvaluePerp J ρ γ c < 0 := by
  exact irs_diversity_eigenvalue_neg hρ hγ hJ hc

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:236

Module Section

## IRS and Firm Scope

In the same file