Documentation

Lean 4 Proof

theorem cesCriticalStep_increasing_in_rho {J : ℕ} (hJ : 0 < J)
    {ρ₁ ρ₂ : ℝ} (hρ12 : ρ₁ < ρ₂) (hρ2 : ρ₂ < 1)
    {c : ℝ} (hc : 0 < c) :
    cesCriticalStep J ρ₁ c < cesCriticalStep J ρ₂ c := by
  rw [cesCriticalStep_eq hJ (by linarith) hc, cesCriticalStep_eq hJ hρ2 hc]
  exact div_lt_div_of_pos_left (by positivity) (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:154

Module Section

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

In the same file