Extended-real-valued concave functions

The concave counterpart of Tdaf/Analysis/Convex/Epigraph.lean, for g : E → EReal. Concavity is defined geometrically, as convexity of the hypograph, exactly as convexity is defined by convexity of the epigraph; -g appears only in the transfer lemmas. Rockafellar mixes the two theories constantly from Part VI on, so the concave notions need first-class names rather than being spelled ConvexFn (-g) at every use.

Sign transfer is not free on EReal, because negation does not distribute over addition: -(⊥ + ⊤) = ⊤ while (-⊥) + (-⊤) = ⊥. This is why concaveFn_iff_le needs ∀ x, g x ≠ ⊤, mirroring the ∀ x, f x ≠ ⊥ of convexFn_iff_le, while concaveFn_iff_forall_gt, which never forms a sum of infinities, needs no hypothesis at all.

Main definitions

• hypo g — the hypograph of g, a subset of E × ℝ. Rockafellar writes epi g for it, overloading the notation; we do not.
• domConcave g — the effective domain, the set where g > -∞. This is not dom.
• ProperConcave g — g is finite somewhere and never ⊤.
• restrictConcave s g — g restricted to s, extended by ⊥.
• ConcaveFn g — g is concave, meaning that hypo g is convex.

Main results

• hypo_neg, epi_neg — hypograph and epigraph are exchanged by the reflection (x, μ) ↦ (x, -μ).
• concaveFn_iff_convexFn_neg — "g is concave when -g is convex", recovered as a theorem. With domConcave_eq_dom_neg and properConcave_iff_proper_neg this is the sign dictionary through which the concave theory is derived from the convex one.
• concaveFn_iff_forall_gt, concaveFn_iff_le — concavity as an inequality on values, strict and non-strict.
• ConcaveFn.convex_gt, ConcaveFn.convex_ge — superlevel sets of a concave function are convex.
• concaveOn_iff_concaveFn — the bridge to Mathlib's ConcaveOn.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §30 for the concave conventions, §4 for the convex statements being mirrored.

Hypographs, domains, properness

def Tdaf.ConvexAnalysis.hypo {E : Type u_1} (g : E → EReal) : Set (E × ℝ)

The hypograph of g : E → EReal, {(x, μ) | μ ∈ ℝ, μ ≤ g x} ⊆ E × ℝ. Rockafellar writes this epi g, reusing the epigraph notation; we keep the two names apart. As with epi, the second coordinate ranges over the reals.

Equations

• Tdaf.ConvexAnalysis.hypo g = {p : E × ℝ | ↑p.2 ≤ g p.1}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_hypo {E : Type u_1} {g : E → EReal} {p : E × ℝ} : p ∈ hypo g ↔ ↑p.2 ≤ g p.1

theorem Tdaf.ConvexAnalysis.mk_mem_hypo {E : Type u_1} {g : E → EReal} {x : E} {μ : ℝ} : (x, μ) ∈ hypo g ↔ ↑μ ≤ g x

theorem Tdaf.ConvexAnalysis.hypo_mono {E : Type u_1} {g h : E → EReal} (hgh : g ≤ h) : hypo g ⊆ hypo h

The hypograph is monotone in the function, where the epigraph is antitone.

theorem Tdaf.ConvexAnalysis.le_iff_hypo_subset {E : Type u_1} {g h : E → EReal} : g ≤ h ↔ hypo g ⊆ hypo h

The hypograph determines the function: g ≤ h exactly when hypo g ⊆ hypo h.

theorem Tdaf.ConvexAnalysis.hypo_neg {E : Type u_1} (g : E → EReal) : hypo g = Prod.map id Neg.neg ⁻¹' epi fun (x : E) => -g x

The hypograph of g is the vertical reflection (x, μ) ↦ (x, -μ) of the epigraph of -g. This — not a definition — is Rockafellar's "g is concave when -g is convex", at the level of sets. It holds for every g, with no side condition, because it involves no addition on EReal.

theorem Tdaf.ConvexAnalysis.epi_neg {E : Type u_1} (g : E → EReal) : (epi fun (x : E) => -g x) = Prod.map id Neg.neg ⁻¹' hypo g

The epigraph of -g is the vertical reflection (x, μ) ↦ (x, -μ) of the hypograph of g; the converse direction of hypo_neg, the reflection being an involution.

