Documentation

Lean 4 Proof

theorem period_two_oscillation (x₀ : ℝ) (n : ℕ) :
    (-1 : ℝ) ^ n * x₀ = if n % 2 = 0 then x₀ else -x₀ := by
  rcases Nat.even_or_odd n with ⟨k, hk⟩ | ⟨k, hk⟩
  · subst hk
    simp only [show (k + k) % 2 = 0 from by omega, ↓reduceIte]
    rw [show k + k = 2 * k from by ring, pow_mul, neg_one_sq, one_pow, one_mul]
  · subst hk
    simp [show (2 * k + 1) % 2 = 1 from by omega, pow_succ, pow_mul, one_pow]

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:93

Module Section

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

In the same file