Documentation

Lean 4 Proof

theorem irs_diversity_eigenvalue_neg {ρ γ : ℝ} (hρ : ρ < 1) (hγ : 0 < γ)
    (hJ : 0 < J) {c : ℝ} (hc : 0 < c) :
    irsEigenvaluePerp J ρ γ c < 0 := by
  simp only [irsEigenvaluePerp]
  apply mul_neg_of_neg_of_pos
  · apply div_neg_of_neg_of_pos
    · exact neg_neg_of_pos (mul_pos hγ (by linarith))
    · exact_mod_cast hJ
  · exact rpow_pos_of_pos hc _

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/IRS.lean:98

Module Section

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

In the same file