Right scalar multiplication and homogenisation

Two operations built from scalar multiplication of epigraphs.

Right scalar multiplication fλ is the function whose epigraph is λ • epi f; for λ > 0 it is (fλ) x = λ * f (λ⁻¹ • x), and f0 = δ(· | 0). It is a monoid action of ([0, ∞), *) on functions, and positive homogeneity of f is exactly fλ = f for all λ > 0.

Homogenisation hom f is the positively homogeneous convex function on ℝ × E assembled from the functions fλ, one for each λ ≥ 0; its epigraph is the convex cone generated by {1} ×ˢ epi f, one dimension up, with one ray added. It is the function generated by the level-1 lift of f, not the one generated by f itself — only the first keeps the λ variable that recession functions, support functions of level sets and the two-step homogenisation used for polarity all integrate over.

Main definitions

• smulRight f a — Rockafellar's fa, defined as ofEpi (a • epi f); smulRightHom packages it as a monoid homomorphism ℝ≥0 →* Function.End (E → EReal).
• levelOneLift f — the level-1 lift h (λ, x) = f x if λ = 1, ⊤ otherwise.
• hom f — the positively homogeneous convex function on ℝ × E generated by levelOneLift f.
• homCone f — the convex cone generated by epi (levelOneLift f), which is what hom f is ofEpi of; homEpiCone bundles epi (hom f) as a ConvexCone ℝ ((ℝ × E) × ℝ).

Main results

• smulRight_apply_pos, smulRight_zero — the values of fa for a > 0 and for a = 0.
• epi_smulRight — epi (fa) = a • epi f, for a > 0 only; see below.
• convexFn_smulRight, smulRight_one, smulRight_smulRight, posHomogeneous_iff_smulRight_eq — convexity is preserved, fa is a monoid action, and f is positively homogeneous exactly when fa = f for all a > 0.
• hom_apply_pos, hom_apply_one, hom_apply_neg, hom_apply_smul — the defining equations.
• posHomogeneous_hom, convexFn_hom, hom_ne_bot — hom f is positively homogeneous, convex as soon as f is, and avoids -∞ as soon as f does.
• hom_isGreatest — the maximality property: hom f is the greatest positively homogeneous convex g with g 0 ≤ 0 and g ≤ levelOneLift f.
• hom_eq_ofEpi_homCone, epi_hom, homCone_eq_preimage, prodAssoc_image_homCone — the cone description, and the shuffle relating it to the cone over {1} ×ˢ epi f in ℝ × (E × ℝ).

Implementation notes

epi (fa) = a • epi f fails at a = 0: there 0 • epi f is {(0, 0)} whenever epi f is nonempty, which is not an epigraph, so epi (f0) = {0} ×ˢ Ici 0 is strictly larger. The definition fa = ofEpi (a • epi f) still delivers Rockafellar's value, since ofEpi sees only the lower boundary; the same degeneracy reappears one dimension up in epi_hom. The side condition f ≢ +∞ on f0 = δ(· | 0) is likewise not decoration: for f ≡ +∞, epi f = ∅ and fa = +∞ for every a. It is needed in smulRight_zero, hom_eq_ofEpi_homCone, epi_hom and the membership half of hom_isGreatest, and nowhere else.

References

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

Auxiliary facts about epigraphs and ofEpi

Right scalar multiplication

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

Right scalar multiplication fa: the function determined by the scaled epigraph a • epi f. For a > 0 this is (fa) x = a * f (a⁻¹ • x) and its epigraph really is a • epi f; at a = 0 the epigraph identity fails, but the definition still delivers Rockafellar's value f0 = δ(· | 0).

Equations

• Tdaf.ConvexAnalysis.smulRight f a = Tdaf.ConvexAnalysis.ofEpi (a • Tdaf.ConvexAnalysis.epi f)

theorem Tdaf.ConvexAnalysis.smul_epi {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a : ℝ} (ha : 0 < a) (f : E → EReal) : a • epi f = epi fun (x : E) => ↑a * f (a⁻¹ • x)

A positively scaled epigraph is an epigraph: scaling epi f by a > 0 is the epigraph of x ↦ a * f (a⁻¹ • x). This is the computation behind every statement about fa for a > 0.

theorem Tdaf.ConvexAnalysis.smulRight_apply_pos {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a : ℝ} (ha : 0 < a) (f : E → EReal) (x : E) : smulRight f a x = ↑a * f (a⁻¹ • x)

(fa) x = a * f (a⁻¹ • x) for a > 0.

theorem Tdaf.ConvexAnalysis.epi_smulRight {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a : ℝ} (ha : 0 < a) (f : E → EReal) : epi (smulRight f a) = a • epi f

