Infimal convolution #
The functional operation f □ g corresponding to addition of epigraphs: the function determined by
epi f + epi g. It is convex whenever f and g are, and it is dual to pointwise addition of
convex functions under conjugacy.
f □ g is defined as ofEpi (epi f + epi g), not by the classical formula
(f □ g) x = ⨅ y, f (x - y) + g y, which is ill-formed as soon as one function reaches ⊤ where
the other reaches ⊥: for f ≡ ⊤ and g 0 = ⊥, epi f + epi g = ∅ so the left side is ⊤ and
the right side ⊤ + ⊥ = ⊥. infConv_apply recovers the formula under f, g ≠ ⊥; since that
example uses only one ⊤ value and one ⊥ value, a single such hypothesis will not do.
Main definitions #
infConv f g— the infimal convolutef □ g.InfConvFn E— the type synonymE → ERealcarrying□as its addition, so thatf₁ □ ⋯ □ fₘis aFinset.sum. A synonym is forced, sinceE → ERealalready carries the pointwise+that□is dual to; additive notation is right,□being addition of epigraphs.
Main results #
convexFn_infConv—□preserves convexity;convexFn_sum_toInfConvFnis the m-ary form.infConv_apply,infConv_le_add— the classical infimum formula and its inequality half;sum_toInfConvFn_apply_le,sum_toInfConvFn_le_sumare the m-ary versions.dom_infConv—dom (f □ g) = dom f + dom g, with no hypothesis at all.InfConvFn.instAddCommMonoid—□is commutative and associative with identityδ(· | 0);infConv_indicatorFn_singletontranslates the graph offbya.subset_epi_infConv,epi_infConv—epi f + epi g ⊆ epi (f □ g)always; equality needsIsEpiLike (epi f + epi g).
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §5.
The definition and its epigraph #
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
Instances For
Rockafellar's description of epi (f □ g), under the hypothesis that makes it true.
The hypothesis is not removable: a sum of epigraphs need not be an epigraph. On ℝ take
f x = 1/x for x > 0 and ⊤ otherwise, and g ≡ 0; both are convex, every vertical section of
epi f + epi g is Ioi 0, so the sum is ℝ ×ˢ Ioi 0, whereas f □ g ≡ 0 has epigraph
ℝ ×ˢ Ici 0.
Vertical sections of a sum of epigraphs are upward closed: the half of IsEpiLike that holds
unconditionally, closedness having to supply the other.
The effective domain #
The infimum formula #
(f □ g) x ≤ f (x - y) + g y. Both ≠ ⊥ hypotheses are needed: without them the right side
can be ⊤ + ⊥ = ⊥ while the left is ⊤.
Rockafellar's formula for □: (f □ g) x = ⨅ y, f (x - y) + g y, "analogous to the
classical formula for integral convolution". The ≠ ⊥ hypotheses make the right side meaningful.
Commutativity, associativity, monotonicity #
Enlarging a summand from F to the epigraph it determines does not move the lower boundary of
the sum: the points epi (ofEpi F) adds are limits from above of points of F. This is what makes
□ associative.
□ is associative. Not a direct consequence of associativity of set addition: epi (f □ g) is
larger than epi f + epi g in general, and epi_ofEpi_add_subset closes the gap.
Indicator functions: the identity element and translation #
Adding the epigraph of δ(· | a) — the half-cylinder {a} ×ˢ Ici 0 — translates an epigraph
horizontally by a. Unlike a general sum of epigraphs, this one is an epigraph.
f □ δ(· | a) translates the graph of f horizontally by a.
δ(· | 0) is the identity element for □.
If g is nonpositive at the origin then f □ g ≤ f, since δ(· | 0) dominates such a g.
Convexity of an infimal convolute #
The infimal convolute of two convex functions is convex. No properness is needed: the classical hypothesis only makes the infimum formula meaningful, and the epigraph definition does not use it.
□ as a commutative monoid #
E → EReal, carrying infimal convolution as its addition and δ(· | 0) as its zero;
∑ i ∈ s, toInfConvFn (f i) is Rockafellar's f₁ □ ⋯ □ fₘ.
Equations
- Tdaf.ConvexAnalysis.InfConvFn E = (E → EReal)
Instances For
A function E → EReal, regarded as an element of the infimal-convolution monoid.
Equations
Instances For
An element of the infimal-convolution monoid, regarded as a function E → EReal.
Equations
Instances For
Infimal convolution is the addition of InfConvFn E.
Equations
δ(· | 0) is the zero of InfConvFn E.
Equations
E → EReal is a commutative monoid under □, with identity δ(· | 0).
Equations
- One or more equations did not get rendered due to their size.
Convexity in m-ary form: f₁ □ ⋯ □ fₘ is convex whenever f₁, …, fₘ are. The empty case is
δ(· | 0), which is convex because {0} is.
The m-ary basic upper bound, infConv_apply_le iterated; no hypothesis is needed.
The m-ary infimum bound: (g₁ □ ⋯ □ gₘ) (y₁ + ⋯ + yₘ) ≤ g₁ y₁ + ⋯ + gₘ yₘ. The ≠ ⊥
hypothesis sits on each gᵢ separately, never on a partial convolute: □ does not preserve
≠ ⊥, since g₁ x = -x and g₂ x = x are everywhere finite with g₁ □ g₂ ≡ -∞.
dom (g₁ □ ⋯ □ gₘ) = dom g₁ + ⋯ + dom gₘ, with no hypothesis; the empty convolute is
δ(· | 0), whose domain {0} is the empty sum of sets.