The simplified polar inequality β(1) ≤ α/(3+α)

This is (lt) ⟹ (beta-bound). Evaluating the integral,

∫₀¹ exp(α(-1 + (2-B)t)) dt = e^{-u} · sinh h / h, u = αB/2, h = α(2-B)/2,

so (lt) says e^u ≤ sinh h / h, and Sendov.log_sinh_div_le turns that into u ≤ √(h²+9) - 3. Since h = α - u, squaring u + 3 ≤ √((α-u)² + 9) gives u(6 + 2α) ≤ α², that is B ≤ α/(3+α).

The constant 3 is optimal: at B = α/(3+α) the slack in (lt) is -α⁵/540 + α⁶/648, so the bound is tight to three orders at α = 0. This is the one link of the chain with no room in it anywhere.

One degenerate case has to be cleared first, and (lt) clears it: if B ≥ 2 then the integrand is at most e^{-α} < 1 throughout, so the integral is below 1. Hence B < 2 and h > 0, which is what the sinh estimate needs.

Main statements

• Sendov.integral_exp_eq: the closed form of the integral in (lt);
• Sendov.beta_lt_two: (lt) forces B < 2;
• Sendov.beta_le: (lt) ⟹ B ≤ α/(3+α).

theorem Sendov.integral_exp_mul {c : ℝ} (hc : c ≠ 0) (a b : ℝ) : ∫ (t : ℝ) in a..b, Real.exp (c * t) = (Real.exp (c * b) - Real.exp (c * a)) / c

∫ₐᵇ exp(ct) dt = (exp(cb) - exp(ca))/c.

theorem Sendov.integral_exp_eq {α B : ℝ} (hα : 0 < α) (hB : B < 2) : ∫ (t : ℝ) in 0..1, Real.exp (α * (-1 + (2 - B) * t)) = Real.exp (-(α * B / 2)) * (Real.sinh (α * (2 - B) / 2) / (α * (2 - B) / 2))

The closed form of the integral in (lt).

theorem Sendov.integral_exp_eq' {α B : ℝ} (hα : 0 < α) (hB : B < 2) : ∫ (t : ℝ) in 0..1, Real.exp (α * (-1 + (2 - B) * t)) = (Real.exp (α * (1 - B)) - Real.exp (-α)) / (α * (2 - B))

The same integral, in the form the logarithmic half of (beta-bound) uses.

theorem Sendov.beta_lt_two {α B : ℝ} (hα : 0 < α) (hlt : 1 ≤ ∫ (t : ℝ) in 0..1, Real.exp (α * (-1 + (2 - B) * t))) : B < 2

(lt) forces B < 2: otherwise the integrand never exceeds e^{-α} < 1.

theorem Sendov.beta_le {α B : ℝ} (hα : 0 < α) (hB0 : 0 ≤ B) (hlt : 1 ≤ ∫ (t : ℝ) in 0..1, Real.exp (α * (-1 + (2 - B) * t))) : B ≤ α / (3 + α)

(lt) ⟹ (beta-bound). The α/(3+α) of the blog post.

theorem Sendov.log_le_alpha_mul {α B : ℝ} (hα : 0 < α) (hB1 : B ≤ 1) (hlt : 1 ≤ ∫ (t : ℝ) in 0..1, Real.exp (α * (-1 + (2 - B) * t))) : Real.log α ≤ α * (1 - B)

The logarithmic half of (beta-bound): log α ≤ α(1 - β(1)). From (lt), e^{α(1-B)} ≥ α(2-B) + e^{-α} > α, since B ≤ 1 makes 2 - B ≥ 1.