Documentation

Lean 4 Proof

theorem knockout_cascade {N : ℕ} (hN : 0 < N) (F : Fin N → ℝ)
    (hF0 : F ⟨0, hN⟩ = 0)
    (hdep : ∀ (i : ℕ) (hi : i < N), 0 < i →
      ∃ (a : ℝ), F ⟨i, hi⟩ = a * F ⟨i - 1, by omega⟩)
    : ∀ (i : ℕ) (hi : i < N), F ⟨i, hi⟩ = 0 := by
  intro i hi
  induction i with
  | zero => convert hF0
  | succ k ih =>
    obtain ⟨a, ha⟩ := hdep (k + 1) hi (by omega)
    rw [ha]
    have : k + 1 - 1 = k := by omega
    simp only [this]
    rw [ih (by omega), mul_zero]

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:241

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file