Support functions

The support function of a set s ⊆ E with respect to a pairing B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ is δ*(y ∣ s) = sup {⟨x, y⟩ ∣ x ∈ s}. It describes all the closed half-spaces containing s, since s ⊆ {x ∣ ⟨x, y⟩ ≤ c} exactly when δ*(y ∣ s) ≤ c. Support functions are the conjugates of indicators (supportFn_eq_conj_indicatorFn), so every property of δ*(· ∣ s) is inherited from Duality/Conjugate.lean rather than proved again.

The main theorem is the correspondence: the support functions of the nonempty convex sets are exactly the closed proper positively homogeneous convex functions, and the two classes are in bijection. Note that the support function lives on the other side of the pairing, supportFn B s : F → EReal for s : Set E, so the correspondence — which asks both that g : F → EReal be closed and that the set it supports be closed in E — needs a topology and a compatible pairing on both sides.

Main definitions

• supportFn B s — the support function δ*(· ∣ s).
• supportSet B f — the set {y ∣ ∀ x, ⟨x, y⟩ ≤ f x}, of which f is the support function when f is closed, proper, positively homogeneous and convex. It inverts the correspondence.
• supportEquiv — the correspondence as a bijection between the nonempty closed convex subsets of E and the closed proper positively homogeneous convex functions on F.

Main results

• supportFn_eq_conj_indicatorFn — δ*(· ∣ s) = (δ(· ∣ s))*.
• mem_closure_convexHull_iff_le_supportFn — x ∈ cl (conv s) if and only if ⟨x, y⟩ ≤ δ*(y ∣ s) for every y (Theorem 13.1 in [^1]).
• conj_supportFn, exists_supportFn_iff, supportEquiv — the indicator and the support function of a closed convex set are conjugate, and the correspondence above (Theorem 13.2 in [^1]). exists_supportFn_finite_iff reads it as bounded ⟺ finite.
• clFn_eq_supportFn_of_posHomogeneous — the closure of a positively homogeneous convex function is a support function. supportSet_clFn is the consequence that closure does not change the set supported.
• conj_eq_indicatorFn_of_posHomogeneous — the engine of both: the conjugate of a positively homogeneous function is an indicator. Reindexing the supremum defining f* along x ↦ a • x shows f*(y) = a f*(y) for every a > 0, so f*(y) is 0, ⊤ or ⊥, and ⊥ is excluded as soon as f ≢ ⊤. No topology is used, which is why none of this needs separation theory beyond what biconjugation already used.
• supportFn_singleton, supportFn_union, supportFn_convexHull, supportFn_closure, supportFn_smul, supportFn_add — the support functions of the basic constructions.

Divergences from the reference

The finite form needs closedness. The classical deduction that a finite positively homogeneous convex function is a support function goes through "a finite convex function on Rⁿ is closed", which is false in infinite dimensions: a discontinuous linear functional is finite, convex and positively homogeneous, is not closed, and is the support function of nothing. So exists_supportFn_finite_iff carries ClosedFn, and reads "bounded" as "⟨·, y⟩ is bounded above on the set, for each y" — which is what the classical proof actually uses.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §13.

The support function

noncomputable def Tdaf.ConvexAnalysis.supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Set E) : F → EReal

The support function δ*(· | s) of a set s ⊆ E, with respect to the pairing B: δ*(y | s) = sup {⟨x, y⟩ | x ∈ s}. The δ* notation is justified by supportFn_eq_conj_indicatorFn: it really is the conjugate of the indicator function.

Equations

• Tdaf.ConvexAnalysis.supportFn B s y = ⨆ x ∈ s, ↑((B x) y)

theorem Tdaf.ConvexAnalysis.supportFn_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Set E) (y : F) : supportFn B s y = ⨆ x ∈ s, ↑((B x) y)

theorem Tdaf.ConvexAnalysis.supportFn_eq_conj_indicatorFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Set E) : supportFn B s = conj B (indicatorFn s)

Support functions are conjugates of indicators. This is why the file is short: every property of δ*(· | s) below is a property of a conjugate, cited from Conjugate.lean.

theorem Tdaf.ConvexAnalysis.le_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} {x : E} (hx : x ∈ s) (y : F) : ↑((B x) y) ≤ supportFn B s y

theorem Tdaf.ConvexAnalysis.supportFn_le_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} {y : F} {c : EReal} : supportFn B s y ≤ c ↔ ∀ x ∈ s, ↑((B x) y) ≤ c

