Commit 2025-05-08 00:39 e01b97be

feat(SpecialFunctions): Integral representation of rpow over Ioo 0 1 (#24393) This file contains an integral representation of the rpow function between 0 and 1: we show that there exists a measure on ℝ such that x ^ p = ∫ t, rpowIntegrand₀₁ p t x ∂μ for the integrand rpowIntegrand₀₁ p t x := t ^ p * (t⁻¹ - (t + x)⁻¹). This representation is useful for showing that rpow is operator monotone and operator concave in this range; that is, cfc rpow is monotone/concave. The integrand can be shown to be operator monotone and concave through direct means, and this integral lifts these properties to rpow.