Documentation

Lean 4 Proof

theorem marginalCurvatureLoss_pos {J ρ : ℝ} (hJ : 1 < J) (hρ : ρ < 1) :
    0 < marginalCurvatureLoss J ρ := by
  simp only [marginalCurvatureLoss]
  exact div_pos (by linarith) (mul_pos (by linarith) (by linarith))

Dependency Graph

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:52

Module Section

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

In the same file