Documentation

Lean 4 Proof

theorem knockout_leontief_total
    {J : ℕ} {ρ : ℝ} (hρ : ρ ≤ 0) {a : Fin J → ℝ} (j : Fin J) :
    weightedKnockoutLoss J ρ a j = 1 := by
  unfold weightedKnockoutLoss
  simp [hρ]

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/PrimalDual.lean:127

Module Section

## Knockout Robustness and Supply Chain Design

In the same file