Documentation

Lean 4 Proof

theorem K_positive_nondegenerate (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 :=
  gen_quadruple_K_pos hJ hρ ha_pos ha_sum hH

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:192

Module Section

## Entry with General Weights

In the same file