Positively homogeneous convex functions

A function f : E → EReal is positively homogeneous when f (a • x) = a * f x for every a > 0, which is to say that its epigraph is a cone. For such functions convexity collapses to subadditivity, and the theory of support functions and gauges rests on that equivalence.

Only positive multipliers are constrained, so the definition says nothing about f 0 beyond f 0 ∈ {0, ⊤, ⊥} (PosHomogeneous.map_zero_trichotomy), and the value f 0 = ⊤ really does occur: δ(· | C) for a convex cone C not containing the origin is positively homogeneous and proper. This is why the finite-combination form of subadditivity carries a nonemptiness hypothesis on the index set — the empty sum would assert f 0 ≤ 0 — and why the spanning-set form of the linearity criterion carries one too.

Main definitions

• PosHomogeneous f — f (a • x) = a * f x for every a > 0.

Main results

• posHomogeneous_iff_isCone_epi — positive homogeneity is exactly the epigraph being a cone.
• convex_iff_add_mem_of_isCone — a cone is convex iff it is closed under addition. This is Mathlib's ConvexCone content, repackaged as a statement about bare sets.
• span_eq_sub_of_isCone — the subspace generated by a convex cone containing the origin is s - s; with vectorSpan_eq_span_of_zero_mem, so is its affine hull.
• smul_closure_eq_of_isCone — the closure of a cone is a cone. The one topological statement in the file; it needs only that each individual scaling is continuous.
• PosHomogeneous.convexFn_iff_subadditive — for a positively homogeneous f, convexity is subadditivity.
• PosHomogeneous.sum_le, PosHomogeneous.neg_le — subadditivity over a finite positive combination, and -(f x) ≤ f (-x).
• PosHomogeneous.isLinearOn_iff, PosHomogeneous.exists_linearMap_iff — linearity on a subspace L is equivalent to f (-x) = -(f x) on L, and PosHomogeneous.neg_eq_of_mem_span reduces the check to a spanning set, in particular a basis.

Implementation notes

Convexity is equivalent to subadditivity for f with values in (-∞, +∞]; that hypothesis is kept inline as ∀ x, f x ≠ ⊥. Positive homogeneity is not stated with a scalar action on EReal — there is no SMul ℝ EReal instance — so (a : EReal) * z is used throughout.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §2 and §4.

Cones

A cone, in Rockafellar's sense, is a set closed under multiplication by positive scalars; it need not contain the origin. The condition is written ∀ a : ℝ, 0 < a → a • s = s, matching posHomogeneous_iff_isCone_epi verbatim.

theorem Tdaf.ConvexAnalysis.smul_mem_iff_of_isCone {M : Type u_1} [AddCommGroup M] [Module ℝ M] {s : Set M} (hs : ∀ (a : ℝ), 0 < a → a • s = s) {a : ℝ} (ha : 0 < a) {x : M} : a • x ∈ s ↔ x ∈ s

Membership of a cone is invariant under positive scaling.

theorem Tdaf.ConvexAnalysis.convex_iff_add_mem_of_isCone {M : Type u_1} [AddCommGroup M] [Module ℝ M] {s : Set M} (hs : ∀ (a : ℝ), 0 < a → a • s = s) : Convex ℝ s ↔ ∀ x ∈ s, ∀ y ∈ s, x + y ∈ s

A cone is convex if and only if it is closed under addition. The "only if" direction is the observation that x + y = 2 * ((x + y) / 2).

theorem Tdaf.ConvexAnalysis.span_eq_sub_of_isCone {M : Type u_1} [AddCommGroup M] [Module ℝ M] {s : Set M} (hs : ∀ (a : ℝ), 0 < a → a • s = s) (hconv : Convex ℝ s) (h0 : 0 ∈ s) : ↑(Submodule.span ℝ s) = s - s

