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.

Dyadic cell-average projections converge strongly in L2 of a bounded set

Statement

Assume Countable Choice. Let $D \subset R^{3}$ be bounded and Lebesgue measurable, and choose a half-open cube $Q$ of positive side length containing $D$ . Subdivide $Q$ into its nested dyadic cubes at mesh $h_{N} = 2^{- N} side (Q)$ . Let $E_{N, j} = D \cap Q_{N, j}$ range over the finitely many cells of positive measure, let $V_{N} \subset L^{2} (D; C)$ be the functions constant on each such cell, and define $P_{N}$ by replacing a function on each $E_{N, j}$ by its cell average. Then $P_{N}$ is the orthogonal projection onto $V_{N}$ , $∥ P_{N} ∥ \leq 1$ , the spaces $V_{N}$ are increasing, and $P_{N} v \to v$ in $L^{2} (D; C)$ for every $v \in L^{2} (D; C)$ .

Facts & Assumptions

Given: Countable Choice, a bounded measurable $D$ , a positive-side containing cube $Q$ , its nested dyadic partitions, and $v \in L^{2} (D; C)$ .

[F1]

Finite linear combinations of dyadic box indicators are dense in real $L^{2}$ of the Borel cube (Base- $b$ box step functions are dense in $L^{2}$ of the cube); the complex conclusion follows by applying the real result to real and imaginary parts.

[F2]

Complex $L^{2}$ Cauchy--Schwarz holds, and Lebesgue measure is invariant under translations and scales under invertible linear changes of variables (The complex $L^{2}$ pairing is well-defined and satisfies Cauchy–Schwarz, Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not, Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ ).

[F3]

Under Countable Choice, a function measurable for the completion is almost everywhere equal to a Borel-measurable function when the base sigma-algebra is Borel (A function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra).

Proof

Given: Countable Choice, a bounded measurable $D$ , a positive-side containing cube $Q$ , its nested dyadic partitions, and $v \in L^{2} (D; C)$ .

1.1givenF2constructalgebra

For each positive-measure cell $E_{N, j}$ the average is finite by Cauchy–Schwarz, since $\int_{E_{N, j}} ∣ v ∣ \leq ∣ E_{N, j} ∣^{1 / 2} ∥ v ∥_{L^{2} (E_{N, j})}$ . For every function constant on the cells, the integral of $v - P_{N} v$ against that function is zero cell by cell. Thus $v - P_{N} v ⊥ V_{N}$ and $P_{N} v \in V_{N}$ , so $P_{N}$ is the orthogonal projection. Pythagoras gives $∥ P_{N} v ∥_{2} \leq ∥ v ∥_{2}$ .

1.2F1F2F3givenconstruct

Extend $v$ by zero from $D$ to $Q$ . The extension is measurable for completed Lebesgue measure; rescale and translate $Q$ to $[0, 1)^{3}$ , which preserves completed measurability by [F2]. Apply [F3] separately to the real and imaginary parts to obtain a Borel-measurable representative of the rescaled extension equal to it almost everywhere. This representative is in Borel $L^{2}$ because the original extension is square integrable and the affine change multiplies its squared integral by the fixed positive factor $side (Q)^{- 3}$ . Applying [F1] to its real and imaginary parts gives dyadic box step functions converging in Borel $L^{2} ([0, 1)^{3})$ , hence also in completed $L^{2}$ . Pulling them back to $Q$ and restricting to $D$ preserves convergence up to the fixed affine measure factor. Every finite family of base-2 boxes is constant on the cells of a sufficiently fine common dyadic partition, so the restrictions belong to some $V_{N}$ . Thus $⋃_{N} V_{N}$ is dense in $L^{2} (D; C)$ ; the partitions are nested, so $V_{N} \subseteq V_{N + 1}$ .

2.1givenstep 1.1step 1.2algebra∎

Fix $ε > 0$ . By step 1.2 choose $w \in V_{m}$ with $∥ v - w ∥_{2} < ε / 2$ . For every $N \geq m$ , nesting gives $P_{N} w = w$ . Therefore $∥ P_{N} v - v ∥_{2} \leq ∥ P_{N} (v - w) ∥_{2} + ∥ v - w ∥_{2} \leq 2 ∥ v - w ∥_{2} < ε$ , by step 1.1. Thus $P_{N} v \to v$ in $L^{2} (D; C)$ .

Depends on

Used by

Dependency tree · two levels

68 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

Art B. Owen, Monte Carlo Variance of Scrambled Net Quadrature, §6 (standard reference, not scraped)
Andreas Neubauer and Ronny Ramlau, Lecture Notes: Integral Equations and Boundary Value Problems (standard reference, not scraped)