Documentation

Lean 4 Proof

theorem iterMul_in_unit_interval {η lam : ℝ} (hlam : 0 < lam) (hη : 0 < η)
    (hlt : η < criticalStepSize lam) :
    -1 < iterationMultiplier η lam ∧ iterationMultiplier η lam < 1 :=
  abs_lt.mp ((abs_iterMul_lt_one_iff hlam hη).mpr hlt)

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:67

Module Section

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

In the same file