Rockafellar, §5: Functional Operations #
The operations that build new convex functions out of old: outer composition, addition, infimal
convolution □, pointwise suprema, the convex hull of a collection, and image and inverse image
under a linear map. All 8 numbered results of §5 are formalized.
Theorems 5.7 and 5.8 carry no letter labels in the book, so the declaration suffixes are the
book's own symbols: gA and Ah for 5.7, and the four displayed function names f, g, h,
k for 5.8. ℝⁿ⁺¹ is Rn n × ℝ here, which is what "a convex set F in ℝⁿ⁺¹" means when
Theorem 5.3 goes on to write (x, μ) ∈ F.
Two traps #
Properness is not preserved by □. No declaration here concludes properness of an infimal
convolute, and exists_not_proper_infimalConvolution is the witness: f x = ⟨v, x⟩ and
g x = -⟨v, x⟩ are proper convex with f □ g ≡ -∞. That is also why the backbone defines □ by
adding epigraphs rather than by the infimum formula, which would be ∞ - ∞;
infimalConvolution_apply recovers the formula under properness.
f0 is defined by cases, as in the book: rightSMul_zero gives f0 = δ(· | 0) when
f ≢ +∞, and rightSMul_zero_of_top gives f0 = f when f ≡ +∞. hom_apply_smul is where
that case split meets §4's 0 · ∞ = 0, and the two agree.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §5.
Linear functionals on ℝⁿ #
Two small pieces of ℝⁿ bookkeeping that the examples of this section need and that the backbone,
which is written for a general topological vector space, has no reason to carry.
The j-th coordinate of ℝⁿ, as a linear functional.
Equations
- Rockafellar.coordFunctional n j = { toFun := fun (x : TdafSurface.Rn n) => x.ofLp j, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Theorem 5.1 #
Theorem 5.1. For convex f : ℝⁿ → (-∞, +∞] and non-decreasing convex φ : ℝ → (-∞, +∞],
φ ∘ f is convex. extendTop φ is φ extended by the book's convention φ (+∞) = +∞.
Theorem 5.2 #
Theorem 5.2. The sum of two proper convex functions is convex. Properness is there only
to avoid ∞ - ∞, and only its ≠ -∞ half is used.
Theorem 5.3 #
Theorem 5.3. The lower boundary f x = inf {μ | (x, μ) ∈ F} of a convex set F in
ℝⁿ⁺¹ is a convex function. ℝⁿ⁺¹ is read as Rn n × ℝ.
Theorem 5.4 #
A convex function of a single coordinate of (ℝⁿ)ᵐ is convex as a function of the whole
tuple: this is the inverse image under the i-th projection, Theorem 5.7.
The linear map (x₁, …, xₘ) ↦ x₁ + ⋯ + xₘ on (ℝⁿ)ᵐ. Every m-ary operation of this
section that "adds in x" is an image under this map, in the sense of Theorem 5.7.
Equations
- Rockafellar.sumLin n m = ∑ i : Fin m, LinearMap.proj i
Instances For
Theorem 5.4. For proper convex f₁, …, fₘ, the infimal convolute
f x = inf {f₁x₁ + ⋯ + fₘxₘ | x₁ + ⋯ + xₘ = x} is convex. Properness is used only through its
≠ -∞ half, which is what makes the sum unambiguous.
Infimal convolution #
Rockafellar, §5, after Theorem 5.4: "The function f in Theorem 5.4 will be denoted by
f₁ □ f₂ □ ⋯ □ fₘ. The operation □ is called infimal convolution."
Infimal convolution f □ g, defined by addition of epigraphs rather than by the infimum
formula (f □ g) x = ⨅ y, f (x - y) + g y, which is ill-formed when f or g takes the value
⊥. The formula is infConv_apply.
Equations
- Rockafellar.«term_□_» = Lean.ParserDescr.trailingNode `Rockafellar.«term_□_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " □ ") (Lean.ParserDescr.cat `term 66))
Instances For
Theorem 5.4, binary case: f □ g is convex whenever f and g are. No properness is
needed, the epigraph definition f □ g = ofEpi (epi f + epi g) being Theorem 5.3 applied to a sum
of convex sets; the book's properness is what makes the infimum formula meaningful.
For two functions, (f □ g) x = infᵧ {f (x - y) + g y} — the analogue of the classical
formula for integral convolution. Properness is what makes the right-hand side unambiguous; □
is defined through epigraph addition, as in the book, because this infimum produces the
forbidden ∞ - ∞ when one function reaches -∞.
Rockafellar, §5. "The effective domain of f □ g is the sum of dom f and dom g." It
needs no hypothesis at all.
Rockafellar, §5. "f □ δ(· | a) is the function whose graph is obtained by translating
the graph of f horizontally by a."
Infimal convolution is commutative and associative on all functions ℝⁿ → [-∞, +∞], with
δ(· | 0) as identity: the monoid structure lives on the type synonym InfConvFn (Rn n).
Properness is not preserved by □. For v ≠ 0 the pair f x = ⟨v, x⟩, g x = -⟨v, x⟩
is finite, hence proper, and convex, while (f □ g) x = -∞ everywhere. This is why no result of
§5 concludes properness of an infimal convolute.
Left and right scalar multiplication #
Rockafellar, §5: (λf) x = λ (f x) for λ ≥ 0, and fλ is the function obtained from
Theorem 5.3 with F = λ (epi f).
Non-negative left scalar multiplication (λ f) x = λ (f x) preserves convexity. EReal
obeys the book's 0 · ∞ = 0, so λ = 0 is not a special case.
Rockafellar, §5. Right scalar multiplication preserves convexity: fλ is Theorem 5.3
applied to the convex set λ (epi f).
Rockafellar, §5, first branch of the definition of fλ:
(fλ) x = λ f (λ⁻¹ x) for λ > 0.
Right scalar multiplication at zero: (f0) x = δ(x | 0) provided f ≢ +∞. The side
condition is the book's own and is not decoration; see rightSMul_zero_of_top.
Rockafellar, §5, third branch: "trivially f0 = f if f ≡ +∞". Together with
rightSMul_zero this is the whole of the book's definition by cases at λ = 0.
Rockafellar, §5. "A function f is positively homogeneous if and only if fλ = f for
every λ > 0."
The positively homogeneous convex function generated by h #
The positively homogeneous convex function generated by h: the greatest positively
homogeneous convex f with f 0 ≤ 0 and f ≤ h, obtained by applying Theorem 5.3 to the convex
cone in ℝⁿ⁺¹ generated by epi h. Not the backbone's hom, which is the same construction
applied to the level-one lift of h and so lives one dimension up.
Rockafellar, §5. f x = inf {(hλ) x | λ ≥ 0} for the positively homogeneous convex function
f generated by h; " λ = 0 can be omitted from the infimum if x ≠ 0 ". This is the form with
λ = 0 omitted.
Theorem 5.5 #
Theorem 5.5. The pointwise supremum of an arbitrary collection of convex functions is convex.
Rockafellar, §5, the illustration after Theorem 5.5: the function assigning to
x = (ξ₁, …, ξₙ) the greatest of its components is convex, "because it is the pointwise supremum
of the linear functions ⟨x, eⱼ⟩". (It is also the support function of the unit simplex.)
Rockafellar, §5: the convexity of k x = max {|ξⱼ| : j = 1, …, n}, "which is called the
Tchebycheff norm on ℝⁿ, can be seen similarly from Theorem 5.5". It is the pointwise supremum
of the 2n linear functions ± ξⱼ.
The convex hull of a function, and of a collection #
conv g is Theorem 5.3 applied to F = conv (epi g), and conv {fᵢ} the same with the convex
hull of the union of the epigraphs.
Rockafellar, §5. conv g "is the greatest convex function majorized by g". Restates
isGreatest_convHullFn.
Rockafellar, §5. conv {fᵢ | i ∈ I} "is the greatest convex function f (not necessarily
proper) on ℝⁿ such that f x ≤ fᵢ x for every x ∈ ℝⁿ and every i ∈ I". Restates
isGreatest_convFn.
Theorem 5.6 #
Theorem 5.6. The convex hull of a collection of proper convex functions is
f x = inf {∑ᵢ λᵢ fᵢ xᵢ | ∑ᵢ λᵢ xᵢ = x}, over all representations of x as a convex combination
with finitely many non-zero coefficients (carried by the Finset). The function-level analogue of
Theorem 2.3.
The convex functions on ℝⁿ, ordered pointwise, form a complete lattice with greatest
lower bound conv {fᵢ} and least upper bound sup {fᵢ}. The lattice is ConvexFns (Rn n), and
ConvexFns.not_coe_inf_eq_inf is the warning behind the book's "(relative to this particular
partially ordered set!)": the meet is not the pointwise infimum.
The other half of the lattice sentence: the least upper bound is the pointwise supremum, which is Theorem 5.5.
Theorem 5.7 #
Theorem 5.7, first assertion. The inverse image (gA) x = g (A x) of a convex function
under a linear transformation is convex.
Theorem 5.7, second assertion. The image (Ah) y = inf {h x | A x = y} of a convex
function is convex. The infimum need not be attained, which is why Ah is not read off the image
of epi h as a set.
Theorem 5.8 #
The book derives the four operations below from partial additions of convex cones in ℝⁿ⁺². The
statements are four explicit formulas, and each is an instance of Theorem 5.7 applied to a jointly
convex function of the auxiliary variables, so nothing here depends on that construction.
The linear map (λ, x) ↦ (λ₁ + ⋯ + λₘ, x), along which the two "adding in λ" operations of
Theorem 5.8 are images.
Equations
- Rockafellar.homSumLin n m = ((∑ i : Fin m, LinearMap.proj i) ∘ₗ LinearMap.fst ℝ (Fin m → ℝ) (TdafSurface.Rn n)).prod (LinearMap.snd ℝ (Fin m → ℝ) (TdafSurface.Rn n))
Instances For
The linear map (λ, x) ↦ (λᵢ, x), which reads off the i-th homogenising variable.
Equations
- Rockafellar.coordHomLin n m i = (LinearMap.proj i ∘ₗ LinearMap.fst ℝ (Fin m → ℝ) (TdafSurface.Rn n)).prod (LinearMap.snd ℝ (Fin m → ℝ) (TdafSurface.Rn n))
Instances For
The joint convexity behind clauses g and h of Theorem 5.8: (λ, x) ↦ (fᵢ λᵢ) x is convex
on ℝᵐ × ℝⁿ, since it is the inverse image of hom fᵢ under (λ, x) ↦ (λᵢ, x).
Theorem 5.8, first function. f x = inf {max {f₁x₁, …, fₘxₘ} | x₁ + ⋯ + xₘ = x} is
convex, the book's "adding in x alone". Stated without the properness the book assumes: the
proof does not use it.
Theorem 5.8, second function. For proper convex f₁, …, fₘ,
g x = inf {(f₁λ₁) x + ⋯ + (fₘλₘ) x | λᵢ ≥ 0, ∑ λᵢ = 1} is convex, the book's "adding in λ and
μ". Not the formula for conv {f₁, …, fₘ} after Theorem 5.6, which has f₁λ₁ □ ⋯ □ fₘλₘ in
place of the pointwise sum.
Theorem 5.8, third function. h x = inf {max {(f₁λ₁) x, …, (fₘλₘ) x} | λᵢ ≥ 0, ∑ λᵢ = 1}
is convex, the book's "adding in λ alone", which "amounts to inverse addition of epigraphs".
Stated without the properness the book assumes: a supremum, unlike a sum, cannot produce
∞ - ∞.
The linear map (λ, y) ↦ (λ₁ + ⋯ + λₘ, y₁ + ⋯ + yₘ) on ℝᵐ × (ℝⁿ)ᵐ, along which the last
operation of Theorem 5.8 — "adding in λ and x" — is an image.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The linear map (λ, y) ↦ (λᵢ, yᵢ).
Equations
- Rockafellar.coordPairLin n m i = (LinearMap.proj i ∘ₗ LinearMap.fst ℝ (Fin m → ℝ) (Fin m → TdafSurface.Rn n)).prod (LinearMap.proj i ∘ₗ LinearMap.snd ℝ (Fin m → ℝ) (Fin m → TdafSurface.Rn n))
Instances For
Theorem 5.8, fourth function. For proper convex f₁, …, fₘ,
k x = inf {max {λ₁f₁x₁, …, λₘfₘxₘ}} over all convex representations x = λ₁x₁ + ⋯ + λₘxₘ is
convex, the book's "adding in λ and x".