Limitation of `ConvexOn` Definition in mathlib4

Stream: maths

[Zichen Wang]

Hello everyone,

I would like to raise a concern regarding the current definition of ConvexOn in mathlib4. Specifically, I think the existing definition is somewhat restrictive and does not accommodate a broader class of functions, particularly those with values in the extended real numbers (EReal).

Current ConvexOn Definition

The ConvexOn definition in mathlib4 is as follows:
https://github.com/leanprover-community/mathlib4/blob/666dd63743750d3bf814c328bd6a1c86ffb52c8e/Mathlib/Analysis/Convex/Function.lean#L49-L52

/-- Convexity of functions -/

def ConvexOn : Prop :=
  Convex 𝕜 s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
    f (a • x + b • y) ≤ a • f x + b • f y

This definition requires that for any two points within the set s and any convex combination of these points, the function value at the combination is less than or equal to the convex combination of the function values at these points.

Issue with EReal-Valued Functions

Consider the following example of a function defined on the real line:

def f (x : ℝ) : EReal :=

  if 0 ≤ x ∧ x ≤ 1 then ⊥ else ⊤

Intuitively, according to Convex Analysis by Ralph Tyrell Rockafellar , this function should be convex because its epigraph (the set of points lying on or above its graph) is a convex set. However, according to the current ConvexOn definition in mathlib4, this function is not recognized as convex. The reason is that when dealing with EReal values, expressions like⊤ + ⊥become ⊥, causing the convexity condition to fail.

I wonder if there's a good way to solve this problem.

[Lua Viana Reis]

PrinChern said:

Intuitively, according to Convex Analysis by Ralph Tyrell Rockafellar , this function should be convex because its epigraph (the set of points lying on or above its graph) is a convex set.

But if it includes the points on the graph, how would you define convexity in ℝ × EReal? Don't you fall into the same sort of problem where there is no useful way to make convex combinations of points?

[Zichen Wang]

You're right :+1: ! So I wonder if there's a good way to solve this problem :sob:

Lucas Viana Reis 发言道：

PrinChern said:

Intuitively, according to Convex Analysis by Ralph Tyrell Rockafellar , this function should be convex because its epigraph (the set of points lying on or above its graph) is a convex set.

But if it includes the points on the graph, how would you define convexity in ℝ × EReal? Don't you fall into the same sort of problem where there is no useful way to make convex combinations of points?

.

[Yaël Dillies]

The Rockafellar definition of convexity seems to be a separate definition to the one we have. If it has applications, then mathlib could acquire it (without touching ConvexOn)

[Yaël Dillies]

Can you clarify whether the definition of concavity is correct according to you for EReal-valued functions?

[Zichen Wang]

Rockafellar says

Let f be a function with its values in [-∞, ∞], and let its domain be a subset S of ℝ^n . The set

{ (x, μ) | x ∈ S, μ ∈ ℝ ,μ ≥ f(x) }

is called the epigraph of f, denoted as epi f.

If epi f is a convex subset of ℝ^{n + 1}, then f is called a convex function on S.

We can write in lean as follow:

variable {E : Type*}[AddCommMonoid E][SMul ℝ E]
def epi (f : E → EReal) (s : Set E) : Set (E × ℝ) :=
  {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}
def ConvexOn_rockafellar (s : Set E) (f : E → EReal) : Prop :=
  Convex ℝ (epi f s)

[Violeta Hernández]

The reason is that when dealing with EReal values, expressions like⊤ + ⊥become ⊥, causing the convexity condition to fail.

I think the condition you want isn't convexity but rather docs#Set.OrdConnected. In a linearly ordered field like ℝ both notions match, but in other linearly ordered semirings they can be distinct.

[Chenyi Li]

I am collaborating with PrinChern on developing a more general definition of convexity for functions whose values lie in the extended real numbers, with the domain potentially being a Hilbert space or a normed space. We are exploring the possibility of using the definition of Set.OrdConnected to characterize convexity but are uncertain about how it can be applied, as the domain may not necessarily be pre-ordered.

[Yaël Dillies]

Yes, I think Violeta is confusing convexity of functions with convexity of sets

[Violeta Hernández]

Both definitions are linked together, aren't they? For a function to be convex on a set, said set must be convex

[Zichen Wang]

/-- Convexity of functions -/
def ConvexOn' : Prop :=
  Convex 𝕜 s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 →
   ∀ ⦃u⦄, f x < u → ∀ ⦃v⦄, f y < v →
    f (a • x + b • y) < a • u + b • v

We can also define as this way?
On the one hand, this definition is the same as before, and on the other hand, it is also applicable to cases where the value range is EReal, since we avoid  expressions like⊤ + ⊥.

[Lua Viana Reis]

But your previous ConvexOn_rockafellar definition already avoids ⊤ + ⊥ and works withf : S -> EReal right? The epigraph as you defined is a subset of  ℝ^{n + 1}.

[Lua Viana Reis]

perhaps I'm not sure of what is the problem that we could help you with

[Zichen Wang]

Lucas Viana Reis 发言道：

But your previous ConvexOn_rockafellar definition already avoids ⊤ + ⊥ and works withf : S -> EReal right? The epigraph as you defined is a subset of  ℝ^{n + 1}.

Yes, you are right. But ConvexOn_rockafellar can only work when the value range is EReal.

ConvexOn' can also work in more general situation.This definition ConvexOn' is equivalent to the previous definition ConvexOn when [LinearOrder 𝕜].

[Zichen Wang]

@Alexander Bentkamp

hi~. Sorry to bother u. We have a little confusion about the definition ConvexOn in mathlib4.

Could u please give us some comments if convenient?

[Alexander Bentkamp]

I cant contribute much to the discussion since I have written the definition only with real valued functions in mind. Nonetheless, your ConvexOn' function looks good to me.