LemmaStatement: Literature-sourcedProof: 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.

The level-set kernel measure estimate for the Slobodeckij kernel

Statement

Assume the Axiom of Countable Choice. Let $d \geq 1$ , $0 < θ < 1$ , $1 \leq p < \infty$ with $p θ < d$ , let $x \in R^{d}$ and let $E \subseteq R^{d}$ be Lebesgue measurable with $0 < ∣ E ∣ < \infty$ . Then $\int_{R^{d} ∖ E} ∣ x - y ∣^{- d - p θ} d y \geq c (d, p, θ) ∣ E ∣^{- p θ / d} .$ One admissible constant is $c = \frac{d}{p θ} ω^{1 + p θ / d}$ , where $ω : = ∣ B (0, 1) ∣$ denotes the Lebesgue measure of the unit ball.

Facts & Assumptions

Given: the Axiom of Countable Choice, $d \geq 1$ , $0 < θ < 1$ , $1 \leq p < \infty$ with $p θ < d$ , a point $x \in R^{d}$ , and a Lebesgue measurable set $E \subseteq R^{d}$ with $0 < ∣ E ∣ < \infty$ . Write $ω : = ∣ B (0, 1) ∣$ for the unit-ball measure and $ρ : = (∣ E ∣ / ω)^{1 / d} > 0$ .

[F1]

The unit ball has positive finite measure. $0 < ω < \infty$ . (Euclidean balls have positive finite Lebesgue measure, Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ )

[F2]

$C^{1}$ change of variables for nonnegative Borel functions. If $U, V \subseteq R^{m}$ are open and $T : U \to V$ is a $C^{1}$ diffeomorphism, then every nonnegative Borel $h : V \to [0, \infty]$ satisfies $\int_{V} h (y) d y = \int_{U} h (T (w)) ∣ \det D T (w) ∣ d w$ , with $0 \cdot \infty = 0$ allowed. (Borel change of variables from the compact-support formula and Radon uniqueness)

[F3]

Polar coordinates. For every nonnegative Borel $f : R^{d} \to [0, \infty]$ , $\int_{R^{d}} f (z) d z = \int_{0}^{\infty} \int_{S^{d - 1}} f (r ζ) r^{d - 1} d σ (ζ) d r$ , where $σ$ is the finite Borel surface measure on the unit sphere. (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, The polar surface set function on the unit sphere)

[F4]

Measures of set differences. If $A \subseteq B$ are measurable with $∣ A ∣ < \infty$ , then $∣ B ∣ = ∣ A ∣ + ∣ B ∖ A ∣$ . (Measure of a set difference when the smaller set has finite measure)

[F5]

Additivity and monotonicity of the nonnegative integral. For measurable $g, h : X \to [0, \infty]$ : $\int (g + h) = \int g + \int h$ , and $g \leq h$ implies $\int g \leq \int h$ ; moreover $\int c g = c \int g$ for real $c > 0$ ; for $c = 0$ the zero function has integral $0$ . (Additivity of the nonnegative Lebesgue integral, Monotonicity and nonnegative homogeneity of the nonnegative integral)

Proof

technique · Choose the radius $\rho$ carrying the mass of $E$, split the complement of $E$ into its part inside and outside $B(x,\rho)$, use the lower bound $|x-y|\ge\rho$ on the outer part and on $E\setminus B(x,\rho)$ to reach all of $B(x,\rho)^c$, and evaluate the resulting radial integral in polar coordinates

1.1F1F2F4given

The map $T (w) = x + ρ w$ is a $C^{1}$ diffeomorphism of $R^{d}$ with $\det D T = ρ^{d}$ , so [F2] applied to the indicator of $B (x, ρ)$ gives $∣ B (x, ρ) ∣ = \int 1_{B (x, ρ)} (y) d y = ρ^{d} \int 1_{B (0, 1)} (w) d w = ρ^{d} ω = ∣ E ∣$ . Since $E \cap B (x, ρ) \subseteq B (x, ρ)$ and $E \cap B (x, ρ) \subseteq E$ are measurable with $∣ E \cap B (x, ρ) ∣ \leq ∣ E ∣ < \infty$ , [F4] gives $∣ (R^{d} ∖ E) \cap B (x, ρ) ∣ = ∣ B (x, ρ) ∣ - ∣ E \cap B (x, ρ) ∣ = ∣ E ∣ - ∣ E \cap B (x, ρ) ∣ = ∣ E ∖ B (x, ρ) ∣$ .

2.1F5step 1.1

Write $C_{1} : = (R^{d} ∖ E) \cap B (x, ρ)$ and $C_{2} : = (R^{d} ∖ E) \cap B (x, ρ)^{c}$ ; these are disjoint measurable sets with union $R^{d} ∖ E$ . On $C_{1}$ one has $∣ x - y ∣^{- d - p θ} \geq ρ^{- d - p θ}$ , on $C_{2}$ and on $E ∖ B (x, ρ)$ one has $∣ x - y ∣ \geq ρ$ ; hence [F5] gives $\int_{R^{d} ∖ E} ∣ x - y ∣^{- d - p θ} d y = \int_{C_{1}} + \int_{C_{2}} \geq ρ^{- d - p θ} ∣ C_{1} ∣ + \int_{C_{2}} ∣ x - y ∣^{- d - p θ} d y = ρ^{- d - p θ} ∣ E ∖ B (x, ρ) ∣ + \int_{C_{2}} ∣ x - y ∣^{- d - p θ} d y \geq \int_{E ∖ B (x, ρ)} ∣ x - y ∣^{- d - p θ} d y + \int_{C_{2}} ∣ x - y ∣^{- d - p θ} d y = \int_{B (x, ρ)^{c}} ∣ x - y ∣^{- d - p θ} d y$ , where the last equality uses that $E ∖ B (x, ρ)$ and $C_{2}$ partition $B (x, ρ)^{c}$ .

3.1F1F2F3step 2.1∎

Substituting $y = x + w$ by [F2] and evaluating the radial integrand by [F3], $\int_{B (x, ρ)^{c}} ∣ x - y ∣^{- d - p θ} d y = \int_{∣ w ∣ > ρ} ∣ w ∣^{- d - p θ} d w = σ (S^{d - 1}) \int_{ρ}^{\infty} r^{- 1 - p θ} d r = \frac{σ (S^{d - 1})}{p θ} ρ^{- p θ}$ . Applying [F3] to the indicator of $B (0, 1)$ gives $ω = \int_{S^{d - 1}} ⁣ ⁣ \int_{0}^{1} r^{d - 1} d r d σ = σ (S^{d - 1}) / d$ , so $σ (S^{d - 1}) = d ω$ and the lower bound is $\frac{d ω}{p θ} (∣ E ∣ / ω)^{- p θ / d} = c ∣ E ∣^{- p θ / d}$ with $c = \frac{d}{p θ} ω^{1 + p θ / d} > 0$ by [F1]; combined with step 2.1 this is the assertion.

Depends on

Used by

The Slobodeckij seminorm bounds the dyadic level-set sum Lemma

Dependency tree · two levels

76 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

Eleonora Di Nezza, Giampiero Palatucci and Enrico Valdinoci, Hitchhiker's guide to the fractional Sobolev spaces (arXiv:1104.4345, survey) (standard reference, not scraped)