Documentation

Lean 4 Proof

theorem irs_scale_eigenvalue_pos {γ : ℝ} (hγ : 1 < γ)
    (hJ : 0 < J) {c : ℝ} (hc : 0 < c) :
    0 < irsEigenvalueScale J γ c := by
  simp only [irsEigenvalueScale]
  apply mul_pos
  · apply div_pos
    · exact mul_pos (by linarith) (by linarith)
    · exact_mod_cast hJ
  · exact rpow_pos_of_pos hc _

Dependency Graph

Location

thesis/CESProofs/Potential/IRS.lean:86

Module Section

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

In the same file