Polyhedral constraint qualifications

The constraint qualifications for exact conjugate addition weaken when one of the two functions is polyhedral: where Duality/Relint.lean asks for a common relative interior point of the two effective domains, the polyhedral side here contributes only a point of its effective domain.

Main results

• IsExactSum.of_polyhedral_pair — both functions polyhedral: no relative interiors at all, only dom f ∩ dom g ≠ ∅.
• IsExactSum.of_polyhedral — a proper polyhedral f and a proper convex g add exactly as soon as dom f meets ri (dom g) (Theorem 20.1 in [^1]). IsExactSum.of_polyhedral_closed is the closed case, which carries the argument, and relint_inter_relint_nonempty_of_subset_affineSpan is the relative-interior step it turns on.
• IsExactFinsetSum.of_polyhedral — the same for m summands; polyhedralFn_finsetSum, a finite sum of proper polyhedral functions being polyhedral, makes the polyhedral block one summand.
• IsExactImage.of_polyhedral — the same weakening on the image side: a proper polyhedral g pulls back exactly as soon as the range of A meets dom g. This is what gives the general image and subgradient rules their polyhedral clauses.
• epi_mapLin_of_polyhedralFn, polyhedralFn_mapLin, exists_mapLin_eq_of_polyhedralFn, polyhedralFn_compLin — the image Af is polyhedral, the infimum defining it is attained, and the composite gA is polyhedral.

Implementation notes

The pair case is the proof of of_relint with its closedness criterion replaced by polyhedrality: both need epi f* + epi g* closed, and here that is free, a sum of polyhedral sets being polyhedral and closed. ClosedFn is a hypothesis on neither side, a proper polyhedral convex function being automatically closed. The general case is the classical reduction, run on an indicator: with M = aff (dom g) and δ = δ(· | M), the function δ + f is polyhedral and M ∩ dom f does meet ri (dom g), so of_relint applies to δ + f and g; the leftover δ* is then re-absorbed, since δ + g = g and δ + (f + g) = f + g.

References

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

theorem Tdaf.ConvexAnalysis.PolyhedralFn.closedProperConvexFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : PolyhedralFn f) (hpf : Proper f) : ClosedProperConvexFn f

A proper polyhedral convex function is a closed proper convex function.

theorem Tdaf.ConvexAnalysis.IsExactSum.of_polyhedral_pair {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hf : PolyhedralFn f) (hpf : Proper f) (hg : PolyhedralFn g) (hpg : Proper g) {x₀ : E} (hxf : x₀ ∈ dom f) (hxg : x₀ ∈ dom g) : IsExactSum B f g

The all-polyhedral case: two proper polyhedral convex functions add exactly as soon as their effective domains meet, with no relative interior on either side. This is the case k = m, to which the general form is reduced.

theorem Tdaf.ConvexAnalysis.indicatorFn_add_eq_self {E : Type u_1} {C : Set E} {k : E → EReal} (hsub : dom k ⊆ C) : indicatorFn C + k = k

An indicator function is absorbed by any function whose effective domain it contains. This is the algebraic device the reduction below runs on: with M = aff (dom g) both indicatorFn M + g and indicatorFn M + (f + g) collapse. No properness is needed — off C the sum is ⊤ + ⊤.

theorem Tdaf.ConvexAnalysis.relint_inter_relint_nonempty_of_subset_affineSpan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {D₁ D₂ : Set E} (h₁ : Convex ℝ D₁) (h₂ : Convex ℝ D₂) (hsub : D₁ ⊆ ↑(affineSpan ℝ D₂)) {x₀ : E} (hx₁ : x₀ ∈ D₁) (hx₂ : x₀ ∈ intrinsicInterior ℝ D₂) : (intrinsicInterior ℝ D₁ ∩ intrinsicInterior ℝ D₂).Nonempty

