LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Bounded-overlap ball chains in a bounded John domain

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $n \geq 2$ and let $Ω \subseteq R^{n}$ be a bounded John domain with distinguished point $x_{0}$ and admissible constant $c_{J} \geq 1$ ; set $r_{0} = \frac{1}{4} dist (x_{0}, \partial Ω)$ and $B_{0} = B (x_{0}, r_{0})$ . There is a constant $M = M (n, c_{J}) \geq 1$ such that for every $x \in Ω$ there are balls $B_{i} = B (x_{i}, r_{i}) \subseteq Ω$ , $i \geq 0$ , with:

$∣ B_{i} \cup B_{i + 1} ∣ \leq M ∣ B_{i} \cap B_{i + 1} ∣$ for all $i \geq 0$ ;
$dist (x, B_{i}) \leq M r_{i}$ for all $i \geq 0$ , and $r_{i} \to 0$ , $x_{i} \to x$ as $i \to \infty$ ;
no point of $Ω$ belongs to more than $M$ of the balls $B_{i}$ .

For $x \notin B (x_{0}, 2 r_{0})$ the chain starts with $B_{0} = B (x_{0}, r_{0})$ and follows a John curve from $x_{0}$ to $x$ ; for $x \in B (x_{0}, 2 r_{0})$ it is the explicit geometric chain constructed below. The choice assumption supplies Countable Choice for the John-domain and Lebesgue-measure interfaces; selecting a curve for one fixed $x$ needs no choice axiom.

Facts & Assumptions

Given: The Axiom of Choice; $n \geq 2$ ; a bounded John domain $Ω$ with distinguished point $x_{0}$ and admissible constant $c_{J} \geq 1$ ; $r_{0} = \frac{1}{4} dist (x_{0}, \partial Ω) > 0$ ; and a point $x \in Ω$ .

[F1]

There is a path $γ : [0, 1] \to Ω$ with $γ (0) = x$ , $γ (1) = x_{0}$ and $dist (γ (t), \partial Ω) \geq c_{J}^{- 1} ∣ x - γ (t) ∣$ for every $t \in [0, 1]$ (John domains and the John constant). Evaluating at $t = 1$ gives $∣ x - x_{0} ∣ \leq c_{J} dist (x_{0}, \partial Ω) = 4 c_{J} r_{0}$ .

[F2]

