LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

First projections are measurable and square-integrable

Statement

For the setup of Two-sample order-r U-statistic and first projections, suppose $h \in L^{2} (P^{\otimes r} \otimes Q^{\otimes r})$ . Then the section integrals defining $g_{X}$ and $g_{Y}$ are finite and measurable almost everywhere, can be assigned measurable values on exceptional null sets, and define square-integrable centered projections. In particular, $E_{P} [g_{X} (X_{1})] = E_{Q} [g_{Y} (Y_{1})] = 0,$ $E_{P} [g_{X} (X_{1})^{2}] \leq E_{P^{\otimes r} \otimes Q^{\otimes r}} [h^{2}], E_{Q} [g_{Y} (Y_{1})^{2}] \leq E_{P^{\otimes r} \otimes Q^{\otimes r}} [h^{2}] .$

Facts & Assumptions

Given: Probability measures $P, Q$ , a product-measurable kernel $h$ with finite second moment under $P^{\otimes r} \otimes Q^{\otimes r}$ , and the projection definitions.

[F1]

Two-sample order-r U-statistic and first projections defines $g_{X}$ and $g_{Y}$ as the corresponding conditional section integrals minus $θ (P, Q; h)$ .

[F2]

Fubini's theorem for L^1 functions on a sigma-finite product gives integrable sections almost everywhere, measurable section-integral versions, and equality of iterated and product integrals.

[F3]

Cauchy-Schwarz inequality for $L^{2}$ gives $∣ \int a b ∣ \leq ∥ a ∥_{2} ∥ b ∥_{2}$ .

[F4]

The product sigma-algebra and its finite iterates supplies the finite product sigma-algebras on which the section maps and product integrals are defined.

Proof

Given: $h \in L^{2} (P^{\otimes r} \otimes Q^{\otimes r})$ and the definitions in [F1]. Prove both projections are measurable, centered, and square-integrable with the displayed bounds.

1.1F1F3

The product measure is a probability measure, so applying [F3] to $h$ and the constant function $1$ gives $E ∣ h ∣ \leq (E h^{2})^{1 / 2} < \infty$ . Thus $h$ is integrable and $θ (P, Q; h) = E h$ is finite.

1.2F1F2F4

By [F4], the product decomposition uses the stated finite product sigma-algebra. Apply [F2] with first coordinate $P$ -distributed and the remaining $2 r - 1$ coordinates distributed according to $P$ or $Q$ . For $P$ -almost every $x$ , the section integral $f_{X} (x) = \int h (x, x_{2}, \dots, x_{r}; y_{1}, \dots, y_{r}) d P^{r - 1} d Q^{r}$ is finite; [F2] supplies a measurable version after setting it to zero on the exceptional null set. Reordering the coordinates and using the $Y_{1}$ section gives a finite measurable $f_{Y}$ for $Q$ -almost every $y$ .

2.1F2F3step 1.2

For each good $x$ , Cauchy–Schwarz [F3] on the remaining probability product measure gives $∣ f_{X} (x) ∣^{2} \leq \int h (x, x_{2}, \dots, x_{r}; y_{1}, \dots, y_{r})^{2} d P^{r - 1} d Q^{r}$ . Integrating in $P$ and using [F2] yields $E_{P} [f_{X} (X_{1})^{2}] \leq E [h^{2}]$ . The same argument for the $Y_{1}$ section gives $E_{Q} [f_{Y} (Y_{1})^{2}] \leq E [h^{2}]$ .

3.1F1F2step 1.1step 2.1∎

By [F2], $E_{P} f_{X} = E h = θ (P, Q; h)$ and $E_{Q} f_{Y} = E h = θ (P, Q; h)$ . Subtracting this finite mean gives the centered projections in [F1]; step 2.1 and finiteness of $θ$ show both remain square-integrable.

Depends on

Used by

The weak null does not center every mixed kernel assignment Counterexample
Pooled-mixture projection and variance Lemma
Two-sample Hoeffding decomposition Lemma
Permutation CLT for a two-sample U-statistic under a weak null Theorem

Cited to discharge well-definedness by Two-sample order-r U-statistic and first projections.

Dependency tree · two levels

20 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

Péter Major, Some Results About U-statistics, in On the Estimation of Multiple Random Integrals and U-Statistics, Lecture Notes in Mathematics 2079, Theorem 9.1 and proof (standard reference, not scraped)
E. Y. Chung and J. P. Romano, Asymptotically Valid and Exact Permutation Tests Based on Two-Sample U-Statistics, Stanford Technical Report 2011-09, §3 (standard reference, not scraped)