The function determined by a set in E × ℝ

To build a convex function on E, build a convex set F ⊆ E × ℝ and take ofEpi F, the function whose graph is the lower boundary of F: ofEpi F x = inf {μ : ℝ | (x, μ) ∈ F}, an infimum in EReal, hence ⊤ over an empty vertical section and ⊥ over one unbounded below. Infimal convolution, right scalar multiplication, the convex hull of a family of functions, the image under a linear map and the lower-semicontinuous hull are all ofEpi of a set built from epigraphs. No structure on E is needed; only the convexity statement itself asks for a real vector space.

epi (ofEpi F) = F is false in general — only F ⊆ epi (ofEpi F) always holds — and IsEpiLike F names the sets where it does. That predicate is not preserved by the operations that matter most: a sum of epigraphs need not be an epigraph, since an infimal convolution need not attain its infimum, and nor need the convex hull of a union. Those modules carry it as a hypothesis.

Main results

• subset_epi_iff_le_ofEpi — the adjunction F ⊆ epi g ↔ g ≤ ofEpi F: epi and ofEpi form an antitone Galois connection (gc_ofEpi_epi, epiClosure) whose closed elements are the epi-like sets, and the order facts below are formal consequences.
• convexFn_ofEpi — ofEpi F is convex when F is.
• ofEpi_epi — ofEpi (epi f) = f, with no hypothesis; epi_ofEpi is the converse, under IsEpiLike.
• IsEpiLike.iInter, .inter, .union, .of_isClosed, .closure — the stability properties the operations of this section consume.

References

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

The function determined by a set

noncomputable def Tdaf.ConvexAnalysis.ofEpi {E : Type u_1} (F : Set (E × ℝ)) : E → EReal

The function whose graph is the lower boundary of a set F ⊆ E × ℝ: ofEpi F x = inf {μ | (x, μ) ∈ F}, an infimum in EReal.

Equations

• Tdaf.ConvexAnalysis.ofEpi F x = ⨅ μ ∈ {μ : ℝ | (x, μ) ∈ F}, ↑μ

theorem Tdaf.ConvexAnalysis.ofEpi_apply_le {E : Type u_1} {F : Set (E × ℝ)} {x : E} {μ : ℝ} (h : (x, μ) ∈ F) : ofEpi F x ≤ ↑μ

theorem Tdaf.ConvexAnalysis.le_ofEpi {E : Type u_1} {F : Set (E × ℝ)} {x : E} {z : EReal} (h : ∀ (μ : ℝ), (x, μ) ∈ F → z ≤ ↑μ) : z ≤ ofEpi F x

theorem Tdaf.ConvexAnalysis.ofEpi_lt_iff {E : Type u_1} {F : Set (E × ℝ)} {x : E} {z : EReal} : ofEpi F x < z ↔ ∃ (μ : ℝ), (x, μ) ∈ F ∧ ↑μ < z

The workhorse: the infimum defining ofEpi F x need not be attained, so arguments about ofEpi proceed through a strict inequality, which does produce a witness.

theorem Tdaf.ConvexAnalysis.subset_epi_iff_le_ofEpi {E : Type u_1} {F : Set (E × ℝ)} {g : E → EReal} : F ⊆ epi g ↔ g ≤ ofEpi F

The universal property: ofEpi F is the greatest function whose epigraph contains F.

theorem Tdaf.ConvexAnalysis.subset_epi_ofEpi {E : Type u_1} (F : Set (E × ℝ)) : F ⊆ epi (ofEpi F)

The reverse inclusion is epi_ofEpi, and needs IsEpiLike.

theorem Tdaf.ConvexAnalysis.ofEpi_mono {E : Type u_1} {F G : Set (E × ℝ)} (h : F ⊆ G) : ofEpi G ≤ ofEpi F

theorem Tdaf.ConvexAnalysis.ofEpi_eq_top_iff {E : Type u_1} {F : Set (E × ℝ)} {x : E} : ofEpi F x = ⊤ ↔ ∀ (μ : ℝ), (x, μ) ∉ F

@[simp]

theorem Tdaf.ConvexAnalysis.ofEpi_empty {E : Type u_1} : ofEpi ∅ = ⊤

@[simp]

