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.

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)⁻¹)
• exists_measure_rpow_eq_integral: there exists a measure on ℝ such that x ^ p = ∫ t, rpowIntegrand₀₁ p t x ∂μ
• CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁: the corresponding statement where x ^ p is defined via the CFC.
• CFC.monotone_nnrpow, CFC.monotone_rpow: a ↦ a ^ p is operator monotone for p ∈ [0,1]
• CFC.monotone_sqrt: CFC.sqrt is operator monotone

TODO

• Show operator concavity of rpow over Icc 0 1
• Give analogous representations for the ranges Ioo (-1) 0 and Ioo 1 2.

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)⁻¹)

@[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 {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)) .

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.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.

theorem CFC.monotone_nnrpow {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : NNReal} (hp : p ∈ Set.Icc 0 1) : Monotone fun (a : A) => a ^ p

a ↦ a ^ p is operator monotone for p ∈ [0,1].

theorem CFC.monotone_sqrt {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Monotone sqrt

CFC.sqrt is operator monotone.

theorem CFC.nnrpow_le_nnrpow {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : NNReal} (hp : p ∈ Set.Icc 0 1) {a b : A} (hab : a ≤ b) : a ^ p ≤ b ^ p

theorem CFC.sqrt_le_sqrt {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a b : A) (hab : a ≤ b) : sqrt a ≤ sqrt b

theorem CFC.monotone_rpow {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : ℝ} (hp : p ∈ Set.Icc 0 1) : Monotone fun (a : A) => a ^ p

a ↦ a ^ p is operator monotone for p ∈ [0,1].

theorem CFC.rpow_le_rpow {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : ℝ} (hp : p ∈ Set.Icc 0 1) {a b : A} (hab : a ≤ b) : a ^ p ≤ b ^ p