theorem Tdaf.ConvexAnalysis.hypo_eq_image_epi_neg {E : Type u_1} (g : E → EReal) : hypo g = Prod.map id Neg.neg '' epi fun (x : E) => -g x

hypo_neg with the reflection applied as an image rather than a preimage.

def Tdaf.ConvexAnalysis.domConcave {E : Type u_1} (g : E → EReal) : Set E

The effective domain of a concave function: the set where g > -∞. It is the projection of the hypograph, domConcave_eq_fst_image_hypo.

Equations

• Tdaf.ConvexAnalysis.domConcave g = {x : E | ⊥ < g x}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_domConcave {E : Type u_1} {g : E → EReal} {x : E} : x ∈ domConcave g ↔ ⊥ < g x

theorem Tdaf.ConvexAnalysis.domConcave_eq_dom_neg {E : Type u_1} (g : E → EReal) : domConcave g = dom fun (x : E) => -g x

The concave effective domain of g is the convex effective domain of -g.

theorem Tdaf.ConvexAnalysis.domConcave_eq_fst_image_hypo {E : Type u_1} (g : E → EReal) : domConcave g = Prod.fst '' hypo g

The mirror of dom_eq_fst_image_epi: domConcave g is the projection of hypo g on E, with no hypothesis on g.

structure Tdaf.ConvexAnalysis.ProperConcave {E : Type u_1} (g : E → EReal) : Prop

g is a proper concave function when it is finite somewhere and never takes the value ⊤; equivalently, when -g is proper (properConcave_iff_proper_neg).

• domConcave_nonempty : (domConcave g).Nonempty

  g is not identically ⊥.

• ne_top (x : E) : g x ≠ ⊤

  g never takes the value ⊤.

theorem Tdaf.ConvexAnalysis.properConcave_iff_proper_neg {E : Type u_1} {g : E → EReal} : ProperConcave g ↔ Proper fun (x : E) => -g x

Rockafellar's own definition of properness for a concave function: g is proper exactly when -g is.

noncomputable def Tdaf.ConvexAnalysis.restrictConcave {E : Type u_1} (s : Set E) (g : E → EReal) : E → EReal

g restricted to s and extended by ⊥ off s: the concave counterpart of restrict, which extends by ⊤. The ⨆ formulation avoids a decidability hypothesis; restrictConcave_of_mem and restrictConcave_of_notMem are the defining equations.

Equations

• Tdaf.ConvexAnalysis.restrictConcave s g x = ⨆ (_ : x ∈ s), g x

@[simp]

theorem Tdaf.ConvexAnalysis.restrictConcave_of_mem {E : Type u_1} {s : Set E} {g : E → EReal} {x : E} (hx : x ∈ s) : restrictConcave s g x = g x

@[simp]

theorem Tdaf.ConvexAnalysis.restrictConcave_of_notMem {E : Type u_1} {s : Set E} {g : E → EReal} {x : E} (hx : x ∉ s) : restrictConcave s g x = ⊥

theorem Tdaf.ConvexAnalysis.neg_restrictConcave {E : Type u_1} (s : Set E) (g : E → EReal) : (fun (x : E) => -restrictConcave s g x) = restrict s fun (x : E) => -g x

Extension by ⊥ and extension by ⊤ correspond under negation.

Concave functions

structure Tdaf.ConvexAnalysis.ConcaveFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] (g : E → EReal) : Prop

A function g : E → EReal is concave when its hypograph is a convex subset of E × ℝ. This mirrors ConvexFn, and agrees with the definition by "-g is convex" through concaveFn_iff_convexFn_neg.

• convex_hypo : Convex ℝ (hypo g)

  The hypograph of a concave function is convex.

@[simp]

theorem Tdaf.ConvexAnalysis.concaveFn_iff_convex_hypo {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} : ConcaveFn g ↔ Convex ℝ (hypo g)

theorem Tdaf.ConvexAnalysis.ConcaveFn.hypo_combo {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} (hg : ConcaveFn g) {x y : E} {μ ν : ℝ} (hx : ↑μ ≤ g x) (hy : ↑ν ≤ g y) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : ↑(a * μ + b * ν) ≤ g (a • x + b • y)

