Operations that preserve convexity: the epigraph-only ones

The operations whose convexity proof needs nothing beyond the epigraph API. Those that instead read a function off a convex set in E × ℝ — infimal convolution, convex hulls of families, images under linear maps — live elsewhere.

Main results

• convexFn_iSup, ConvexFn.sup — pointwise suprema, via epi_iSup.
• ConvexFn.add, ConvexFn.sum, dom_add — sums, and the effective domain of a sum.
• ConvexFn.smul — multiplication by a nonnegative real.
• ConvexFn.comp, ConvexFn.comp_extendTop — composition with a nondecreasing convex function of one real variable.
• ConvexFn.restrict, ConvexFn.add_indicatorFn — restriction to a convex set, the same operation as adding an indicator function.

Implementation notes

Sums carry ∀ x, f x ≠ ⊥ where Rockafellar assumes properness: that is the half which avoids ∞ - ∞, and it cannot be dropped. On ℝ let f be ⊥ on Ioi 0 and ⊤ elsewhere, g be ⊥ on Iio 0 and ⊤ elsewhere; both are convex, but f + g is ⊥ off 0 and ⊤ at 0, with a nonconvex epigraph (ℝ \ {0}) ×ˢ univ. The other half, dom f nonempty, is irrelevant.

References

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

Epigraphs of suprema, sums and restrictions: no linear structure on E is used

theorem Tdaf.ConvexAnalysis.epi_iSup {E : Type u_1} {ι : Sort u_2} (f : ι → E → EReal) : (epi fun (x : E) => ⨆ (i : ι), f i x) = ⋂ (i : ι), epi (f i)

The epigraph of a pointwise supremum is the intersection of the epigraphs. Support functions are computed this way.

theorem Tdaf.ConvexAnalysis.epi_biSup {E : Type u_1} {ι : Type u_2} (s : Set ι) (f : ι → E → EReal) : (epi fun (x : E) => ⨆ i ∈ s, f i x) = ⋂ i ∈ s, epi (f i)

theorem Tdaf.ConvexAnalysis.epi_sup {E : Type u_1} (f g : E → EReal) : epi (f ⊔ g) = epi f ∩ epi g

theorem Tdaf.ConvexAnalysis.dom_add {E : Type u_1} {f g : E → EReal} (hf : ∀ (x : E), f x ≠ ⊥) (hg : ∀ (x : E), g x ≠ ⊥) : dom (f + g) = dom f ∩ dom g

The effective domain of a sum is the intersection of the effective domains. Both ≠ ⊥ hypotheses are needed: for f x = ⊥ and g x = ⊤, x lies in dom (f + g) but not in dom g.

theorem Tdaf.ConvexAnalysis.epi_restrict {E : Type u_1} (s : Set E) (f : E → EReal) : epi (restrict s f) = epi f ∩ s ×ˢ Set.univ

Convexity of the operations

theorem Tdaf.ConvexAnalysis.convexFn_const {E : Type u_1} [AddCommGroup E] [Module ℝ E] (c : EReal) : ConvexFn fun (x : E) => c

theorem Tdaf.ConvexAnalysis.convexFn_coe_linearMap {E : Type u_1} [AddCommGroup E] [Module ℝ E] (l : E →ₗ[ℝ] ℝ) : ConvexFn fun (x : E) => ↑(l x)

Its negative is convex too, which is why the functions both convex and concave are exactly the affine ones. The pairing-presented form is convexFn_affineFn.

Pointwise suprema

theorem Tdaf.ConvexAnalysis.convexFn_iSup {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Sort u_2} {f : ι → E → EReal} (h : ∀ (i : ι), ConvexFn (f i)) : ConvexFn fun (x : E) => ⨆ (i : ι), f i x

A pointwise supremum of convex functions is convex. The index is a Sort*, so the empty family is allowed: the supremum is then ⊥, whose epigraph is all of E × ℝ.

theorem Tdaf.ConvexAnalysis.convexFn_biSup {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} {s : Set ι} {f : ι → E → EReal} (h : ∀ i ∈ s, ConvexFn (f i)) : ConvexFn fun (x : E) => ⨆ i ∈ s, f i x

A pointwise supremum over an index set of convex functions is convex.

theorem Tdaf.ConvexAnalysis.ConvexFn.sup {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f g : E → EReal} (hf : ConvexFn f) (hg : ConvexFn g) : ConvexFn (f ⊔ g)

Sums

