LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Whitney-type ball cover with disjoint small balls and bounded overlap

Statement

Assume Countable Choice. Let $n \geq 1$ and let $Ω \subseteq R^{n}$ be nonempty, open and proper. Put $ρ (x) = dist (x, R^{n} ∖ Ω)$ for $x \in R^{n}$ . Then there is a countable family of points $ξ_{j} \in Ω$ , $j \in N$ , with $ρ_{j} : = ρ (ξ_{j})$ , such that

$Ω = ⋃_{j} B (ξ_{j}, ρ_{j} / 2)$ ;
the balls $B (ξ_{j}, ρ_{j} / 8)$ are pairwise disjoint (the source's maximal-selection construction records $ρ_{j} / 5$ , which the present choice-free greedy selection replaces by the fixed larger constant $8$ ; only the existence of a fixed constant matters below);
if $B (ξ_{j}, 3 ρ_{j} / 4) \cap B (ξ_{ν}, 3 ρ_{ν} / 4) \neq \emptyset$ , then $\frac{1}{7} ρ_{j} \leq ρ_{ν} \leq 7 ρ_{j}$ ;
for every $j$ at most $K (n) : = 785^{n}$ of the balls $B (ξ_{ν}, 3 ρ_{ν} / 4)$ meet $B (ξ_{j}, 3 ρ_{j} / 4)$ .

The family is the greedy subfamily of the countable rational grid ${B (q, ρ (q)) : q \in Ω \cap Q^{n}}$ : the grid is enumerated by restriction of a fixed enumeration of $Q^{n}$ , and the point $q^{(j)}$ is selected exactly when $B (q^{(j)}, ρ (q^{(j)}) / 8)$ meets none of the balls $B (q^{(i)}, ρ (q^{(i)}) / 8)$ with $i < j$ already selected. In particular no maximality principle and no choice beyond Countable Choice is used.

Facts & Assumptions

Given: $n \geq 1$ , $Ω$ nonempty, open and proper, and the distance function $ρ$ as in the statement.

[L1]

Since $Ω$ is proper, $A = R^{n} ∖ Ω$ is nonempty, so $ρ (x) = \inf_{a \in A} ∣ x - a ∣$ is finite and $∣ ρ (x) - ρ (y) ∣ \leq ∣ x - y ∣$ by $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz. If $x \in Ω$ , openness gives $r > 0$ with $B (x, r) \subseteq Ω$ , hence $ρ (x) \geq r > 0$ ; if $x \notin Ω$ , then $x \in A$ and $ρ (x) = 0$ . Here $B (x, r) = {y : ∣ y - x ∣ < r}$ as in Open ball, closed ball and sphere in a metric space.

[L2]

$Q^{n}$ is countable and dense in $R^{n}$ , so $Q^{n}$ admits a fixed enumeration $q^{(0)}, q^{(1)}, \dots$ and every nonempty open subset of $Ω$ contains a point of $Ω \cap Q^{n}$ ( $Q$ is countably infinite, Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable).

[L3]

For every $a \in R^{n}$ and $r > 0$ , $λ (B (a, r)) = c_{n} r^{n}$ with $c_{n} = ω_{n - 1} / n > 0$ ; this follows from the centred-ball formula and translation invariance. Lebesgue measure is finitely additive on disjoint measurable sets and monotone. Hence a finite family of pairwise disjoint open balls of common radius $r > 0$ with centres in a ball of radius $R$ has at most $(2 R / r + 1)^{n}$ members: they lie in the ball of radius $R + r$ , and comparing the volume of their union with that containing ball gives the bound (Sphere and ball measures scale in Rn, Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, Measures are monotone).

Proof technique: greedy selection on the countable rational grid, then the covering, comparison and packing estimates.

Proof

technique · constructive

1.1L1L2algebraconstruct

Grid covers $Ω$ . For $x \in Ω$ and $δ = ρ (x) / 64 > 0$ , density [L2] gives $q \in Ω \cap Q^{n}$ with $∣ x - q ∣ < δ$ . Then [L1] gives $ρ (q) \geq ρ (x) - ∣ x - q ∣ > (63 / 64) ρ (x)$ , so $ρ (q) > 0$ and $∣ x - q ∣ < ρ (x) / 64 < ρ (q) / 2$ ; hence $x \in B (q, ρ (q) / 2)$ . Thus ${B (q, ρ (q) / 2) : q \in Ω \cap Q^{n}}$ covers $Ω$ .

1.2L2given

Greedy selection. Enumerate $Ω \cap Q^{n}$ as $q^{(0)}, q^{(1)}, \dots$ by restriction of the fixed enumeration of $Q^{n}$ . Define $J \subseteq N$ recursively: $j \in J$ if and only if the ball $B (q^{(j)}, ρ (q^{(j)}) / 8)$ meets none of the balls $B (q^{(i)}, ρ (q^{(i)}) / 8)$ with $i < j$ , $i \in J$ ; the decision at step $j$ depends only on finitely many previous data, so this is a deterministic recursion requiring no choice. Writing $ξ_{j} = q^{(j)}$ and $ρ_{j} = ρ (ξ_{j})$ for $j \in J$ , the selected balls $B (ξ_{j}, ρ_{j} / 8)$ are pairwise disjoint by construction.

2.1step 1.1step 1.2L1L2algebra

Covering property. Let $x \in Ω$ and let $q = q^{(j)} \in Ω \cap Q^{n}$ satisfy $∣ x - q ∣ < ρ (x) / 64$ , which exists by density [L2]. If $j \in J$ , then $∣ x - ξ_{j} ∣ = ∣ x - q ∣ < ρ (x) / 64$ and $ρ_{j} = ρ (q) > 63 ρ (x) / 64$ , so $∣ x - ξ_{j} ∣ < ρ (x) / 64 < ρ_{j} / 63 < ρ_{j} / 2$ and $x \in B (ξ_{j}, ρ_{j} / 2)$ . If $j \notin J$ , then at step $j$ the ball $B (q, ρ (q) / 8)$ met some selected ball $B (ξ_{i}, ρ_{i} / 8)$ with $i < j$ , so $∣ q - ξ_{i} ∣ < \frac{ρ (q) + ρ_{i}}{8}, hence ρ (q) \leq ρ_{i} + ∣ q - ξ_{i} ∣ < ρ_{i} + \frac{ρ (q) + ρ_{i}}{8},$ which gives $\frac{7}{8} ρ (q) < \frac{9}{8} ρ_{i}$ , that is $ρ (q) < \frac{9}{7} ρ_{i}$ . Therefore $∣ q - ξ_{i} ∣ < \frac{1}{8} (\frac{9}{7} + 1) ρ_{i} = \frac{2}{7} ρ_{i} < \frac{1}{2} ρ_{i}$ , and, since $∣ x - q ∣ < ρ (x) / 64$ while $ρ (x) \leq ρ (q) + ∣ x - q ∣ < ρ (q) + ρ (x) / 64$ gives $ρ (x) < \frac{64}{63} ρ (q) < \frac{64}{63} \cdot \frac{9}{7} ρ_{i} = \frac{64}{49} ρ_{i}$ , we obtain $∣ x - ξ_{i} ∣ \leq ∣ x - q ∣ + ∣ q - ξ_{i} ∣ < \frac{ρ (x)}{64} + \frac{2}{7} ρ_{i} < \frac{1}{49} ρ_{i} + \frac{2}{7} ρ_{i} = \frac{15}{49} ρ_{i} < \frac{1}{2} ρ_{i} .$ Hence $x \in B (ξ_{i}, ρ_{i} / 2)$ in this case as well, which proves claim 1.

2.2step 1.2L1algebra

Comparison of meeting balls. Suppose $B (ξ_{j}, 3 ρ_{j} / 4) \cap B (ξ_{ν}, 3 ρ_{ν} / 4) \neq \emptyset$ . Then $∣ ξ_{j} - ξ_{ν} ∣ < \frac{3}{4} (ρ_{j} + ρ_{ν})$ and [L1] gives $ρ_{j} \leq ρ_{ν} + ∣ ξ_{j} - ξ_{ν} ∣ < ρ_{ν} + \frac{3}{4} ρ_{j} + \frac{3}{4} ρ_{ν}$ , hence $\frac{1}{4} ρ_{j} < \frac{7}{4} ρ_{ν}$ , that is $ρ_{j} < 7 ρ_{ν}$ ; interchanging $j, ν$ gives the reverse inequality. This proves claim 3.

3.1step 1.2step 2.2L3algebra

Bounded overlap. Fix $j$ and let $N$ be the set of $ν$ with $B (ξ_{ν}, 3 ρ_{ν} / 4) \cap B (ξ_{j}, 3 ρ_{j} / 4) \neq \emptyset$ . For $ν \in N$ step 2.2 gives $ρ_{ν} \leq 7 ρ_{j}$ , and $∣ ξ_{ν} - ξ_{j} ∣ < \frac{3}{4} (ρ_{j} + ρ_{ν}) \leq 6 ρ_{j}$ . The selected balls $B (ξ_{ν}, ρ_{ν} / 8)$ are pairwise disjoint, and their radii satisfy $ρ_{ν} / 8 \geq r : = ρ_{j} / 56$ . Thus the smaller balls $B (ξ_{ν}, r)$ , $ν \in N$ , remain pairwise disjoint. Their centres lie in $B (ξ_{j}, 6 ρ_{j})$ , so each smaller ball lies in $B (ξ_{j}, 6 ρ_{j} + r) \subset B (ξ_{j}, 7 ρ_{j})$ . For any finite subfamily, finite additivity and the ball-volume formula [L3] give $# F c_{n} r^{n} \leq c_{n} (7 ρ_{j})^{n},$ so $# F \leq (7 ρ_{j} / r)^{n} = 392^{n} \leq 785^{n}$ . Hence $N$ itself has at most $785^{n}$ members. This proves claim 4.

4.1step 1.1step 1.2step 2.1step 2.2step 3.1discharge-construct∎

Conclusion. Steps 1.1 and 1.2 provide a countable greedy family with covering property 1 and pairwise disjoint $B (ξ_{j}, ρ_{j} / 8)$ ; step 2.1 proves the covering property 1, step 2.2 gives the comparison property 3; step 3.1 gives the explicit finite overlap bound of property 4. This proves the lemma.

Depends on

Used by

Level decomposition of an Hᵖ distribution produces atoms Lemma

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

Shai Dekel, Gerard Kerkyacharian, George Kyriazis, Pencho Petrushev, A New Proof of the Atomic Decomposition of Hardy Spaces, Constructive Theory of Functions (Sozopol 2016), pp. 59-73 (standard reference, not scraped)
Juha Kinnunen, Harmonic Analysis (Aalto University lecture notes) (standard reference, not scraped)