The defining property of concavity, in the form in which it is used: a convex combination of two points of the hypograph lies in the hypograph.

theorem Tdaf.ConvexAnalysis.concaveFn_of_hypo_combo {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} (h : ∀ (x y : E) (μ ν : ℝ), ↑μ ≤ g x → ↑ν ≤ g y → ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → a + b = 1 → ↑(a * μ + b * ν) ≤ g (a • x + b • y)) : ConcaveFn g

Conversely, the combination property characterises concavity.

theorem Tdaf.ConvexAnalysis.concaveFn_iff_convexFn_neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} : ConcaveFn g ↔ ConvexFn fun (x : E) => -g x

A function is concave exactly when its negative is convex. Like hypo_neg, this needs no side condition: negation reverses only the order here, never a sum.

theorem Tdaf.ConvexAnalysis.ConcaveFn.convexFn_neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} (hg : ConcaveFn g) : ConvexFn fun (x : E) => -g x

The forward direction of concaveFn_iff_convexFn_neg.

theorem Tdaf.ConvexAnalysis.ConvexFn.concaveFn_neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) : ConcaveFn fun (x : E) => -f x

The mirror of ConcaveFn.convexFn_neg: a convex function has a concave negative.

Concavity as a strict inequality on values

theorem Tdaf.ConvexAnalysis.concaveFn_iff_forall_gt {E : Type u_1} [AddCommGroup E] [Module ℝ E] (g : E → EReal) : ConcaveFn g ↔ ∀ (x y : E) (a b : ℝ), 0 < a → 0 < b → a + b = 1 → ∀ (α β : ℝ), ↑α < g x → ↑β < g y → ↑(a * α + b * β) < g (a • x + b • y)

Concavity in strict inequalities. A function g : E → EReal is concave if and only if g ((1 - λ) x + λ y) > (1 - λ) α + λ β whenever g x > α, g y > β and 0 < λ < 1. The strict inequalities keep α and β real, so no ∞ - ∞ arises and no hypothesis on g is needed.

Concavity as an inequality on values

theorem Tdaf.ConvexAnalysis.concaveFn_iff_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} (hg : ∀ (x : E), g x ≠ ⊤) : ConcaveFn g ↔ ∀ (x y : E) (a b : ℝ), 0 < a → 0 < b → a + b = 1 → ↑a * g x + ↑b * g y ≤ g (a • x + b • y)

For a function g that never takes the value ⊤ — equivalently, a function into [-∞, +∞) — concavity is the familiar reversed inequality. The hypothesis is what makes the right-hand side of the convex form negate to the left-hand side here: on EReal, -(u + v) = -u + -v fails when one summand is ⊤ and the other ⊥.

Level sets and the effective domain

theorem Tdaf.ConvexAnalysis.ConcaveFn.convex_gt {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} (hg : ConcaveFn g) (α : EReal) : Convex ℝ {x : E | α < g x}

Strict superlevel sets of a concave function are convex.

theorem Tdaf.ConvexAnalysis.ConcaveFn.convex_ge {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} (hg : ConcaveFn g) (α : EReal) : Convex ℝ {x : E | α ≤ g x}

Superlevel sets of a concave function are convex. These are the sets whose closedness characterises upper semicontinuity.

theorem Tdaf.ConvexAnalysis.ConcaveFn.convex_domConcave {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} (hg : ConcaveFn g) : Convex ℝ (domConcave g)

The effective domain of a concave function is convex.

The bridge to Mathlib's ConcaveOn

theorem Tdaf.ConvexAnalysis.hypo_restrictConcave_coe {E : Type u_1} (s : Set E) (g : E → ℝ) : hypo (restrictConcave s fun (x : E) => ↑(g x)) = {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1}

The hypograph of a real-valued function extended by ⊥, in the shape Mathlib's concaveOn_iff_convex_hypograph expects.

theorem Tdaf.ConvexAnalysis.concaveOn_iff_concaveFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s : Set E) (g : E → ℝ) : ConcaveOn ℝ s g ↔ ConcaveFn (restrictConcave s fun (x : E) => ↑(g x))

Mathlib's ConcaveOn for a real-valued function on a set agrees with ConcaveFn for its extension by ⊥; compare convexOn_iff_convexFn.