Lower integrals of a real power, and the layer cake formula in ℝ≥0∞

This file collects the two lower integrals of t ↦ t ^ s on a half-line that the real interpolation method needs, and uses them to transport Mathlib's layer cake formula from real-valued to ℝ≥0∞-valued functions.

For -1 < s the function t ↦ t ^ s is integrable near 0 and not integrable near ∞, and the two computations below are the two halves of that dichotomy: TauCeti.lintegral_ofReal_rpow_Ioo evaluates ∫⁻ t in (0, a), t ^ s to the expected antiderivative for such an s, while TauCeti.lintegral_ofReal_rpow_Ioi records that ∫⁻ t in (0, ∞), t ^ s diverges — the latter for every exponent s, since a power that is integrable at the origin is not integrable at infinity and conversely.

TauCeti.lintegral_indicator_ofReal_rpow_Ioi packages the two together as the single formula the real interpolation method uses: the integral over (0, ∞) of t ^ s cut off at the height where c * t reaches a threshold a : ℝ≥0∞, which is the finite antiderivative when a is finite and ∞ when it is not.

TauCeti.lintegral_indicator_le_ofReal_rpow_Ioi is the companion over the complementary region, where c * t has already passed the threshold. There the roles of the two endpoints are exchanged: the integral converges at infinity and diverges at the origin, so the exponent range is s < -1 and the value is ∞ exactly when the threshold is 0. The two together are what the real interpolation method between two finite exponents integrates against, the first for the part of a function above a height and the second for the part below it.

The layer cake formula ∫⁻ u ^ p = p * ∫⁻ t in (0, ∞), ν {u > t} * t ^ (p - 1) is in Mathlib as MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul, but only for a nonnegative real-valued u. Analysis in ℝ≥0∞ — where the operators of interpolation theory naturally land, since a supremum of averages such as the Hardy–Littlewood maximal function is defined without any finiteness hypothesis — needs the version for u : β → ℝ≥0∞, which is TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul below. The superlevel sets there are cut at the ℝ≥0∞-valued threshold ENNReal.ofReal t, which is what distinguishes the statement from Mathlib's.

The passage between the two is by ENNReal.toReal, which is faithful exactly where u is finite. Where u = ∞ on a set of positive measure both sides are ∞: the left because u ^ p = ∞ there, and the right because every superlevel set then has measure at least that of {u = ∞}, and ∫⁻ t in (0, ∞), t ^ (p - 1) diverges. That is where TauCeti.lintegral_ofReal_rpow_Ioi is used, and it is why the statement needs no finiteness hypothesis on u.

Main declarations

• TauCeti.lintegral_ofReal_rpow_Ioo: ∫⁻ t in (0, a), t ^ s = a ^ (s + 1) / (s + 1) for -1 < s and 0 ≤ a.
• TauCeti.lintegral_ofReal_rpow_Ioi: ∫⁻ t in (0, ∞), t ^ s = ∞, for every s.
• TauCeti.lintegral_indicator_ofReal_rpow_Ioi: the same integral truncated at the height where c * t reaches a : ℝ≥0∞, evaluated to c ^ (-(s + 1)) / (s + 1) * a ^ (s + 1).
• TauCeti.lintegral_indicator_le_ofReal_rpow_Ioi: the integral over the complementary region, where c * t is at least a, evaluated to c ^ (-(s + 1)) / (-(s + 1)) * a ^ (s + 1) for s < -1.
• TauCeti.setLIntegral_Ioc_ite_rpow_le: an upper-tail bound for a negative power restricted by a linear threshold.
• TauCeti.setLIntegral_Ioc_rpow_mul_ite_le: the same bound with constant and linear weights.
• TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul: the layer cake formula for an ℝ≥0∞-valued function.
• TauCeti.sigmaFinite_restrict_pos_of_lintegral_rpow_ne_top: a function with finite positive power integral is carried by a σ-finite part of the measure.

References

• L. Grafakos, Classical Fourier Analysis, Proposition 1.1.4.

theorem TauCeti.lintegral_ofReal_rpow_Ioo {s : ℝ} (hs : -1 < s) {a : ℝ} (ha : 0 ≤ a) : ∫⁻ (t : ℝ) in Set.Ioo 0 a, ENNReal.ofReal (t ^ s) = ENNReal.ofReal (a ^ (s + 1) / (s + 1))

The lower integral of t ^ s over a bounded interval (0, a), for -1 < s and 0 ≤ a: the power is integrable at the origin and the value is the expected antiderivative.

Nonnegativity of a is needed: for a < 0 the interval is empty while a ^ (s + 1), a real power at a negative base, need not vanish.

theorem TauCeti.lintegral_ofReal_rpow_Ioi (s : ℝ) : ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (t ^ s) = ⊤

The lower integral of t ^ s over (0, ∞) diverges, for every exponent s: the power fails to be integrable at the origin or at infinity, according as s ≤ -1 or -1 < s.

