Minkowski's integral inequality

For 1 ≤ p and a jointly a.e. measurable f : α → β → ℝ≥0∞ on a product of a σ-finite and an s-finite measure space,

(∫⁻ x, (∫⁻ y, f x y ∂ν) ^ p ∂μ) ^ (1 / p) ≤ ∫⁻ y, (∫⁻ x, f x y ^ p ∂μ) ^ (1 / p) ∂ν:

the Lᵖ(μ) seminorm of an integral over ν is at most the integral over ν of the Lᵖ(μ) seminorms. This is the continuous form of Minkowski's inequality ENNReal.lintegral_Lp_add_le for a sum of two functions. A typical use bounds the Lᵖ size of a quantity accumulated along a time interval, such as the length ∫ |γ'|(t) dt of a random curve, by the time integral of the Lᵖ sizes of the integrand.

The statement is in ℝ≥0∞, so it needs no integrability hypotheses.

The proof is by duality. Write G x = ∫⁻ y, f x y ∂ν and let R be the right-hand side. Hölder's inequality in x for each y, followed by Tonelli's theorem, gives ∫⁻ x, G x * h x ∂μ ≤ R * (∫⁻ x, h x ^ q ∂μ) ^ (1 / q) for every measurable h, where q is the conjugate exponent. Testing against the indicator of a set of finite measure shows that G is finite almost everywhere when R is finite; testing against G ^ (p - 1) on the sets where G is bounded and μ is finite bounds the truncated integrals of G ^ p, and monotone convergence removes the truncation.

A typical consequence bounds a weighted Lʳ norm, over a parameter t, of the integrals of g over a family of sets {x | R t x}: pulling the power inside makes it an integral of g against the Lʳ norms in t of the truncated weights (TauCeti.lintegral_mul_setLIntegral_rpow_le). Off-diagonal Marcinkiewicz interpolation uses it with the sets cut out by a height c * t ^ γ.

Main declarations

• TauCeti.lintegral_Lp_lintegral_le: Minkowski's integral inequality.
• TauCeti.lintegral_mul_setLIntegral_rpow_le: Minkowski's integral inequality for weighted truncations.

References

• G. B. Folland, Real Analysis: Modern Techniques and Their Applications, 2nd ed., Theorem 6.19.

theorem TauCeti.lintegral_Lp_lintegral_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SFinite ν] {f : α → β → ENNReal} (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) {p : ℝ} (hp : 1 ≤ p) : (∫⁻ (x : α), (∫⁻ (y : β), f x y ∂ν) ^ p ∂μ) ^ (1 / p) ≤ ∫⁻ (y : β), (∫⁻ (x : α), f x y ^ p ∂μ) ^ (1 / p) ∂ν

Minkowski's integral inequality. For 1 ≤ p and a jointly a.e. measurable f : α → β → ℝ≥0∞, the Lᵖ(μ) seminorm of x ↦ ∫⁻ y, f x y ∂ν is at most the integral over ν of the Lᵖ(μ) seminorms of the functions x ↦ f x y: (∫⁻ x, (∫⁻ y, f x y ∂ν) ^ p ∂μ) ^ (1 / p) ≤ ∫⁻ y, (∫⁻ x, f x y ^ p ∂μ) ^ (1 / p) ∂ν.

theorem TauCeti.lintegral_mul_setLIntegral_rpow_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite ν] [MeasureTheory.SFinite μ] {R : β → α → Prop} (hR : MeasurableSet {z : β × α | R z.1 z.2}) {w : β → ENNReal} (hw : Measurable w) {g : α → ENNReal} (hg : Measurable g) {r : ℝ} (hr : 1 ≤ r) : ∫⁻ (t : β), w t * (∫⁻ (x : α) in {x : α | R t x}, g x ∂μ) ^ r ∂ν ≤ (∫⁻ (x : α), g x * (∫⁻ (t : β), {t : β | R t x}.indicator w t ∂ν) ^ r⁻¹ ∂μ) ^ r

Minkowski's integral inequality for weighted truncations. For 1 ≤ r, a weight w and a measurable relation R, the weighted Lʳ(ν) norm in t of the truncated integrals ∫⁻ x in {x | R t x}, g x ∂μ is at most the integral of g against the Lʳ(ν) norms in t of the truncations of the weight:

∫⁻ t, w t * (∫⁻ x in {R t ·}, g ∂μ) ^ r ∂ν ≤ (∫⁻ x, g x * (∫⁻ t in {R · x}, w ∂ν) ^ r⁻¹ ∂μ) ^ r.