CES Eigenvalue Perp Neg

theorem proved Dynamics & Crises

Documentation

Lean 4 Proof

theorem cesEigenvaluePerp_neg {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) :
    cesEigenvaluePerp J ρ c < 0 := by
  simp only [cesEigenvaluePerp]
  apply div_neg_of_neg_of_pos
  · linarith
  · exact mul_pos (Nat.cast_pos.mpr hJ) hc

Dependency Graph

Used by

cesEigenvaluePerp_abs_pos

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:107

Module Section

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

In the same file

iterationMultiplier criticalStepSize abs_iterMul_lt_one_iff iterMul_eq_neg_one_at_critical one_lt_abs_iterMul_above_critical iterMul_in_unit_interval iterate_tendsto_zero iterate_norm_tendsto_top period_two_oscillation 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