Lean 4 Proof

private theorem cesEigenvaluePerp_abs_pos {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) :
    0 < |cesEigenvaluePerp J ρ c| :=
  abs_pos.mpr (ne_of_lt (cesEigenvaluePerp_neg hJ hρ hc))

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:115

Module Section

Discrete-Time Stability of CES Tâtonnement (Edge of Stability)

In the same file