Documentation

Lean 4 Proof

theorem failure_cascade_monotone {J ρ τ r r' : ℝ}
    (hJ : 2 < J) (hρ : ρ < 1) (hr : r < 1) (hr' : r' < 1)
    (hτ : 0 < τ)
    (hδ : (r - r') / (1 - r) > 1 / ((J - 1) * (J - 2))) :
    diversityBonus J ρ τ r < diversityBonus (J - 1) ρ τ r' :=
  failure_improves_bonus hτ (failure_threshold_small hJ hρ hr hr' hδ)

Dependency Graph

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:196

Module Section

Firm Failure Resilience: Optimal Failure Rate for Long-Run Diversity

In the same file