Documentation

Lean 4 Proof

theorem marginalCurvatureLoss_eq {J ρ : ℝ} (hJ : 1 < J) :
    curvatureKReal J ρ - curvatureKReal (J - 1) ρ = marginalCurvatureLoss J ρ := by
  simp only [curvatureKReal, marginalCurvatureLoss]
  have hJpos : 0 < J := by linarith
  have hJm1pos : 0 < J - 1 := by linarith
  rw [div_sub_div _ _ (ne_of_gt hJpos) (ne_of_gt hJm1pos)]
  congr 1
  ring

Dependency Graph

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:41

Module Section

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

In the same file