Shao's Lemma 2.2: the asymmetric averaging inequality
ProvedShaoThreeUnits.averaging_asymmetricLet be even with and let , , each be decreasing sequences of reals in , with averages , and . Suppose that for every triple of indices with we have
Then .
This is the three-sequence version of Lemma 2.1, and it is what lets the induction split a function into three different fibers rather than three copies of one.
import Mathlib open scoped Classical
namespace ShaoThreeUnits
theorem averaging_asymmetric (n : ℕ) (hn : 10 ≤ n) (hev : Even n)
(a b c : Fin n → ℝ) (ha : Antitone a) (hb : Antitone b) (hc : Antitone c)
(h0 : ∀ i, 0 ≤ a i ∧ 0 ≤ b i ∧ 0 ≤ c i)
(h1 : ∀ i, a i ≤ 1 ∧ b i ≤ 1 ∧ c i ≤ 1)
(htriple : ∀ i j k : Fin n, n ≤ (i : ℕ) + (j : ℕ) + (k : ℕ) →
a i * b j + b j * c k + c k * a i ≤ 5 / 8 * (a i + b j + c k))
(A B C : ℝ) (hA : A = (∑ i, a i) / n) (hB : B = (∑ i, b i) / n)
(hC : C = (∑ i, c i) / n) :
A * B + B * C + C * A ≤ 5 / 8 * (A + B + C) := by sorry
end ShaoThreeUnits
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
Fix an even natural number n with n at least 10. Let a, b, c be real sequences indexed by 0 through n-1. Each is non-increasing in the index, and each takes values in [0,1]. Assume that for every index triple (i,j,k) with i+j+k at least n, the quantity a_i b_j + b_j c_k + c_k a_i is at most (5/8)(a_i + b_j + c_k). Let A, B, C be the arithmetic means of a, b, c over the whole index range. The conclusion is AB + BC + CA at most (5/8)(A + B + C). The constant 5/8 is the same in hypothesis and conclusion, and both inequalities are non-strict. The pointwise hypothesis binds only triples of index sum at least n. Indices stop at n-1, so a triple such as (n-1, 1, 0) has sum exactly n and is constrained. The hypothesis therefore couples the last entry of one sequence to near-first entries of the other two, not just late entries of all three.
QUANTIFIER ORDER n, universal, outermost. hn, then hev, constraints on n. a, b, c, universal, functions from the index set to the reals. ha, hb, hc, then h0, h1, pointwise constraints on those functions. htriple, with i, j, k universally quantified inside it, each over the full index set, guarded by n at most i+j+k. A, B, C, universal reals, pinned by hA, hB, hC to the three averages, so they carry no freedom. Nothing is existentially quantified anywhere in the statement.
HYPOTHESES 10 at most n: nothing is asserted for n at most 9, and n is nonzero, so the division by n is by a nonzero real. Even n: nothing is asserted for odd n. Antitone (three times): rules out any increase at any step, and allows equal consecutive values. h0 and h1: confine every value to [0,1], ruling out negative entries and entries above 1. htriple: one inequality family. It rules out a = b = c = 1, where the left side is 3 and the right side is 15/8.
DEGENERATE CASES a = b = c = 0 satisfies every hypothesis, and the conclusion reads 0 at most 0. The constant sequences a = b = c = 5/8 satisfy htriple with equality, and make the conclusion an equality. So the hypotheses are satisfiable, the statement is not vacuous, and the constant is attained. The index set is never empty, since n is at least 10. The constrained triple family is never empty, since (n-1, n-1, n-1) has sum 3n-3.
UNREADABLE Nothing. Casts read as follows: the index coercion gives the numeric value 0 through n-1, the denominator n is the real cast, and 5/8 is real division equal to 0.625, not truncated natural division.
Confirmed by the mission captain (proposal self-audit).