Documentation

Lean 4 Proof

theorem Tstar_increasing_in_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₂) :
    generalCriticalFriction J ρ a₁ c d_sq
    < generalCriticalFriction J ρ a₂ c d_sq := by
  unfold generalCriticalFriction
  have hK1 : 0 < generalCurvatureK J ρ a₁ :=
    gen_quadruple_K_pos hJ hρ ha1_pos ha1_sum hH1
  have hK2 : 0 < generalCurvatureK J ρ a₂ :=
    gen_quadruple_K_pos hJ hρ ha2_pos ha2_sum hH2
  have hKdecr : generalCurvatureK J ρ a₂ < generalCurvatureK J ρ a₁ :=
    K_decreasing_in_herfindahl hρ hH
  have hJge : (2 : ℝ) ≤ ↑J := Nat.ofNat_le_cast.mpr hJ
  have hJpos : (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

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:374

Module Section

## General-Weight Effective Curvature Theorems

In the same file