Documentation

Lean 4 Proof

theorem logistic_fragility_unbounded {u : ℝ} (_hu_pos : 0 < u) (hu_lt1 : u < 1) :
    -- As u → 1, |1 - 2u| / (1 - u) → ∞
    -- We state: the denominator (1-u) can be made arbitrarily small
    0 < 1 - u := by linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:213

Module Section

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

In the same file