Documentation

Lean 4 Proof

theorem cesCriticalStep_eq {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) :
    cesCriticalStep J ρ c = 2 * ↑J * c / (1 - ρ) := by
  simp only [cesCriticalStep, criticalStepSize, cesEigenvaluePerp]
  have hJc : 0 < (↑J : ℝ) * c := mul_pos (Nat.cast_pos.mpr hJ) hc
  rw [abs_of_neg (div_neg_of_neg_of_pos (by linarith) hJc)]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hcne : c ≠ 0 := ne_of_gt hc
  have hρne : (1 : ℝ) - ρ ≠ 0 := by linarith
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:125

Module Section

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

In the same file