The subspace generated by a convex cone containing the origin is the set of its differences. Closure under addition and positive scaling collects the positive terms of a linear combination into one element of s and the negative terms into another. With vectorSpan_eq_span_of_zero_mem, span, affine hull and s - s all coincide.

theorem Tdaf.ConvexAnalysis.smul_closure_eq_of_isCone {M : Type u_1} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] [ContinuousConstSMul ℝ M] {s : Set M} (hs : ∀ (a : ℝ), 0 < a → a • s = s) (a : ℝ) (ha : 0 < a) : a • closure s = closure s

The closure of a cone is a cone. Multiplication by a non-zero scalar is a homeomorphism, so it commutes with closure. Convexity plays no part, and only continuity of the individual scalings is used — not a topological vector space structure.

Positively homogeneous functions

def Tdaf.ConvexAnalysis.PosHomogeneous {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : Prop

A function f : E → EReal is positively homogeneous (of degree one) when f (a • x) = a * f x for every a > 0. Only positive scalars are constrained; in particular f 0 is not determined, see PosHomogeneous.map_zero_trichotomy.

Equations

• Tdaf.ConvexAnalysis.PosHomogeneous f = ∀ (a : ℝ), 0 < a → ∀ (x : E), f (a • x) = ↑a * f x

theorem Tdaf.ConvexAnalysis.PosHomogeneous.map_zero_trichotomy {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) : f 0 = 0 ∨ f 0 = ⊤ ∨ f 0 = ⊥

Positive homogeneity leaves only three possible values at the origin. Rockafellar notes the same: f 0 may be 0 or -∞ for a positively homogeneous function, and +∞ as well once improper functions are admitted.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.zero_le_map_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (h : f 0 ≠ ⊥) : 0 ≤ f 0

A positively homogeneous function that never takes the value ⊥ is nonnegative at the origin.

theorem Tdaf.ConvexAnalysis.posHomogeneous_iff_isCone_epi {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} : PosHomogeneous f ↔ ∀ (a : ℝ), 0 < a → a • epi f = epi f

Positive homogeneity of f is exactly the statement that epi f is a cone.

theorem Tdaf.ConvexAnalysis.posHomogeneous_indicatorFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Set E} : PosHomogeneous (indicatorFn s) ↔ ∀ (a : ℝ), 0 < a → a • s = s

The indicator function of a set is positively homogeneous exactly when the set is a cone.

Convexity is subadditivity

theorem Tdaf.ConvexAnalysis.PosHomogeneous.convexFn_iff_subadditive {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hbot : ∀ (x : E), f x ≠ ⊥) : ConvexFn f ↔ ∀ (x y : E), f (x + y) ≤ f x + f y

A positively homogeneous function f with values in (-∞, +∞] is convex if and only if it is subadditive. Subadditivity of f is precisely closure of the cone epi f under addition.

Finite combinations, and the value at -x

theorem Tdaf.ConvexAnalysis.PosHomogeneous.sum_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) {a : ι → ℝ} (ha : ∀ i ∈ s, 0 < a i) (x : ι → E) : f (∑ i ∈ s, a i • x i) ≤ ∑ i ∈ s, ↑(a i) * f (x i)

Subadditivity of a positively homogeneous convex function extends to positive linear combinations. The index set must be nonempty: the empty sum would assert f 0 ≤ 0, and f 0 = ⊤ is possible.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.neg_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) (x : E) : -f x ≤ f (-x)

A positively homogeneous convex function with values in (-∞, +∞] satisfies -(f x) ≤ f (-x).

Linearity on a subspace

theorem Tdaf.ConvexAnalysis.ne_top_of_neg_eq {E : Type u_1} [AddCommGroup E] {f : E → EReal} (hbot : ∀ (x : E), f x ≠ ⊥) {x : E} (h : f (-x) = -f x) : f x ≠ ⊤

Where a function with values in (-∞, +∞] is odd, it is finite.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.map_zero_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {b : E} (hb : f (-b) = -f b) : f 0 = 0

