Documentation

Lean 4 Proof

theorem rho_ordering_preserved_general_weights
    {J : ℕ} (hJ : 2 ≤ J) {ρ₁ ρ₂ : ℝ} (hρ₁ : ρ₁ < 1) (hρ₂ : ρ₂ < 1)
    (hρ : ρ₁ < ρ₂)
    {a : Fin J → ℝ} (ha_pos : ∀ j, 0 < a j) (ha_sum : ∑ j, a j = 1)
    (hH : herfindahlIndex J a < 1)
    {c d_sq : ℝ} (hc : 0 < c) (hd : 0 < d_sq) :
    -- More complementary (lower ρ) has lower T* → crosses first
    CESProofs.Potential.generalCriticalFriction J ρ₁ a c d_sq
    < CESProofs.Potential.generalCriticalFriction J ρ₂ a c d_sq := by
  unfold CESProofs.Potential.generalCriticalFriction
  have hK1 : 0 < generalCurvatureK J ρ₁ a :=
    gen_quadruple_K_pos hJ hρ₁ ha_pos ha_sum hH
  have hK2 : 0 < generalCurvatureK J ρ₂ a :=
    gen_quadruple_K_pos hJ hρ₂ ha_pos ha_sum hH
  have hKdecr : generalCurvatureK J ρ₂ a < generalCurvatureK J ρ₁ a := by
    unfold generalCurvatureK herfindahlIndex at *
    nlinarith [show 0 < 1 - herfindahlIndex J a from by unfold herfindahlIndex; linarith]
  have hJge : (2 : ℝ) ≤ ↑J := Nat.ofNat_le_cast.mpr hJ
  have hJm1 : (0 : ℝ) < ↑J - 1 := by linarith
  have hnum : 0 < 2 * (↑J - 1) * c ^ 2 * d_sq := by positivity
  exact div_lt_div_of_pos_left hnum hK2 hKdecr

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:436

Module Section

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

In the same file