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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-convex-function/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-convex-function-01 · production-20261019-adopted-96



## 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

S01 · equivalentBefore

f\ \text{convex on}\ I

After

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)

Conditions: none

Rule: mko_cvxf · Uses: G1, mko_cvxf

Leaf basis: mko_cvxf + def_unfold

Unfold the MKO's definition. It has two parts: the domain must be convex (otherwise λx+(1−λ)y may leave the domain, where f has no value), and the Jensen inequality must hold for all x, y, λ. Both parts must be proved.



S02 · impliesBefore

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

After

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

Conditions: \lambda\in[0,1]

Rule: L_interval · Uses: G1, L_interval, mko_cvxset

Leaf basis: L_interval + forall_intro

Apply Lemma L_interval (α=−1, β=4, s=x, t=y): z stays in [−1,4]. Since x, y, λ are arbitrary, I satisfies the definition of a convex set; therefore f(z) is defined and the Jensen inequality makes sense. The lemma is proved in S02.1 and S02.2.



S03 · equivalentBefore

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

After

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

Conditions: none

Rule: order_basics · Uses: S01, S02

Leaf basis: order_basics + def_intro

Define the Jensen gap G_f=λf(x)+(1−λ)f(y)−f(z). Subtracting f(z) from both sides keeps the direction, so the Jensen inequality is equivalent to G_f≥0. From now on only the sign of G_f matters.



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: L_gap · Uses: L_gap

Leaf basis: distributive + power_laws + add_inverse

Lemma L_gap: the Jensen gap of any univariate quadratic (including the affine case a=0) equals aλ(1−λ)(x−y)², for all reals x, y, λ. The proof has three sub-steps: the constant and linear parts cancel (S04.1), the square is expanded (S04.2), and the quadratic part becomes a perfect square (S04.3). N1 checks the whole identity as a polynomial identity.



S05 · equivalentBefore

G_f(x,y,\lambda)

After

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

Conditions: none

Rule: forall_elim · Uses: S04, G1

Leaf basis: forall_elim + eq_replace

Apply L_gap to f with a=2, b=−3, c=1 (instantiating a universal statement). b and c do not appear in the result; only a=2 determines the gap.



S06 · impliesBefore

0\le\lambda\le 1

After

\lambda(1-\lambda)\ge 0

Conditions: \lambda\ge 0; 1-\lambda\ge 0

Rule: mono_nonneg · Uses: S02.1, mono_nonneg, mul_zero

Leaf basis: mono_nonneg + mul_zero

Multiply 0≤1−λ by λ≥0: λ·0≤λ(1−λ), and λ·0=0. So λ(1−λ)≥0.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: mono_nonneg · Uses: S05, S06, square_nonneg, mono_nonneg

Leaf basis: square_nonneg + mono_nonneg + mul_zero

Squares are nonnegative: (x−y)²≥0. Multiplying 0≤(x−y)² by λ(1−λ)≥0 gives 0≤λ(1−λ)(x−y)²; multiplying by 2>0 gives 0≤2λ(1−λ)(x−y)². By S05, G_f≥0.



S08 · impliesBefore

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

After

f\ \text{convex on}\ I

Conditions: none

Rule: forall_intro · Uses: S01, S02, S03, S07, forall_intro

Leaf basis: forall_intro + and_intro_elim

x, y, λ were arbitrary and S03 to S07 put no extra assumption on them, so by ∀-introduction the Jensen inequality holds for all x,y∈I and λ∈[0,1]; together with the convexity of I from S02 and by S01, f is convex on I. This is a positive certificate covering every case (MKO assumption a2).



S09 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S05, G1

Leaf basis: numeric_evaluation

One concrete instance as an illustration: z=(1/5)(−1)+(4/5)·4=3; f(3)=18−9+1=10; f(−1)=6 and f(4)=21, so (1/5)·6+(4/5)·21=18. The gap 18−10=8 agrees with the formula of S05, 2·(1/5)·(4/5)·(−5)²=8. This is an illustration only, not a proof; the proof is S02 to S08.



S10 · impliesBefore

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

After

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

Conditions: none

Rule: forall_elim · Uses: S04, S02, G2, forall_intro

Leaf basis: forall_elim + mul_zero + forall_intro

ℓ is the case a=0, so by L_gap G_ℓ=0 for all x, y, λ, that is ℓ(z)=λℓ(x)+(1−λ)ℓ(y): Jensen holds with equality (MKO para0). The domain I was shown convex in S02, so ℓ is convex on I (and the reverse inequality holds too).



