Documentation

Lean 4 Proof

theorem cesCriticalStep_via_curvatureK {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) :
    cesCriticalStep J ρ c = 2 * (↑J - 1) * c / curvatureK J ρ := by
  rw [cesCriticalStep_eq (by omega) hρ hc]
  simp only [curvatureK]
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (show 0 < J by omega)
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  have hJ1ne : (↑J : ℝ) - 1 ≠ 0 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    linarith
  have hρne : (1 : ℝ) - ρ ≠ 0 := by linarith
  have hcne : c ≠ 0 := ne_of_gt hc
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:162

Module Section

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

In the same file