Shao's Lemma 2.1: the symmetric averaging inequality

Proved

ShaoThreeUnits.averaging_symmetric

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsnumber-theory

Let $n$ be even with $n \ge 6$ and let $a_0 \ge a_1 \ge \dots \ge a_{n-1}$ be reals in $[0,1]$ . Suppose that for every triple of indices $i, j, k$ with $i + j + k \ge n$ we have

a_i a_j + a_j a_k + a_k a_i \le \tfrac{5}{8}(a_i + a_j + a_k).

Then $\sum_i a_i \le \frac{5}{8} n$ .

The proof uses this through its contrapositive: an average above $5/8$ yields one triple of indices summing to at least $n$ on which the inequality is strict the other way.

The hypothesis $n \ge 6$ is needed. Shao gives the counterexample $a = (1, 0.6, 0.5, 0.41)$ at $n = 4$ .

Preamble

import Mathlib
open scoped Classical

Formal statement

namespace ShaoThreeUnits

theorem averaging_symmetric (n : ℕ) (hn : 6 ≤ n) (hev : Even n) (a : Fin n → ℝ)
    (hmono : Antitone a) (h0 : ∀ i, 0 ≤ a i) (h1 : ∀ i, a i ≤ 1)
    (htriple : ∀ i j k : Fin n, n ≤ (i : ℕ) + (j : ℕ) + (k : ℕ) →
      a i * a j + a j * a k + a k * a i ≤ 5 / 8 * (a i + a j + a k)) :
    (∑ i, a i) ≤ 5 / 8 * n := by sorry

end ShaoThreeUnits

Source

Xuancheng Shao, "A density version of the Vinogradov three primes theorem", Duke Math. J. 163 (2014) 489-512, arXiv:1206.6139v2, https://arxiv.org/abs/1206.6139, Lemma 2.1

Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

The claim: let n be a natural number that is even and at least 6, and let a be a real-valued function on the index set {0, 1, ..., n-1}. Suppose a is non-increasing in the index, every value lies in the closed interval [0, 1], and the following holds for every ordered triple of indices (i, j, k), repetitions allowed, whose 0-based indices sum to at least n: a_i a_j + a_j a_k + a_k a_i is at most (5/8)(a_i + a_j + a_k). Then the total sum of all n values is at most (5/8)n. Both 5/8 is exact real division, and n in the conclusion is the cast of the natural number into the reals. No constant is existentially quantified; 5/8 is fixed in both the hypothesis and the conclusion, and both inequalities are non-strict.

QUANTIFIER ORDER

n : N, universal, scopes over everything.
hn, hev: conditions on n.
a : Fin n -> R, universal, depends on n.
hmono, h0, h1, htriple: conditions on a.
Inside htriple: i, j, k : Fin n, all universal, for the same fixed a. No existential quantifier occurs anywhere.

HYPOTHESES hn: 6 <= n. Rules out n = 0..5, so the index set is nonempty. hev: n is even. Rules out odd n. It appears nowhere else in the statement. hmono (Antitone): i <= j implies a_j <= a_i. Rules out any increase; a_0 is the largest value. h0: every a_i >= 0. h1: every a_i <= 1, non-strict. htriple: the pairwise-product bound, applied to ordered triples with (i : N) + (j : N) + (k : N) >= n, arithmetic in N on 0-based indices, so no wraparound. It does not require i, j, k distinct, so it also constrains triples with repeats. It says nothing about triples of index sum at most n-1.

DEGENERATE CASES The constant zero function satisfies every hypothesis and gives 0 <= 5n/8, so the hypotheses are satisfiable and the theorem is not vacuous. Taking i = j = k with 3i >= n gives 3a_i^2 <= (15/8)a_i, hence a_i <= 5/8 for every index i >= n/3. Taking i = j alone gives a_i^2 + 2a_i a_k <= (5/8)(2a_i + a_k). The constrained family is nonempty: (n-1, n-1, n-1) has index sum 3n-3 >= n. The top entries are unconstrained by htriple: for instance a_0 and a_1 are bounded only by 1, since any triple containing enough small indices has sum below n. Note the 0-based convention: in 1-based index notation the triple condition would read i + j + k >= n + 3.

UNREADABLE nothing.

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by aarontcao · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph