LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-10-22 (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Loomis–Whitney integral inequality

Statement

Assume Countable Choice. Let $n \geq 2$ . For each $i \in {1, \dots, n}$ let $g_{i} : R^{n - 1} \to [0, \infty)$ be Lebesgue-measurable and integrable, with its arguments identified with all coordinates except $x_{i}$ . Then $\int_{R^{n}} \prod_{i = 1}^{n} g_{i} (x_{1}, \dots, \hat{x_{i}}, \dots, x_{n})^{1 / (n - 1)} d x \leq \prod_{i = 1}^{n} {(\int_{R^{n - 1}} g_{i})}^{1 / (n - 1)} .$

Statement references

Hölder's inequality for integrals.

Tonelli's theorem for nonnegative product integrals.

Facts & Assumptions

Given: Countable Choice and an integer $n \geq 2$ and nonnegative integrable functions $g_{i}$ on the coordinate hyperplanes.

[F1]

Tonelli applies to nonnegative product-measurable functions on sigma-finite measure spaces. Under Countable Choice, Euclidean Lebesgue measure is the completion of each product of its coordinate factors. In particular Borel functions on a Euclidean product are product-measurable and their product integrals equal their Euclidean integrals. (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, The Euclidean Lebesgue measure is the completion of the product of the factor Lebesgue measures)

[F3]

Under Countable Choice, Lebesgue measure is the completion of its Borel restriction, and every completion-measurable function has a base-measurable representative. Thus each nonnegative finite Lebesgue-measurable $g_{i}$ has a nonnegative finite Borel representative equal almost everywhere. ( $L (R^{n})$ is exactly the completion of the restriction of $λ_{n}$ to the Borel sets, A function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra)

[A2]

Countable Choice is used in the Borel-representative and Euclidean-product identification suppliers. No unqualified choice-free Lebesgue product identity is asserted. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F2]

For nonnegative integrable functions, Hölder's inequality bounds the integral of a product by the product of the corresponding norms. (Holder's inequality for integrals, including the endpoint cases)

[A1]

For the induction step in dimension $n \geq 3$ , assume the inequality in dimension $n - 1$ .

Proof

Given: Countable Choice, the integer $n$ and nonnegative integrable coordinate functions $g_{i}$ .

1.1A2F1F3givenbase

First replace the $g_{i}$ by their Borel representatives from [F3], setting each representative to zero on its Borel set of nonfinite or negative values. The exceptional sets lie in Borel null sets $N_{i}$ . Their coordinate lifts are null in $R^{n}$ : intersect $N_{i} \times R$ with slabs $N_{i} \times [- k, k]$ , $k \geq 1$ , and apply the product rectangle formula in [F1], then take their countable union and permute coordinates. Completeness in [F1] therefore makes the original product Lebesgue-measurable with the same integral as the Borel product; the right-hand integrals are unchanged as well. We may henceforth assume all inputs Borel. For $n = 2$ , Tonelli [F1] factors the left side as $(\int_{R} g_{1}) (\int_{R} g_{2})$ , which is the right side.

2.1A1F1F2step 1.1givenIH

For $n \geq 3$ , assume [A1]. For $i < n$ define $h_{i} (x_{1}, \dots, \hat{x_{i}}, \dots, x_{n - 1}) : = \int_{R} g_{i} (x_{1}, \dots, \hat{x_{i}}, \dots, x_{n - 1}, x_{n}) d x_{n}$ . Apply Tonelli [F1] using the Borel sigma-algebras: each $h_{i}$ is Borel and integrable, possibly infinite on a Borel null set. Set it to zero there. The lifted exceptional sets in $R^{n - 1}$ are null by the slab argument of step 1.1. Consequently all the following sectional inequalities hold almost everywhere, and the modified $h_{i}$ are admissible finite inputs for [A1]. Applying Hölder [F2] in $x_{n}$ to the first $n - 1$ factors and then Tonelli gives an upper bound for the left side of $\int_{R^{n - 1}} g_{n} (x^{'})^{1 / (n - 1)} \prod_{i < n} h_{i} ({\hat{x_{i}}}^{'})^{1 / (n - 1)} d x^{'}$ . Set $H (x^{'}) : = \prod_{i < n} h_{i} ({\hat{x_{i}}}^{'})^{1 / (n - 2)}$ . Hölder in $x^{'}$ with exponents $(n - 1) / (n - 2)$ and $n - 1$ bounds this by $(\int H)^{(n - 2) / (n - 1)} (\int g_{n})^{1 / (n - 1)}$ . The induction hypothesis [A1] bounds $\int H \leq \prod_{i < n} (\int h_{i})^{1 / (n - 2)}$ , while Tonelli gives $\int h_{i} = \int g_{i}$ . Substitution yields the claimed product bound in dimension $n$ .

3.1step 1.1step 2.1discharge-induction: step 2.1∎

Induction from the base case [step 1.1] through step 2.1 proves the inequality for every integer $n \geq 2$ .

Depends on

Used by

BV Sobolev inequality in full space Lemma

Dependency tree · two levels

42 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gláucio Terra, Introduction to Geometric Measure Theory — Lecture Notes, version 1.6 (standard reference, not scraped)