Documentation

Lean 4 Proof

theorem rho_ordering_with_herfindahl
    {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {a₁ a₂ : Fin J → ℝ}
    (ha1_pos : ∀ j, 0 < a₁ j) (ha1_sum : ∑ j, a₁ j = 1)
    (ha2_pos : ∀ j, 0 < a₂ j) (ha2_sum : ∑ j, a₂ j = 1)
    (hH1 : herfindahlIndex J a₁ < 1) (hH2 : herfindahlIndex J a₂ < 1)
    {c d_sq : ℝ} (hc : 0 < c) (hd : 0 < d_sq)
    (hH : herfindahlIndex J a₁ < herfindahlIndex J a₂) :
    -- More concentrated sector has higher T* (harder to destabilize)
    CESProofs.Potential.generalCriticalFriction J ρ a₁ c d_sq
    < CESProofs.Potential.generalCriticalFriction J ρ a₂ c d_sq := by
  exact CESProofs.Potential.Tstar_increasing_in_herfindahl hJ hρ ha1_pos ha1_sum
    ha2_pos ha2_sum hH1 hH2 hc hd hH

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:420

Module Section

## Theorem 3b.4: ρ-Ordering with Weight Heterogeneity

In the same file