The refined theorems of the alternative #
The recession hypothesis of the alternative for an infinite system of weak convex inequalities can
be weakened when the constraint set is the whole space: instead of asking that the fᵢ have no
common direction of recession, it is enough that finitely many of them be affine and that every
common direction of recession be a direction of constancy for all the others. The corresponding
weakening of Helly's theorem asks that finitely many of the Cᵢ be polyhedral and that every
common direction of recession be a direction of linearity for the rest.
The proof changes exactly one step of the unrefined one. Both run on the positively homogeneous
convex function k generated by conv {fᵢ*} and both finish with
exists_multipliers_of_posHomGen_convFn_conj_eq_bot (in Helly.lean) once k(0) = -∞ is known.
The unrefined proof gets k(0) = -∞ from 0 ∈ ri (dom k); here it comes from splitting the family
in two and separating the halves, one of which is polyhedral.
Only the case of the whole space is treated, as in the book. A version relative to a closed convex
C needs no new mathematics — fold δ(· ∣ C) into the family — but then carries the hypothesis
that C is linear in every common direction of recession, or polyhedral and cut into half-spaces.
Main results #
conj_affineFn,epi_conj_affineFn— the conjugate of⟨·, a⟩ - cisδ(· ∣ a) + c, and its epigraph is a single translated vertical ray. This is what makesk₀below polyhedral.polyhedralFn_posHomGen_convFn_conj_affineFn— the affine halfk₀is polyhedral.conj_posHomGen_convFn_conj—kⱼ* = δ(· ∣ Cⱼ).nonempty_neg_dom_inter_relint_dom— the separation step:(-dom k₀) ∩ ri (dom k₁) ≠ ∅, from polyhedral separation and the constancy hypothesis.apply_zero_eq_bot_of_le_of_le— the heart of the refinement:k(0) = -∞.alternative_infinite_system_univ_of_affine_tail— the refined alternative for functions; Theorem 21.4 in [^1].exists_forall_le_zero_of_forall_subsystem_of_affine_tailis the matching solvability criterion.helly_of_polyhedral_tail— the refined Helly theorem; Theorem 21.5 in [^1].Polyhedral.exists_finset_pairing— a polyhedral set is cut out by finitely many inequalities of the pairing, which is what lets the refined Helly theorem feed its half-spaces to the refined alternative.constancySpace_indicatorFn,recessionFn_affineFn_nonpos_iff,mem_recessionCone_of_forall_pairing_nonpos— the translation between the language of sets and the language of functions.PosHomogeneous.add_le_add_of_ne_top— subadditivity of a positively homogeneous convex function at the points where it is< +∞.
Implementation notes #
k = conv {k₀, k₁} is never formed: only k(0) ≤ k₀(-z) + k₁(z) is used, so
apply_zero_eq_bot_of_le_of_le takes an arbitrary positively homogeneous convex k below both.
The two halves are indexed by subtypes of ι and neither need be nonempty — Rockafellar adjoins
identically-zero functions to avoid that, but posHomGen h is ≤ 0 at the origin whatever h is,
and for an empty family posHomGen (convFn g) is δ(· ∣ 0), polyhedral with domain {0}. The
hypothesis B.SeparatingRight replaces Rockafellar's identification of Rⁿ with its dual: it is
what makes fᵢ* a point indicator rather than the indicator of an affine subspace.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §13, §19, §20 and §21.
Away from a the conjugate of ⟨·, a⟩ - c is +∞: the pairing separates y - a from 0,
so ⟨·, y - a⟩ is unbounded above.
The conjugate of an affine function is a translated point indicator: fᵢ(x) = ⟨aᵢ, x⟩ - αᵢ
has fᵢ*(x*) = δ(x* ∣ aᵢ) + αᵢ. The separating hypothesis on the pairing is what replaces
Rockafellar's identification of Rⁿ with its dual.
The epigraph of the conjugate of an affine function is a single translated vertical ray.
This is the hypothesis shape of epi_convFn_of_epi_eq, and it is what makes Rockafellar's k₀
finitely generated.
A positively homogeneous convex function is subadditive wherever it is not +∞. The usual
form of this asks instead that the function never take -∞, which cannot be paid here, because the
functions kⱼ built below may be improper; the epigraph, a convex cone, supplies subadditivity
directly wherever both values are < +∞. The hypothesis cannot be dropped: on ℝ² the function
with epigraph {(s, t, μ) ∣ s > 0} ∪ {(0, 0, μ) ∣ μ ≥ 0} is positively homogeneous and convex and
vanishes at the origin, yet g(0, 0) = 0 > ⊥ = g(-1, 0) + g(1, 0).
The effective domain of the convex hull of a family is the convex hull of the union of the
effective domains: Prod.fst is linear, so it carries the convex hull of the union of epigraphs to
the convex hull of the union of their projections.
A linear inequality valid on every dom (g i) is valid on dom (posHomGen (convFn g)).
dom k₁ is the convex cone generated by the sets dom fᵢ*; this is the only consequence of that
description the refinement uses.
The reflection (x, μ) ↦ (-x, μ) of E × ℝ, as a linear map. It carries epi f to
epi (f ∘ -·).
Equations
Instances For
The epigraph of x ↦ f (-x) is the reflection of the epigraph of f.
The effective domain of x ↦ f (-x) is -dom f.
A function proper at -x is proper.
Directions of recession, read off the conjugate: a direction is a direction of recession of
a closed proper convex g exactly when the pairing with it is nonpositive on dom g*.
kⱼ* is the indicator of Cⱼ. For a family of closed proper convex functions, the
conjugate of the positively homogeneous convex function generated by conv {gᵢ*} is the indicator
of {x ∣ gᵢ(x) ≤ 0 for every i}. The conjugate of a convex hull is the pointwise supremum, and the
Fenchel–Moreau theorem closes the loop; it is used below for both k₀ and k₁.
The affine half k₀ is polyhedral. The positively homogeneous convex function generated by
the convex hull of the conjugates of finitely many affine functions is polyhedral, and so is its
effective domain: a convex hull of finitely many polyhedral epigraphs is polyhedral, and by
epi_conj_affineFn each fᵢ* is a point indicator whose epigraph is a single translated vertical
ray.
The separation step: (-dom k₀) ∩ ri (dom k₁) is nonempty. Both sets contain the origin,
so a separating hyperplane passes through it. If they could be separated properly without the
hyperplane containing dom k₁ — the only way they can miss each other, dom k₀ being polyhedral —
the separating direction would be a common direction of recession of the whole family, hence a
direction of constancy for the g₁, and then the hyperplane would contain dom k₁ after all.
Reflecting the argument of a polyhedral convex function leaves it polyhedral.
The heart of the refinement: if the two half-systems {g₀ i} and {g₁ i} have no common
solution of gᵢ(x) ≤ 0, if k₀ is polyhedral, and if every common direction of recession of the
whole family is a direction of constancy of the g₁, then any positively homogeneous convex
minorant k of both k₀ and k₁ has k(0) = -∞.
Separation puts a z in (-dom k₀) ∩ ri (dom k₁); if either kⱼ is improper there, k(0) = -∞
at once; otherwise the conjugate of the sum k₀(-·) + k₁ is the infimal convolution of the two
conjugates, which are the indicators of the two solution sets, and those have empty intersection.
The textbook applies this to k = conv {k₀, k₁}, but only through k(0) ≤ k₀(-z) + k₁(z), which
needs nothing of k beyond k ≤ k₀, k ≤ k₁ and subadditivity.
An affine function of a continuous pairing is closed, proper and convex.
The effective domain of the conjugate of an affine function is the single point a.
A direction of recession of the affine function ⟨·, a⟩ - c is one that pairs nonpositively
with a: the effective domain of its conjugate is the single point a.
Every polyhedral convex set is cut out by finitely many inequalities of the pairing. The usual definition uses linear functionals; in finite dimensions a compatible pairing represents every one of them, which lets the refined Helly theorem replace the polyhedral members of a family by half-spaces described by affine functions of the pairing.
A direction pairing nonpositively with every constraint vector recedes in the polyhedron those constraints cut out.
The constancy space of an indicator function is the lineality space of the set. This is
what turns "a direction in which Cᵢ is linear" into "a direction in which fᵢ is constant".
The refined alternative over the whole space. The recession hypothesis may be weakened: it
is enough that there be a finite set of indices I₀ on which the fᵢ are affine, such that
every direction of recession common to all the fᵢ is a direction in which fᵢ is constant
for every i ∉ I₀. The unrefined hypothesis — that the only common direction of recession is 0 —
implies this one with I₀ = ∅. The gain is that the affine members may now recede, and so may the
others provided they are flat in every direction the whole family recedes in. Only one step of the
unrefined proof changes: the passage to k(0) = -∞, which is here
apply_zero_eq_bot_of_le_of_le.
The solvability criterion under the refined hypothesis. An infinite system of weak convex
inequalities is solvable as soon as every subsystem of at most n + 1 of the inequalities is
solvable to within an arbitrarily small tolerance — provided that, outside a finite set of indices
carrying affine functions, every common direction of recession is a direction of constancy.
The refined Helly theorem. The recession hypothesis of Helly's theorem for infinite
families may be weakened: it is enough that there be a finite set of indices I₀ on which the
Cᵢ are polyhedral, such that every direction of recession common to all the Cᵢ is a direction
in which Cᵢ is linear for every i ∉ I₀. Compare helly_of_no_common_recession, whose
hypothesis is that the only common direction of recession is 0. Each polyhedral Cᵢ, i ∈ I₀,
is replaced by the finitely many closed half-spaces cutting it out, and the refined alternative
applies with those as its affine part.