S11 · equivalentBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: G3, mko_cvxf, L_interval, quantifier_negation

Leaf basis: quantifier_negation + order_basics + L_interval

J=[0,2] is convex by L_interval, so the first part of the definition holds; g is not convex exactly when the Jensen part fails. ¬∀ is equivalent to ∃¬, and ¬(u≤v) is equivalent to u>v. So one choice of x, y, λ with g(z) strictly greater than the right side is enough.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G3

Leaf basis: numeric_evaluation

Take the endpoints x=0, y=2 of J and λ=1/2∈[0,1]: z=1∈J. Exact evaluation: g(1)=−1+1=0, g(0)=0, g(2)=−4+2=−2, and the right side is (1/2)·0+(1/2)·(−2)=−1.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: exists_intro · Uses: S11, S12, exists_intro

Leaf basis: exists_intro + order_basics

0>−1, so this choice of x, y, λ violates the Jensen inequality. By ∃-introduction the existential statement of S11 holds, and g is not convex on J. One exact violation suffices (MKO assumption a2).



S14 · impliesBefore

G_g(x,y,\lambda)

After

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

Conditions: none

Rule: forall_elim · Uses: S04, S06, S12, square_nonneg

Leaf basis: forall_elim + square_nonneg + order_basics

Cross-check: g has a=−1, so by L_gap G_g=−λ(1−λ)(x−y)². At (0,2,1/2): −(1/2)(1/2)·4=−1, exactly the right side of S12 minus g(z): −1−0=−1. More generally, whenever x≠y and 0<λ<1, G_g<0: every nontrivial Jensen instance fails.



S15 · impliesBefore

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

After

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

Conditions: none

Rule: mul_zero · Uses: S13, S14

Leaf basis: mul_zero + square_nonneg

When λ=0, λ=1 or x=y, λ(1−λ)(x−y)²=0, so g passes Jensen with equality on these samples. Yet S13 proved g is not convex. Hence 'some Jensen samples pass' does not imply convexity; a positive conclusion must cover every x, y, λ, as S02 to S08 do.







## Substeps and lemmas

S02.1 · impliesBefore

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

After

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

Conditions: 0\le\lambda\le 1

Rule: mono_nonneg · Uses: mono_nonneg, ineq_add, distributive

Leaf basis: mono_nonneg + ineq_add + distributive + order_basics

From 0≤λ≤1 we get λ≥0 and 1−λ≥0. Multiplying α≤s by λ gives λα≤λs, and α≤t by 1−λ gives (1−λ)α≤(1−λ)t; adding gives λα+(1−λ)α≤λs+(1−λ)t, and by distributivity the left side is (λ+1−λ)α=α.



S02.2 · impliesBefore

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

After

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

Conditions: 0\le\lambda\le 1

Rule: mono_nonneg · Uses: S02.1, mono_nonneg, ineq_add, distributive

Leaf basis: mono_nonneg + ineq_add + distributive

The upper bound follows similarly: multiply s≤β by λ and t≤β by 1−λ, add, and simplify the right side to β by distributivity. S02.1 and S02.2 together prove Lemma L_interval.



S04.1 · equivalentBefore

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

After

0

Conditions: none

Rule: distributive · Uses: distributive

Leaf basis: distributive + add_inverse + mul_one

Linear part: λbx+(1−λ)by−b(λx+(1−λ)y)=0 by distributivity. Constant part: λc+(1−λ)c−c=(λ+1−λ)c−c=0. So only the quadratic part of the gap remains.



S04.2 · equivalentBefore

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

After

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

Conditions: none

Rule: distributive · Uses: distributive, power_laws

Leaf basis: distributive + power_laws + mul_comm

Use (p+q)²=p²+2pq+q² (expansion by distributivity) with p=λx and q=(1−λ)y.



S04.3 · equivalentBefore

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

After

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

Conditions: none

Rule: distributive · Uses: S04.1, S04.2, distributive

Leaf basis: distributive + power_laws + mul_comm + add_comm

Substitute S04.2: the coefficient of x² is λ−λ²=λ(1−λ); that of y² is (1−λ)−(1−λ)²=(1−λ)(1−(1−λ))=λ(1−λ); that of xy is −2λ(1−λ). Factor out λ(1−λ): λ(1−λ)(x²−2xy+y²)=λ(1−λ)(x−y)². Multiply by a and add the 0 of S04.1 to get G_q=aλ(1−λ)(x−y)². S04.1 to S04.3 prove Lemma L_gap.







## 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 convexityThe 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 convexAnother 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 gapBy 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-convex-function-01.json)