A Local Maximum of a Concave Function
is a Global Maximum

TheoryGuru applications

Load Economicreasoning package only if it is not already loaded

If[Length@Names["PLTools`*"]<10,
Get["http://economicreasoning.com"]]

Setup

fisaconcavefunction=0≤λ≤1\[Implies](1-λ) f[x]+λ f[y]≤f[(1-λ) x+λ y]; (* for any x and y and λ *)

xachieveslocalmax=0<λ≤ϵ[y]< 1&&f[x]≥f[(1-λ) x+λ y] (*
 x is any allocation.
y is any allocation not local to x.
ϵ[y] is the radius bounding what is local to x *);

xachievesglobalmax=f[x]≥f[y];

Result on Local vs Global Maximum

TheoryGuru[{fisaconcavefunction,xachieveslocalmax},
xachievesglobalmax]

Proof is from Beck (2014, Section 8.1), and many others.

Variable interpretations

x and y are not necessarily real numbers

x=;
y=;

TheoryGuru[{fisaconcavefunction,xachieveslocalmax},
xachievesglobalmax]

Column@MostRecentAssumption
MostRecentHypothesis

This model only says that λ, f[x], f[y], f[λx+(1-λ)y], ϵ[y] are real numbers because those five appear as part of inequalities.

x and y appear in the model only as arguments of f and therefore could be vectors, flags, an abstract object, etc.  It is up to the user to ensure that convex combinations of x and y are meaningful.

TheoryGuru only “knows” that f[x], f[y], and f[λx+(1-λ)y] are potentially distinct real numbers because the arguments of f are different.  e.g., it automatically assumes that f[x] == f[x] but not that f[x] == f[y].

Setup for Unique Maximum

Strict concavity references equality.  If x and y are, say, vectors rather than scalars, then == should not be used because TheoryGuru interprets the arguments of == as real numbers (e.g., by having the assumption x == y, then x and y are automatically interpreted as real numbers).

Here I define my own vector equality function SameVector (you could name it whatever you want), which I interpret as mapping pairs of vector to a Boolean according to whether the two vectors are the same.

Remove[x,y]

fisastrictlyconcavefunction=(Not@SameVector[x,y]∧0<λ<1)\[Implies]
(1-λ) f[x]+λ f[y]<f[(1-λ) x+λ y]; (* for any x and y and λ *)

xachievesglobalmax=f[x]≥f[(1-λ) x+λ y];
yachievesglobalmax=f[y]≥f[(1-λ) x+λ y];

Result: the Global Maximum of a Strictly Concave Function is Unique

TheoryGuru[{0<λ<1,
fisastrictlyconcavefunction,xachievesglobalmax,yachievesglobalmax},

SameVector[x,y]]

TheoryGuru[{0<λ<1,
fisastrictlyconcavefunction,xachievesglobalmax},

SameVector[x,y]∨Not@yachievesglobalmax]

Proof is from Beck (2014, Section 8.1), and many others.

Use the TheoryBooleans command to see which variable was (variables were) automatically recognized as Booleans.

TheoryBooleans

Variable interpretations