theorem Tdaf.ConvexAnalysis.supportFn_le_coe_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} {y : F} {c : ℝ} : supportFn B s y ≤ ↑c ↔ ∀ x ∈ s, (B x) y ≤ c

The closed half-spaces containing s: s ⊆ {x | ⟨x, y⟩ ≤ c} if and only if c ≥ δ*(y | s).

theorem Tdaf.ConvexAnalysis.supportFn_le_zero_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} {y : F} : supportFn B s y ≤ 0 ↔ ∀ x ∈ s, (B x) y ≤ 0

δ*(y | s) ≤ 0 says that the pairing with y is nowhere positive on s — the level 0 of supportFn_le_coe_iff, which is where a polar cone is cut out.

theorem Tdaf.ConvexAnalysis.zero_lt_supportFn_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} {y : F} : 0 < supportFn B s y ↔ ∃ x ∈ s, 0 < (B x) y

0 < δ*(y | s) says that the pairing with y is positive somewhere on s.

theorem Tdaf.ConvexAnalysis.supportFn_mono {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s t : Set E} (h : s ⊆ t) : supportFn B s ≤ supportFn B t

@[simp]

theorem Tdaf.ConvexAnalysis.supportFn_empty {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : supportFn B ∅ = fun (x : F) => ⊥

@[simp]

theorem Tdaf.ConvexAnalysis.supportFn_singleton {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (x : E) : supportFn B {x} = fun (y : F) => ↑((B x) y)

theorem Tdaf.ConvexAnalysis.supportFn_union {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s t : Set E) : supportFn B (s ∪ t) = supportFn B s ⊔ supportFn B t

theorem Tdaf.ConvexAnalysis.supportFn_iUnion {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {ι : Sort u_3} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (u : ι → Set E) : supportFn B (⋃ (i : ι), u i) = fun (y : F) => ⨆ (i : ι), supportFn B (u i) y

theorem Tdaf.ConvexAnalysis.supportFn_ne_bot {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} (hs : s.Nonempty) (y : F) : supportFn B s y ≠ ⊥

@[simp]

theorem Tdaf.ConvexAnalysis.supportFn_zero {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} (hs : s.Nonempty) : supportFn B s 0 = 0

theorem Tdaf.ConvexAnalysis.proper_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} (hs : s.Nonempty) : Proper (supportFn B s)

theorem Tdaf.ConvexAnalysis.dom_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Set E) : dom (supportFn B s) = {y : F | ∃ (c : ℝ), ∀ x ∈ s, (B x) y ≤ c}

The effective domain of a support function is the barrier cone of s: the directions in which the pairing is bounded above on s.

theorem Tdaf.ConvexAnalysis.supportFn_lt_top_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} {y : F} : supportFn B s y < ⊤ ↔ ∃ (c : ℝ), ∀ x ∈ s, (B x) y ≤ c

Convexity and positive homogeneity

Both are inherited: convexity from conj, and homogeneity by reindexing the supremum.

theorem Tdaf.ConvexAnalysis.convexFn_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Set E) : ConvexFn (supportFn B s)

The support function of any set is convex — it is a conjugate.

theorem Tdaf.ConvexAnalysis.posHomogeneous_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Set E) : PosHomogeneous (supportFn B s)

The support function of any set is positively homogeneous.

theorem Tdaf.ConvexAnalysis.supportFn_add_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} (hs : s.Nonempty) (y₁ y₂ : F) : supportFn B s (y₁ + y₂) ≤ supportFn B s y₁ + supportFn B s y₂

Support functions are subadditive in the dual variable: a positively homogeneous convex function is subadditive, applied to posHomogeneous_supportFn.

theorem Tdaf.ConvexAnalysis.convex_setOf_pairing_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (y : F) (M : EReal) : Convex ℝ {x : E | ↑((B x) y) ≤ M}

theorem Tdaf.ConvexAnalysis.supportFn_convexHull {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Set E) : supportFn B ((convexHull ℝ) s) = supportFn B s

The support function does not see the convex hull.

