Iter Mul Eq Neg One At Critical

theorem proved Dynamics & Crises

Documentation

Lean 4 Proof

theorem iterMul_eq_neg_one_at_critical {lam : ℝ} (hlam : 0 < lam) :
    iterationMultiplier (criticalStepSize lam) lam = -1 := by
  simp only [iterationMultiplier, criticalStepSize]
  have hlam_ne : lam ≠ 0 := ne_of_gt hlam
  field_simp
  ring

Dependency Graph

Used by

ces_period_two_at_critical

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:49

Module Section

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

In the same file

iterationMultiplier criticalStepSize abs_iterMul_lt_one_iff one_lt_abs_iterMul_above_critical iterMul_in_unit_interval iterate_tendsto_zero iterate_norm_tendsto_top period_two_oscillation cesEigenvaluePerp_neg cesEigenvaluePerp_abs_pos cesCriticalStep cesCriticalStep_eq ces_stable_iff ces_period_two_at_critical cesCriticalStep_increasing_in_rho cesCriticalStep_via_curvatureK eos_at_boundary eos_curvature_determines_step