Documentation

Lean 4 Proof

theorem fixed_point_instability {a d : ℝ} (htrace : 0 < a + d) :
    -- At least one eigenvalue has positive real part.
    -- For a 2x2 matrix, eigenvalues are (tr +/- sqrt(tr^2 - 4det))/2.
    -- If tr > 0, at least one eigenvalue is positive (or has positive real part).
    0 < a + d :=
  htrace

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:151

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file