Minimum of a convex function exists

Stream: Is there code for X?

[Snir Broshi]

A convex function doesn't always have a minimum, e.g. the identity function, but I think a sufficient condition is having x < y < z such that f y < f x ∧ f y < f z, or more generally not being monotone nor antitone:

theorem foo {α β 𝕜 : Type*} [Preorder α] [PartialOrder β] [Semiring 𝕜] [PartialOrder 𝕜]
    [AddCommMonoid α] [AddCommMonoid β] [SMul 𝕜 α] [SMul 𝕜 β]
    {f : α → β} {s : Set α} (hf : ConvexOn 𝕜 s f) :
    ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, IsMinOn f s a := by
  sorry

Is this theorem true? Is there code for it, or an easy way to prove it?

(this might require adding LinearOrder or IsStrictOrderedRing or Field)
(I could reach for the extreme-value-theorem (docs#IsCompact.exists_isMinOn + docs#ConvexOn.continuousOn_interior) but that requires changing the statement to be about reals)

[Kenny Lau]

take $(x-\pi)^2 : \Bbb Q \to \Bbb R$

[Snir Broshi]

Hmm, does requiring the domain and range to be the same fix it?
Is there any way to fix it without requiring fancy stuff like continuity (of f) or completeness (of the domain)?

[Snir Broshi]

I think a similar example can work for $\Bbb Q \to \Bbb Q$ but I'm not sure

[Bhavik Mehta]

$(x^2 - 2)^2 : \mathbb{Q} \to \mathbb{Q}$ ought to break it; this feels like you need completeness of the domain

[Snir Broshi]

Bhavik Mehta said:

$x^2 - 2 : \mathbb{Q} \to \mathbb{Q}$ ought to break it; this feels like you need completeness of the domain

That has a minimum at x = 0

[Bhavik Mehta]

oops, edited

[Snir Broshi]

ooh nice

[Snir Broshi]

I guess I can require compactness of the domain rather than completeness, which eliminates the rational examples at least

[Snir Broshi]

Though that makes the statement pretty close to the extreme-value-theorem

[Snir Broshi]

Maybe weakening the requirements of docs#ConvexOn.continuousOn_interior is the way to go, can they be weaker? Surely it can't be true only for reals

[Bhavik Mehta]

To me, it seems like you want something much closer to docs#IsCompact.exists_isMinOn, but it's hard to tell without your application.

[Snir Broshi]

Yeah but that requires converting ConvexOn to ContinuousOn somehow

[Snir Broshi]

the application is not very relevant - I was trying to find a minimum of the gamma function, but since it's continuous for positive reals I don't need anything generic about convex functions and can just use the extreme-value-theorem directly (#31409). I'm still curious about whether convexity can help finding a minimum

[Aaron Liu]

For a nonempty compact set K and a linear order L and an arbitrary function f : K -> L, according to my intuition there should exists a point x in K such that the liminf of f(y) as y -> x is globally minimized

[Aaron Liu]

maybe if you're also convex that would let the liminf minimizer to be also minimizing the function value

[Aaron Liu]

note that f doesn't need to be continuous (if I'm intuiting this correctly)