Documentation

Lean 4 Proof

theorem knockout_risk_increases_with_concentration
    {J : ℕ} {ρ : ℝ} (hρ : ρ < 1)
    {a₁ a₂ : Fin J → ℝ}
    (hH : herfindahlIndex J a₁ < herfindahlIndex J a₂) :
    -- Higher concentration → lower curvature K → less resilience
    generalCurvatureK J ρ a₂ < generalCurvatureK J ρ a₁ := by
  exact K_decreasing_in_herfindahl_sector hρ hH

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:481

Module Section

## Proposition 3b.6: Knockout-Triggered Regime Shift

In the same file