The dual operations table

Every operation on convex functions has a dual operation, and conjugacy exchanges the two.

primal	dual	form
a • f	smulRight (conj B f) a	unconditional
smulRight f a	a • conj B f	unconditional
mapLin A f	compLin (conj B f) A'	unconditional
compLin g A	mapLin A' (conj B' g)	up to closure
infConv f g	conj B f + conj B g	unconditional
f + g	infConv (conj B f) (conj B g)	up to closure
convFn f	⨆ i, conj B (f i)	unconditional
⨆ i, f i	convFn fun i => conj B (f i)	up to closure

Each row appears in up to three forms. The unconditional half is an identity valid for arbitrary functions; the rows marked "up to closure" hold for closed convex functions with a clFn on the dual side; and the exact forms, in which the closure is dropped and the infimum attained, are the consequences of IsExactSum and IsExactImage in Duality/Exact.lean. Nothing in this file needs a constraint qualification.

Main results

• conj_ofEpi — the conjugate read off an epigraph-defining set.
• conj_smul, conj_smulRight — scalar multiplication is dual to right scalar multiplication.
• conj_mapLin — the image row, unconditional half; conj_compLin_eq_clFn_mapLin is the closure form.
• conj_infConv — the convolution row, unconditional half; conj_add_eq_clFn_infConv the closure form. conj_sum_toInfConvFn is the m-ary version, (f₁ □ ⋯ □ fₘ)* = ∑ fᵢ*, which says that conj B is a monoid homomorphism out of InfConvFn E.
• conj_convFn, conj_convHullFn, conj_convFn₂ — the convex-hull row, unconditional half; conj_iSup_eq_clFn_convFn the closure form.

Implementation notes

Most of the unconditional identities are proved by showing that both sides are ≤ (c : EReal) under the same condition on c — that is, by comparing the two collections of affine minorants rather than by manipulating suprema. The exception is conj_infConv, whose right-hand side is a sum, which has no such characterisation.

Each closure form is the unconditional identity for the dual operation, conjugated once more and read through Fenchel–Moreau; that is why each needs compatible topologies on both spaces and closed convex inputs.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §16.

Conjugates through the epigraph

theorem Tdaf.ConvexAnalysis.conj_ofEpi {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (S : Set (E × ℝ)) (y : F) : conj B (ofEpi S) y = ⨆ p ∈ S, ↑((B p.1) y - p.2)

The conjugate reads off an epigraph-defining set. (ofEpi S)*(y) is the supremum of ⟨x, y⟩ - μ over the points (x, μ) of S. The infimum defining ofEpi S need not be attained, so this is not a rearrangement of the supremum defining conj.

theorem Tdaf.ConvexAnalysis.conj_eq_biSup_epi {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 = ⨆ p ∈ epi f, ↑((B p.1) y - p.2)

conj_ofEpi for the epigraph itself: the conjugate is a supremum over the epigraph.

Scalar multiplication

theorem Tdaf.ConvexAnalysis.conj_smul {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {a : ℝ} (ha : 0 < a) (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : (conj B fun (x : E) => ↑a * f x) = smulRight (conj B f) a

(af)* = f*a for a > 0: ordinary scalar multiplication is dual to right scalar multiplication.

theorem Tdaf.ConvexAnalysis.conj_smulRight {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {a : ℝ} (ha : 0 < a) (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : conj B (smulRight f a) = fun (y : F) => ↑a * conj B f y

(fa)* = a(f*) for a > 0, the other half.

Linear images

theorem Tdaf.ConvexAnalysis.conj_mapLin {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [AddCommGroup H] [Module ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} (hA : IsAdjointPair B B' A A') (f : E → EReal) : conj B' (mapLin A f) = compLin (conj B f) A'

The image row, unconditional half: (Af)* = f*A'. The conjugate of an image is the inverse image of the conjugate under the transpose, with no hypothesis on f and no closure. Contrast IsExactImage.conj_compLin, the other row, which needs a constraint qualification.

Infimal convolution

theorem Tdaf.ConvexAnalysis.conj_infConv {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f g : E → EReal) : conj B (infConv f g) = conj B f + conj B g

The convolution row, unconditional half: (f □ g)* = f* + g*, with no hypothesis on f and g. The reverse row, (f + g)* = f* □ g*, is IsExactSum.conj_add and needs a constraint qualification.

@[simp]

theorem Tdaf.ConvexAnalysis.conj_indicatorFn_zero {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : conj B (indicatorFn {0}) = 0

The conjugate of δ(· | 0) is the zero function — the identity of □ goes to the identity of +, which is what makes conjugacy a monoid homomorphism here.

theorem Tdaf.ConvexAnalysis.conj_sum_toInfConvFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {ι : Type u_3} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Finset ι) (f : ι → E → EReal) : conj B (ofInfConvFn (∑ i ∈ s, toInfConvFn (f i))) = ∑ i ∈ s, conj B (f i)

The convolution row in its m-ary form: (f₁ □ ⋯ □ fₘ)* = f₁* + ⋯ + fₘ*, unconditionally. The □-product being the AddCommMonoid sum of InfConvFn E, this says that conj B is a monoid homomorphism from (E → EReal, □, δ(· | 0)) to (F → EReal, +, 0). No properness is needed, and none may be assumed: □ does not preserve it.

Convex hulls of families

theorem Tdaf.ConvexAnalysis.conj_convFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {ι : Sort u_3} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : ι → E → EReal) : conj B (convFn f) = ⨆ (i : ι), conj B (f i)

The convex-hull row, unconditional half: (conv {fᵢ})* = sup {fᵢ*}, with no hypothesis on the family. The empty family is not an exception: both sides are then ⊥.

theorem Tdaf.ConvexAnalysis.conj_convHullFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) : conj B (convHullFn g) = conj B g

A function and its convex hull have the same conjugate, since they have the same affine minorants.

theorem Tdaf.ConvexAnalysis.conj_convFn₂ {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f g : E → EReal) : conj B (convFn₂ f g) = conj B f ⊔ conj B g

The closure forms

The second row of each pair carries a closure on the dual side: (fA)* = cl(A'f*), (f + g)* = cl(f* □ g*), (sup fᵢ)* = cl conv{fᵢ*}.

theorem Tdaf.ConvexAnalysis.conj_add_eq_clFn_infConv {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {f g : E → EReal} (hf : ConvexFn f) (hfc : ClosedFn f) (hg : ConvexFn g) (hgc : ClosedFn g) : conj B (f + g) = clFn (infConv (conj B f) (conj B g))

The convolution row, closure form: (f + g)* = cl(f* □ g*) for closed convex f and g. IsExactSum.conj_add is the same statement with the closure dropped.

theorem Tdaf.ConvexAnalysis.conj_iSup_eq_clFn_convFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {ι : Sort u_3} {f : ι → E → EReal} (hf : ∀ (i : ι), ConvexFn (f i)) (hfc : ∀ (i : ι), ClosedFn (f i)) : conj B (⨆ (i : ι), f i) = clFn (convFn fun (i : ι) => conj B (f i))

The convex-hull row, closure form: (sup fᵢ)* = cl conv {fᵢ*} for a family of closed convex functions.

theorem Tdaf.ConvexAnalysis.conj_compLin_eq_clFn_mapLin {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [AddCommGroup H] [Module ℝ H] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul ℝ G] [LocallyConvexSpace ℝ G] {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 : ConvexFn g) (hgc : ClosedFn g) : conj B (compLin g A) = clFn (mapLin A' (conj B' g))

The image row, closure form: (gA)* = cl(A'g*) for closed convex g. IsExactImage.conj_compLin is the same statement with the closure dropped.