Documentation

Lean 4 Proof

theorem bridge_eigenvalue {tree_coeff : ℝ} (hc : 0 < tree_coeff)
    {J : ℕ} (hJ : 2 ≤ J)
    {Fbar : ℝ} (hF : 0 < Fbar)
    {ρ c : ℝ} (hrho : ρ < 1) (hcpos : 0 < c) :
    0 < institutionalQuality tree_coeff J Fbar *
      |logCesEigenvaluePerp J ρ c| := by
  apply mul_pos (institutionalQuality_pos hc hJ hF)
  rw [abs_pos]
  exact ne_of_lt (logCesEigenvaluePerp_neg hrho (by omega) hcpos)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:130

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file