Diversity Bonus

def proved Curvature Roles

Documentation

Lean 4 Proof

def diversityBonus (J ρ τ r : ℝ) : ℝ :=
  curvatureKReal J ρ * τ ^ 2 * (1 - r)

Dependency Graph

Used by

failure_improves_bonus diversityBonus_pos failure_cascade_monotone

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:26

Module Section

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

In the same file

marginalCurvatureLoss marginalCurvatureLoss_eq marginalCurvatureLoss_pos marginalCurvatureLoss_bound curvatureK_ratio_bound diversityBonus_pos failure_improves_bonus failure_threshold_small failure_cascade_monotone