Documentation

Lean 4 Proof

theorem diversityBonus_pos {J ρ τ r : ℝ} (hJ : 1 < J) (hρ : ρ < 1)
    (hτ : 0 < τ) (hr : r < 1) :
    0 < diversityBonus J ρ τ r := by
  simp only [diversityBonus]
  exact mul_pos (mul_pos (curvatureKReal_pos hJ hρ) (sq_pos_of_pos hτ)) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:103

Module Section

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

In the same file