theorem Tdaf.ConvexAnalysis.ofEpi_univ {E : Type u_1} : ofEpi Set.univ = ⊥

@[simp]

theorem Tdaf.ConvexAnalysis.ofEpi_epi {E : Type u_1} (f : E → EReal) : ofEpi (epi f) = f

No hypothesis: a vertical section of an epigraph is ∅, ℝ or a closed half-line, and in each case its infimum is the value of f.

theorem Tdaf.ConvexAnalysis.eq_ofEpi_of_epi_eq {E : Type u_1} {F : Set (E × ℝ)} {f : E → EReal} (h : epi f = F) : f = ofEpi F

theorem Tdaf.ConvexAnalysis.ofEpi_apply_congr {E : Type u_1} {F G : Set (E × ℝ)} {x : E} (h : ∀ (μ : ℝ), (x, μ) ∈ F ↔ (x, μ) ∈ G) : ofEpi F x = ofEpi G x

theorem Tdaf.ConvexAnalysis.dom_ofEpi {E : Type u_1} (F : Set (E × ℝ)) : dom (ofEpi F) = Prod.fst '' F

For any F: ofEpi F x < ⊤ says exactly that the vertical section over x is nonempty.

The Galois connection between sets and functions

OrderDual on the function side makes the antitone adjunction fit Mathlib's monotone GaloisConnection.

theorem Tdaf.ConvexAnalysis.gc_ofEpi_epi {E : Type u_1} : GaloisConnection (fun (F : Set (E × ℝ)) => OrderDual.toDual (ofEpi F)) fun (g : (E → EReal)ᵒᵈ) => epi (OrderDual.ofDual g)

noncomputable def Tdaf.ConvexAnalysis.gi_ofEpi_epi {E : Type u_1} : GaloisInsertion (fun (F : Set (E × ℝ)) => OrderDual.toDual (ofEpi F)) fun (g : (E → EReal)ᵒᵈ) => epi (OrderDual.ofDual g)

An insertion, because ofEpi (epi f) = f on the nose.

Equations

• Tdaf.ConvexAnalysis.gi_ofEpi_epi = ⋯.toGaloisInsertion ⋯

noncomputable def Tdaf.ConvexAnalysis.epiClosure {E : Type u_1} : ClosureOperator (Set (E × ℝ))

The closure operator F ↦ epi (ofEpi F); its closed elements are the epi-like sets.

Equations

• Tdaf.ConvexAnalysis.epiClosure = ⋯.closureOperator

@[simp]

theorem Tdaf.ConvexAnalysis.epiClosure_apply {E : Type u_1} (F : Set (E × ℝ)) : epiClosure F = epi (ofEpi F)

theorem Tdaf.ConvexAnalysis.epi_injective {E : Type u_1} : Function.Injective epi

Sets that are epigraphs

def Tdaf.ConvexAnalysis.IsEpiLike {E : Type u_1} (F : Set (E × ℝ)) : Prop

F ⊆ E × ℝ is epi-like when it is the epigraph of some function E → EReal. Equivalently (isEpiLike_iff_forall), every vertical section {μ | (x, μ) ∈ F} is upward closed and attains its infimum — is ∅, ℝ, or a closed half-line Set.Ici c.

Both halves are needed: it fails for {p | 0 < p.2} (upward closed, does not attain) and for {(0, 0)} (attains, not upward closed). The witness is always ofEpi F (isEpiLike_iff).

Equations

• Tdaf.ConvexAnalysis.IsEpiLike F = ∃ (f : E → EReal), F = Tdaf.ConvexAnalysis.epi f

@[simp]

theorem Tdaf.ConvexAnalysis.isEpiLike_epi {E : Type u_1} (f : E → EReal) : IsEpiLike (epi f)

@[simp]

theorem Tdaf.ConvexAnalysis.epi_ofEpi {E : Type u_1} {F : Set (E × ℝ)} (h : IsEpiLike F) : epi (ofEpi F) = F

The point of IsEpiLike. For an epi-like set the two constructions are inverse.

theorem Tdaf.ConvexAnalysis.isEpiLike_iff {E : Type u_1} {F : Set (E × ℝ)} : IsEpiLike F ↔ epi (ofEpi F) = F

