Documentation

Lean 4 Proof

theorem abs_iterMul_lt_one_iff {η lam : ℝ} (hlam : 0 < lam) (hη : 0 < η) :
    |iterationMultiplier η lam| < 1 ↔ η < criticalStepSize lam := by
  simp only [iterationMultiplier, criticalStepSize]
  constructor
  · intro h
    rw [abs_lt] at h
    rw [lt_div_iff₀ hlam]
    linarith [h.1]
  · intro h
    rw [lt_div_iff₀ hlam] at h
    rw [abs_lt]
    constructor <;> nlinarith [mul_pos hη hlam]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:35

Module Section

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

In the same file