Maclaurin's inequality, top case

The origin inequality needs

(1/N) ∑ⱼ ∏_{k≠j} bₖ ≤ ((1/N) ∑ₖ bₖ) ^ (N-1),

that is p_{N-1} ≤ p₁^{N-1} for the elementary symmetric means. Mathlib has neither Maclaurin's nor Newton's inequalities, and the usual route to them — real-rootedness of the derivative, via Rolle — is a sizeable development on its own.

It is not needed. Writing E s for ∑ⱼ ∏_{k≠j}, splitting off one element gives

E (a ::ₘ t) = t.prod + a * E t,

and after the inductive hypothesis and AM–GM the step reduces, on dividing by uᴺ where u is the mean of t, to 1 + N(w-1) ≤ wᴺ — Bernoulli's inequality, which Mathlib has.

AM–GM itself is proved here the same way rather than imported, because the Mathlib version is stated for a Finset-indexed family and the whole development uses multisets (roots come as multisets, and repeated roots must be allowed). Its induction step reduces to Bernoulli too, so the two proofs share their only real ingredient.

Neither statement mentions anything Sendov-specific; both are candidates for upstreaming.

Main statements

• Sendov.Multiset.prod_le_mean_pow: ∏ s ≤ (mean s) ^ card s;
• Sendov.Multiset.esymm_card_pred_le: e_{N-1}(s) ≤ N (mean s)^{N-1}.

The two Bernoulli steps

theorem Sendov.amgm_step {a : ℝ} (N : ℕ) {u : ℝ} (hu : 0 < u) (ha : 0 ≤ a) : a * u ^ N ≤ ((a + ↑N * u) / (↑N + 1)) ^ (N + 1)

The AM–GM induction step: a uᴺ ≤ μ^{N+1} where μ is the mean of a together with N copies of u. Dividing by u^{N+1} this is Bernoulli.

theorem Sendov.maclaurin_step {a : ℝ} (N : ℕ) (hN : 1 ≤ N) {u : ℝ} (hu : 0 < u) (ha : 0 ≤ a) : u ^ N + ↑N * a * u ^ (N - 1) ≤ (↑N + 1) * ((a + ↑N * u) / (↑N + 1)) ^ N

The Maclaurin induction step.

AM–GM

theorem Sendov.Multiset.prod_le_mean_pow (s : Multiset ℝ) : (∀ x ∈ s, 0 ≤ x) → s.prod ≤ (s.sum / ↑s.card) ^ s.card

AM–GM for multisets. ∏ s ≤ (mean s) ^ card s.

Maclaurin

theorem Sendov.esymm_card_cons (a : ℝ) (t : Multiset ℝ) (ht : t ≠ 0) : (a ::ₘ t).esymm t.card = t.prod + a * t.esymm (t.card - 1)

Splitting off one element: E (a ::ₘ t) = ∏ t + a · E t.

theorem Sendov.Multiset.esymm_card_pred_le (s : Multiset ℝ) : (∀ x ∈ s, 0 ≤ x) → s ≠ 0 → s.esymm (s.card - 1) ≤ ↑s.card * (s.sum / ↑s.card) ^ (s.card - 1)

Maclaurin's inequality, top case. e_{N-1}(s) ≤ N (mean s)^{N-1}.