The continuity constraint qualification

If one of two proper convex functions is continuous at a point where the other is finite, they add exactly: (f + g)* = f* □ g*, with the infimal convolution attained.

The classical qualification (Theorem 16.4 in [^1]) asks instead that ri (dom f) and ri (dom g) meet, which is sharp in finite dimensions but is not available in general, ri being empty for most infinite-dimensional convex sets. Continuity is the condition that replaces it, and the one every application in a Banach space actually verifies — typically because one summand is finite and continuous everywhere.

Main results

• IsExactSum.of_continuousAt — the qualification, the third constructor of IsExactSum alongside IsExactSum.of_relint (finite dimensions) and IsExactSum.of_polyhedral.

Implementation notes

The only topological input is geometric_hahn_banach_open, which separates a nonempty open convex set from a disjoint convex set in any real topological vector space; local convexity, which is what separating two closed sets needs, is not required. Continuity at x₀ is what supplies the open set: it makes f bounded above near x₀, so the strict epigraph of f has interior.

With a = (f + g)* y finite, the hypothesis to be contradicted is f x + g x < ⟨x, y⟩ - a, so the two sets separated are the strict epigraph of f and the hypograph of the concave function x ↦ ⟨x, y⟩ - a - g x. The separating functional is non-vertical, and its ℝ-coefficient is negative rather than positive because the strict epigraph is unbounded upwards.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §16.

theorem Tdaf.ConvexAnalysis.ConvexFn.convex_strictEpi {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) : Convex ℝ {p : E × ℝ | f p.1 < ↑p.2}

The strict epigraph of a convex function is convex: the strict form of the epigraph inequality (convexFn_iff_forall_lt) read as a statement about a set.

theorem Tdaf.ConvexAnalysis.IsExactSum.of_continuousAt {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {f g : E → EReal} (hf : ConvexFn f) (hpf : Proper f) (hg : ConvexFn g) (hpg : Proper g) {x₀ : E} (hfx₀ : x₀ ∈ dom f) (hgx₀ : x₀ ∈ dom g) (hcont : ContinuousAt f x₀) : IsExactSum B f g

The continuity constraint qualification. If f and g are proper convex functions and f is continuous at some point where both are finite, then f and g add exactly. This is the constructor of IsExactSum that survives into infinite dimensions.