A positive weighted sum of supporting inequalities exposes exactly their common tight face

Proved

Hirsch.positive_weighted_support_equals_common_tight_face

by jjosh · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-geometryhirsch-conjecturepolyhedrasupporting-faces

Let finitely many linear functionals be bounded above on a set P by values b_i, and give every row a strictly positive weight w_i. A point of P attains the weighted sum of all upper bounds if and only if it attains every individual upper bound. Hence the supporting face exposed by the positive weighted sum is exactly the common tight face of all the component inequalities.

Preamble

import Mathlib
open Set
open scoped BigOperators

Formal statement

theorem Hirsch.positive_weighted_support_equals_common_tight_face
    {E : Type*} [AddCommGroup E] [Module ℝ E]
    {ι : Type*} [Fintype ι]
    (P : Set E) (a : ι → E →ₗ[ℝ] ℝ) (b w : ι → ℝ)
    (hw : ∀ i, 0 < w i)
    (hb : ∀ i, ∀ x ∈ P, a i x ≤ b i) :
    {x : E | x ∈ P ∧ (∑ i, w i * a i x) = (∑ i, w i * b i)} =
      {x : E | x ∈ P ∧ ∀ i, a i x = b i} := by sorry

Source

Standalone proof extracted from PR #210 support-intersection work: https://github.com/jjoshua2/prove2me-work/blob/formal/dual-wall-carrier-routing/research/publication_packets/pr210_catchup/positive_weighted_common_face/solution.lean

View graph