Documentation

Lean 4 Proof

theorem one_lt_abs_iterMul_above_critical {η lam : ℝ} (hlam : 0 < lam)
    (hη : criticalStepSize lam < η) :
    1 < |iterationMultiplier η lam| := by
  simp only [iterationMultiplier, criticalStepSize] at *
  rw [div_lt_iff₀ hlam] at hη
  have hneg : 1 - η * lam < -1 := by linarith
  rw [abs_of_neg (by linarith)]
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:57

Module Section

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

In the same file