theorem Tdaf.ConvexAnalysis.supportFn_smul {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {a : ℝ} (ha : 0 < a) (s : Set E) (y : F) : supportFn B (a • s) y = ↑a * supportFn B s y

The support function of a positive multiple of a set is the corresponding multiple of the support function.

theorem Tdaf.ConvexAnalysis.supportFn_add {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s t : Set E) : supportFn B (s + t) = supportFn B s + supportFn B t

The support function of a sum of sets is the sum of the support functions. Unconditional, unlike the corresponding statement for a sum of functions, because the two suprema never interact through an ∞ - ∞.

Conjugates of positively homogeneous functions

The mechanism behind everything that follows, and it needs no topology: reindexing the supremum that defines f* along x ↦ a • x shows that f*(y) is fixed by every positive scalar.

def Tdaf.ConvexAnalysis.supportSet {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : Set F

The set {y | ∀ x, ⟨x, y⟩ ≤ f x}. When f is closed, proper, convex and positively homogeneous this is the set whose support function is f (supportFn_supportSet); in general it is the effective domain of f*, viewed as an indicator.

Equations

• Tdaf.ConvexAnalysis.supportSet B f = {y : F | ∀ (x : E), ↑((B x) y) ≤ f x}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_supportSet {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {y : F} : y ∈ supportSet B f ↔ ∀ (x : E), ↑((B x) y) ≤ f x

theorem Tdaf.ConvexAnalysis.supportSet_eq_setOf_conj_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : supportSet B f = {y : F | conj B f y ≤ 0}

theorem Tdaf.ConvexAnalysis.convex_supportSet {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : Convex ℝ (supportSet B f)

theorem Tdaf.ConvexAnalysis.conj_smul_eq_self {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hf : PosHomogeneous f) {a : ℝ} (ha : 0 < a) (y : F) : conj B f y = ↑a * conj B f y

The conjugate of a positively homogeneous function is fixed by every positive scalar: the substance of f = λf ↔ f* = f*λ, obtained by reindexing the defining supremum.

theorem Tdaf.ConvexAnalysis.conj_eq_indicatorFn_of_posHomogeneous {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hf : PosHomogeneous f) (hne : ∃ (x : E), f x ≠ ⊤) : conj B f = indicatorFn (supportSet B f)

The conjugate of a positively homogeneous function is an indicator function. With supportFn_eq_conj_indicatorFn this is the duality between positive homogeneity and being an indicator that gauges and polarity rest on. The one hypothesis, f ≢ +∞, is genuinely needed: (+∞)* = -∞ is no indicator.

Closedness of the support function

theorem Tdaf.ConvexAnalysis.lowerSemicontinuous_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsContinuousPairing B.flip] {s : Set E} : LowerSemicontinuous (supportFn B s)

theorem Tdaf.ConvexAnalysis.closedFn_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsContinuousPairing B.flip] {s : Set E} [IsTopologicalAddGroup F] : ClosedFn (supportFn B s)

The support function of any set is a closed convex function — it is a conjugate.

The closure of the set

theorem Tdaf.ConvexAnalysis.isClosed_setOf_pairing_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsContinuousPairing B] (y : F) (M : EReal) : IsClosed {x : E | ↑((B x) y) ≤ M}

theorem Tdaf.ConvexAnalysis.supportFn_closure {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsContinuousPairing B] (s : Set E) : supportFn B (closure s) = supportFn B s

The support function does not see the closure.

theorem Tdaf.ConvexAnalysis.isClosed_supportSet {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsContinuousPairing B] (g : F → EReal) : IsClosed (supportSet B.flip g)

The closed convex hull

theorem Tdaf.ConvexAnalysis.mem_closure_convexHull_iff_le_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] (s : Set E) (x : E) : x ∈ closure ((convexHull ℝ) s) ↔ ∀ (y : F), ↑((B x) y) ≤ supportFn B s y

A point lies in the closed convex hull of s if and only if it satisfies every weak linear inequality that the support function of s records.

theorem Tdaf.ConvexAnalysis.closure_convexHull_subset_iff_supportFn_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] (s t : Set E) : closure ((convexHull ℝ) s) ⊆ closure ((convexHull ℝ) t) ↔ supportFn B s ≤ supportFn B t

Closed convex hulls are ordered by their support functions.

The closure of a positively homogeneous convex function

Only the space F carries a topology here: this is biconj_eq_clFn for the flipped pairing.

theorem Tdaf.ConvexAnalysis.clFn_eq_supportFn_of_posHomogeneous {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B.flip] {g : F → EReal} (hg : PosHomogeneous g) (hconv : ConvexFn g) (hne : ∃ (y : F), g y ≠ ⊤) : clFn g = supportFn B (supportSet B.flip g)