The relative-interior step the reduction below turns on. If a convex set D₁ lies in the affine hull of a convex set D₂ and the two share a point x₀ of ri D₂, then ri D₁ and ri D₂ already share a point.

x₀ need not itself be in ri D₁, but ri D₂ is a relatively open neighbourhood of x₀ inside aff D₂ ⊇ aff D₁, so a small push from x₀ towards any point of ri D₁ lands in both.

theorem Tdaf.ConvexAnalysis.IsExactSum.of_polyhedral_closed {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hf : PolyhedralFn f) (hpf : Proper f) (hg : ClosedProperConvexFn g) {x₀ : E} (hxf : x₀ ∈ dom f) (hxg : x₀ ∈ intrinsicInterior ℝ (dom g)) : IsExactSum B f g

A proper polyhedral convex function and a closed proper convex function add exactly as soon as dom f meets ri (dom g): the polyhedral side contributes only a point of its effective domain, not of its relative interior.

With M = aff (dom g), δ = δ(· | M) and h = δ + f, ri (dom h) does meet ri (dom g), so of_relint splits (h + g)* = (f + g)* exactly; the pair case splits h* as δ* □ f*, and δ* □ g* = (δ + g)* = g* re-absorbs the leftover δ*.

theorem Tdaf.ConvexAnalysis.IsExactSum.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 →ₗ[ℝ] ℝ} {f g : E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hf : PolyhedralFn f) (hpf : Proper f) (hg : ConvexFn g) (hpg : Proper g) {x₀ : E} (hxf : x₀ ∈ dom f) (hxg : x₀ ∈ intrinsicInterior ℝ (dom g)) : IsExactSum B f g

A proper polyhedral convex function and a proper convex function add exactly as soon as dom f meets ri (dom g). Neither closedness of g nor a relative interior point of dom f is needed.

The reduction to IsExactSum.of_polyhedral_closed runs through the conjugate form conj_add_eq_conj_clFn_add_clFn, whose two segment hypotheses are met on opposite grounds: f is closed proper (only x₀ ∈ dom f needed) and g is proper convex (x₀ ∈ ri (dom g)). That asymmetry is the asymmetry of the theorem itself.

Exact addition of m summands

theorem Tdaf.ConvexAnalysis.polyhedralFn_finsetSum {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Finset ι} {f : ι → E → EReal} (hs : s.Nonempty) (hpoly : ∀ i ∈ s, PolyhedralFn (f i)) (hbot : ∀ i ∈ s, ∀ (x : E), f i x ≠ ⊥) : PolyhedralFn (∑ i ∈ s, f i)

A finite non-empty sum of proper polyhedral convex functions is polyhedral.

theorem Tdaf.ConvexAnalysis.IsExactFinsetSum.of_polyhedral_pair {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Finset ι} {f : ι → E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hs : s.Nonempty) (hpoly : ∀ i ∈ s, PolyhedralFn (f i)) (hpf : ∀ i ∈ s, Proper (f i)) {x₀ : E} (hx₀ : ∀ i ∈ s, x₀ ∈ dom (f i)) : IsExactFinsetSum B s f

The all-polyhedral case, for m summands: finitely many proper polyhedral convex functions add exactly as soon as their effective domains have a point in common.

theorem Tdaf.ConvexAnalysis.IsExactFinsetSum.of_polyhedral {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s t u : Finset ι} {f : ι → E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hs : s.Nonempty) (hdisj : Disjoint t u) (hmem : ∀ (i : ι), i ∈ s ↔ i ∈ t ∨ i ∈ u) (hpoly : ∀ i ∈ t, PolyhedralFn (f i)) (hconv : ∀ i ∈ u, ConvexFn (f i)) (hpf : ∀ i ∈ s, Proper (f i)) {x₀ : E} (hxt : ∀ i ∈ t, x₀ ∈ dom (f i)) (hxu : ∀ i ∈ u, x₀ ∈ intrinsicInterior ℝ (dom (f i))) : IsExactFinsetSum B s f

