Convex function: a complete certificate via the Jensen gap of a quadratic, and a single Jensen counterexample

Goal and scope

(1) Prove that f(x)=2x²−3x+1 is convex on the interval I=[−1,4]: first confirm that I is convex, then prove f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y) for all x,y∈I and all λ∈[0,1], by showing that the Jensen gap of a quadratic equals aλ(1−λ)(x−y)². (2) From the same identity, the affine function ℓ(x)=3x−5 gives equality on I. (3) Refute the convexity of g(x)=−x²+x on J=[0,2] with one exact Jensen violation, and explain why a few passing samples cannot prove convexity.

Stays inside the MKO's slice: explicitly declared nonempty real intervals as domains, univariate affine and quadratic functions, exact coefficients. Positive conclusions use algebraic certificates covering every x, y, λ; negative ones use a single exact violation. Strict convexity, subgradients, second-derivative tests and multivariate convex functions are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• order_basics
• square_nonneg
• distributive
• power_laws
• forall_intro
• quantifier_negation

• G1 — I=[−1,4]; f:I→ℝ, f(x)=2x²−3x+1 (a=2, b=−3, c=1).
• G2 — ℓ:I→ℝ, ℓ(x)=3x−5 (a=0, b=3, c=−5, affine).
• G3 — J=[0,2]; g:J→ℝ, g(x)=−x²+x (a=−1, b=1, c=0).

• I=[-1,4],\ J=[0,2] — the declared domain intervals
• \lambda\in[0,1] — the weight of the Jensen combination
• z=\lambda x+(1-\lambda)y — the convex combination of x and y
• G_q(x,y,\lambda) — the Jensen gap of q: λq(x)+(1−λ)q(y)−q(z)
• a,\ b,\ c — coefficients of the quadratic ax²+bx+c

Rules and sources

• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• mko_cvxf · cited — On a convex domain C, f is convex if f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y) for every x,y∈C and every λ∈[0,1]. One Jensen violation suffices to refute convexity, but one passing instance cannot prove it; positive certificates must cover every x, y and λ. · mko-convex-function
• mko_cvxset · cited — A subset C of a real vector space is convex if λx+(1−λ)y belongs to C for every x,y∈C and every λ∈[0,1]. · mko-convex-set
• mono_nonneg · prerequisite — Multiplying by a nonnegative number keeps the inequality: if u≤v and w≥0, then wu≤wv (for w>0 by the order of the reals; for w=0 both sides are 0).
• ineq_add · prerequisite — Adding inequalities: if u₁≤v₁ and u₂≤v₂, then u₁+u₂≤v₁+v₂.
• L_interval · lemma — If α≤s≤β, α≤t≤β and λ∈[0,1], then α≤λs+(1−λ)t≤β; hence every closed interval [α,β] is convex.
• L_gap · lemma — For q(x)=ax²+bx+c and any reals x, y, λ: λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)=aλ(1−λ)(x−y)².

Main derivation

f\ \text{convex on}\ I

I\ \text{convex}\ \land\ \forall x,y\in I\ \forall\lambda\in[0,1]:\ f(\lambda x+(1-\lambda)y)\le\lambda f(x)+(1-\lambda)f(y)

x,y\in[-1,4],\ \lambda\in[0,1]

z=\lambda x+(1-\lambda)y\in[-1,4];\ I\ \text{convex}

f(z)\le\lambda f(x)+(1-\lambda)f(y)

G_f(x,y,\lambda)=\lambda f(x)+(1-\lambda)f(y)-f(z)\ge 0

G_q(x,y,\lambda)\ \text{for } q(x)=ax^2+bx+c

G_q(x,y,\lambda)=a\lambda(1-\lambda)(x-y)^2

G_f(x,y,\lambda)

G_f(x,y,\lambda)=2\lambda(1-\lambda)(x-y)^2

0\le\lambda\le 1

\lambda(1-\lambda)\ge 0

2>0,\ \lambda(1-\lambda)\ge 0,\ (x-y)^2\ge 0

G_f(x,y,\lambda)=2\lambda(1-\lambda)(x-y)^2\ge 0

