Scalar left/right relative-entropy integral provider

This module contains the one-dimensional integral identities used by the Lindblad/Effros left/right relative-entropy route. They are scalar inputs for the later spectral-overlap, density-integrability, and matrix integral representation leaves.

It does not prove matrix relative-entropy joint convexity, Epstein, Lieb, Tropp, Golden-Thompson, or Matrix Bernstein.

theorem HighDimProb.RelativeEntropy.real_log_perspective_integral {x : ℝ} (hx : 0 < x) : ∫ (t : ℝ) in Set.Ioi 0, (x - 1) ^ 2 * t / ((x + t) * (1 + t) ^ 2) = x * Real.log x - x + 1

Scalar improper-integral representation for the perspective of x log x.

The representation measure has density t / (1 + t)^2 on (0, inf).

theorem HighDimProb.RelativeEntropy.real_relativeEntropy_integral_representation {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : ∫ (t : ℝ) in Set.Ioi 0, (a - b) ^ 2 * t / ((a + t * b) * (1 + t) ^ 2) = a * (Real.log a - Real.log b) - (a - b)

Two-parameter scalar relative-entropy representation with denominator a + t b.

theorem HighDimProb.RelativeEntropy.real_relativeEntropy_integral_representation_density {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : ∫ (t : ℝ) in Set.Ioi 0, t / (1 + t) ^ 2 * ((a - b) ^ 2 / (a + t * b)) = a * (Real.log a - Real.log b) - (a - b)

Density form of real_relativeEntropy_integral_representation.

theorem HighDimProb.RelativeEntropy.real_relativeEntropy_integrand_integrableOn {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (a - b) ^ 2 * t / ((a + t * b) * (1 + t) ^ 2)) (Set.Ioi 0) MeasureTheory.volume

Integrability of the scalar relative-entropy representation integrand on (0, inf).