LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 measurable set of positive finite measure occupies more than any prescribed proportion of some dyadic cube

Statement

Let $n \geq 1$ , assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), let $E \subseteq R^{n}$ be Lebesgue measurable with $0 < λ_{n} (E) < + \infty$ , and let $θ$ be a real with $0 < θ < 1$ . Then there is a dyadic cube $Q$ (Dyadic cubes of generation $k$ in $R^{n}$ ) with

$λ_{n} (E \cap Q) > θ λ_{n} (Q) .$

Both hypotheses on $λ_{n} (E)$ are used: positivity is what makes the strict inequality available, and finiteness is what makes the division by $θ$ legitimate.

Facts & Assumptions

Given: A natural number $n \geq 1$ , the Axiom of Countable Choice, a Lebesgue measurable set $E$ with $0 < λ_{n} (E) < + \infty$ , and a real $θ$ with $0 < θ < 1$ .

[L1]

Assuming countable choice, $λ_{n}^{*} (E) = \inf {λ_{n} (U) : U$ open and $E \subseteq U}$ (Assuming countable choice, the Lebesgue outer measure of an arbitrary subset of $R^{n}$ is the infimum of the measures of the open sets containing it).

[L2]

Every open $U \subseteq R^{n}$ is the union of an at most countable family of pairwise disjoint dyadic cubes (Every open subset of $R^{n}$ is the union of a countable pairwise disjoint family of dyadic cubes).

[L3]

Assuming countable choice, $L (R^{n})$ is a sigma-algebra and $λ_{n}$ is a complete measure on it and is the restriction of $λ_{n}^{*}$ (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume); every Borel set, in particular every open set and every dyadic cube, is Lebesgue measurable (Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[F1]

A measure is countably additive on pairwise disjoint measurable sequences (Measures on sigma-algebras) and monotone (Measures are monotone).

[F2]

The nonnegative extended sum of a sequence in $[0, + \infty]$ is $\sum_{k = 0}^{\infty} a_{k} : = \sup_{n \in N} s_{n}$ , the supremum of its nondecreasing partial sums (Series in the nonnegative extended real line), and an at most countable family may be presented as a sequence (Finite, countably infinite, countable, uncountable).

[F3]

For $a, b \in \overline{R}$ the product $a b$ is $+ \infty$ when one factor is $\pm \infty$ and the other is a nonzero real of the same sign; multiplication by a strictly positive real is therefore an order isomorphism of $[0, + \infty]$ (The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $λ_{n} (E \cap Q) \leq θ λ_{n} (Q)$ for every dyadic cube $Q$ .

assume-contra

1.2

Since $0 < θ < 1$ and $λ_{n} (E)$ is a strictly positive real, $λ_{n} (E) / θ$ is a real strictly above $λ_{n} (E) = λ_{n}^{*} (E)$ , so outer regularity supplies an open $U \supseteq E$ with $λ_{n} (U) < λ_{n} (E) / θ$ .

L1L3F3

2.1

Write $U$ as the union of an at most countable pairwise disjoint family of dyadic cubes; the family is nonempty because $E$ is, and presenting it as a sequence $(Q_{j})$ when it is infinite, or using finite additivity when it is finite, countable additivity gives $λ_{n} (U) = \sum_{j} λ_{n} (Q_{j})$ and, since $E \subseteq U$ and the cubes are disjoint, also $λ_{n} (E) = λ_{n} (E \cap U) = \sum_{j} λ_{n} (E \cap Q_{j})$ .

step 1.2L2L3F1F2

3.1

Applying the assumption of step 1.1 termwise and scaling the sum by the strictly positive real $θ$ gives $λ_{n} (E) = \sum_{j} λ_{n} (E \cap Q_{j}) \leq θ \sum_{j} λ_{n} (Q_{j}) = θ λ_{n} (U) < θ \cdot λ_{n} (E) / θ = λ_{n} (E)$ , which is impossible; so some dyadic cube satisfies the displayed strict inequality.

step 1.1step 1.2step 2.1F2F3discharge-contradiction∎

Depends on

Used by

If a Lebesgue measurable subset of ℝⁿ has positive measure, its difference set contains an open ball about the origin Theorem

Dependency tree · two levels

72 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

T. Tao, An Introduction to Measure Theory (GSM 126), Exercise 1.6.25 (standard reference, not scraped)