Conjugates of polyhedral convex functions

The conjugate of a polyhedral convex function is polyhedral.

The proof uses the Minkowski–Weyl dictionary once in each direction. Write epi f = conv P + cone D with P and D finite. An affine function x ↦ ⟨x, y⟩ - c lies below f exactly when the linear functional p ↦ ⟨p.1, y⟩ - p.2 is bounded by c on epi f, and on a sum of a convex hull and a cone that is two finite families of conditions: ⟨p.1, y⟩ - c ≤ p.2 for the generating points p ∈ P, and ⟨d.1, y⟩ ≤ d.2 for the generating directions d ∈ D. Both are linear in (y, c), so they cut epi (conj B f) out of F × ℝ as a polyhedral set.

Main results

• mem_epi_conj_iff — the epigraph of conj B f, read off epi f, with no hypothesis on f. In particular none excluding f x = ⊥: in that case both sides are false.
• PolyhedralFn.conj — the conjugate of a polyhedral convex function is polyhedral (Theorem 19.2 in [^1]). The case P = ∅ is separate: then f ≡ ⊤ and epi (conj B f) is all of F × ℝ, whereas the generator argument needs a base point to slide along a recession direction.

References

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

def Tdaf.ConvexAnalysis.epiFunctional {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (x : E) : F × ℝ →ₗ[ℝ] ℝ

The linear functional (y, c) ↦ ⟨x, y⟩ - c on F × ℝ, one for each generating point x of epi f.

Equations

• Tdaf.ConvexAnalysis.epiFunctional B x = B x ∘ₗ LinearMap.fst ℝ F ℝ - LinearMap.snd ℝ F ℝ

@[simp]

theorem Tdaf.ConvexAnalysis.epiFunctional_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (x : E) (q : F × ℝ) : (epiFunctional B x) q = (B x) q.1 - q.2

def Tdaf.ConvexAnalysis.dirFunctional {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (x : E) : F × ℝ →ₗ[ℝ] ℝ

The linear functional (y, c) ↦ ⟨x, y⟩ on F × ℝ, one for each generating direction x of epi f.

Equations

• Tdaf.ConvexAnalysis.dirFunctional B x = B x ∘ₗ LinearMap.fst ℝ F ℝ

@[simp]

theorem Tdaf.ConvexAnalysis.dirFunctional_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (x : E) (q : F × ℝ) : (dirFunctional B x) q = (B x) q.1

def Tdaf.ConvexAnalysis.recFunctional {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (y : F) : E × ℝ →ₗ[ℝ] ℝ

The linear functional p ↦ ⟨p.1, y⟩ - p.2 on E × ℝ, whose boundedness on epi f is what the conjugate measures.

Equations

• Tdaf.ConvexAnalysis.recFunctional B y = B.flip y ∘ₗ LinearMap.fst ℝ E ℝ - LinearMap.snd ℝ E ℝ

@[simp]

theorem Tdaf.ConvexAnalysis.recFunctional_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (y : F) (p : E × ℝ) : (recFunctional B y) p = (B p.1) y - p.2

theorem Tdaf.ConvexAnalysis.mem_epi_conj_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {q : F × ℝ} : q ∈ epi (conj B f) ↔ ∀ p ∈ epi f, (B p.1) q.1 - q.2 ≤ p.2

The epigraph of a conjugate. (y, c) lies over conj B f exactly when the linear functional p ↦ ⟨p.1, y⟩ - p.2 is bounded by c on epi f. This is conj_le_coe_iff with the affine minorant traded for its epigraph, and it holds with no hypothesis on f.

theorem Tdaf.ConvexAnalysis.PolyhedralFn.conj {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [FiniteDimensional ℝ E] (hf : PolyhedralFn f) : PolyhedralFn (ConvexAnalysis.conj B f)

The conjugate of a polyhedral convex function is polyhedral.

epi f = conv P + cone D turns the condition "x ↦ ⟨x, y⟩ - c lies below f" into finitely many linear inequalities on (y, c): one per generating point, one per generating direction.