Conjugates of concave functions

The concave conjugate of g : E → EReal is g*(y) = inf_x (⟨x, y⟩ - g x), the mirror of the convex conjugate with inf, ≥ and -∞ in place of sup, ≤ and +∞. Convex and concave duality are used together throughout — the dual objective of a convex program is the concave conjugate of -inf F, and Fenchel's duality theorem pairs a convex f against a concave g — so the concave conjugate needs a name of its own rather than being spelled through -g at every use.

The sign trap. g* ≠ -(-g)*. What is true is g*(y) = -(-g)*(-y): there is a reflection on the dual side as well. neg_concaveConj is the dictionary, and every result below is derived through it.

Main definitions

• concaveConj B g, biconcaveConj B g — the concave conjugate g* and biconjugate g**.
• clConcave g, ClosedConcaveFn g — the concave closure -(cl (-g)), the upper semicontinuous hull that Rockafellar also writes cl g, and the functions fixed by it.

Main results

• neg_concaveConj, concaveConj_eq_neg_conj_neg, conj_eq_neg_concaveConj_neg — the sign dictionary, in both directions, with no side condition.
• add_concaveConj_le — Fenchel's inequality g x + g*(y) ≤ ⟨x, y⟩. Unconditional, unlike the convex le_add_conj: the collapsing sum ⊤ + ⊥ = ⊥ falls on the smaller side here.
• coe_le_concaveConj_iff, le_concaveConj_iff — c ≤ g*(y) says exactly that the affine function x ↦ ⟨x, y⟩ - c lies above g; and concaveConj B is adjoint to concaveConj B.flip. Every concave conjugate is concave (concaveFn_concaveConj).
• biconcaveConj_eq_clConcave — Fenchel–Moreau for concave functions: the concave biconjugate is the concave closure. The double reflection cancels on the way (biconcaveConj_eq_neg_biconj_neg: g** = -(-g)**, with no sign on the argument).

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §12, §30, §31.

The concave conjugate

noncomputable def Tdaf.ConvexAnalysis.concaveConj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) : F → EReal

The concave conjugate of g with respect to the pairing B: g*(y) = inf_x (⟨x, y⟩ - g x). This is not -(conj B (-g)); the dictionary g*(y) = -(-g)*(-y) is concaveConj_eq_neg_conj_neg.

Equations

• Tdaf.ConvexAnalysis.concaveConj B g y = ⨅ (x : E), ↑((B x) y) - g x

@[reducible, inline]

noncomputable abbrev Tdaf.ConvexAnalysis.biconcaveConj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) : E → EReal

Equations

• Tdaf.ConvexAnalysis.biconcaveConj B g = Tdaf.ConvexAnalysis.concaveConj B.flip (Tdaf.ConvexAnalysis.concaveConj B g)

theorem Tdaf.ConvexAnalysis.concaveConj_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) (y : F) : concaveConj B g y = ⨅ (x : E), ↑((B x) y) - g x

theorem Tdaf.ConvexAnalysis.biconcaveConj_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) (x : E) : biconcaveConj B g x = ⨅ (y : F), ↑((B x) y) - concaveConj B g y

theorem Tdaf.ConvexAnalysis.concaveConj_le_sub {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) (x : E) (y : F) : concaveConj B g y ≤ ↑((B x) y) - g x

Fenchel's inequality for concave functions, ∞ - ∞-free: it holds for every g, x and y.

The sign dictionary

theorem Tdaf.ConvexAnalysis.neg_concaveConj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) (y : F) : -concaveConj B g y = conj B (fun (x : E) => -g x) (-y)

The dictionary between the two conjugates: -g*(y) = (-g)*(-y). Both the values and the arguments are reflected; only one of the two reflections is visible in the informal statement g*(y) = -(-g)*(-y).

theorem Tdaf.ConvexAnalysis.concaveConj_eq_neg_conj_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) (y : F) : concaveConj B g y = -conj B (fun (x : E) => -g x) (-y)

The dictionary, solved for the concave conjugate: g*(y) = -(-g)*(-y).

theorem Tdaf.ConvexAnalysis.conj_eq_neg_concaveConj_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (y : F) : conj B f y = -concaveConj B (fun (x : E) => -f x) (-y)

The dictionary in the other direction: f*(y) = -(-f)*(-y), where the starred operation on the right is the concave conjugate.

Order-theoretic API

theorem Tdaf.ConvexAnalysis.coe_le_concaveConj_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {y : F} {c : ℝ} : ↑c ≤ concaveConj B g y ↔ g ≤ affineFn B y c

c ≤ g*(y) says exactly that the affine function x ↦ ⟨x, y⟩ - c lies above g. The mirror of conj_le_coe_iff, and like it unconditional.

theorem Tdaf.ConvexAnalysis.concaveConj_antitone {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : Antitone (concaveConj B)

theorem Tdaf.ConvexAnalysis.le_concaveConj_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {h : F → EReal} : h ≤ concaveConj B g ↔ g ≤ concaveConj B.flip h

The adjunction. h ≤ g* and g ≤ h* say the same thing, namely that g x + h y ≤ ⟨x, y⟩ for all x and y in the ∞ - ∞-free reading.

theorem Tdaf.ConvexAnalysis.le_biconcaveConj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) : g ≤ biconcaveConj B g

The biconjugate is always a majorant: g ≤ g**, with no hypothesis on g.

The improper cases

theorem Tdaf.ConvexAnalysis.concaveConj_eq_top_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {y : F} : concaveConj B g y = ⊤ ↔ ∀ (x : E), g x = ⊥

