Chord bounds and the Beta integrals

Both halves of the argument replace a power of the quadratic by a power of its chord and integrate. The blog post does this twice, with different weights:

• with weight t, to bound ∫₀¹ t β(t)^{(n-2)/2} in the proof of α ≤ 17;
• with weight t³, to bound ∫₀¹ t³ Q^{(n-4)/2} in the large-degree argument.

Both reduce to a Beta integral, and the split is the same in both cases, so it is proved once: Sendov.integral_le_tail_gen bounds ∫₀¹ t^k QQ^r by the chord integral over [0,1/c] plus QQ 1 ^ r / (k+1), for any natural k, leaving the Beta value to be substituted afterwards.

The informal write-up instead uses QQ ≤ exp(-ct) and the Gamma integral ∫₀^∞ t³ e^{-rct} dt = 6/(rc)⁴. The Beta route is preferable in Lean — no improper integral and no Real.exp — and is strictly sharper, since 6/((s+1)(s+2)(s+3)(s+4)) ≤ 6/s⁴ (Sendov.beta_le_six_div_pow), so every numerical constant downstream of the Gamma bound stays valid.

Main statements

• Sendov.integral_lin_mul_rpow, Sendov.integral_cube_mul_rpow: the Beta values;
• Sendov.integral_chord_lin, Sendov.integral_chord_pow: the same, scaled to [0,1/c];
• Sendov.integral_le_tail_gen: the split, for an arbitrary weight t^k;
• Sendov.integral_le_tail_lin, Sendov.integral_le_tail_cube: the two instances used.

The Beta integrals

theorem Sendov.integral_lin_mul_rpow {s : ℝ} (hs : 0 < s) : ∫ (x : ℝ) in 0..1, x * (1 - x) ^ s = 1 / ((s + 1) * (s + 2))

The Beta integral B(2, s+1).

theorem Sendov.integral_cube_mul_rpow {s : ℝ} (hs : 0 < s) : ∫ (x : ℝ) in 0..1, x ^ 3 * (1 - x) ^ s = 6 / ((s + 1) * (s + 2) * (s + 3) * (s + 4))

The Beta integral B(4, s+1).

theorem Sendov.beta_le_six_div_pow {s : ℝ} (hs : 0 < s) : 6 / ((s + 1) * (s + 2) * (s + 3) * (s + 4)) ≤ 6 / s ^ 4

The Beta value is at most 6/s⁴; this is the form the informal argument uses, obtained there from the Gamma integral.

theorem Sendov.integral_chord_lin {s c : ℝ} (hs : 0 < s) (hc : 0 < c) : ∫ (t : ℝ) in 0..1 / c, t * (1 - c * t) ^ s = 1 / (c ^ 2 * ((s + 1) * (s + 2)))

The chord integral with weight t, over [0, 1/c].

theorem Sendov.integral_chord_pow {s c : ℝ} (hs : 0 < s) (hc : 0 < c) : ∫ (t : ℝ) in 0..1 / c, t ^ 3 * (1 - c * t) ^ s = 6 / (c ^ 4 * ((s + 1) * (s + 2) * (s + 3) * (s + 4)))

The chord integral with weight t³, over [0, 1/c].

The split

theorem Sendov.integral_le_tail_gen {c A : ℝ} (hfeas : c ^ 2 ≤ A) (hc : 0 < c) (hc1 : c ≤ 1) {r : ℝ} (hr : 0 < r) (k : ℕ) : ∫ (t : ℝ) in 0..1, t ^ k * QQ c A t ^ r ≤ (∫ (t : ℝ) in 0..1 / c, t ^ k * (1 - c * t) ^ r) + QQ c A 1 ^ r / (↑k + 1)

The tail bound, for an arbitrary weight t^k. QQ is a convex parabola with vertex at c/A; below the vertex it lies under the chord 1 - ct, above it it is increasing and so at most QQ 1. Splitting ∫₀¹ there gives the bound.

Two points shape the proof. The chord bound needs 1 - ct ≥ 0, which comes from ct ≤ c²/A ≤ 1 — feasibility again. And the vertex may lie outside [0,1]: the split is made at s = min (c/A) 1, after which the first piece is enlarged to [0, 1/c] (legitimate because s ≤ 1/c, using c ≤ 1 when the vertex is to the right) and the second piece is empty when the vertex is beyond 1.

theorem Sendov.integral_QQ_anti {c₁ c₂ A : ℝ} (hle : c₁ ≤ c₂) (hfeas : c₂ ^ 2 ≤ A) {r : ℝ} (hr : 0 ≤ r) (k : ℕ) : ∫ (t : ℝ) in 0..1, t ^ k * QQ c₂ A t ^ r ≤ ∫ (t : ℝ) in 0..1, t ^ k * QQ c₁ A t ^ r

The integral is antitone in c: raising c lowers QQ pointwise on [0,1]. Note that nonnegativity is only needed for the larger c; for the smaller one it comes free from the pointwise comparison. (Sendov.integral_anti in FiniteRange.Batch is the same trick applied to the degree instead.)

theorem Sendov.integral_le_tail_lin {c A : ℝ} (hfeas : c ^ 2 ≤ A) (hc : 0 < c) (hc1 : c ≤ 1) {r : ℝ} (hr : 0 < r) : ∫ (t : ℝ) in 0..1, t * QQ c A t ^ r ≤ 1 / (c ^ 2 * ((r + 1) * (r + 2))) + QQ c A 1 ^ r / 2

The instance with weight t, used for α ≤ 17.

theorem Sendov.integral_le_tail_cube {c A : ℝ} (hfeas : c ^ 2 ≤ A) (hc : 0 < c) (hc1 : c ≤ 1) {r : ℝ} (hr : 0 < r) : ∫ (t : ℝ) in 0..1, t ^ 3 * QQ c A t ^ r ≤ 6 / (c ^ 4 * ((r + 1) * (r + 2) * (r + 3) * (r + 4))) + QQ c A 1 ^ r / 4

The instance with weight t³, used by the large-degree argument.