theorem Tdaf.ConvexAnalysis.ConvexFn.add {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f g : E → EReal} (hf : ConvexFn f) (hg : ConvexFn g) (hf' : ∀ (x : E), f x ≠ ⊥) (hg' : ∀ (x : E), g x ≠ ⊥) : ConvexFn (f + g)

A sum of two convex functions is convex. Where the classical statement assumes properness this needs only its ≠ ⊥ half, which prevents ∞ - ∞ and cannot be dropped; the module docstring has a counterexample.

theorem Tdaf.ConvexAnalysis.ConvexFn.sum {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} {s : Finset ι} {f : ι → E → EReal} (hf : ∀ i ∈ s, ConvexFn (f i)) (hf' : ∀ i ∈ s, ∀ (x : E), f i x ≠ ⊥) : ConvexFn fun (x : E) => ∑ i ∈ s, f i x

A finite sum of convex functions, none of which takes the value ⊥, is convex.

Multiplication by a nonnegative scalar

theorem Tdaf.ConvexAnalysis.ConvexFn.smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (a : ℝ) (ha : 0 ≤ a) (hf : ConvexFn f) : ConvexFn fun (x : E) => ↑a * f x

The case a = 0 is covered: EReal obeys the convention 0 · ∞ = 0, so (0 : EReal) * f is the zero function.

Composition with a nondecreasing convex function

noncomputable def Tdaf.ConvexAnalysis.extendTop (φ : ℝ → EReal) : EReal → EReal

φ : ℝ → EReal extended to EReal → EReal by φ (+∞) = +∞ and φ (-∞) = -∞, the choice that keeps the extension monotone; the composition rule never applies φ at ⊥.

Equations

• Tdaf.ConvexAnalysis.extendTop φ a = EReal.rec ⊥ φ ⊤ a

@[simp]

theorem Tdaf.ConvexAnalysis.extendTop_coe (φ : ℝ → EReal) (r : ℝ) : extendTop φ ↑r = φ r

@[simp]

theorem Tdaf.ConvexAnalysis.extendTop_top (φ : ℝ → EReal) : extendTop φ ⊤ = ⊤

@[simp]

theorem Tdaf.ConvexAnalysis.extendTop_bot (φ : ℝ → EReal) : extendTop φ ⊥ = ⊥

theorem Tdaf.ConvexAnalysis.monotone_extendTop {φ : ℝ → EReal} (h : Monotone φ) : Monotone (extendTop φ)

theorem Tdaf.ConvexAnalysis.ConvexFn.comp {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {φ : EReal → EReal} (hf : ConvexFn f) (hf' : ∀ (x : E), f x ≠ ⊥) (hφ : ConvexFn fun (r : ℝ) => φ ↑r) (hmono : Monotone φ) (htop : φ ⊤ = ⊤) : ConvexFn fun (x : E) => φ (f x)

A nondecreasing convex φ composed with a convex f is convex, stated for φ : EReal → EReal rather than the classical φ : ℝ → (-∞, +∞]. EReal is not an ℝ-module, so convexity of φ is required only where it is statable; off the reals the proof uses just monotonicity and φ ⊤ = ⊤. That last is not decoration — a monotone convex φ : ℝ → EReal bounded above is constant, and gluing a strictly larger finite value at ⊤ breaks convexity of φ ∘ f as soon as dom f has nonconvex complement.

theorem Tdaf.ConvexAnalysis.ConvexFn.comp_extendTop {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {φ : ℝ → EReal} (hf : ConvexFn f) (hf' : ∀ (x : E), f x ≠ ⊥) (hφ : ConvexFn φ) (hmono : Monotone φ) : ConvexFn fun (x : E) => extendTop φ (f x)

The same composition rule in its classical shape: φ is a nondecreasing convex function of one real variable, and x ↦ φ (f x) is convex under the convention φ (+∞) = +∞.

Restriction to a convex set

theorem Tdaf.ConvexAnalysis.ConvexFn.restrict {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {s : Set E} (hf : ConvexFn f) (hs : Convex ℝ s) : ConvexFn (ConvexAnalysis.restrict s f)

theorem Tdaf.ConvexAnalysis.ConvexFn.add_indicatorFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {s : Set E} (hf : ConvexFn f) (hf' : ∀ (x : E), f x ≠ ⊥) (hs : Convex ℝ s) : ConvexFn (f + indicatorFn s)

Adding the indicator function of a convex set is restriction to that set, and preserves convexity.