Documentation

Lean 4 Proof

theorem expected_knockout_loss_nonneg_leontief
    {J : ℕ} {ρ : ℝ} (hρ : ρ ≤ 0) {a : Fin J → ℝ}
    (ha_pos : ∀ j, 0 ≤ a j) :
    0 ≤ expectedKnockoutLoss J ρ a := by
  unfold expectedKnockoutLoss
  apply Finset.sum_nonneg
  intro j _
  apply mul_nonneg (ha_pos j)
  rw [knockout_leontief_total hρ]
  linarith

Dependency Graph

Location

thesis/CESProofs/Potential/PrimalDual.lean:135

Module Section

## Knockout Robustness and Supply Chain Design

In the same file