Documentation

Lean 4 Proof

theorem gen_quadruple_K_pos (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {a : Fin J → ℝ} (ha_pos : ∀ j, 0 < a j) (ha_sum : ∑ j : Fin J, a j = 1)
    (hH : herfindahlIndex J a < 1) :
    0 < generalCurvatureK J ρ a := by
  simp only [generalCurvatureK, herfindahlIndex] at *
  apply mul_pos
  · linarith
  · linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/GeneralWeights.lean:130

Module Section

General-weight CES results (Paper 1, Section 10):

In the same file