Documentation

Lean 4 Proof

theorem eos_curvature_determines_step {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) {η : ℝ} (_hη : 0 < η)
    (h : η = cesCriticalStep J ρ c) :
    curvatureK J ρ = 2 * (↑J - 1) * c / η := by
  have hK : curvatureK J ρ ≠ 0 := ne_of_gt (curvatureK_pos hJ hρ)
  rw [h, cesCriticalStep_via_curvatureK hJ hρ hc]
  have hJ1ne : (↑J : ℝ) - 1 ≠ 0 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    linarith
  have hcne : c ≠ 0 := ne_of_gt hc
  field_simp

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:191

Module Section

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

In the same file