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.
A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included
Statement
Let , assume the Axiom of Countable Choice (The Axiom of Countable Choice ()), and let be reals for . Write
(Axis-parallel rectangles in and their volume). Then is open and is closed, so both are Borel and Lebesgue measurable, and every set with is Lebesgue measurable with
In particular this covers the four one-dimensional face conventions in each coordinate — the open box, the closed box , the half-open box of Half-open boxes in and their volume, and every mixture of them, in any combination of coordinates — and it gives measure to all of them whenever for some . For a half-open box with infinite parameters the value is already (Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume).
Facts & Assumptions
Given: A natural number , the Axiom of Countable Choice, reals for , and the sets , displayed in the Statement.
Assuming countable choice, is a sigma-algebra, is a complete measure on it, every set of Lebesgue outer measure zero is Lebesgue measurable of measure zero, and for every half-open box (Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume).
Assuming countable choice, every Borel subset of is Lebesgue measurable (Assuming countable choice, every Borel subset of is Lebesgue measurable).
Assuming countable choice, is an outer measure on (Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume), so it is monotone and countably subadditive (Outer measures, Lebesgue outer measure on ).
For a nonempty box when every and every is real, and a box is nonempty exactly when for every (Half-open boxes in and their volume).
A measure on is a function with that is countably additive on pairwise disjoint sequences (Measures on sigma-algebras).
For every real there is a natural number with (For every in a complete ordered field there is a natural with ).
; if for all then , with when every ; and finite products are defined by the recursion , (Laws of finite sums and finite products, claim 6; Finite sums and finite products, by recursion).
A subset is open in if for every there is a real with ; a subset is closed if its complement is open (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).
The forms and are half-open, and an interval is open when both of its written endpoints are excluded, closed when both are included (Intervals of : the nine order-convex forms, nondegeneracy, and length).
Proof
is open and is closed in , by the same coordinatewise estimate in each case, so both are Borel and hence Lebesgue measurable.
A closed rectangle with a degenerate side is Lebesgue null: let be reals with for some , and let be a positive real; the half-open box with parameter pairs for and in coordinate is nonempty, contains , and has volume where with and otherwise, so monotonicity of the outer measure gives for every positive real and hence .
The difference is contained in the union of the closed rectangles obtained from by replacing the -th side by the degenerate side or by , each of which is Lebesgue null by step 1.2, so countable subadditivity of the outer measure, applied to that finite list padded with empty sets, gives ; every subset of is therefore Lebesgue measurable of measure .
Suppose instead for some . Then , the rectangle is Lebesgue null by step 1.2, every between them is a subset of it and so is measurable of measure , and the product has the factor and is therefore as well.
Suppose first that for every . Then is a nonempty half-open box with and . For with , both and are contained in , hence are measurable of measure by step 2.1, so is measurable, and additivity on the two disjoint decompositions and gives .
Steps 3.1 and 2.2 exhaust the two cases and give the displayed value in each, and step 1.1 supplies the Borel and measurability clauses for and .
Depends on
- Assuming countable choice, $\mathcal{L}(\mathbb{R}^n)$ is a sigma-algebra containing every elementary set and $\lambda_n$ is a complete measure extending elementary volume
- Assuming countable choice, every Borel subset of $\mathbb{R}^n$ is Lebesgue measurable
- Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume
- Outer measures
- Axis-parallel rectangles in $\mathbb{R}^m$ and their volume
- Half-open boxes in $\mathbb{R}^n$ and their volume
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Measures on sigma-algebras
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Lebesgue outer measure on $\mathbb{R}^n$
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- A C¹ diffeomorphism satisfies the change-of-variables formula for L¹ functions Corollary
- Compactly supported nonzero terminal profiles are outside the heat range Corollary
- Lebesgue measure is the Lebesgue-Stieltjes measure of the identity function Corollary
- One-dimensional W^1,p functions have unique absolutely continuous representatives Corollary
- Positive open-set and metric-ball volume Corollary
- The Nyquist no-aliasing condition Corollary
- The Solovay model has no Banach–Tarski decomposition Corollary
- The Solovay model has no Vitali or Bernstein set Corollary
- Weak differentiation has a closed graph on its natural domains Corollary
- A compactly supported L¹ function of nonzero integral is not in H¹ Counterexample
- A hypersurface jump is not W^1,p Counterexample
- A mild heat solution need not be classical at the initial time Counterexample
- A modification need not be indistinguishable Counterexample
- A nonintegrable observable with divergent ergodic averages Counterexample
- A nonmeasurable subset of a null line shows that the product of complete measures need not be complete Counterexample
- A nonzero boundary value creates a zero-extension jump Counterexample
- A normalised cube indicator is not an H¹ atom Counterexample
- A null set can fail to be the discontinuity set of any function Counterexample
- A smooth positive density with infinite mass Counterexample
- A step has no locally integrable weak derivative Counterexample
- An H¹ atom need not be smooth or continuous Counterexample
- Assuming Choice, a proper subgroup of (ℝ,+) can be nonmeasurable Counterexample
- Boundary point values are not a function of the interior Lᵖ class Counterexample
- Feller negligibility cannot be removed from the converse Counterexample
- Finite target bounds do not supply an infinite target bound Counterexample
- Finite variance is not compact support Counterexample
- Hilbert transform does not map L-infinity to L-infinity Counterexample
- Hilbert transform is not strong type (1,1) Counterexample
- Iid strong law fails at infinite absolute mean Counterexample
- Infinite variance can defeat square-root-n CLT scaling Counterexample
- Kac normalization needs ergodicity Counterexample
- Not every compact set is conformally removable Counterexample
- Point evaluation at 0 is not well defined on Lᵖ[0,1] Counterexample
- Point evaluation is unbounded below the Sobolev continuity threshold Counterexample
- Pointwise modification can destroy path continuity Counterexample
- Sharp frequency cutoffs have kernels that are not in L1 Counterexample
- Strong fractional integration fails at p equal to one Counterexample
- The critical Riesz potential can diverge and be essentially unbounded Counterexample
- The fundamental Hessian is not absolutely locally integrable Counterexample
- The indicator of a fat Cantor set is upper semicontinuous and equal almost everywhere to no Riemann integrable function Counterexample
…and 161 more results.
Dependency tree · two levels
60 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
- John K. Hunter, Measure Theory (UC Davis lecture notes), Proposition 2.7 (standard reference, not scraped)
- T. Tao, An Introduction to Measure Theory (GSM 126), Section 1.2 (standard reference, not scraped)