The closure of a positively homogeneous convex function that is not identically +∞ is the support function of the closed convex set supportSet B.flip g = {x | ∀ y, ⟨x, y⟩ ≤ g y}.

The improper case is included: if g takes -∞ then both sides are the support function of ∅.

theorem Tdaf.ConvexAnalysis.supportSet_clFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B.flip] {g : F → EReal} (hg : PosHomogeneous g) (hne : ∃ (y : F), g y ≠ ⊤) : supportSet B.flip (clFn g) = supportSet B.flip g

Taking the closure of a positively homogeneous function does not change the set it supports: the two conjugates agree and both are indicators, so the two supported sets agree. Convexity of g is not needed.

theorem Tdaf.ConvexAnalysis.supportFn_supportSet {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B.flip] {g : F → EReal} (hg : PosHomogeneous g) (hconv : ConvexFn g) (hcl : ClosedFn g) (hne : ∃ (y : F), g y ≠ ⊤) : supportFn B (supportSet B.flip g) = g

A closed positively homogeneous convex function is the support function of supportSet B.flip g.

theorem Tdaf.ConvexAnalysis.nonempty_supportSet {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B.flip] {g : F → EReal} (hg : PosHomogeneous g) (hcpc : ClosedProperConvexFn g) : (supportSet B.flip g).Nonempty

Sets and their support functions, in bijection

Both spaces carry topologies compatible with the pairing, exactly as for conjEquiv.

theorem Tdaf.ConvexAnalysis.conj_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} [IsCompatiblePairing B] (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) : conj B.flip (supportFn B s) = indicatorFn s

The indicator and the support function are conjugate to each other, for a closed convex set.

theorem Tdaf.ConvexAnalysis.conj_supportFn_of_convex {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} [IsCompatiblePairing B] (hs₁ : Convex ℝ s) : conj B.flip (supportFn B s) = indicatorFn (closure s)

The same with the closedness hypothesis dropped: the conjugate of a support function is the indicator of the closure of the set. This is the form a closedness conclusion is read off from, dom of the left side being cl s.

theorem Tdaf.ConvexAnalysis.supportSet_supportFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} [IsCompatiblePairing B] (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) : supportSet B.flip (supportFn B s) = s

A closed convex set is recovered from its support function.

theorem Tdaf.ConvexAnalysis.exists_supportFn_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : F → EReal} [IsContinuousPairing B] [IsCompatiblePairing B.flip] : (∃ (C : Set E), C.Nonempty ∧ Convex ℝ C ∧ IsClosed C ∧ g = supportFn B C) ↔ ClosedProperConvexFn g ∧ PosHomogeneous g

The characterisation: the support functions of the nonempty convex sets are exactly the closed proper positively homogeneous convex functions.

Stated for the nonempty closed convex sets, which give the same functions since the support function sees neither the closure nor the convex hull, so that the correspondence is one-to-one.

noncomputable def Tdaf.ConvexAnalysis.supportEquiv {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsCompatiblePairing B] [IsCompatiblePairing B.flip] : { C : Set E // C.Nonempty ∧ Convex ℝ C ∧ IsClosed C } ≃ { g : F → EReal // ClosedProperConvexFn g ∧ PosHomogeneous g }

The correspondence as a bijection between the nonempty closed convex sets and the closed proper positively homogeneous convex functions: the restriction of conjEquiv along the embeddings s ↦ δ(· | s) and "positively homogeneous".

Equations

• One or more equations did not get rendered due to their size.

theorem Tdaf.ConvexAnalysis.exists_supportFn_finite_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : F → EReal} [IsContinuousPairing B] [IsCompatiblePairing B.flip] : (∃ (C : Set E), C.Nonempty ∧ (∀ (y : F), ∃ (c : ℝ), ∀ x ∈ C, (B x) y ≤ c) ∧ g = supportFn B C) ↔ (∀ (y : F), g y ≠ ⊥) ∧ (∀ (y : F), g y ≠ ⊤) ∧ ConvexFn g ∧ ClosedFn g ∧ PosHomogeneous g

The support functions of the nonempty sets on which every ⟨·, y⟩ is bounded above are exactly the finite closed positively homogeneous convex functions.

The book has no ClosedFn hypothesis; it is needed outside finite dimensions, where a discontinuous linear functional is finite, convex, positively homogeneous and not closed.