Documentation

Lean 4 Proof

theorem ceiling_cascade {N : ℕ} (ceiling : Fin N → ℝ)
    (h0 : ∀ (h : 0 < N), ceiling ⟨0, h⟩ = 0)
    (hdep : ∀ (i : ℕ) (hi : i < N), 0 < i →
      ∃ (a : ℝ), 0 ≤ a ∧ ceiling ⟨i, hi⟩ ≤ a * ceiling ⟨i - 1, by omega⟩) :
    ∀ (i : ℕ) (hi : i < N), ceiling ⟨i, hi⟩ ≤ 0 := by
  intro i hi
  induction i with
  | zero => rw [h0 (by omega)]
  | succ k ih =>
    obtain ⟨a, ha, hle⟩ := hdep (k + 1) hi (by omega)
    have : k + 1 - 1 = k := by omega
    simp only [this] at hle
    calc ceiling ⟨k + 1, hi⟩
        ≤ a * ceiling ⟨k, by omega⟩ := hle
      _ ≤ a * 0 := mul_le_mul_of_nonneg_left (ih (by omega)) ha
      _ = 0 := mul_zero a

Dependency Graph

Location

thesis/CESProofs/Hierarchy/TransitionDynamics.lean:57

Module Section

Propositions 8-11, Theorems 10-12: Transition Dynamics

In the same file