Minkowski's integral inequality

This file was automatically generated by Claude.

Minkowski's integral inequality states that the L^p norm of an integral is at most the integral of the L^p norms: for 1 ≤ p, a jointly measurable f : α × β → [0, ∞], a σ-finite measure μ on α and an s-finite measure ν on β, (∫ (∫ f(x, y) dν(y))^p dμ(x))^{1/p} ≤ ∫ (∫ f(x, y)^p dμ(x))^{1/p} dν(y).

The proof is the textbook duality argument: for a truncation G ≤ F = ∫ f(·, y) dν with finite ∫ G^p, write ∫ G^p ≤ ∫ G^{p-1} F, exchange the integrals (Tonelli), apply Hölder's inequality in x for each y, and divide by (∫ G^p)^{1 - 1/p}. The truncations G_n = min(F, n) 1_{S_n} on the spanning sets of μ increase to F, and monotone convergence concludes.

References: E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton University Press, 1970, Appendix A.1; G. H. Hardy, J. E. Littlewood, G. Pólya, Inequalities, Cambridge University Press, 2nd ed., 1952, Theorem 202. The statement and all definitions depend only on Mathlib.

theorem TrilinearHT.Auto.ennreal_rpow_sub_one_mul_self {p : ℝ} (hp : 1 < p) (x : ENNReal) : x ^ (p - 1) * x = x ^ p

theorem TrilinearHT.Auto.minkowski_truncated {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {p : ℝ} (hp : 1 ≤ p) {f : α → β → ENNReal} (hf : Measurable (Function.uncurry f)) {G : α → ENNReal} (hG : Measurable G) (hGF : ∀ (x : α), G x ≤ ∫⁻ (y : β), f x y ∂ν) (hfin : ∫⁻ (x : α), G x ^ p ∂μ ≠ ⊤) : (∫⁻ (x : α), G x ^ p ∂μ) ^ (1 / p) ≤ ∫⁻ (y : β), (∫⁻ (x : α), f x y ^ p ∂μ) ^ (1 / p) ∂ν

The truncated duality step of Minkowski's integral inequality: for G ≤ F = ∫ f(·, y) dν with finite ∫ G^p, (∫ G^p)^{1/p} ≤ ∫ (∫ f(·, y)^p)^{1/p} dν.

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

Minkowski's integral inequality for nonnegative functions: for 1 ≤ p, a jointly measurable f : α × β → [0, ∞], a σ-finite measure μ and an s-finite measure ν, (∫ (∫ f(x, y) dν(y))^p dμ(x))^{1/p} ≤ ∫ (∫ f(x, y)^p dμ(x))^{1/p} dν(y).