Documentation

Lean 4 Proof

theorem eos_at_boundary {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) {η : ℝ} (_hη : 0 < η)
    (h : η = cesCriticalStep J ρ c) :
    abs (cesEigenvaluePerp J ρ c) = 2 / η := by
  have habsne : abs (cesEigenvaluePerp J ρ c) ≠ 0 :=
    ne_of_gt (cesEigenvaluePerp_abs_pos hJ hρ hc)
  rw [h, cesCriticalStep, criticalStepSize]
  field_simp

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:181

Module Section

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

In the same file