Documentation

Lean 4 Proof

theorem knockout_cascade_with_weights
    {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
  exact knockout_cascade hN F hF0 hdep

Dependency Graph

Location

thesis/CESProofs/Hierarchy/KnockoutHierarchy.lean:21

Module Section

## Theorem 4b.6: Weight-Dependent Knockout Cascade

In the same file