Systems of convex inequalities: theorems of the alternative #
The engine of the section is this: for proper convex functions f₁, …, f_m that are finite on
ri C, either the strict system fᵢ(x) < 0 has a solution in C, or some non-trivial
non-negative combination λ₁f₁ + ⋯ + λ_mf_m is non-negative on all of C. It is the existence
workhorse behind the Lagrange multiplier theorems.
The hypothesis ri C ⊆ dom fᵢ is not decoration. On ℝ take f₁ x = -√x for x ≥ 0 and +∞
otherwise, f₂ x = x, C = ℝ; neither alternative holds.
The refinements that weaken the recession hypothesis of the infinite-system alternative are in
Tdaf/Analysis/Convex/HellyRefined.lean; they share this file's tail, since
exists_multipliers_of_posHomGen_convFn_conj_eq_bot is the half of it that does not mention
recession at all.
Main results #
alternative_of_convex_system— the substantial half of the alternative for a finite strict system (Theorem 21.1 in [^1]);not_exists_forall_neg_of_forall_zero_le_weightedis the easy half, that the two alternatives exclude each other.alternative_of_convex_system_affine— the refinement that keeps affine constraints apart and so sharpens alternative (b) to "not all of theλᵢon the convex constraints vanish".helly_finite— Helly's theorem for finite collections (Mathlib'sConvex.helly_theorem').exists_mem_of_forall_subsystem,exists_mem_of_forall_subsystem_lt— a finite mixed system of convex inequalities is solvable as soon as every subsystem of at mostn + 1of them is.sparse_alternative_of_convex_system— the multipliers may be taken supported on at mostn + 1indices.alternative_infinite_system_univ,alternative_infinite_system— the alternative for weak inequalities over an arbitrary index set (Theorem 21.3 in [^1]).exists_multipliers_of_posHomGen_convFn_conj_eq_bot— its multiplier half, withk(0) = -∞as a hypothesis rather than a consequence of the recession assumption.exists_forall_le_zero_of_forall_subsystem— the solvability criterion for an infinite system, where the subsystems need only be solvable to within an arbitrary tolerance.helly_of_no_common_recession— Helly's theorem for an infinite family of closed convex sets with no common direction of recession.helly_of_exists_isBounded_biInter— when every finite subfamily has a common point, that recession hypothesis may be replaced by "some finite subfamily has a bounded intersection".finrank_eq_of_isCompatiblePairing— the bookkeeping lemma that lets the multiplier count be stated asdim E + 1although Carathéodory is applied inF.
Implementation notes #
The weighted sum is read in EReal with the convention 0 · ∞ = 0: ∑ i, (l i : EReal) * f i x
is exactly λ₁f₁(x) + ⋯ + λ_mf_m(x), and a vanishing multiplier silently drops its constraint.
Multipliers are not normalised to sum to 1; alternative (b) is ∑ λᵢ fᵢ(x) ≥ ε with the λᵢ
unnormalised, and that is what is proved.
The affine refinement keeps the affine constraints in a separate index type — the convex
constraints in ι, the affine ones in κ, and the separating space (ι ⊕ κ) → ℝ. They enter as
equations aⱼ(x) = z(inr j) rather than inequalities, which is what makes the non-containment
clause of polyhedral separation usable, and they are modelled as E →ᵃ[ℝ] ℝ rather than as
EReal-valued convex functions. The unrefined alternative is the case κ = Empty but is proved
independently, needing only proper separation where the refinement needs the polyhedral form.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §21.
The two alternatives exclude each other: a point of C at which every fᵢ is negative
makes every term of λ₁f₁ + ⋯ + λ_mf_m non-positive, and the terms with λᵢ ≠ 0 strictly
negative.
The alternative for a finite system of strict convex inequalities. For proper convex
functions finite on ri C, exactly one of the two alternatives holds: either the strict system
fᵢ(x) < 0 is solvable in C, or a non-trivial non-negative combination of the fᵢ is
non-negative throughout C. This is the half with content; exclusivity is
not_exists_forall_neg_of_forall_zero_le_weighted.
The alternative with affine constraints #
A finite real combination of affine functions is affine along segments.
The affine step: a combination of affine functions that is non-negative on a convex set C and
non-positive at a relative interior point of C vanishes on all of C. This is the affine
analogue of eq_zero_of_nonpos_of_mem_relint, and the reason the multipliers on the convex
constraints cannot all vanish.
The alternative with affine constraints treated separately. If the affine system
a_j x ≤ 0 is solvable in ri C, then either the mixed system f_i x < 0, a_j x ≤ 0 is
solvable in C, or there are non-negative multipliers — not all of the λ_i zero — making the
combined function non-negative on C. The unrefined alternative is the case κ = Empty; what the
affine constraints buy is the sharper conclusion l ≠ 0, at the price of needing polyhedral
separation rather than proper separation.
Helly's theorem and its corollaries: finite collections #
Helly's theorem for finite collections: a finite collection of convex sets in an
n-dimensional space has a common point as soon as every n + 1 of them do. No closedness and no
recession hypothesis is needed — that is what distinguishes it from the infinite version
helly_of_no_common_recession. This is Mathlib's Convex.helly_theorem', restated.
A finite system of convex inequalities — some strict, some weak — is solvable in a convex
set C as soon as every subsystem of at most n + 1 inequalities is solvable in C. Counting is
the only fiddly point: a subcollection of at most n + 1 of the sets C, {fᵢ < 0}, {gⱼ ≤ 0}
uses at most n + 1 of the inequalities whether or not it also uses C.
The same for a system of strict inequalities only — the form the sparse alternative uses.
The multipliers can be chosen supported on at most n + 1 indices: if alternative (a)
fails, it already fails for a subsystem of at most n + 1 inequalities, and the multipliers the
alternative produces for that subsystem extend by zero — harmless in EReal because
0 · (+∞) = 0.
Weak inequalities over an arbitrary index set #
The proof runs on two prerequisites: clFn_posHomGen identifies the conjugate of the positively
homogeneous convex function k generated by h = conv {fᵢ* | i ∈ I}, and
exists_affineIndependent_of_convFn_lt extracts finitely many multipliers from h(0) < 0.
In finite dimensions a compatible pairing forces the two spaces to have equal dimension:
evalCLM B and evalCLM B.flip are surjective onto the two continuous duals, which in finite
dimensions have the dimension of the space. This is what lets the multiplier count be stated as
n + 1 with n = dim E, although Carathéodory is applied in F.
The multiplier half of the infinite alternative, isolated from the recession hypothesis.
Once the positively homogeneous convex function k generated by conv {fᵢ*} has k(0) = -∞, the
multipliers come out directly. alternative_infinite_system gets k(0) = -∞ from a recession
hypothesis; the refinement in HellyRefined.lean gets it from a polyhedral subfamily instead
(apply_zero_eq_bot_of_le_of_le), and that is the only difference between the two.
The infinite alternative over the whole space. Either the weak system fᵢ(x) ≤ 0 is
solvable, or finitely many non-negative multipliers — at most n + 1 of them non-zero — make
∑ λᵢ fᵢ bounded away from 0 from above.
With h = conv {fᵢ*} and k the positively homogeneous convex function it generates, cl k is
the support function of {x | ∀ i, fᵢ(x) ≤ 0}, which is empty when (a) fails, so (cl k)(0) = -∞;
the recession hypothesis puts 0 in ri (dom k), so k(0) = -∞; and that turns into the
multipliers. The final step is not the textbook's: the inequality ∑ λᵢ fᵢ(x) ≥ -∑ λᵢ fᵢ*(yᵢ) is
Fenchel's inequality summed termwise, using only ∑ λᵢ yᵢ = 0, so no infimal convolution is
needed.
The alternative for an infinite system of weak convex inequalities. For a collection of
closed proper convex functions indexed by an arbitrary set and a non-empty closed convex set C,
exactly one of the following holds: the weak system fᵢ(x) ≤ 0 is solvable in C, or there are
non-negative multipliers — only finitely many non-zero, and at most n + 1 of them — with
∑ λᵢ fᵢ ≥ ε > 0 throughout C. The hypothesis is that the fᵢ have no common direction of
recession which is also a direction of recession of C; a family built from two hyperbolas shows
it cannot be dropped. C is folded into the collection as its indicator function, which is why the
index type of the auxiliary system is Option ι.
Multipliers are incompatible with approximate solvability of every subsystem. Multipliers
that keep ∑ λᵢ fᵢ at least ε > 0 on C cannot coexist with subsystems solvable to within
ε / (2 ∑ λᵢ). Rockafellar normalises the multipliers to sum to 1 and argues with a strict
inequality; halving the tolerance instead makes every step non-strict, which matters because
EReal is not a cancellative ordered monoid and strict sums do not add.
Under the same recession hypothesis, an infinite system of weak convex inequalities is solvable
in C as soon as every subsystem of at most n + 1 of the inequalities is solvable in C to
within an arbitrarily small tolerance.
Helly's theorem for an infinite family. A family of non-empty closed convex sets with
no common direction of recession has a common point as soon as every n + 1 of them do. The
recession hypothesis cannot be dropped: a family built from two hyperbolas has the
(n+1)-intersection property and empty total intersection. Compare helly_finite, where the
family is finite and neither closedness nor a recession hypothesis is needed.
Helly's theorem with a bounded subfamily in place of the recession hypothesis. A family of
closed convex sets every finite subfamily of which has a common point has a common point
outright, as soon as some finite subfamily has a bounded intersection. Under that standing
hypothesis the recession and the bounded-subfamily hypotheses are equivalent
(iInter_recessionCone_eq_zero_iff_exists_isBounded), and the bounded subfamily is in practice a
single bounded K i.