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

This is (1Q) ⟹ (lt) of the blog post: the raw polar inequality

1 ≤ ∫₀¹ (a² + 2atx(1-a²) + t²(1-a²)²)^((n-1)/2) dt

implies

1 ≤ ∫₀¹ exp(α(-1 + (2-β(1))t)) dt.

The step is pointwise, and it is remarkably tight. Writing β(1) = 1 - 2ax + a² and α = (n-1)(1-a²)/2, one has the identity

1 + (1-a²)(-1 + (2-β(1))t) - P(t) = (1-a²)² (t - t²),

so the only inequality used in the whole implication is t² ≤ t on [0,1] — with equality at both endpoints — followed by 1 + y ≤ exp y. Raising to the power (n-1)/2 then turns (1-a²)/2 · (n-1) into α.

The blog post states (lt) with a strict inequality. Nothing downstream needs that: every later use of (beta-bound) is non-strict, so this file proves the non-strict form and avoids having to argue that the integrand is strictly smaller on a set of positive measure.

Main statements

• Sendov.Ppolar_le_lin: the pointwise identity-with-t² ≤ t;
• Sendov.polar_exp: (1Q) ⟹ (lt).

theorem Sendov.Ppolar_le_lin {t : ℝ} (a x : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Ppolar a x t ≤ 1 + (1 - a ^ 2) * (-1 + (2 - QQ (a * x) (a ^ 2) 1) * t)

The pointwise bound (at). An identity apart from t² ≤ t.

theorem Sendov.Ppolar_rpow_le {n : ℕ} {a x t α : ℝ} (hn : 2 ≤ n) (hx : x ^ 2 ≤ 1) (hα : α = M n * (1 - a ^ 2) / 2) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Ppolar a x t ^ ((↑n - 1) / 2) ≤ Real.exp (α * (-1 + (2 - QQ (a * x) (a ^ 2) 1) * t))

The pointwise bound after raising to the power (n-1)/2.

theorem Sendov.polar_exp {n : ℕ} {a x α : ℝ} (hn : 2 ≤ n) (hx : x ^ 2 ≤ 1) (hα : α = M n * (1 - a ^ 2) / 2) (hpolar : 1 ≤ ∫ (t : ℝ) in 0..1, Ppolar a x t ^ ((↑n - 1) / 2)) : 1 ≤ ∫ (t : ℝ) in 0..1, Real.exp (α * (-1 + (2 - QQ (a * x) (a ^ 2) 1) * t))

(1Q) ⟹ (lt).