The quadratic 1 - 2ct + At²

Two quadratics drive the whole development, and they are the same object with different parameters:

• β(t) = 1 - 2axt + a²t², the quantity the blog post's inequalities are stated in;
• Q n α t = 1 - 2c(α)t + a²t², what β becomes after β(1) is replaced by α/(3+α).

So the facts about them — nonnegativity under feasibility, the chord bound below the vertex, monotonicity above it — are proved once here for

QQ c A t = 1 - 2ct + At²,

and Sendov.Q n α t = QQ (c n α) (A n α) t holds by rfl.

Note which hypothesis each fact needs. Nonnegativity is exactly feasibility c² ≤ A, since QQ = (1-ct)² + (A-c²)t². The bound QQ ≤ 1 on [0,1] needs only 0 ≤ c together with QQ 1 ≤ 1: writing QQ t - 1 = t(At - 2c), the value at t = 1 already gives A ≤ 2c, and then At ≤ 2c whether A is nonnegative (as At ≤ A) or negative (as At ≤ 0 ≤ 2c). That matters, because A is genuinely negative in parts of the range.

Main statements

• Sendov.QQ_nonneg, Sendov.QQ_le_one;
• Sendov.QQ_le_chord: QQ t ≤ 1 - ct below the vertex;
• Sendov.QQ_le_at_one: QQ t ≤ QQ 1 above it.

noncomputable def Sendov.QQ (c A t : ℝ) : ℝ

The quadratic 1 - 2ct + At².

Equations

• Sendov.QQ c A t = 1 - 2 * c * t + A * t ^ 2

theorem Sendov.Q_eq_QQ (n : ℕ) (α t : ℝ) : Q n α t = QQ (c n α) (A n α) t

Sendov.Q is an instance of Sendov.QQ. Stated before the section variables below, which deliberately shadow Sendov.c and Sendov.A.

theorem Sendov.QQ_eq (c A t : ℝ) : QQ c A t = (1 - c * t) ^ 2 + (A - c ^ 2) * t ^ 2

QQ as a sum of squares.

theorem Sendov.QQ_zero (c A : ℝ) : QQ c A 0 = 1

theorem Sendov.QQ_one (c A : ℝ) : QQ c A 1 = 1 - 2 * c + A

theorem Sendov.QQ_nonneg {c A : ℝ} (hfeas : c ^ 2 ≤ A) (t : ℝ) : 0 ≤ QQ c A t

Feasibility c² ≤ A says exactly that QQ is a sum of squares.

theorem Sendov.QQ_le_one {c A t : ℝ} (hc : 0 ≤ c) (hB : QQ c A 1 ≤ 1) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : QQ c A t ≤ 1

QQ ≤ 1 on [0,1], from QQ 1 ≤ 1 and 0 ≤ c alone.

theorem Sendov.QQ_le_chord {c A t : ℝ} (ht0 : 0 ≤ t) (ht : A * t ≤ c) : QQ c A t ≤ 1 - c * t

Below the vertex, QQ lies under the chord 1 - ct.

theorem Sendov.QQ_le_at_one {c A t : ℝ} (hA : 0 ≤ A) (ht : c ≤ A * t) (ht1 : t ≤ 1) : QQ c A t ≤ QQ c A 1

Above the vertex, QQ is increasing, so it is at most its value at t = 1.

theorem Sendov.continuous_pow_mul_QQ (c A : ℝ) (k : ℕ) {e : ℝ} (he : 0 ≤ e) : Continuous fun (t : ℝ) => t ^ k * QQ c A t ^ e

t ^ k * QQ ^ e is continuous, hence interval integrable: needed wherever an integral of this shape is split or compared.