theorem TauCeti.setLIntegral_Ioc_ite_rpow_le {n : ℕ} (hn : 0 < n) {r D : ℝ} (hr : 0 < r) : (∫⁻ (t : ℝ) in Set.Ioc 0 1, if r ≤ t * D then ENNReal.ofReal (t ^ (-↑n - 1)) else 0) ≤ ENNReal.ofReal (D ^ n / ↑n) * ENNReal.ofReal (r ^ (-↑n))

The tail integral ∫_{r / D}^∞ t ^ (-n - 1) dt = D ^ n r ^ (-n) / n bounds the integral of t ^ (-n - 1) over those t ∈ (0, 1] with r ≤ t * D.

theorem TauCeti.setLIntegral_Ioc_rpow_mul_ite_le {n : ℕ} (hn : 0 < n) (a : ENNReal) {r : ℝ} (hr : 0 ≤ r) (D : ℝ) : ∫⁻ (t : ℝ) in Set.Ioc 0 1, ENNReal.ofReal (t ^ (-↑n - 1)) * (a * if r ≤ t * D then ENNReal.ofReal r else 0) ≤ ENNReal.ofReal (D ^ n / ↑n) * (a * ENNReal.ofReal r ^ (1 - ↑n))

The bound of setLIntegral_Ioc_ite_rpow_le, multiplied by the length r of a segment and by a weight a, gives the kernel r ^ (1 - n).

theorem TauCeti.lintegral_indicator_ofReal_rpow_Ioi {s : ℝ} (hs : -1 < s) {c : ℝ} (hc : 0 < c) (a : ENNReal) : ∫⁻ (t : ℝ) in Set.Ioi 0, {t : ℝ | ENNReal.ofReal (c * t) < a}.indicator (fun (t : ℝ) => ENNReal.ofReal (t ^ s)) t = ENNReal.ofReal (c ^ (-(s + 1)) / (s + 1)) * a ^ (s + 1)

The lower integral of t ^ s over (0, ∞), truncated at the height where c * t reaches a threshold a : ℝ≥0∞: for -1 < s and 0 < c,

∫⁻ t in (0, ∞), [c * t < a] * t ^ s = c ^ (-(s + 1)) / (s + 1) * a ^ (s + 1).

For a finite a the cut-off makes this the integral over (0, a / c) evaluated by TauCeti.lintegral_ofReal_rpow_Ioo; for a = ∞ the cut-off is vacuous and both sides are ∞, by TauCeti.lintegral_ofReal_rpow_Ioi. This is the inner integral of the real interpolation method, where a is the value of the function being interpolated at a point.

theorem TauCeti.lintegral_indicator_le_ofReal_rpow_Ioi {s : ℝ} (hs : s < -1) {c : ℝ} (hc : 0 < c) (a : ENNReal) : ∫⁻ (t : ℝ) in Set.Ioi 0, {t : ℝ | a ≤ ENNReal.ofReal (c * t)}.indicator (fun (t : ℝ) => ENNReal.ofReal (t ^ s)) t = ENNReal.ofReal (c ^ (-(s + 1)) / -(s + 1)) * a ^ (s + 1)

The lower integral of t ^ s over (0, ∞), restricted to the heights at which c * t has already reached a threshold a : ℝ≥0∞: for s < -1 and 0 < c,

∫⁻ t in (0, ∞), [a ≤ c * t] * t ^ s = c ^ (-(s + 1)) / (-(s + 1)) * a ^ (s + 1).

For a nonzero a this is the convergent tail integral over [a / c, ∞); for a = 0 the restriction is vacuous and both sides are ∞, by TauCeti.lintegral_ofReal_rpow_Ioi, while for a = ∞ the region is empty and both sides vanish. This is the inner integral that the real interpolation method pairs with the part of a function below the height c * t, the exponent range s < -1 being the one in which the power is integrable at infinity; the complementary region is TauCeti.lintegral_indicator_ofReal_rpow_Ioi.

theorem TauCeti.sigmaFinite_restrict_pos_of_lintegral_rpow_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} {p : ℝ} (hf : AEMeasurable f μ) (hp : 0 < p) (htop : ∫⁻ (x : α), f x ^ p ∂μ ≠ ⊤) : MeasureTheory.SigmaFinite (μ.restrict {x : α | 0 < f x})

A function with a finite L^p norm is carried by a σ-finite part of the measure: the level sets {f ≥ 1 / (n + 1)} have finite measure by Chebyshev's inequality applied to f ^ p, and they exhaust {f > 0}.

theorem TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul {β : Type u_2} [MeasurableSpace β] (ν : MeasureTheory.Measure β) {u : β → ENNReal} (hu : AEMeasurable u ν) {p : ℝ} (hp : 0 < p) : ∫⁻ (y : β), u y ^ p ∂ν = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, ν {y : β | ENNReal.ofReal t < u y} * ENNReal.ofReal (t ^ (p - 1))

The layer cake formula for an ℝ≥0∞-valued function: for 0 < p,

∫⁻ u ^ p ∂ν = p * ∫⁻ t in (0, ∞), ν {u > t} * t ^ (p - 1),

where the superlevel set is cut at the threshold ENNReal.ofReal t.

This is MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul for a function that is allowed to take the value ∞; no finiteness hypothesis is needed, because both sides are ∞ as soon as {u = ∞} has positive measure.