From the raw origin inequality to its α, β(1) form

This is (origin-exact) + (beta-bound) ⟹ (1le). The work is in replacing

∫₀¹ t β(t)^((n-2)/2) dt

by a Beta value plus the t³ integral that stat is stated with. Writing β as a sum of squares, β(t) = (1-axt)² + a²t²(1-x²), the blog post applies the mean value theorem to s ↦ ((1-axt)² + s)^((n-2)/2). Here that step is Bernoulli's inequality instead: dividing

(P+Q)^p ≤ P^p + p Q (P+Q)^(p-1)

through by (P+Q)^p turns it into 1 ≤ θ^p + p(1-θ) at θ = P/(P+Q), which is exactly one_add_mul_self_le_rpow_one_add. No derivative and no mean value theorem is needed.

After that, ∫₀¹ t (1-axt)^(n-2) dt is enlarged to [0, 1/ax] — legitimate since ax ≤ 1 and the integrand stays nonnegative — and evaluated by Sendov.integral_chord_lin, the k = 1 Beta integral of Sendov.Common.Chord. What is left is algebra in α and β(1), using 1 - x² ≤ β(1) (which is (x-a)² ≥ 0) and ax = 1 - β(1)/2 - α/(n-1).

(beta-bound) enters only through β(1) < 1, which is what makes x > a/2 > 0, hence 1/x² finite and 1/(ax) ≥ 1.

Main statements

• Sendov.rpow_add_le_of_one_le: the Bernoulli form of the mean-value step;
• Sendov.beta_split: the pointwise consequence for β;
• Sendov.one_le_of_origin: (origin-exact) + (beta-bound) ⟹ (1le).

theorem Sendov.rpow_add_le_of_one_le {P Q p : ℝ} (hP : 0 ≤ P) (hPQ : 0 < P + Q) (hp : 1 ≤ p) : (P + Q) ^ p ≤ P ^ p + p * Q * (P + Q) ^ (p - 1)

(P+Q)^p ≤ P^p + p Q (P+Q)^(p-1) for p ≥ 1. This is the blog post's mean-value step, obtained from Bernoulli's inequality after dividing by (P+Q)^p.

theorem Sendov.one_sub_mul_pos {a x t : ℝ} (ha : 0 < a) (ha1 : a < 1) (hx : x ^ 2 ≤ 1) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 0 < 1 - a * x * t

ax t < 1 on [0,1], so the chord 1 - axt is positive.

theorem Sendov.beta_split {n : ℕ} {a x t : ℝ} (hn : 5 ≤ n) (ha : 0 < a) (ha1 : a < 1) (hx : x ^ 2 ≤ 1) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : QQ (a * x) (a ^ 2) t ^ ((↑n - 2) / 2) ≤ (1 - a * x * t) ^ (↑n - 2) + (↑n - 2) / 2 * (a ^ 2 * t ^ 2 * (1 - x ^ 2)) * QQ (a * x) (a ^ 2) t ^ ((↑n - 4) / 2)

The pointwise step: β^((n-2)/2) split into a chord power and a β^((n-4)/2) remainder.

theorem Sendov.integral_beta_split {n : ℕ} {a x : ℝ} (hn : 5 ≤ n) (ha : 0 < a) (ha1 : a < 1) (hx : x ^ 2 ≤ 1) (hax : 0 < a * x) : ∫ (t : ℝ) in 0..1, t * QQ (a * x) (a ^ 2) t ^ ((↑n - 2) / 2) ≤ 1 / ((a * x) ^ 2 * ((↑n - 1) * ↑n)) + (↑n - 2) / 2 * (a ^ 2 * (1 - x ^ 2)) * ∫ (t : ℝ) in 0..1, t ^ 3 * QQ (a * x) (a ^ 2) t ^ ((↑n - 4) / 2)

The integral form of the split, with the chord piece evaluated by the Beta integral.

theorem Sendov.one_le_of_origin {n : ℕ} {a x α : ℝ} (hn : 5 ≤ n) (ha : 0 < a) (ha1 : a < 1) (hx : x ^ 2 ≤ 1) (hα : α = M n * (1 - a ^ 2) / 2) (hα0 : 0 < α) (hB1lt : QQ (a * x) (a ^ 2) 1 < 1) (horigin : 2 * α + a * x ≤ (1 - x ^ 2) / (2 * M n) + a ^ 2 * ↑n * M n * ∫ (t : ℝ) in 0..1, t * QQ (a * x) (a ^ 2) t ^ ((↑n - 2) / 2)) : 1 ≤ QQ (a * x) (a ^ 2) 1 / (2 * α * (1 - QQ (a * x) (a ^ 2) 1)) + QQ (a * x) (a ^ 2) 1 / (4 * α) + 1 / (2 * M n) + QQ (a * x) (a ^ 2) 1 / (4 * α * M n) + (a ^ 2) ^ 2 * ↑n * M n * (↑n - 2) * QQ (a * x) (a ^ 2) 1 / (4 * α) * ∫ (t : ℝ) in 0..1, t ^ 3 * QQ (a * x) (a ^ 2) t ^ ((↑n - 4) / 2)

(origin-exact) + (beta-bound) ⟹ (1le). (beta-bound) enters only as β(1) < 1.