Documentation

Lean 4 Proof

theorem ces_stable_iff {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) {η : ℝ} (hη : 0 < η) :
    abs (iterationMultiplier η (abs (cesEigenvaluePerp J ρ c))) < 1 ↔
    η < cesCriticalStep J ρ c :=
  abs_iterMul_lt_one_iff (cesEigenvaluePerp_abs_pos hJ hρ hc) hη

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:137

Module Section

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

In the same file