The sine substitution with an inverse square-root weight

On the monotone branch of sine, substituting t = sin θ replaces dθ by (1 - t²)^(-1/2) dt. The integral identity and its integrability equivalence include both endpoints ±π/2; the resulting algebraic integrand can be singular at ±1. These formulas turn trigonometric elliptic integrals into algebraic integrals.

The integral identity adapts B. Braams' Carlson.integral_legendre_eq in lean-codes/Carlson/Elliptic/Standard.lean (Apache-2.0), allowing either orientation and arbitrary endpoints in the monotone branch. Integrability uses the same substitution.

theorem TauCeti.integral_comp_sin_eq_integral_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (ha : |a| ≤ Real.pi / 2) (hb : |b| ≤ Real.pi / 2) (g : ℝ → E) : ∫ (θ : ℝ) in a..b, g (Real.sin θ) = ∫ (t : ℝ) in Real.sin a..Real.sin b, (1 - t ^ 2) ^ (-1 / 2) • g t

The substitution t = sin θ, including the singular endpoints of the inverse square-root weight. No integrability hypothesis is needed for this identity of total integrals.

theorem TauCeti.intervalIntegrable_comp_sin_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (ha : |a| ≤ Real.pi / 2) (hb : |b| ≤ Real.pi / 2) (g : ℝ → E) : IntervalIntegrable (fun (θ : ℝ) => g (Real.sin θ)) MeasureTheory.volume a b ↔ IntervalIntegrable (fun (t : ℝ) => (1 - t ^ 2) ^ (-1 / 2) • g t) MeasureTheory.volume (Real.sin a) (Real.sin b)

Integrability under the sine substitution. The equivalence includes the endpoints t = ±1, where the inverse square-root weight is singular.