If a positively homogeneous convex function is odd anywhere, then it vanishes at the origin.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.neg_eq_iff_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {x : E} : f (-x) = -f x ↔ f (-x) ≤ -f x

Since -(f x) ≤ f (-x) always holds, oddness at x is a single inequality.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.map_smul_of_neg_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {x : E} (hx : f (-x) = -f x) (c : ℝ) : f (c • x) = ↑c * f x

At a point where a positively homogeneous convex function is odd, it is homogeneous for all real scalars, not merely the positive ones.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.map_add_of_neg_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {x y : E} (hx : f (-x) = -f x) (hy : f (-y) = -f y) : f (x + y) = f x + f y

At two points where a positively homogeneous convex function is odd, it is additive.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.neg_eq_add {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {x y : E} (hx : f (-x) = -f x) (hy : f (-y) = -f y) : f (-(x + y)) = -f (x + y)

Oddness of a positively homogeneous convex function is preserved by addition.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.neg_eq_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {x : E} (hx : f (-x) = -f x) (c : ℝ) : f (-(c • x)) = -f (c • x)

Oddness of a positively homogeneous convex function is preserved by scalar multiplication.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.neg_eq_of_mem_span {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {s : Set E} (hs : s.Nonempty) (hb : ∀ b ∈ s, f (-b) = -f b) {x : E} (hx : x ∈ Submodule.span ℝ s) : f (-x) = -f x

If a positively homogeneous convex function is odd on a nonempty set s, it is odd on the whole subspace spanned by s. The nonemptiness hypothesis is not decoration: it is what supplies f 0 = 0, needed when a coefficient λᵢ vanishes.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.isLinearOn_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) (L : Submodule ℝ E) : ((∀ x ∈ L, ∀ y ∈ L, f (x + y) = f x + f y) ∧ ∀ (c : ℝ), ∀ x ∈ L, f (c • x) = ↑c * f x) ↔ ∀ x ∈ L, f (-x) = -f x

A positively homogeneous convex function with values in (-∞, +∞] is linear on a subspace L — additive and homogeneous there — if and only if f (-x) = -(f x) for every x ∈ L.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.exists_linearMap_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) (L : Submodule ℝ E) : (∃ (g : ↥L →ₗ[ℝ] ℝ), ∀ (x : ↥L), f ↑x = ↑(g x)) ↔ ∀ x ∈ L, f (-x) = -f x

The same criterion in packaged form: f agrees on L with a genuine linear functional L →ₗ[ℝ] ℝ exactly when f (-x) = -(f x) for every x ∈ L. Such an f is automatically finite on L, which is why a real-valued linear map can be extracted.

theorem Tdaf.ConvexAnalysis.PosHomogeneous.exists_linearMap_span {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) {s : Set E} (hs : s.Nonempty) (hb : ∀ b ∈ s, f (-b) = -f b) : ∃ (g : ↥(Submodule.span ℝ s) →ₗ[ℝ] ℝ), ∀ (x : ↥(Submodule.span ℝ s)), f ↑x = ↑(g x)

To know that f is linear on the subspace spanned by a nonempty set s, it is enough to check f (-b) = -(f b) for b ∈ s — in particular on a basis of that subspace.

def Tdaf.ConvexAnalysis.PosHomogeneous.epiCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) : ConvexCone ℝ (E × ℝ)

The epigraph of a positively homogeneous convex function, bundled as a Mathlib ConvexCone, which makes Mathlib's ConvexCone API available to support functions and polarity. No hypothesis on the values of f is needed: closure under addition comes from convexity of the cone, not from subadditivity.

Equations

• hf.epiCone hconv = { carrier := Tdaf.ConvexAnalysis.epi f, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.PosHomogeneous.coe_epiCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : PosHomogeneous f) (hconv : ConvexFn f) : ↑(hf.epiCone hconv) = epi f

The carrier of PosHomogeneous.epiCone is the epigraph.