Marginal Curvature Loss

def proved Curvature Roles

Documentation

Lean 4 Proof

def marginalCurvatureLoss (J ρ : ℝ) : ℝ :=
  (1 - ρ) / (J * (J - 1))

Dependency Graph

Used by

marginalCurvatureLoss_pos marginalCurvatureLoss_eq marginalCurvatureLoss_bound

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:32

Module Section

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

In the same file

diversityBonus marginalCurvatureLoss_eq marginalCurvatureLoss_pos marginalCurvatureLoss_bound curvatureK_ratio_bound diversityBonus_pos failure_improves_bonus failure_threshold_small failure_cascade_monotone