Documentation

Lean 4 Proof

theorem logistic_fragility_positive {u : ℝ} (hu_lt : u < 1 / 2) (_hu_lt1 : u < 1) :
    0 < logisticElasticity u := by
  simp only [logisticElasticity]
  apply div_pos
  · linarith
  · linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:197

Module Section

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

In the same file