Documentation

Lean 4 Proof

theorem failure_improves_bonus {J ρ τ r r' : ℝ}
    (hτ : 0 < τ)
    (hcond : curvatureKReal J ρ * (1 - r) < curvatureKReal (J - 1) ρ * (1 - r')) :
    diversityBonus J ρ τ r < diversityBonus (J - 1) ρ τ r' := by
  simp only [diversityBonus]
  have hτ2 : 0 < τ ^ 2 := sq_pos_of_pos hτ
  calc curvatureKReal J ρ * τ ^ 2 * (1 - r)
      = curvatureKReal J ρ * (1 - r) * τ ^ 2 := by ring
    _ < curvatureKReal (J - 1) ρ * (1 - r') * τ ^ 2 :=
        mul_lt_mul_of_pos_right hcond hτ2
    _ = curvatureKReal (J - 1) ρ * τ ^ 2 * (1 - r') := by ring

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:119

Module Section

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

In the same file