Integral representations of rpow

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. These results can be found in Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order.

Notes

Here we only compute the integral up to a constant, even though the actual constant can be computed via contour integration. We chose to avoid this, as the constant is seldom if ever relevant in applications, and would needlessly complicate the proof.

Main declarations

• rpowIntegrand₀₁ p t x := t ^ p * (t⁻¹ - (t + x)⁻¹)
• rpowIntegrand₁₂ p t x := t ^ (p - 1) * (x * t⁻¹ + t * (t + x)⁻¹ - 1)
• exists_measure_rpow_eq_integral_rpowIntegrand₀₁ and exists_measure_rpow_eq_integral_rpowIntegrand₁₂: there exists a measure on ℝ such that x ^ p = ∫ t, rpowIntegrand₀₁ p t x ∂μ (resp x ^ p = ∫ t, rpowIntegrand₁₂ p t x ∂μ)
• CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ and CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₁₂: the corresponding statements where x ^ p is defined via the CFC.

TODO

• Give analogous representations for the range Ioo (-1) 0.

References

• [Car10] Eric A. Carlen, "Trace inequalities and quantum entropies: An introductory course" (see Lemma 2.8)

noncomputable def Real.rpowIntegrand₀₁ (p t x : ℝ) : ℝ

Integrand for representing x ↦ x ^ p for p ∈ (0,1)

Equations

• p.rpowIntegrand₀₁ t x = t ^ p * (t⁻¹ - (t + x)⁻¹)

noncomputable def Real.rpowIntegrand₁₂ (p t x : ℝ) : ℝ

Integrand for representing x ↦ x^p for p ∈ (1,2)

Equations

• p.rpowIntegrand₁₂ t x = t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1)

@[simp]

theorem Real.rpowIntegrand₀₁_zero_right {p t : ℝ} : p.rpowIntegrand₀₁ t 0 = 0

theorem Real.rpowIntegrand₀₁_zero_left {p x : ℝ} (hp : 0 < p) : p.rpowIntegrand₀₁ 0 x = 0

theorem Real.rpowIntegrand₀₁_nonneg {p t x : ℝ} (hp : 0 < p) (ht : 0 ≤ t) (hx : 0 ≤ x) : 0 ≤ p.rpowIntegrand₀₁ t x

theorem Real.rpowIntegrand₀₁_eq_pow_div {p t x : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 ≤ t) (hx : 0 ≤ x) : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

theorem Real.rpowIntegrand₀₁_eqOn_pow_div {p x : ℝ} (hp : p ∈ Set.Ioo 0 1) (hx : 0 ≤ x) : Set.EqOn (fun (x_1 : ℝ) => p.rpowIntegrand₀₁ x_1 x) (fun (t : ℝ) => t ^ (p - 1) * x / (t + x)) (Set.Ioi 0)

theorem Real.rpowIntegrand₀₁_apply_mul {p t x : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 ≤ t) (hx : 0 ≤ x) : p.rpowIntegrand₀₁ (x * t) x = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)

theorem Real.rpowIntegrand₀₁_apply_mul' {p t x : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 ≤ t) (hx : 0 ≤ x) : p.rpowIntegrand₀₁ (x * t) x * x = p.rpowIntegrand₀₁ t 1 * x ^ p

theorem Real.rpowIntegrand₀₁_apply_mul_eqOn_Ici {p x : ℝ} (hp : p ∈ Set.Ioo 0 1) (hx : 0 ≤ x) : Set.EqOn (fun (t : ℝ) => p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) => p.rpowIntegrand₀₁ t 1 * x ^ p) (Set.Ici 0)

theorem Real.continuousOn_rpowIntegrand₀₁ {p x : ℝ} (hp : p ∈ Set.Ioo 0 1) (hx : 0 ≤ x) : ContinuousOn (fun (x_1 : ℝ) => p.rpowIntegrand₀₁ x_1 x) (Set.Ioi 0)

