Documentation

Lean 4 Proof

theorem diversification_degradation_ratio {T Tstar : ℝ}
    (hTs : 0 < Tstar) (hT : 0 < T) (hTlt : T < Tstar) :
    (1 - T / Tstar) ^ 2 < (1 - T / Tstar) := by
  exact crisis_sequence_ordering (div_pos hT hTs) (by rw [div_lt_one hTs]; exact hTlt)

Dependency Graph

Location

thesis/CESProofs/Potential/BilateralTrade.lean:81

Module Section

Bilateral Trade Collapse Ordering

In the same file