For every ball $λ_{n} (B (z, ρ)) = ω_{n - 1} ρ^{n} / n$ with $0 < ω_{n - 1} = σ (S^{n - 1}) < \infty$ ; hence $λ_{n} (B (z, ρ)) / λ_{n} (B (z^{'}, ρ^{'})) = (ρ / ρ^{'})^{n}$ and every ball has positive finite measure (Sphere and ball measures scale in Rn, Euclidean balls have positive finite Lebesgue measure).

[F3]

A measure is countably additive on pairwise disjoint measurable sets and monotone under inclusion (Measures on sigma-algebras, Measures are monotone).

[F4]

The curve $γ$ is uniformly continuous on $[0, 1]$ . Indeed, for each $t$ continuity gives a radius $a_{t} > 0$ such that $∣ s - t ∣ < 2 a_{t}$ implies $∣ γ (s) - γ (t) ∣ < ε / 2$ . Compactness gives a finite subcover of the intervals $∣ s - t ∣ < a_{t}$ ; the minimum of its $a_{t}$ is positive. If two parameters are closer than this minimum, place the first in a covering interval and apply the two continuity bounds to obtain image distance $< ε$ .

Proof

technique · direct

1.1F1givenalgebra

Setup. By [F1] fix a John curve $γ$ from $x$ to $x_{0}$ ; the John inequality at $t = 1$ gives $∣ x - x_{0} ∣ \leq 4 c_{J} r_{0}$ . If $x \in B (x_{0}, 2 r_{0})$ we use the explicit geometric chain below; if $x \notin B (x_{0}, 2 r_{0})$ we use the recursive construction below along the John curve. In both cases all constants below depend only on $n$ and $c_{J}$ , and we collect them at the end into a single $M$ . Also $x \notin B (x_{0}, 2 r_{0})$ implies $∣ x - x_{0} ∣ \geq 2 r_{0} > r_{0}$ , so $x \notin B_{0}$ in that case.

1.2F2F3givenalgebra

The near case $x \in B (x_{0}, 2 r_{0})$ . Put $d : = ∣ x - x_{0} ∣ \leq 2 r_{0}$ . If $d > 0$ put $x_{i} : = x + 2^{- i} (x_{0} - x)$ and $r_{i} : = 2^{- i - 1} d$ for $i \geq 0$ ; if $d = 0$ fix the first standard basis vector $e_{1}$ and put $x_{i} : = x_{0} + 2^{- i} (r_{0} / 2) e_{1}$ , $r_{i} : = 2^{- i - 2} r_{0}$ . In both cases $r_{i + 1} = r_{i} / 2$ , $∣ x_{i} - x ∣ = 2 r_{i}$ , $∣ x_{i} - x_{i + 1} ∣ = r_{i}$ , $r_{i} \leq r_{0}$ and $∣ x_{i} - x_{0} ∣ \leq 2 r_{0}$ , so $dist (x_{i}, \partial Ω) \geq 4 r_{0} - ∣ x_{i} - x_{0} ∣ \geq 2 r_{0} > r_{i}$ and $B_{i} = B (x_{i}, r_{i}) \subseteq Ω$ . Consecutive balls: $B_{i} \cup B_{i + 1} \subseteq B (x_{i}, \frac{3}{2} r_{i})$ , because a point of $B_{i + 1}$ is within $∣ x_{i} - x_{i + 1} ∣ + r_{i + 1} = r_{i} + r_{i} / 2$ of $x_{i}$ , while the ball of radius $r_{i} / 4$ centred at the point of the segment from $x_{i}$ to $x_{i + 1}$ at distance $3 r_{i} / 4$ from $x_{i}$ lies in $B_{i} \cap B_{i + 1}$ (its centre is at distance $3 r_{i} / 4 < r_{i}$ from $x_{i}$ and at distance $r_{i} / 4 < r_{i + 1} = r_{i} / 2$ from $x_{i + 1}$ ); hence $∣ B_{i} \cup B_{i + 1} ∣ \leq 6^{n} ∣ B_{i} \cap B_{i + 1} ∣$ by [F2] and [F3]. Also $dist (x, B_{i}) \leq ∣ x - x_{i} ∣ = 2 r_{i}$ , and $r_{i} \to 0$ , $x_{i} \to x$ . Finally, if $y \in B_{i}$ then $r_{i} \leq ∣ x - y ∣ \leq 3 r_{i}$ ; the radii halve at each step, so the interval $[∣ x - y ∣ / 3, ∣ x - y ∣]$ of ratio $3$ contains at most two of the numbers $r_{i}$ , and $y$ therefore belongs to at most two of the balls $B_{i}$ . Hence (1), (2) and (3) hold in the near case, with ratio $6^{n}$ and multiplicity $2$ .

1.3F1givenalgebra

The far case: the recursive construction and comparability. Assume now $x \notin B (x_{0}, 2 r_{0})$ , so $x \notin B_{0}$ and $∣ x - x_{0} ∣ \geq 2 r_{0}$ . We construct $B_{i} = B (x_{i}, r_{i})$ recursively, starting with $x_{0}$ , $B_{0} = B (x_{0}, r_{0})$ . Suppose $B_{i}$ with centre $x_{i} = γ (t_{i})$ has been constructed, $B_{i} \subseteq Ω$ , and $x \notin B_{i}$ . Put $T_{i} : = {t \in [0, t_{i}] : γ (t) \in B_{i}}$ , a nonempty set containing a relative neighbourhood of $t_{i}$ in $[0, t_{i}]$ , and define $t_{i + 1} : = \inf T_{i}$ , $x_{i + 1} : = γ (t_{i + 1})$ , $r_{i + 1} : = \frac{1}{4 c_{J}} ∣ x - x_{i + 1} ∣$ and $B_{i + 1} : = B (x_{i + 1}, r_{i + 1})$ . Then $t_{i + 1} < t_{i}$ . For every $t < t_{i + 1}$ one has $γ (t) \notin B_{i}$ , while points of $T_{i}$ arbitrarily close to $t_{i + 1}$ lie in $B_{i}$ ; by continuity $x_{i + 1} \in \partial B_{i}$ , so $∣ x_{i} - x_{i + 1} ∣ = r_{i}$ , and $x_{i + 1} \neq x$ . The John inequality [F1] at $x_{i + 1}$ gives $dist (x_{i + 1}, \partial Ω) \geq c_{J}^{- 1} ∣ x - x_{i + 1} ∣ = 4 r_{i + 1} > r_{i + 1}$ , so $B_{i + 1} \subseteq Ω$ ; and $x \notin B_{i + 1}$ because $∣ x - x_{i + 1} ∣ = 4 c_{J} r_{i + 1} > r_{i + 1}$ as $c_{J} \geq 1$ . For the first transition, $∣ x_{0} - x_{1} ∣ = r_{0}$ and $∣ x - x_{0} ∣ \geq 2 r_{0}$ , so $∣ x - x_{1} ∣ \geq ∣ x - x_{0} ∣ - r_{0} \geq r_{0}$ ; also [F1] gives $∣ x - x_{0} ∣ \leq 4 c_{J} r_{0}$ , hence $∣ x - x_{1} ∣ \leq (4 c_{J} + 1) r_{0}$ . Since $r_{1} = ∣ x - x_{1} ∣ / (4 c_{J})$ , this yields $r_{0} / (4 c_{J}) \leq r_{1} \leq (1 + 1 / (4 c_{J})) r_{0}$ . For every $i \geq 1$ , the defining identity $∣ x - x_{i} ∣ = 4 c_{J} r_{i}$ and $∣ x_{i} - x_{i + 1} ∣ = r_{i}$ give $(1 - 1 / (4 c_{J})) r_{i} \leq r_{i + 1} \leq (1 + 1 / (4 c_{J})) r_{i}$ . Thus consecutive radii are comparable with ratio at most $5 / 4$ from the second transition onward, and $∣ x_{i} - x_{i + 1} ∣ = r_{i}$ is comparable to both radii for $i \geq 1$ .

2.1F1F4step 1.3givenalgebra

The far case: limit properties. The times $t_{i}$ are strictly decreasing in $[0, 1]$ , so the intervals $[t_{i + 1}, t_{i}]$ are pairwise disjoint and $\sum_{i} (t_{i} - t_{i + 1}) \leq 1$ . If $r_{i} \geq ε > 0$ for an index $i$ , then $∣ x_{i} - x_{i + 1} ∣ = r_{i} \geq ε$ , and uniform continuity [F4] of $γ$ on $[0, 1]$ gives $t_{i} - t_{i + 1} \geq δ (ε) > 0$ ; since the intervals are disjoint, only finitely many indices satisfy $r_{i} \geq ε$ . Hence $r_{i} \to 0$ ; and since $∣ x - x_{i} ∣ = 4 c_{J} r_{i}$ for every $i \geq 1$ , also $x_{i} \to x$ . Consequently $dist (x, B_{i}) \leq ∣ x - x_{i} ∣ = 4 c_{J} r_{i}$ for $i \geq 1$ , while for $i = 0$ we have $dist (x, B_{0}) \leq ∣ x - x_{0} ∣ - r_{0} \leq 4 c_{J} r_{0}$ . This gives (2) in the far case.

3.1F2F3step 1.3step 2.1algebra

The far case: multiplicity. Suppose $y$ belongs to $B_{i_{1}} \cap \dots \cap B_{i_{k}}$ with $i_{1} < \dots < i_{k}$ . Since $y \in B_{i_{j}}$ and $∣ x - x_{i_{j}} ∣ = 4 c_{J} r_{i_{j}}$ for $i_{j} \geq 1$ (while for $i_{j} = 0$ one has $∣ x - x_{0} ∣ \leq 4 c_{J} r_{0}$ and $∣ x - y ∣ \geq ∣ x - x_{0} ∣ - r_{0} \geq r_{0}$ ), the triangle inequality gives $c_{1} r_{i_{j}} \leq ∣ x - y ∣ \leq c_{2} r_{i_{j}}$ for constants $c_{1}, c_{2}$ depending only on $c_{J}$ : the upper bound is $∣ x - y ∣ \leq (4 c_{J} + 1) r_{i_{j}}$ , and the lower bound is $∣ x - y ∣ \geq (4 c_{J} - 1) r_{i_{j}}$ for $i_{j} \geq 1$ , while for $i_{j} = 0$ one has $r_{0} \leq ∣ x - y ∣ \leq (4 c_{J} + 1) r_{0}$ , so $r_{0} \geq ∣ x - y ∣ / (4 c_{J} + 1)$ and $∣ x - y ∣ \geq r_{0} / (4 c_{J} + 1) \cdot 1$ , which is the same shape with adjusted constants. Hence all the radii $r_{i_{j}}$ are comparable to $∣ x - y ∣$ . For $j < m$ one has $x_{i_{m}} \notin B_{i_{j}}$ , because $t_{i_{m}} \leq t_{i_{j} + 1}$ and $γ (t) \notin B_{i_{j}}$ for every $t < t_{i_{j} + 1}$ by step 1.3; hence $∣ x_{i_{j}} - x_{i_{m}} ∣ \geq r_{i_{j}}$ , while $∣ x_{i_{j}} - x_{i_{m}} ∣ \leq ∣ x_{i_{j}} - x ∣ + ∣ x - x_{i_{m}} ∣ \leq 4 c_{J} (r_{i_{j}} + r_{i_{m}})$ . So the $k$ centres have pairwise distances between $c_{1}^{'} ∣ x - y ∣$ and $c_{2}^{'} ∣ x - y ∣$ with constants depending only on $c_{J}$ . If $y = x$ this is impossible, because $∣ x - x_{i} ∣ = 4 c_{J} r_{i} > r_{i}$ for $i \geq 1$ and $∣ x - x_{0} ∣ \geq 2 r_{0} > r_{0}$ for $i = 0$ , so $x$ lies in no $B_{i}$ . The balls $B (x_{i_{j}}, c_{1}^{'} ∣ x - y ∣ / 3)$ are pairwise disjoint and all lie in $B (x_{i_{1}}, (c_{2}^{'} + c_{1}^{'} / 3) ∣ x - y ∣)$ , so by [F2] and [F3], $k (c_{1}^{'} / 3)^{n} \leq (c_{2}^{'} + c_{1}^{'} / 3)^{n}$ , an explicit bound $N (n, c_{J})$ .

4.1step 1.2step 1.3step 2.1step 3.1givenalgebra∎

Assembly. In the near case step 1.2 gives (1), (2) and (3) with constants depending only on $n$ : ratio at most $6^{n}$ , $dist (x, B_{i}) \leq 2 r_{i}$ , $r_{i} \to 0$ , $x_{i} \to x$ , and multiplicity $2$ . In the far case, the first pair has a separate overlap bound: the ball from step 1.3 of radius $r_{1} / 2 \geq r_{0} / (8 c_{J})$ , centred halfway from $x_{1}$ toward $x_{0}$ by $r_{1} / 2$ , lies in $B_{0} \cap B_{1}$ , while $B_{0} \cup B_{1} \subseteq B (x_{0}, r_{0} + r_{1})$ and $r_{1} \leq (1 + 1 / (4 c_{J})) r_{0}$ , so $∣ B_{0} \cup B_{1} ∣ \leq (16 c_{J} + 2)^{n} ∣ B_{0} \cap B_{1} ∣$ . For $i \geq 1$ , step 1.3 gives $r_{i + 1} \geq (3 / 4) r_{i}$ and centre separation $r_{i}$ ; the midpoint ball of radius $r_{i} / 4$ lies in $B_{i} \cap B_{i + 1}$ , while the union is contained in $B (x_{i}, 3 r_{i})$ , giving ratio at most $12^{n}$ . Step 2.1 gives $dist (x, B_{i}) \leq 4 c_{J} r_{i}$ , $r_{i} \to 0$ and $x_{i} \to x$ ; and step 3.1 gives multiplicity at most $N (n, c_{J})$ . Taking $M \geq \max (6^{n}, (16 c_{J} + 2)^{n}, 12^{n}, 4 c_{J}, N (n, c_{J}), 2, 1)$ completes the proof. A John curve was selected once, for the given $x$ , in step 1.1.

Source notes

The construction and properties are Kinnunen's, printed pp. 141-142: the radius $r_{i + 1} = ∣ x - x_{i + 1} ∣ / (4 c_{J})$ at the last exit point of the ball, the comparability of consecutive radii and centre distances, the packing bound on centres with pairwise comparable distances, and the terminal convergence $r_{i} \to 0$ , $x_{i} \to x$ . Kinnunen leaves the case $x \in B (x_{0}, 2 r_{0})$ as an exercise; the explicit overlapping geometric chain of step 1.2 supplies it. The roles of the constants are kept separate: the John inequality is used only to put every ball inside $Ω$ and to bound $∣ x - x_{0} ∣$ , the packing bound uses only the comparability of the radii to $∣ x - y ∣$ , and no monotonicity of the radii is claimed.

Depends on

Used by

The mean-zero Poincare inequality on bounded John domains Theorem

Dependency tree · two levels

45 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

Juha Kinnunen, Sobolev Spaces (Aalto University, 2026, complete graduate lecture notes) (standard reference, not scraped)