Documentation

Lean 4 Proof

theorem failure_threshold_small {J ρ r r' : ℝ}
    (hJ : 2 < J) (hρ : ρ < 1) (hr : r < 1) (hr' : r' < 1)
    (hδ : (r - r') / (1 - r) > 1 / ((J - 1) * (J - 2))) :
    curvatureKReal J ρ * (1 - r) < curvatureKReal (J - 1) ρ * (1 - r') := 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 h1r : 0 < 1 - r := by linarith
  have h1ρ : 0 < 1 - ρ := by linarith
  -- From hδ: (1-r') > (1-r)(1 + 1/((J-1)(J-2)))
  have h_rr : (1 - r') > (1 - r) * (1 + 1 / ((J - 1) * (J - 2))) := by
    have := mul_lt_mul_of_pos_right hδ h1r
    rw [div_mul_cancel₀ _ (ne_of_gt h1r)] at this
    linarith
  -- Cross-multiply: need (J-1)²(1-r) < J(J-2)(1-r')
  rw [div_mul_eq_mul_div, div_mul_eq_mul_div]
  rw [div_lt_div_iff₀ hJpos hJm1pos]
  rw [show J - 1 - 1 = J - 2 from by ring]
  -- Goal: (1-ρ)*(J-1)*(1-r)*(J-1) < (1-ρ)*(J-2)*(1-r')*J
  -- Reduce to: (J-1)*(1-r)*(J-1) < (J-2)*(1-r')*J
  -- Clear divisions in h_rr to get a polynomial inequality
  have hprod : 0 < (J - 1) * (J - 2) := mul_pos hJm1pos hJm2pos
  -- h_rr: (1-r') > (1-r) + (1-r)/((J-1)(J-2))
  -- Multiply by (J-1)(J-2): (1-r')*(J-1)*(J-2) > (1-r)*(J-1)*(J-2) + (1-r)
  have h_rr_clear : (1 - r') * ((J - 1) * (J - 2)) >
      (1 - r) * ((J - 1) * (J - 2)) + (1 - r) := by
    have := mul_lt_mul_of_pos_right h_rr hprod
    rw [mul_comm (1 - r) (1 + 1 / ((J - 1) * (J - 2)))] at this
    have expand : (1 + 1 / ((J - 1) * (J - 2))) * (1 - r) * ((J - 1) * (J - 2)) =
        (1 - r) * ((J - 1) * (J - 2)) + (1 - r) := by
      field_simp
    linarith
  -- Key step: (J-1)*(1-r)*(J-1) < (J-2)*(1-r')*J
  -- Equivalently: (1-r)*(J-1)² < (1-r')*J*(J-2)
  have key : (1 - r) * ((J - 1) * (J - 1)) < (1 - r') * ((J - 2) * J) := by
    -- From h_rr_clear: (1-r')*(J-1)*(J-2) > (1-r)*((J-1)*(J-2)+1)
    -- (J-1)*(J-2)+1 = (J-1)² - (J-1) + 1 = J²-3J+3
    -- Need: (1-r')*(J-2)*J > (1-r)*(J-1)²
    -- From h_rr_clear multiply by J/(J-1):
    -- (1-r')*(J-2)*J > ((1-r)*(J-1)*(J-2)+(1-r))*J/(J-1)
    -- = (1-r)*J*(J-2) + (1-r)*J/(J-1)
    -- And J/(J-1) > 1, so > (1-r)*J*(J-2) + (1-r) = (1-r)*(J²-2J+1) = (1-r)*(J-1)²
    have hJdiv : J / (J - 1) > 1 := by
      rw [gt_iff_lt, lt_div_iff₀ hJm1pos]; linarith
    nlinarith
  nlinarith

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/FirmFailureResilience.lean:142

Module Section

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

In the same file