Integrals against the square root of a quadratic between its roots

For a < b the quadratic (x - a) (b - x) is positive exactly on (a, b), and the integrals of √((x - a) (b - x)) and its reciprocal against 1, x and 1 / x over [a, b] have closed forms in terms of π, a + b and the geometric mean √(a b):

• ∫ x in a..b, 1 / √((x - a) (b - x)) = π;
• ∫ x in a..b, x / √((x - a) (b - x)) = π (a + b) / 2;
• ∫ x in a..b, 1 / (x √((x - a) (b - x))) = π / √(a b) for 0 < a;
• ∫ x in a..b, √((x - a) (b - x)) / x = π ((a + b) / 2 - √(a b)) for 0 ≤ a.

These are the quadratures of classical mechanics in one degree of freedom between two simple turning points: after factoring the radial kinetic energy of a Kepler orbit or an isotropic oscillator as such a quadratic, they compute the radial action, the radial period and the angle swept between the turning points. The integrands 1 / √((x - a) (b - x)), (x - a) / √((x - a) (b - x)) and, for 0 < a, 1 / (x √((x - a) (b - x))) are in general unbounded at the endpoints, but they are nonnegative derivatives of continuous functions, hence integrable; x / √((x - a) (b - x)) is handled through the split x = (x - a) + a.

The antiderivatives are arcsin ((2 x - a - b) / (b - a)) for 1 / √((x - a) (b - x)) and arcsin (((a + b) x - 2 a b) / ((b - a) x)) / √(a b) for 1 / (x √((x - a) (b - x))).

The quadratic is the model for every function with simple zeros at a and b. If g is continuous on [a, b], positive on (a, b), and vanishes at a and b with nonzero one-sided derivatives there, then g dominates a positive multiple of (x - a) (b - x) on [a, b], so by comparison 1 / √(g x) is interval integrable as well. This is the convergence of the time quadrature of a one-dimensional motion between two simple turning points.

Main declarations

• TauCeti.integral_one_div_sqrt_mul_sub_mul_sub
• TauCeti.integral_div_sqrt_mul_sub_mul_sub
• TauCeti.integral_one_div_mul_sqrt_mul_sub_mul_sub
• TauCeti.integral_sqrt_mul_sub_mul_sub_div
• TauCeti.intervalIntegrable_one_div_sqrt_mul_sub_mul_sub, TauCeti.intervalIntegrable_div_sqrt_mul_sub_mul_sub, TauCeti.intervalIntegrable_one_div_mul_sqrt_mul_sub_mul_sub and TauCeti.intervalIntegrable_sqrt_mul_sub_mul_sub_div: the integrability of the integrands that are in general unbounded at the endpoints.
• TauCeti.exists_pos_forall_mul_mul_sub_mul_sub_le and TauCeti.intervalIntegrable_one_div_sqrt_of_hasDerivWithinAt: domination by the quadratic and integrability of 1 / √g for a function g with simple zeros at both ends.
• TauCeti.hasDerivAt_arcsin_two_mul_sub_sub_div_sub, TauCeti.hasDerivAt_arcsin_add_mul_sub_div_sub_mul and TauCeti.hasDerivAt_sqrt_mul_sub_mul_sub: the derivatives of the antiderivatives on (a, b).

References

• I. S. Gradshteyn, I. M. Ryzhik, Table of Integrals, Series, and Products, 7th ed., Academic Press, 2007, Section 2.26.