theorem Real.aestronglyMeasurable_rpowIntegrand₀₁ {p x : ℝ} (hp : p ∈ Set.Ioo 0 1) (hx : 0 ≤ x) : MeasureTheory.AEStronglyMeasurable (fun (x_1 : ℝ) => p.rpowIntegrand₀₁ x_1 x) (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem Real.rpowIntegrand₀₁_monotoneOn {p t : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 ≤ t) : MonotoneOn (p.rpowIntegrand₀₁ t) (Set.Ici 0)

theorem Real.continuousOn_rpowIntegrand₀₁_uncurry {p : ℝ} (hp : p ∈ Set.Ioo 0 1) (s : Set ℝ) (hs : s ⊆ Set.Ici 0) : ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (Set.Ioi 0 ×ˢ s)

theorem Real.continuousOn_rpowIntegrand₀₁_Ici {p t : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 < t) : ContinuousOn (p.rpowIntegrand₀₁ t) (Set.Ici 0)

theorem Real.rpowIntegrand₀₁_le_rpow_sub_two_mul_self {p t x : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 < t) (hx : 0 ≤ x) : p.rpowIntegrand₀₁ t x ≤ t ^ (p - 2) * x

theorem Real.rpowIntegrand₀₁_le_rpow_sub_one {p t x : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 ≤ t) (hx : 0 ≤ x) : p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

theorem Real.rpowIntegrand₀₁_one_ge_rpow_sub_two {p t : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 1 ≤ t) : 1 / 2 * t ^ (p - 2) ≤ p.rpowIntegrand₀₁ t 1

theorem Real.rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one {p t : ℝ} (ht : 0 < t) : Set.EqOn (p.rpowIntegrand₀₁ t) (fun (x : ℝ) => t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Set.Ici 0)

theorem Real.integrableOn_rpowIntegrand₀₁_Ioi {p x : ℝ} (hp : p ∈ Set.Ioo 0 1) (hx : 0 ≤ x) : MeasureTheory.IntegrableOn (fun (x_1 : ℝ) => p.rpowIntegrand₀₁ x_1 x) (Set.Ioi 0) MeasureTheory.volume

theorem Real.integrableOn_rpowIntegrand₀₁_Ici {p x : ℝ} (hp : p ∈ Set.Ioo 0 1) (hx : 0 ≤ x) : MeasureTheory.IntegrableOn (fun (x_1 : ℝ) => p.rpowIntegrand₀₁ x_1 x) (Set.Ici 0) MeasureTheory.volume

theorem Real.integral_rpowIntegrand₀₁_eq_rpow_mul_const {p x : ℝ} (hp : p ∈ Set.Ioo 0 1) (hx : 0 ≤ x) : ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t x = x ^ p * ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t 1

theorem Real.le_integral_rpowIntegrand₀₁_one {p : ℝ} (hp : p ∈ Set.Ioo 0 1) : -1 / (2 * (p - 1)) ≤ ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t 1

theorem Real.integral_rpowIntegrand₀₁_one_pos {p : ℝ} (hp : p ∈ Set.Ioo 0 1) : 0 < ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t 1

theorem Real.rpow_eq_const_mul_integral {p x : ℝ} (hp : p ∈ Set.Ioo 0 1) (hx : 0 ≤ x) : x ^ p = (∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t x

The integral representation of the function x ↦ x^p (where p ∈ (0, 1)) .

theorem Real.exists_measure_rpow_eq_integral_rpowIntegrand₀₁ {p : ℝ} (hp : p ∈ Set.Ioo 0 1) : ∃ (μ : MeasureTheory.Measure ℝ), ∀ x ∈ Set.Ici 0, MeasureTheory.IntegrableOn (fun (t : ℝ) => p.rpowIntegrand₀₁ t x) (Set.Ioi 0) μ ∧ x ^ p = ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t x ∂μ

The integral representation of the function x ↦ x ^ p (where p ∈ (0, 1)) .

@[deprecated Real.exists_measure_rpow_eq_integral_rpowIntegrand₀₁ (since := "2026-04-03")]

theorem Real.exists_measure_rpow_eq_integral {p : ℝ} (hp : p ∈ Set.Ioo 0 1) : ∃ (μ : MeasureTheory.Measure ℝ), ∀ x ∈ Set.Ici 0, MeasureTheory.IntegrableOn (fun (t : ℝ) => p.rpowIntegrand₀₁ t x) (Set.Ioi 0) μ ∧ x ^ p = ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t x ∂μ

Alias of Real.exists_measure_rpow_eq_integral_rpowIntegrand₀₁.

---

The integral representation of the function x ↦ x ^ p (where p ∈ (0, 1)) .

theorem Real.rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ {p t x : ℝ} (hx : 0 ≤ x) (ht : 0 < t) : p.rpowIntegrand₁₂ t x = x * (p - 1).rpowIntegrand₀₁ t x

theorem Real.rpowIntegrand₁₂_nonneg {p t x : ℝ} (hp : 1 < p) (ht : 0 ≤ t) (hx : 0 ≤ x) : 0 ≤ p.rpowIntegrand₁₂ t x

theorem Real.rpowIntegrand₁₂_zero {p t : ℝ} (ht : 0 < t) : p.rpowIntegrand₁₂ t 0 = 0

theorem Real.continuousOn_rpowIntegrand₁₂_uncurry {p : ℝ} (hp : p ∈ Set.Ioi 1) (s : Set ℝ) (hs : s ⊆ Set.Ici 0) : ContinuousOn (Function.uncurry p.rpowIntegrand₁₂) (Set.Ioi 0 ×ˢ s)

theorem Real.monotoneOn_rpowIntegrand₁₂ {p t : ℝ} (hp : p ∈ Set.Ioo 1 2) (ht : 0 < t) : MonotoneOn (p.rpowIntegrand₁₂ t) (Set.Ici 0)

theorem Real.integrableOn_rpowIntegrand₁₂ {p x : ℝ} (hp : p ∈ Set.Ioo 1 2) (hx : 0 ≤ x) : MeasureTheory.IntegrableOn (fun (x_1 : ℝ) => p.rpowIntegrand₁₂ x_1 x) (Set.Ioi 0) MeasureTheory.volume

theorem Real.rpow_eq_const_mul_integral_rpowIntegrand₁₂ {p x : ℝ} (hp : p ∈ Set.Ioo 1 2) (hx : 0 ≤ x) : x ^ p = (∫ (t : ℝ) in Set.Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₁₂ t x

The integral representation of the function x ↦ x^p (where p ∈ (1, 2)) .

theorem Real.exists_measure_rpow_eq_integral_rpowIntegrand₁₂ {p : ℝ} (hp : p ∈ Set.Ioo 1 2) : ∃ (μ : MeasureTheory.Measure ℝ), ∀ x ∈ Set.Ici 0, MeasureTheory.IntegrableOn (fun (t : ℝ) => p.rpowIntegrand₁₂ t x) (Set.Ioi 0) μ ∧ x ^ p = ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₁₂ t x ∂μ

The integral representation of the function x ↦ x^p (where p ∈ (1, 2)) .

theorem CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {p t : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 < t) (a : A) (ha : 0 ≤ a) : cfcₙ (p.rpowIntegrand₀₁ t) a = t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

theorem CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ (A : Type u_1) [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [CompleteSpace A] {p : NNReal} (hp : p ∈ Set.Ioo 0 1) : ∃ (μ : MeasureTheory.Measure ℝ), ∀ a ∈ Set.Ici 0, MeasureTheory.IntegrableOn (fun (t : ℝ) => cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Set.Ioi 0) μ ∧ a ^ p = ∫ (t : ℝ) in Set.Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ

The integral representation of the function x ↦ x ^ p (where p ∈ (0, 1)).

theorem CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₁₂ (A : Type u_1) [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [CompleteSpace A] {p : NNReal} (hp : p ∈ Set.Ioo 1 2) : ∃ (μ : MeasureTheory.Measure ℝ), ∀ a ∈ Set.Ici 0, MeasureTheory.IntegrableOn (fun (t : ℝ) => cfcₙ ((↑p).rpowIntegrand₁₂ t) a) (Set.Ioi 0) μ ∧ a ^ p = ∫ (t : ℝ) in Set.Ioi 0, cfcₙ ((↑p).rpowIntegrand₁₂ t) a ∂μ

The integral representation of the function x ↦ x ^ p (where p ∈ (1, 2)).

theorem CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁ {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p t : ℝ} (hp : p ∈ Set.Ioo 0 1) (ht : 0 < t) : MonotoneOn (cfcₙ (p.rpowIntegrand₀₁ t)) (Set.Ici 0)

rpowIntegrand₀₁ p t is operator monotone for all p ∈ Ioo 0 1 and all t ∈ Ioi 0.