Documentation

Lean 4 Proof

theorem knockout_permanent_leontief
    {J : ℕ} {ρ : ℝ} (hρ : ρ ≤ 0) {a : Fin J → ℝ} (j : Fin J) :
    CESProofs.Potential.weightedKnockoutLoss J ρ a j = 1 := by
  exact CESProofs.Potential.knockout_leontief_total hρ j

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:458

Module Section

## Theorem 3b.5: Dynamic Knockout Propagation

In the same file