Essential strict convexity #
A closed proper convex function is essentially strictly convex — strictly convex on every convex
subset of dom ∂f — exactly when its conjugate is essentially smooth. Together with the matching
characterisation of essential smoothness this is the duality that makes the Legendre transformation
an involution: strict convexity on one side is smoothness on the other. Since ∂f* is the inverse
of ∂f, single-valuedness of ∂f* is the statement that distinct points never share a
subgradient of f, and essentiallyStrictlyConvex_iff_pairwise_disjoint identifies that with
essential strict convexity.
Main definitions #
StrictConvexOnFn f C—fsatisfies the convexity inequality strictly between distinct points ofC.EssentiallyStrictlyConvex f—fis strictly convex on every convex subset ofdom ∂f.
Main results #
mem_subgradient_of_combo,le_combo_of_mem_subgradient— a subgradient shared by two points is a subgradient at every point between them, andfis affine along that segment.mem_subgradient_conj_innerL_iff,pairwise_disjoint_subgradient_conj_iff—∂f*inverts∂ffor the self-pairing, and the transfer it gives between single-valuedness and injectivity.essentiallySmooth_conj_iff_essentiallyStrictlyConvexandessentiallyStrictlyConvex_conj_iff_essentiallySmooth— the duality, both ways round (Theorem 26.3 in [^1]).subgradient_injective_iff—∂fis one-to-one exactly whenfis essentially smooth and strictly convex onint (dom f).
Implementation notes #
Every value in sight is finite, so the arithmetic is real: points of dom ∂f lie in dom f and
f is proper. The only EReal case split is on f z at the test point of the subgradient
inequality, where f z = ⊤ makes it trivial. The definitions need only a real vector space;
The duality needs an inner-product space, because EssentiallySmooth does.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §26.
Strict convexity on a set. Between two distinct points of C the convexity inequality
is strict. Nothing is asked off C, and nothing is asked about the finiteness of f.
Equations
Instances For
Strict convexity is inherited by subsets.
The bridge to Mathlib's StrictConvexOn. On a convex set where f is finite, strict
convexity of the EReal-valued f and of its real trace are the same condition — and so the only
way in for a concrete function, since Mathlib's strict-convexity API and its second-derivative
criteria are stated for real-valued functions. Finiteness is needed in both directions: where
f x = ⊤ the EReal inequality is vacuous and the real one is not, and where f x = ⊥ the real
one is vacuous and the EReal one is not.
Essential strict convexity: f is strictly convex on every convex subset of dom ∂f.
This is weaker than strict convexity on dom f and stronger than strict convexity on
ri (dom f), and examples separate it from both.
Equations
- Tdaf.ConvexAnalysis.EssentiallyStrictlyConvex f = ∀ ⦃C : Set E⦄, Convex ℝ C → C ⊆ Tdaf.ConvexAnalysis.domSubgradient B f → Tdaf.ConvexAnalysis.StrictConvexOnFn f C
Instances For
The subgradient inequality between real numbers. Both values are finite — f x because a
subgradient exists there, f z by hypothesis — so the EReal inequality is a real one.
The subgradient inequality, in the direction that has to be proved: a real bound at every
point of dom f is the EReal subgradient inequality everywhere, since off dom f it reads
≤ ⊤.
The pairing at a convex combination splits, because z - (a x₁ + b x₂) is the same
combination of z - x₁ and z - x₂.
A subgradient shared by two points is a subgradient all along the segment between them.
The graph of ⟨·, v⟩ - f*(v) is a supporting hyperplane touching epi f at both endpoints, so it
touches it along the whole segment.
A shared subgradient makes f affine along the segment, so the convexity inequality there
is an equality and strict convexity fails.
The converse computation: if f fails to be strictly convex between x₁ and x₂ and has
a subgradient at the point between them, that subgradient serves at both endpoints.
The two endpoint inequalities add up to the failed strict inequality, so neither can be strict.
The reformulation the duality runs on: a proper convex function is essentially strictly
convex exactly when two distinct points never share a subgradient. Forwards, a shared subgradient
makes the whole segment lie in dom ∂f and f affine on it, so strict convexity fails there.
Backwards, a failure of strict convexity on a convex C ⊆ dom ∂f puts a subgradient at a point
between two points of C, and the failed inequality forces it to serve at both of them.
∂f* is the inverse of ∂f, for the self-pairing of an inner-product space. The flip of
innerₗ E is discharged once here so that no later rewrite has to reach inside conj.
Single-valuedness of ∂f* is injectivity of ∂f.
Injectivity of ∂f* is single-valuedness of ∂f — the mirror of
subsingleton_subgradient_conj_iff.
A closed proper convex function is essentially strictly convex exactly when its conjugate is essentially smooth.
f** = f for the self-pairing of an inner-product space, with the flip of innerₗ E
discharged so that the equation is stated in terms of conj (innerₗ E) twice.
The same duality read in the other direction: the conjugate of a closed proper convex function
is essentially strictly convex exactly when the function itself is essentially smooth. This is the
previous theorem applied to f*, together with f** = f.
∂f is a one-to-one mapping — single-valued and injective — exactly when f is essentially
smooth and strictly convex on int (dom f). Under essential smoothness dom ∂f is
int (dom f), so essential strict convexity, which quantifies over all convex subsets of
dom ∂f, collapses to strict convexity on that one set.