Right scalar multiplication by a > 0 is scalar multiplication of the epigraph.

The hypothesis 0 < a is essential: see not_isEpiLike_zero_smul_epi.

theorem Tdaf.ConvexAnalysis.smulRight_of_epi_eq_empty {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (h : epi f = ∅) (a : ℝ) : smulRight f a = ⊤

If f ≡ +∞ then so is fa, for every a — including a = 0. This is Rockafellar's parenthetical remark "trivially f0 = f if f ≡ +∞".

theorem Tdaf.ConvexAnalysis.zero_smul_epi {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (h : (dom f).Nonempty) : 0 • epi f = {0}

0 • epi f is the single point (0, 0) as soon as f ≢ +∞.

theorem Tdaf.ConvexAnalysis.ofEpi_singleton_zero {E : Type u_1} [AddCommGroup E] : ofEpi {0} = indicatorFn {0}

The function determined by the single point (0, 0) is δ(· | 0).

theorem Tdaf.ConvexAnalysis.smulRight_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (h : (dom f).Nonempty) : smulRight f 0 = indicatorFn {0}

f0 = δ(· | 0) when f ≢ +∞.

theorem Tdaf.ConvexAnalysis.not_isEpiLike_zero_smul_epi {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (h : (dom f).Nonempty) : ¬IsEpiLike (0 • epi f)

0 • epi f is never an epigraph, unless f ≡ +∞: its vertical section over the origin is the single point {0}, which is not upward closed. This is why epi_smulRight is stated for a > 0 only — epi (f0) = {0} ×ˢ Ici 0 is strictly larger than 0 • epi f.

theorem Tdaf.ConvexAnalysis.epi_smulRight_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (h : (dom f).Nonempty) : epi (smulRight f 0) = {0} ×ˢ Set.Ici 0

The epigraph of f0, for f ≢ +∞: the closed half-line over the origin, which strictly contains 0 • epi f = {(0, 0)}.

theorem Tdaf.ConvexAnalysis.indicatorFn_le_smulRight_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : indicatorFn {0} ≤ smulRight f 0

δ(· | 0) ≤ f0, with no hypothesis on f: the two sides agree when f ≢ +∞ and the right-hand side is +∞ otherwise. This is the uniform form of smulRight_zero.

theorem Tdaf.ConvexAnalysis.convexFn_smulRight {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (a : ℝ) (hf : ConvexFn f) : ConvexFn (smulRight f a)

Right scalar multiplication preserves convexity. No sign hypothesis on a is needed, although fa is only intended for 0 ≤ a < ∞, the range in which it has its meaning.

@[simp]

theorem Tdaf.ConvexAnalysis.smulRight_one {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : smulRight f 1 = f

f1 = f: right scalar multiplication by 1 is the identity.

theorem Tdaf.ConvexAnalysis.posHomogeneous_iff_smulRight_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} : PosHomogeneous f ↔ ∀ a > 0, smulRight f a = f

f is positively homogeneous if and only if fa = f for every a > 0; both directions read a • epi f = epi f through ofEpi_epi and epi_smulRight.

theorem Tdaf.ConvexAnalysis.posHomogeneous_smulRight_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : PosHomogeneous (smulRight f 0)

f0 is positively homogeneous, whatever f is: it is either δ(· | 0), the indicator of a cone, or +∞. This is the degenerate case that makes posHomogeneous_hom work at λ = 0.

theorem Tdaf.ConvexAnalysis.zero_smul_epi_ofEpi {E : Type u_1} [AddCommGroup E] [Module ℝ E] (F : Set (E × ℝ)) : 0 • epi (ofEpi F) = 0 • F

Scaling an epigraph by 0 does not see the difference between a set and the epigraph it determines: both are empty together, and otherwise both collapse to {(0, 0)}.

theorem Tdaf.ConvexAnalysis.smulRight_smulRight {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a b : ℝ} (f : E → EReal) (ha : 0 ≤ a) (hb : 0 ≤ b) : smulRight (smulRight f a) b = smulRight f (a * b)

Right scalar multiplication is an action, f(ab) = (fa)b. The case b = 0 is where the failure of epi (fa) = a • epi f at a = 0 is shown not to propagate.

noncomputable def Tdaf.ConvexAnalysis.smulRightHom {E : Type u_1} [AddCommGroup E] [Module ℝ E] : NNReal →* Function.End (E → EReal)

Right scalar multiplication as a monoid action of ([0, ∞), *) on E → EReal, packaged as a monoid homomorphism into Function.End (E → EReal); smulRight_one and smulRight_smulRight are the two axioms. It is deliberately not a MulAction ℝ≥0 (E → EReal) instance, since on the bare Pi type • already means the pointwise action; MulAction.ofEndHom turns it into an action on demand.

Equations

• Tdaf.ConvexAnalysis.smulRightHom = { toFun := fun (a : NNReal) (f : E → EReal) => Tdaf.ConvexAnalysis.smulRight f ↑a, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.smulRightHom_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] (a : NNReal) (f : E → EReal) : smulRightHom a f = smulRight f ↑a

The monoid homomorphism smulRightHom is right scalar multiplication.

The level-1 lift

noncomputable def Tdaf.ConvexAnalysis.levelOneLift {E : Type u_1} (f : E → EReal) : ℝ × E → EReal

The level-1 lift of f to ℝ × E: h (λ, x) = f x if λ = 1, and +∞ otherwise. hom f is the positively homogeneous convex function generated by this lift, not the one generated by f.

Equations

• Tdaf.ConvexAnalysis.levelOneLift f = Tdaf.ConvexAnalysis.restrict {p : ℝ × E | p.1 = 1} fun (p : ℝ × E) => f p.2

@[simp]

theorem Tdaf.ConvexAnalysis.levelOneLift_of_fst_eq_one {E : Type u_1} {f : E → EReal} {p : ℝ × E} (h : p.1 = 1) : levelOneLift f p = f p.2

The defining equation of the level-1 lift on the hyperplane λ = 1.

@[simp]

theorem Tdaf.ConvexAnalysis.levelOneLift_of_fst_ne_one {E : Type u_1} {f : E → EReal} {p : ℝ × E} (h : p.1 ≠ 1) : levelOneLift f p = ⊤

The level-1 lift is +∞ off the hyperplane λ = 1.

theorem Tdaf.ConvexAnalysis.levelOneLift_apply_one {E : Type u_1} (f : E → EReal) (x : E) : levelOneLift f (1, x) = f x

The level-1 lift, evaluated on the hyperplane λ = 1.

theorem Tdaf.ConvexAnalysis.levelOneLift_apply_of_ne {E : Type u_1} {f : E → EReal} {a : ℝ} (h : a ≠ 1) (x : E) : levelOneLift f (a, x) = ⊤

The level-1 lift, evaluated off the hyperplane λ = 1.

theorem Tdaf.ConvexAnalysis.epi_levelOneLift {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : epi (levelOneLift f) = ⇑(LinearEquiv.prodAssoc ℝ ℝ E ℝ) ⁻¹' {1} ×ˢ epi f

The epigraph of the level-1 lift is {1} ×ˢ epi f, read in (ℝ × E) × ℝ through the associativity shuffle.

theorem Tdaf.ConvexAnalysis.mem_epi_levelOneLift {E : Type u_1} {f : E → EReal} {q : (ℝ × E) × ℝ} : q ∈ epi (levelOneLift f) ↔ q.1.1 = 1 ∧ f q.1.2 ≤ ↑q.2

Membership of the epigraph of the level-1 lift, unfolded: ((λ, x), μ) lies in it exactly when λ = 1 and μ ≥ f x.

theorem Tdaf.ConvexAnalysis.mk_one_mem_epi_levelOneLift {E : Type u_1} {f : E → EReal} {x : E} {μ : ℝ} : ((1, x), μ) ∈ epi (levelOneLift f) ↔ f x ≤ ↑μ

The vectors that generate the cone of homCone: ((1, x), μ) with μ ≥ f x.

theorem Tdaf.ConvexAnalysis.convexFn_levelOneLift {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) : ConvexFn (levelOneLift f)

The level-1 lift of a convex function is convex: its epigraph is a linear preimage of the convex set {1} ×ˢ epi f.

Homogenisation

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

The positively homogeneous convex function generated by the level-1 lift of f, assembled slice by slice out of the right scalar multiples fλ: hom f (λ, x) = (fλ) x for λ ≥ 0, and +∞ for λ < 0. No closure is taken.

Equations

• Tdaf.ConvexAnalysis.hom f p = if 0 ≤ p.1 then Tdaf.ConvexAnalysis.smulRight f p.1 p.2 else ⊤

theorem Tdaf.ConvexAnalysis.hom_apply_nonneg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a : ℝ} (ha : 0 ≤ a) (f : E → EReal) (x : E) : hom f (a, x) = smulRight f a x

The defining equation at λ ≥ 0: the slice of hom f at level λ is fλ.

theorem Tdaf.ConvexAnalysis.hom_apply_pos {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a : ℝ} (ha : 0 < a) (f : E → EReal) (x : E) : hom f (a, x) = ↑a * f (a⁻¹ • x)

The defining equation at λ > 0: hom f (λ, x) = λ * f (λ⁻¹ • x).

theorem Tdaf.ConvexAnalysis.hom_apply_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) (x : E) : hom f (0, x) = smulRight f 0 x

The defining equation at λ = 0: the slice is f0, which is δ(· | 0) unless f ≡ +∞.

theorem Tdaf.ConvexAnalysis.hom_apply_one {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) (x : E) : hom f (1, x) = f x

hom f restricts to f on the level λ = 1: this is the sense in which hom f is a homogenisation of f.

theorem Tdaf.ConvexAnalysis.hom_apply_neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a : ℝ} (ha : a < 0) (f : E → EReal) (x : E) : hom f (a, x) = ⊤

hom f is +∞ on the half-space λ < 0.

theorem Tdaf.ConvexAnalysis.hom_of_epi_eq_empty {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (h : epi f = ∅) : hom f = ⊤

If f ≡ +∞ then hom f ≡ +∞.

theorem Tdaf.ConvexAnalysis.hom_ne_bot {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ∀ (x : E), f x ≠ ⊥) (q : ℝ × E) : hom f q ≠ ⊥

The homogenisation of a function that avoids -∞ avoids it too. Only the ne_bot half of Proper f is needed: if dom f is empty then hom f ≡ +∞.

theorem Tdaf.ConvexAnalysis.hom_apply_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {a : ℝ} (hdom : (dom f).Nonempty) (ha : 0 ≤ a) (z : E) : hom f (a, a • z) = ↑a * f z

hom f (λ, λ x) = λ * f x for λ ≥ 0: the substitution y = λ x that turns homogenisation into left scalar multiplication. At λ = 0 both sides are 0, by f0 = δ(· | 0) and 0 · ∞ = 0.

theorem Tdaf.ConvexAnalysis.hom_le_levelOneLift {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : hom f ≤ levelOneLift f

hom f never exceeds the level-1 lift, and agrees with it at λ = 1.

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

hom f is positively homogeneous, with no hypothesis on f at all. The λ = 0 slice is where the a = 0 degeneracy of right scalar multiplication is absorbed, by positive homogeneity of f0.

theorem Tdaf.ConvexAnalysis.le_hom {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {g : ℝ × E → EReal} (hg : PosHomogeneous g) (h0 : g 0 ≤ 0) (hle : g ≤ levelOneLift f) : g ≤ hom f

The upper-bound half of the maximality property: every positively homogeneous g with g 0 ≤ 0 that is majorised by the level-1 lift of f is majorised by hom f. Convexity of g is not used, and neither is f ≢ +∞. The hypothesis g 0 ≤ 0 is not removable: for f ≡ 0 on E = ℝ, the indicator of {λ > 0} is positively homogeneous, convex and below the level-1 lift, yet takes the value +∞ > 0 = hom f 0 at the origin.

The cone generated by the level-1 lift

noncomputable def Tdaf.ConvexAnalysis.homCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : Set ((ℝ × E) × ℝ)

The convex cone in (ℝ × E) × ℝ generated by the epigraph of the level-1 lift of f: the origin together with all positive multiples of epi (levelOneLift f). This is the cone from which hom f is recovered by ofEpi. It is not itself an epigraph; epi_hom describes the ray that has to be added.

Equations

• Tdaf.ConvexAnalysis.homCone f = {0} ∪ ⋃ (a : ℝ), ⋃ (_ : a > 0), a • Tdaf.ConvexAnalysis.epi (Tdaf.ConvexAnalysis.levelOneLift f)

theorem Tdaf.ConvexAnalysis.mem_homCone_iff_exists {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {q : (ℝ × E) × ℝ} : q ∈ homCone f ↔ q = 0 ∨ ∃ a > 0, q ∈ a • epi (levelOneLift f)

Membership of the generated cone, unfolded.

theorem Tdaf.ConvexAnalysis.mem_smul_epi_levelOneLift {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {a : ℝ} {q : (ℝ × E) × ℝ} (ha : 0 < a) : q ∈ a • epi (levelOneLift f) ↔ q.1.1 = a ∧ f (a⁻¹ • q.1.2) ≤ ↑(a⁻¹ * q.2)

Membership of a • epi (levelOneLift f) for a > 0: the first coordinate pins down a.

theorem Tdaf.ConvexAnalysis.mem_homCone_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {q : (ℝ × E) × ℝ} : q ∈ homCone f ↔ q = 0 ∨ 0 < q.1.1 ∧ f (q.1.1⁻¹ • q.1.2) ≤ ↑(q.1.1⁻¹ * q.2)

The membership criterion for the generated cone, in closed form.

theorem Tdaf.ConvexAnalysis.smul_homCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a : ℝ} (hc : 0 < a) (f : E → EReal) : a • homCone f = homCone f

The generated cone is a cone: it is invariant under multiplication by positive scalars.

theorem Tdaf.ConvexAnalysis.convex_homCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) : Convex ℝ (homCone f)

The generated cone is convex: for a cone it is enough to check closure under addition, and that is a • S + b • S = (a + b) • S for convex S.

theorem Tdaf.ConvexAnalysis.mk_ne_zero_of_ne_zero {E : Type u_1} [AddCommGroup E] {a : ℝ} (ha : a ≠ 0) (x : E) (μ : ℝ) : ((a, x), μ) ≠ 0

A point of (ℝ × E) × ℝ whose homogenising coordinate is nonzero is not the origin.

theorem Tdaf.ConvexAnalysis.hom_eq_ofEpi_homCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hdom : (dom f).Nonempty) : hom f = ofEpi (homCone f)

hom f is ofEpi of the convex cone generated by the epigraph of the level-1 lift of f. The hypothesis f ≢ +∞ is needed: for f ≡ +∞ the cone degenerates to {0}, whose associated function is δ(· | 0).

theorem Tdaf.ConvexAnalysis.convexFn_hom {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) : ConvexFn (hom f)

hom f is convex whenever f is. The degenerate case f ≡ +∞ is included: there hom f ≡ +∞, whose epigraph is empty.

theorem Tdaf.ConvexAnalysis.hom_isGreatest {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) (hdom : (dom f).Nonempty) : IsGreatest {g : ℝ × E → EReal | PosHomogeneous g ∧ ConvexFn g ∧ g 0 ≤ 0 ∧ g ≤ levelOneLift f} (hom f)

The maximality property of hom f. It is the greatest positively homogeneous convex g on ℝ × E with g 0 ≤ 0 and g ≤ levelOneLift f. The side condition g 0 ≤ 0 cannot be dropped (see le_hom), and f ≢ +∞ is needed only for membership: for f ≡ +∞ one has hom f ≡ +∞, and the greatest element of the set is δ(· | 0) instead.

theorem Tdaf.ConvexAnalysis.epi_hom {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hdom : (dom f).Nonempty) : epi (hom f) = homCone f ∪ {0} ×ˢ Set.Ici 0

The epigraph of hom f against the cone that generates it. epi (hom f) is not homCone f: the cone meets the hyperplane λ = 0 in the single point 0, whereas an epigraph must contain the whole ray above it. The two differ exactly by that ray, {0} ×ˢ Ici 0.

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

The epigraph of hom f, bundled as a Mathlib ConvexCone: posHomogeneous_hom and convexFn_hom say precisely that epi (hom f) is a convex cone in (ℝ × E) × ℝ. Unlike PosHomogeneous.epiCone, this needs no ∀ x, f x ≠ ⊥, because closure under addition comes from convexity of the cone rather than from subadditivity.

Equations

• Tdaf.ConvexAnalysis.homEpiCone hf = { carrier := Tdaf.ConvexAnalysis.epi (Tdaf.ConvexAnalysis.hom f), smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.coe_homEpiCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) : ↑(homEpiCone hf) = epi (hom f)

The carrier of homEpiCone is the epigraph of hom f.

The associativity shuffle

epi (hom f) and homCone f live in (ℝ × E) × ℝ, while the cone generated by {1} ×ˢ epi f — the form the downstream applications use — lives in ℝ × (E × ℝ). LinearEquiv.prodAssoc ℝ ℝ E ℝ relates them.

theorem Tdaf.ConvexAnalysis.homCone_eq_preimage {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : homCone f = ⇑(LinearEquiv.prodAssoc ℝ ℝ E ℝ) ⁻¹' ({0} ∪ ⋃ (a : ℝ), ⋃ (_ : a > 0), a • {1} ×ˢ epi f)

The generated cone, read in ℝ × (E × ℝ): it is the cone generated by {1} ×ˢ epi f, pulled back along the associativity shuffle.

theorem Tdaf.ConvexAnalysis.prodAssoc_image_homCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : ⇑(LinearEquiv.prodAssoc ℝ ℝ E ℝ) '' homCone f = {0} ∪ ⋃ (a : ℝ), ⋃ (_ : a > 0), a • {1} ×ˢ epi f

The generated cone, transported to ℝ × (E × ℝ): it is the convex cone generated by {1} ×ˢ epi f.