The m-ary form: let f₁, …, fₘ be proper convex with f₁, …, f_k polyhedral, and suppose

dom f₁ ∩ ⋯ ∩ dom f_k ∩ ri (dom f_{k+1}) ∩ ⋯ ∩ ri (dom fₘ) ≠ ∅.

Then f₁, …, fₘ add exactly.

t is {1, …, k} and u is its complement; the splitting is spelled membership-wise rather than as s = t ∪ u so that no DecidableEq instance enters the statement. ∑_{i ∈ t} fᵢ is polyhedral and adds exactly to ∑_{i ∈ u} fᵢ by the binary case, while each block adds exactly on its own — the polyhedral one by the all-polyhedral case, the other by the relative-interior criterion.

The polyhedral companion of the image rule

theorem Tdaf.ConvexAnalysis.epi_mapLin_of_polyhedralFn {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] {f : E → EReal} (hf : PolyhedralFn f) (A : E →ₗ[ℝ] G) : epi (mapLin A f) = ⇑(A.prodMap LinearMap.id) '' epi f

An identity of epigraphs: for a polyhedral f the epigraph of the image Af really is the image of epi f under (x, μ) ↦ (Ax, μ).

In general epi (Af) is only the epigraph closure of that image, because an infimum need not be attained. Here the image is polyhedral, hence closed, and a closed set with upward-closed vertical sections is already an epigraph. Both conclusions — polyhedrality of Af and attainment of the infimum — fall out of this one identity.

theorem Tdaf.ConvexAnalysis.polyhedralFn_mapLin {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] {f : E → EReal} (hf : PolyhedralFn f) (A : E →ₗ[ℝ] G) : PolyhedralFn (mapLin A f)

The image of a polyhedral convex function under a linear transformation is polyhedral. By epi_mapLin_of_polyhedralFn, epi (Af) is the image of epi f, and a linear image of a polyhedral set is polyhedral.

theorem Tdaf.ConvexAnalysis.polyhedralFn_compLin {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {g : G → EReal} (hg : PolyhedralFn g) (A : E →ₗ[ℝ] G) : PolyhedralFn (compLin g A)

A polyhedral convex function composed with a linear map is polyhedral. epi (gA) is epi g pulled back along (x, μ) ↦ (A x, μ), and a preimage of a polyhedral set under a linear map is polyhedral (Polyhedral.comap).

This is much the cheaper direction: pulling back needs neither closedness nor attainment, so no finite dimension is used on either side.

theorem Tdaf.ConvexAnalysis.exists_mapLin_eq_of_polyhedralFn {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] {f : E → EReal} (hf : PolyhedralFn f) (A : E →ₗ[ℝ] G) {y : G} {μ : ℝ} (hy : mapLin A f y = ↑μ) : ∃ (x : E), A x = y ∧ f x = mapLin A f y

The attainment clause: wherever (Af)(y) is finite the infimum defining it is attained, some x in the fibre over y realising the value. By epi_mapLin_of_polyhedralFn the point (y, μ) of epi (Af) is literally an image point.

theorem Tdaf.ConvexAnalysis.IsExactImage.of_polyhedral {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} {g : G → EReal} [IsCompatiblePairing B'] [IsCompatiblePairing B.flip] (hA : IsAdjointPair B B' A A') (hg : PolyhedralFn g) (hp : Proper g) {x₀ : E} (hx₀ : A x₀ ∈ dom g) : IsExactImage B B' A A' hA g

The companion on the image side: a proper polyhedral g pulls back exactly along A as soon as the range of A meets dom g — no relative interior anywhere, exactly as on the sum side.

None of the sum theory is used. g* is polyhedral, so A' g* is polyhedral and therefore closed, and the general image rule's closure formula has nothing left to close; the same fact attains the infimum over the fibre. Properness of g enters twice and cheaply: it makes g closed, and A x₀ ∈ dom g stops (g A)* from being -∞.