G_f(x,y,\lambda)\ge 0\ \text{for arbitrary } x,y\in I,\ \lambda\in[0,1]

f\ \text{convex on}\ I

x=-1,\ y=4,\ \lambda=\tfrac15

z=3,\ f(3)=10\le 18=\tfrac15 f(-1)+\tfrac45 f(4),\ G_f=8=2\cdot\tfrac15\cdot\tfrac45\cdot 25

G_\ell(x,y,\lambda)\ \text{for}\ \ell(x)=3x-5

G_\ell=0\cdot\lambda(1-\lambda)(x-y)^2=0;\ \ell\ \text{convex on}\ I\ \text{with equality}

\neg(g\ \text{convex on}\ J)

\exists x,y\in J\ \exists\lambda\in[0,1]:\ g(\lambda x+(1-\lambda)y)>\lambda g(x)+(1-\lambda)g(y)

x=0,\ y=2,\ \lambda=\tfrac12

z=1\in J,\ g(1)=0,\ \tfrac12 g(0)+\tfrac12 g(2)=\tfrac12\cdot 0+\tfrac12\cdot(-2)=-1

g(1)=0,\ \tfrac12 g(0)+\tfrac12 g(2)=-1

0>-1;\ g\ \text{is not convex on}\ J

G_g(x,y,\lambda)

G_g=-\lambda(1-\lambda)(x-y)^2;\ G_g(0,2,\tfrac12)=-1

\lambda\in\{0,1\}\ \text{or}\ x=y

G_g=0\ \text{(samples pass)},\ \text{yet } g\ \text{not convex}

Substeps and lemmas

\alpha\le s,\ \alpha\le t,\ \lambda\ge 0,\ 1-\lambda\ge 0

\alpha=\lambda\alpha+(1-\lambda)\alpha\le\lambda s+(1-\lambda)t

s\le\beta,\ t\le\beta

\lambda s+(1-\lambda)t\le\lambda\beta+(1-\lambda)\beta=\beta

\lambda(bx+c)+(1-\lambda)(by+c)-\big(b(\lambda x+(1-\lambda)y)+c\big)

0

(\lambda x+(1-\lambda)y)^2

\lambda^2x^2+2\lambda(1-\lambda)xy+(1-\lambda)^2y^2

a\big(\lambda x^2+(1-\lambda)y^2-(\lambda x+(1-\lambda)y)^2\big)

a\lambda(1-\lambda)(x-y)^2

Reverse audits

• S15 · premise_audit · S13, S14, mul_zero — It uses only multiplication by zero and the counterexample of S13; the conclusion, that passing samples are not enough to prove convexity, is supported by the concrete counterexample g.
• S14 · premise_audit · S04, S12, forall_elim — This is a check independent of S13; S13's conclusion does not depend on it. 'G_g<0 when x≠y and 0<λ<1' uses λ(1−λ)>0 and (x−y)²>0, both of which hold under these conditions.
• S13 · premise_audit · S11, S12, exists_intro — It needs the witness to lie in range and the inequality to be strictly reversed; both were checked.
• S12 · premise_audit · G3, numeric_evaluation — Exact computation; x and y do lie in J and λ in [0,1].
• S11 · inverse_equivalence · quantifier_negation, order_basics, L_interval — Quantifier negation and trichotomy of order are both two-way; the convexity of J is a premise of this equivalence.
• S10 · premise_audit · S04, S02, forall_elim, forall_intro — It needs L_gap and the convex domain. Equality here does not mean non-affine functions also give equality.
• S09 · premise_audit · S05, numeric_evaluation — An exact rational computation; it concerns this one choice of x, y, λ and implies no universal conclusion.
• S08 · premise_audit · S01, S02, S03, S07, forall_intro — It needs both parts (convex domain and Jensen) proved, and the arbitrariness of x, y, λ.
• S07 · premise_audit · S05, S06, square_nonneg, mono_nonneg — The key is a=2≥0; if a<0, the same argument gives gap≤0 (see S14). No converse is claimed.
• S06 · premise_audit · mono_nonneg, mul_zero — It needs λ∈[0,1]; for λ>1 or λ<0 one has λ(1−λ)<0, which is why the definition restricts λ.
• S05 · inverse_equivalence · S04, forall_elim — After substitution it is still an identity; both sides are equal, valid both ways.
• S04.3 · inverse_equivalence · distributive, power_laws, S04.2 — Expanding aλ(1−λ)(x−y)² returns the left side; L_gap itself is not used.
• S04.2 · inverse_equivalence · distributive, power_laws — Expansion and factoring undo each other, so it holds both ways.
• S04.1 · inverse_equivalence · distributive, add_inverse — A polynomial identity, valid both ways.
• S04 · inverse_equivalence · L_gap — This is a polynomial identity; both sides are the same polynomial, so it holds both ways with no side condition.
• S03 · inverse_equivalence · order_basics, def_intro — Subtracting f(z) and adding f(z) undo each other and both keep the direction, so the step holds both ways.
• S02.2 · premise_audit · mono_nonneg, ineq_add, distributive — Symmetric to S02.1; L_interval itself is not used.
• S02.1 · premise_audit · mono_nonneg, ineq_add, distributive — It needs both weights nonnegative; it proves the lower bound of L_interval without using L_interval itself.
• S02 · premise_audit · L_interval, mko_cvxset — It needs x, y in the interval and λ∈[0,1]; no converse is claimed.
• S01 · inverse_equivalence · mko_cvxf, def_unfold — Unfolding and folding the definition undo each other, so the step holds both ways.

