Documentation

Lean 4 Proof

theorem curvatureK_ratio_bound {J ρ : ℝ} (hJ : 2 < J) (hρ : ρ < 1) :
    curvatureKReal J ρ / curvatureKReal (J - 1) ρ ≤ 1 + 1 / (J - 2) := by
  simp only [curvatureKReal]
  have hJpos : (0 : ℝ) < J := by linarith
  have hJm1pos : (0 : ℝ) < J - 1 := by linarith
  have hJm2pos : (0 : ℝ) < J - 2 := by linarith
  have h1ρ : (0 : ℝ) < 1 - ρ := by linarith
  -- K(J-1) > 0
  have hKm1 : 0 < (1 - ρ) * (J - 1 - 1) / (J - 1) :=
    div_pos (mul_pos h1ρ (by linarith)) hJm1pos
  -- Reduce to: (1-ρ)(J-1)/J ≤ (1+1/(J-2)) · (1-ρ)(J-2)/(J-1)
  rw [div_le_iff₀ hKm1, show J - 1 - 1 = J - 2 from by ring]
  -- Cross-multiply: clear all denominators at once
  rw [div_le_iff₀ hJpos]
  -- Goal: (1-ρ)*(J-1) ≤ (1+1/(J-2))*((1-ρ)*(J-2)/(J-1))*J
  -- Rewrite 1+1/(J-2) as (J-1)/(J-2), then simplify
  rw [show (1 + 1 / (J - 2)) * ((1 - ρ) * (J - 2) / (J - 1)) * J =
    (1 - ρ) * J from by field_simp; ring]
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:77

Module Section

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

In the same file