Documentation

Lean 4 Proof

noncomputable def weightedKnockoutLoss
    (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) (j : Fin J) : ℝ :=
  if ρ ≤ 0 then 1  -- total failure for Leontief
  else 1 - (1 - (a j) ^ (1 / (1 - ρ))) ^ (1 / ρ)

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:273

Module Section

## General-Weight and IRS Effective Curvature Definitions

In the same file