Documentation

Lean 4 Proof

theorem marginalCurvatureLoss_bound {J ρ : ℝ} (hJ : 2 ≤ J) (hρ : ρ < 1) :
    (1 - ρ) / J ^ 2 ≤ marginalCurvatureLoss J ρ := by
  simp only [marginalCurvatureLoss]
  apply div_le_div_of_nonneg_left (by linarith)
    (mul_pos (by linarith : (0 : ℝ) < J) (by linarith : (0 : ℝ) < J - 1))
  · have hJpos : 0 < J := by linarith
    rw [sq]
    exact mul_le_mul_of_nonneg_left (by linarith : J - 1 ≤ J) (le_of_lt hJpos)

Dependency Graph

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:60

Module Section

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

In the same file