theorem TauCeti.hasDerivAt_arcsin_two_mul_sub_sub_div_sub {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : HasDerivAt (fun (y : ℝ) => Real.arcsin ((2 * y - a - b) / (b - a))) (1 / √((x - a) * (b - x))) x

arcsin ((2 x - a - b) / (b - a)) is an antiderivative of 1 / √((x - a) (b - x)).

theorem TauCeti.hasDerivAt_arcsin_add_mul_sub_div_sub_mul {a b : ℝ} (ha : 0 < a) {x : ℝ} (hx : x ∈ Set.Ioo a b) : HasDerivAt (fun (y : ℝ) => Real.arcsin (((a + b) * y - 2 * a * b) / ((b - a) * y))) (√(a * b) / (x * √((x - a) * (b - x)))) x

arcsin (((a + b) x - 2 a b) / ((b - a) x)) is an antiderivative of √(a b) / (x √((x - a) (b - x))) for 0 < a.

theorem TauCeti.hasDerivAt_sqrt_mul_sub_mul_sub {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : HasDerivAt (fun (y : ℝ) => √((y - a) * (b - y))) ((a + b - 2 * x) / (2 * √((x - a) * (b - x)))) x

√((x - a) (b - x)) has derivative (a + b - 2 x) / (2 √((x - a) (b - x))) on (a, b).

theorem TauCeti.intervalIntegrable_one_div_sqrt_mul_sub_mul_sub {a b : ℝ} : IntervalIntegrable (fun (x : ℝ) => 1 / √((x - a) * (b - x))) MeasureTheory.volume a b

x ↦ 1 / √((x - a) (b - x)) is interval integrable between a and b, although it is in general unbounded at the endpoints.

theorem TauCeti.intervalIntegrable_div_sqrt_mul_sub_mul_sub {a b : ℝ} : IntervalIntegrable (fun (x : ℝ) => x / √((x - a) * (b - x))) MeasureTheory.volume a b

x ↦ x / √((x - a) (b - x)) is interval integrable between a and b, although it is in general unbounded at the endpoints.

theorem TauCeti.intervalIntegrable_one_div_mul_sqrt_mul_sub_mul_sub {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : IntervalIntegrable (fun (x : ℝ) => 1 / (x * √((x - a) * (b - x)))) MeasureTheory.volume a b

x ↦ 1 / (x √((x - a) (b - x))) is interval integrable between positive a and b, although it is in general unbounded at the endpoints.

theorem TauCeti.integral_one_div_sqrt_mul_sub_mul_sub {a b : ℝ} (hab : a < b) : ∫ (x : ℝ) in a..b, 1 / √((x - a) * (b - x)) = Real.pi

∫ x in a..b, 1 / √((x - a) (b - x)) = π for a < b.

theorem TauCeti.integral_div_sqrt_mul_sub_mul_sub {a b : ℝ} (hab : a < b) : ∫ (x : ℝ) in a..b, x / √((x - a) * (b - x)) = Real.pi * (a + b) / 2

∫ x in a..b, x / √((x - a) (b - x)) = π (a + b) / 2 for a < b.

theorem TauCeti.integral_one_div_mul_sqrt_mul_sub_mul_sub {a b : ℝ} (ha : 0 < a) (hab : a < b) : ∫ (x : ℝ) in a..b, 1 / (x * √((x - a) * (b - x))) = Real.pi / √(a * b)

∫ x in a..b, 1 / (x √((x - a) (b - x))) = π / √(a b) for 0 < a < b.

theorem TauCeti.intervalIntegrable_sqrt_mul_sub_mul_sub_div {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : IntervalIntegrable (fun (x : ℝ) => √((x - a) * (b - x)) / x) MeasureTheory.volume a b

x ↦ √((x - a) (b - x)) / x is interval integrable between nonnegative a and b, although it is unbounded near 0 when an endpoint is 0.

theorem TauCeti.integral_sqrt_mul_sub_mul_sub_div {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) : ∫ (x : ℝ) in a..b, √((x - a) * (b - x)) / x = Real.pi * ((a + b) / 2 - √(a * b))

∫ x in a..b, √((x - a) (b - x)) / x = π ((a + b) / 2 - √(a b)) for 0 ≤ a ≤ b.

Functions with simple zeros at both ends

theorem TauCeti.exists_pos_forall_mul_mul_sub_mul_sub_le {a b : ℝ} {g : ℝ → ℝ} {ga gb : ℝ} (hab : a < b) (hg : ContinuousOn g (Set.Icc a b)) (hpos : ∀ x ∈ Set.Ioo a b, 0 < g x) (ha : g a = 0) (hb : g b = 0) (hga : HasDerivWithinAt g ga (Set.Ici a) a) (hga0 : ga ≠ 0) (hgb : HasDerivWithinAt g gb (Set.Iic b) b) (hgb0 : gb ≠ 0) : ∃ c > 0, ∀ x ∈ Set.Icc a b, c * ((x - a) * (b - x)) ≤ g x

A function with simple zeros at both ends of an interval dominates the quadratic with the same zeros. If g is continuous on [a, b], positive on (a, b), and vanishes at a and b with nonzero one-sided derivatives there, then c (x - a) (b - x) ≤ g x on [a, b] for some c > 0.

theorem TauCeti.intervalIntegrable_one_div_sqrt_of_hasDerivWithinAt {a b : ℝ} {g : ℝ → ℝ} {ga gb : ℝ} (hab : a < b) (hg : ContinuousOn g (Set.Icc a b)) (hpos : ∀ x ∈ Set.Ioo a b, 0 < g x) (ha : g a = 0) (hb : g b = 0) (hga : HasDerivWithinAt g ga (Set.Ici a) a) (hga0 : ga ≠ 0) (hgb : HasDerivWithinAt g gb (Set.Iic b) b) (hgb0 : gb ≠ 0) : IntervalIntegrable (fun (x : ℝ) => 1 / √(g x)) MeasureTheory.volume a b

Quadratures across simple zeros converge. If g is continuous on [a, b], positive on (a, b), and vanishes at a and b with nonzero one-sided derivatives there, then x ↦ 1 / √(g x) is interval integrable on [a, b], although it is unbounded at both ends.