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 ∂μ

TODO

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

References

• [carlen2010] 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₀₁_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.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 ℝ), (∀ᵐ (t : ℝ) ∂μ, 0 < t) ∧ ∀ (x : ℝ), 0 ≤ x → x ^ p = ∫ (t : ℝ), p.rpowIntegrand₀₁ t x ∂μ

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