Error controls and negative controls

A few passing Jensen samples do not prove convexity

The mistake named by the MKO is to declare global convexity because a few Jensen samples pass. g passes on every sample with λ=0, λ=1 or x=y (S15), yet it is not convex. The instance S09 for f is likewise only an illustration; the convexity of f comes from the identity and sign argument of S04 to S08 covering all x, y, λ.

The domain must be convex

Another misconception identified in the MKO is to speak of a convex function in the general sense on a non-convex domain. If the domain is D=[0,1]∪[2,3], then x=1, y=2, λ=1/2 gives 3/2∉D, where the function has no value, so the Jensen inequality cannot even be stated. That is why S02 first proves that I is convex, and S11 first confirms that J is.

The sign of a decides the sign of the gap

By L_gap, the Jensen gap of a quadratic is aλ(1−λ)(x−y)². For a=2 the gap is ≥0 (convex), for a=0 it is 0 (affine, equality), and for a=−1 it is ≤0, strictly negative when x≠y and 0<λ<1 (not convex). 'Every quadratic is convex' is false.

• g satisfies Jensen on the samples with λ=0, λ=1 and x=y, so g is convex on [0,2] → reject — x=0, y=2, λ=1/2: g(1)=0>−1.
• The Jensen instance of f at x=−1, y=4, λ=1/5 passes, which proves that f is convex on I → reject — One passing instance cannot prove convexity (MKO assumption a2); the conclusion holds because S04 to S08 cover every x, y, λ.
• x² on D=[0,1]∪[2,3] is a convex function in the MKO's sense → reject — D is not convex: 1, 2∈D but (1/2)·1+(1/2)·2=3/2∉D; the definition requires a convex domain.
• Every quadratic function is convex → reject — g(x)=−x²+x has a=−1 and violates Jensen at x=0, y=2, λ=1/2.

Result and limitations

I=[−1,4] is convex, and for all x,y∈I and λ∈[0,1] the Jensen gap of f(x)=2x²−3x+1 equals 2λ(1−λ)(x−y)²≥0, so f is convex on I. The gap of ℓ(x)=3x−5 is identically 0, so Jensen holds with equality. g(x)=−x²+x is not convex on J=[0,2]: with x=0, y=2, λ=1/2, g(1)=0>−1=(1/2)g(0)+(1/2)g(2).

• mono_nonneg and ineq_add are premises of this guide and are not derived here from the axioms of the reals (mono_nonneg is proved as a lemma in the convex-set guide).
• N7 to N10 check only the one instance of S09; they are illustrations and the proof does not depend on them.

Verification and source binding

17 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 3f396010579d87300f52e4a41245fcd8d02d372b3712f863225c958c4632db0c
• original source SHA-256: 3f396010579d87300f52e4a41245fcd8d02d372b3712f863225c958c4632db0c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)