Documentation

Lean 4 Proof

theorem logistic_fragility_negative {u : ℝ} (hu_gt : 1 / 2 < u) (hu_lt1 : u < 1) :
    logisticElasticity u < 0 := by
  simp only [logisticElasticity]
  apply div_neg_of_neg_of_pos
  · linarith
  · linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:205

Module Section

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

In the same file