Closedness of a sum with a polyhedral set

The general criterion keeps C₁ + C₂ closed only when every cancelling pair of recession directions lies in both lineality spaces. If C₁ is polyhedral, the requirement on the C₁ side disappears altogether.

Main results

• isClosed_add_of_polyhedral — a nonempty polyhedral set plus a nonempty closed convex set is closed as soon as C₂ is linear in every direction of recession the two share (Theorem 20.3 in [^1]); separatesStrongly_of_polyhedral_of_recession is the separation form.
• nonempty_dom_supportFn_inter_relint — the constraint qualification that carries it, read off from polyhedral separation applied to the two barrier cones.

Implementation notes

Closedness is read off effective domains rather than from an infimal convolution formula: once IsExactSum.of_polyhedral gives (δ*(· | C₁) + δ*(· | C₂))* = δ(· | C₁) □ δ(· | C₂), the left side is δ(· | cl (C₁ + C₂)) and the domain of the right side is C₁ + C₂.

References

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

theorem Tdaf.ConvexAnalysis.polyhedral_dom_supportFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {C₁ : Set E} (h₁ : Polyhedral C₁) : Polyhedral (dom (supportFn B C₁))

The barrier cone of a polyhedral convex set is polyhedral: its support function is the conjugate of a polyhedral indicator, hence polyhedral, and the effective domain of a polyhedral function is polyhedral.

theorem Tdaf.ConvexAnalysis.zero_mem_dom_supportFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {C₁ : Set E} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (hne : C₁.Nonempty) : 0 ∈ dom (supportFn B C₁)

theorem Tdaf.ConvexAnalysis.nonempty_dom_supportFn_inter_relint {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {C₁ C₂ : Set E} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (h₁ : Polyhedral C₁) (hne₁ : C₁.Nonempty) (h₂ : Convex ℝ C₂) (hcl₂ : IsClosed C₂) (hne₂ : C₂.Nonempty) (hrec : ∀ v ∈ recessionCone C₁, -v ∈ recessionCone C₂ → v ∈ recessionCone C₂) : (dom (supportFn B C₁) ∩ intrinsicInterior ℝ (dom (supportFn B C₂))).Nonempty

The constraint qualification. Under the recession hypothesis the barrier cone of C₁ meets the relative interior of the barrier cone of C₂. This is where polyhedrality of C₁ is spent: otherwise polyhedral separation separates the two barrier cones by a hyperplane, whose normal is a recession direction violating the hypothesis.

theorem Tdaf.ConvexAnalysis.isClosed_add_of_polyhedral {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {C₁ C₂ : Set E} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (h₁ : Polyhedral C₁) (hne₁ : C₁.Nonempty) (h₂ : Convex ℝ C₂) (hcl₂ : IsClosed C₂) (hne₂ : C₂.Nonempty) (hrec : ∀ v ∈ recessionCone C₁, -v ∈ recessionCone C₂ → v ∈ recessionCone C₂) : IsClosed (C₁ + C₂)

Let C₁ be a nonempty polyhedral convex set and C₂ a nonempty closed convex set. If every direction of recession of C₁ whose opposite recedes C₂ is itself a direction of recession of C₂ — that is, a direction in which C₂ is linear — then C₁ + C₂ is closed. The general criterion asks in addition that such a direction lie in the lineality space of C₁; polyhedrality of C₁ removes that requirement.

theorem Tdaf.ConvexAnalysis.separatesStrongly_of_polyhedral_of_recession {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {C₁ C₂ : Set E} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (h₁ : Polyhedral C₁) (hne₁ : C₁.Nonempty) (h₂ : Convex ℝ C₂) (hcl₂ : IsClosed C₂) (hne₂ : C₂.Nonempty) (hdisj : Disjoint C₁ C₂) (hrec : ∀ v ∈ recessionCone C₁, v ∈ recessionCone C₂ → -v ∈ recessionCone C₂) : ∃ (f : E →L[ℝ] ℝ) (c : ℝ), SeparatesStrongly f c C₁ C₂

Two disjoint sets, one polyhedral and the other closed, can be separated strongly as soon as their only common direction of recession is one in which the closed one is linear. The general criterion asks for no common direction of recession at all; when both sets are polyhedral (separatesStrongly_of_polyhedral) no recession hypothesis is needed.