g* takes the value ⊤ at a point exactly when g ≡ -∞ — a condition independent of the point.

theorem Tdaf.ConvexAnalysis.concaveConj_of_eq_top {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x₀ : E} (hx : g x₀ = ⊤) : concaveConj B g = fun (x : F) => ⊥

If g takes the value +∞ anywhere, its concave conjugate is identically -∞.

theorem Tdaf.ConvexAnalysis.concaveConj_bot {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : (concaveConj B fun (x : E) => ⊥) = fun (x : F) => ⊤

theorem Tdaf.ConvexAnalysis.concaveConj_top {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : (concaveConj B fun (x : E) => ⊤) = fun (x : F) => ⊥

theorem Tdaf.ConvexAnalysis.concaveConj_ne_top {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} (hd : (domConcave g).Nonempty) (y : F) : concaveConj B g y ≠ ⊤

g* never takes the value ⊤ when g has nonempty effective domain.

theorem Tdaf.ConvexAnalysis.add_concaveConj_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) (x : E) (y : F) : g x + concaveConj B g y ≤ ↑((B x) y)

Fenchel's inequality for concave functions: g x + g*(y) ≤ ⟨x, y⟩.

Needs no properness, unlike its convex mirror le_add_conj: the collapse ⊤ + ⊥ = ⊥ happens here on the smaller side of the inequality, where ⊥ is harmless.

Concavity of the concave conjugate

theorem Tdaf.ConvexAnalysis.concaveFn_concaveConj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) : ConcaveFn (concaveConj B g)

The concave conjugate of an arbitrary function is concave, with no hypothesis on g.

The biconjugate

theorem Tdaf.ConvexAnalysis.biconcaveConj_eq_neg_biconj_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) (x : E) : biconcaveConj B g x = -biconj B (fun (x' : E) => -g x') x

The double reflection cancels: g** = -(-g)**, with no sign on the argument, the reflection introduced on the dual side by the first conjugation being undone by the second.

The concave closure

noncomputable def Tdaf.ConvexAnalysis.clConcave {E : Type u_1} [TopologicalSpace E] (g : E → EReal) : E → EReal

The concave closure: the counterpart of clFn obtained by conjugating it with negation. Rockafellar writes cl g for it too; here it needs a name of its own.

Equations

• Tdaf.ConvexAnalysis.clConcave g x = -Tdaf.ConvexAnalysis.clFn (fun (z : E) => -g z) x

theorem Tdaf.ConvexAnalysis.clConcave_apply {E : Type u_1} [TopologicalSpace E] (g : E → EReal) (x : E) : clConcave g x = -clFn (fun (z : E) => -g z) x

@[simp]

theorem Tdaf.ConvexAnalysis.neg_clConcave {E : Type u_1} [TopologicalSpace E] (g : E → EReal) (x : E) : -clConcave g x = clFn (fun (z : E) => -g z) x

theorem Tdaf.ConvexAnalysis.clConcave_neg {E : Type u_1} [TopologicalSpace E] (f : E → EReal) (x : E) : clConcave (fun (z : E) => -f z) x = -clFn f x

theorem Tdaf.ConvexAnalysis.clConcave_mono {E : Type u_1} [TopologicalSpace E] {g₁ g₂ : E → EReal} (h : g₁ ≤ g₂) : clConcave g₁ ≤ clConcave g₂

def Tdaf.ConvexAnalysis.ClosedConcaveFn {E : Type u_1} [TopologicalSpace E] (g : E → EReal) : Prop

g is concave-closed when it equals its concave closure.

Equations

• Tdaf.ConvexAnalysis.ClosedConcaveFn g = (Tdaf.ConvexAnalysis.clConcave g = g)

theorem Tdaf.ConvexAnalysis.closedConcaveFn_iff {E : Type u_1} [TopologicalSpace E] {g : E → EReal} : ClosedConcaveFn g ↔ ClosedFn fun (z : E) => -g z

theorem Tdaf.ConvexAnalysis.le_clConcave {E : Type u_1} [TopologicalSpace E] (g : E → EReal) : g ≤ clConcave g

theorem Tdaf.ConvexAnalysis.closedConcaveFn_clConcave {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] (g : E → EReal) : ClosedConcaveFn (clConcave g)

theorem Tdaf.ConvexAnalysis.clConcave_idem {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] (g : E → EReal) : clConcave (clConcave g) = clConcave g

theorem Tdaf.ConvexAnalysis.concaveFn_clConcave {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {g : E → EReal} (hg : ConcaveFn g) : ConcaveFn (clConcave g)

Fenchel–Moreau for concave functions

theorem Tdaf.ConvexAnalysis.biconcaveConj_eq_neg_clFn_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {g : E → EReal} (hg : ConcaveFn g) : biconcaveConj B g = fun (x : E) => -clFn (fun (x' : E) => -g x') x

Fenchel–Moreau for concave functions. The concave biconjugate of a concave function is its concave closure, spelled out as -(cl (-g)).

theorem Tdaf.ConvexAnalysis.biconcaveConj_eq_clConcave {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {g : E → EReal} (hg : ConcaveFn g) : biconcaveConj B g = clConcave g

Fenchel–Moreau for concave functions, stated against clConcave: g** = cl g.

theorem Tdaf.ConvexAnalysis.biconcaveConj_eq_self {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {g : E → EReal} (hg : ConcaveFn g) (hc : ClosedFn fun (x : E) => -g x) : biconcaveConj B g = g

A closed concave function — one whose negative is a closed convex function — is its own concave biconjugate.