Real powers, shared by both ranges

The exponent (n-4)/2 in Sendov.R is a real exponent, so both halves of the development — the finite range and the large-degree argument — manipulate Real.rpow, and both need the integrand t ^ 3 * Q ^ e to be continuous in order to integrate it. Those facts have no connection to either strategy, so they live here rather than in the strategy-specific files.

In particular:

• the finite range uses Sendov.continuous_integrand to compare integrals in Sendov.integral_rpow_le, and the large-degree argument needs the same fact to split ∫₀¹ at the vertex of Q;
• Sendov.rpow_add_nat_pos is used by the Beta integral, and the same splitting of a real power into a real and a natural part is what turns B ^ ((n-4)/2) into B ^ k * √B in the large-degree reduction.

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

∫₀¹ xˢ dx = 1/(s+1) for s > -1.

theorem Sendov.rpow_add_nat_pos {x : ℝ} (hx : 0 < x) (s : ℝ) (m : ℕ) : x ^ (s + ↑m) = x ^ s * x ^ m

x ^ (s + m) = x ^ s * x ^ m for positive x and a natural m.

theorem Sendov.continuous_rpow_const {e : ℝ} (he : 0 ≤ e) : Continuous fun (x : ℝ) => x ^ e

fun x ↦ x ^ e is continuous on all of ℝ for a nonnegative real exponent e. The exponent must be nonnegative: at e < 0 the function blows up at the origin.

theorem Sendov.continuous_integrand (n : ℕ) (α : ℝ) {e : ℝ} (he : 0 ≤ e) : Continuous fun (t : ℝ) => t ^ 3 * Q n α t ^ e

The integrand of Sendov.R is continuous, hence interval integrable. Needed wherever an integral involving Q ^ e is split or compared.

theorem Sendov.rpow_le_rpow_of_le_one {x s t : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hts : t ≤ s) : x ^ s ≤ x ^ t

On [0,1] a real power is decreasing in the exponent: x ^ s ≤ x ^ t for t ≤ s. Used to drop the √B from B ^ (k + 1/2).