theorem Tdaf.ConvexAnalysis.isEpiLike_iff_isClosed {E : Type u_1} {F : Set (E × ℝ)} : IsEpiLike F ↔ epiClosure.IsClosed F

theorem Tdaf.ConvexAnalysis.IsEpiLike.mem_of_le {E : Type u_1} {F : Set (E × ℝ)} {x : E} {μ ν : ℝ} (h : IsEpiLike F) (hμ : (x, μ) ∈ F) (hμν : μ ≤ ν) : (x, ν) ∈ F

theorem Tdaf.ConvexAnalysis.IsEpiLike.mem_of_forall_lt {E : Type u_1} {F : Set (E × ℝ)} {x : E} {μ : ℝ} (h : IsEpiLike F) (hμ : ∀ (ν : ℝ), μ < ν → (x, ν) ∈ F) : (x, μ) ∈ F

theorem Tdaf.ConvexAnalysis.isEpiLike_of_forall {E : Type u_1} {F : Set (E × ℝ)} (hmono : ∀ (x : E) (μ ν : ℝ), (x, μ) ∈ F → μ ≤ ν → (x, ν) ∈ F) (hbelow : ∀ (x : E) (μ : ℝ), (∀ (ν : ℝ), μ < ν → (x, ν) ∈ F) → (x, μ) ∈ F) : IsEpiLike F

The criterion one checks in practice.

theorem Tdaf.ConvexAnalysis.isEpiLike_iff_forall {E : Type u_1} {F : Set (E × ℝ)} : IsEpiLike F ↔ (∀ (x : E) (μ ν : ℝ), (x, μ) ∈ F → μ ≤ ν → (x, ν) ∈ F) ∧ ∀ (x : E) (μ : ℝ), (∀ (ν : ℝ), μ < ν → (x, ν) ∈ F) → (x, μ) ∈ F

theorem Tdaf.ConvexAnalysis.IsEpiLike.iInter {E : Type u_1} {ι : Sort u_2} {F : ι → Set (E × ℝ)} (h : ∀ (i : ι), IsEpiLike (F i)) : IsEpiLike (⋂ (i : ι), F i)

An intersection of epigraphs is an epigraph: that of the pointwise supremum.

theorem Tdaf.ConvexAnalysis.IsEpiLike.inter {E : Type u_1} {F G : Set (E × ℝ)} (hF : IsEpiLike F) (hG : IsEpiLike G) : IsEpiLike (F ∩ G)

theorem Tdaf.ConvexAnalysis.IsEpiLike.union {E : Type u_1} {F G : Set (E × ℝ)} (hF : IsEpiLike F) (hG : IsEpiLike G) : IsEpiLike (F ∪ G)

The epigraph of the pointwise minimum. This uses linearity of EReal and fails for infinite unions: the union of the epigraphs of the constants 1 / (n + 1) is not an epigraph.

Convexity of the function determined by a set

theorem Tdaf.ConvexAnalysis.convexFn_ofEpi {E : Type u_1} [AddCommGroup E] [Module ℝ E] {F : Set (E × ℝ)} (hF : Convex ℝ F) : ConvexFn (ofEpi F)

The function whose graph is the lower boundary of a convex set is convex. The route is convexFn_iff_forall_lt, which asks only for strict upper bounds, a non-strict one yielding no witness.

Epi-likeness and topology

theorem Tdaf.ConvexAnalysis.IsEpiLike.of_isClosed {E : Type u_1} [TopologicalSpace E] {F : Set (E × ℝ)} (hmono : ∀ (x : E) (μ ν : ℝ), (x, μ) ∈ F → μ ≤ ν → (x, ν) ∈ F) (hF : IsClosed F) : IsEpiLike F

Closedness buys the attainment half of IsEpiLike — a closed vertical section contains the infimum of its points — but not the other: {(0, 0)} is closed and is not an epigraph.

theorem Tdaf.ConvexAnalysis.IsEpiLike.closure {E : Type u_1} [TopologicalSpace E] {F : Set (E × ℝ)} [AddZeroClass E] [ContinuousAdd E] (h : IsEpiLike F) : IsEpiLike (_root_.closure F)

What lscHull f := ofEpi (closure (epi f)) needs, to satisfy epi (lscHull f) = cl (epi f).