Documentation

Lean 4 Proof

theorem knockout_cascade_step {F_below : ℝ} (hF : F_below = 0)
    {beta sigma : ℝ} (_hb : 0 < beta) (_hs : 0 < sigma) :
    -- If the level below has zero output, the gain function produces zero
    -- For the logistic: phi(0) = 0/(1+0) = 0
    -- So Fbar_above = phi(F_below) / sigma = 0 / sigma = 0
    beta * F_below / sigma = 0 := by
  rw [hF, mul_zero, zero_div]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:231

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file