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.

Ball-mean oscillation bound by the Riesz potential of the gradient

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $n \geq 2$ , let $1 \leq p < \infty$ , let $B (x, r) \subseteq R^{n}$ be a ball, and let $u \in W^{1, p} (B (x, r); K)$ with ball average $u_{B (x, r)}$ . Then $∣ u (z) - u_{B (x, r)} ∣ \leq C (n) \int_{B (x, r)} ∣ D u (y) ∣ ∣ z - y ∣^{1 - n} d y$ for almost every $z \in B (x, r)$ ; here $∣ D u ∣$ is the Euclidean norm of the weak gradient and $C (n)$ depends only on $n$ .

Facts & Assumptions

Given: Countable Choice; $n \geq 2$ ; $x \in R^{n}$ and $r > 0$ ; $1 \leq p < \infty$ ; a field $K \in {R, C}$ ; and a class $u \in W^{1, p} (B (x, r); K)$ .

[F1]

The polar surface measure is normalized by $σ (E) = n λ_{n} ({t ω : ω \in E, 0 < t \leq 1})$ on Borel $E \subseteq S^{n - 1}$ , and for nonnegative Borel $h$ one has $\int_{R^{n}} h d λ_{n} = \int_{0}^{\infty} \int_{S^{n - 1}} h (t ω) t^{n - 1} d σ (ω) d t$ (The polar surface set function on the unit sphere, Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[F2]

For every ball $λ_{n} (B (z, ρ)) = σ (S^{n - 1}) ρ^{n} / n$ , and this is positive and finite (Sphere and ball measures scale in Rn).

[F3]

If a curve is composed from differentiable maps then the chain rule computes its derivative, and a differentiable curve with integrable derivative satisfies the fundamental theorem of calculus (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz).

[F4]

On completed sigma-finite products nonnegative measurable functions may be integrated in either order (Tonelli-Fubini), and an invertible linear map scales Lebesgue measure by $∣ \det ∣$ (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability, A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not).

[F5]

Truncated Riesz kernel bound: for measurable $Ω \subseteq B (z_{0}, ρ)$ and $f \in L^{p} (Ω; K)$ , $∥ \int_{Ω} ∣ x - y ∣^{1 - n} ∣ f (y) ∣ d y ∥_{L^{p} (Ω)} \leq C (n) ρ ∥ f ∥_{L^{p} (Ω)}$ (The truncated Riesz kernel is bounded on $L^{p}$ of a bounded set).

[F6]

Interior mollifications converge to $u$ in $W^{1, p} (U)$ on every $U ⋐ B (x, r)$ (Local smooth approximation in integer-order Sobolev spaces). Norm convergence has an almost-everywhere convergent subsequence (Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$ , Complex Lp completeness and almost-everywhere subsequences). Dominated convergence applies to integrable majorants (Dominated convergence).

[F7]

The ball average $u_{B} = ∣ B ∣^{- 1} \int_{B} u$ is the normalized integral of the class, and $W^{1, p}$ consists of the $L^{p}$ classes with weak gradient in $L^{p}$ (The average of a locally integrable function over a Euclidean ball, Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions).

[F8]

On a finite measure space $L^{p}$ includes into $L^{1}$ , so $u_{i} \to u$ in $L^{p}$ implies $(u_{i})_{B} \to u_{B}$ (Finite-measure $L^{r}$ includes into $L^{p}$ for $p < r$ ).

[F9]

The Axiom of Countable Choice is available and is used through the cited measure-theoretic and approximation interfaces (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1F1F3F4givenalgebra

Spherical oscillation bound for a smooth function. Let $v \in C^{\infty} (R^{n}; K)$ , $B : = B (x, r)$ , and fix $z \in B$ and $ρ > 0$ . For $y \in B$ the chain rule and the fundamental theorem [F3] applied to $t \mapsto v (t y + (1 - t) z)$ give $v (y) - v (z) = \int_{0}^{1} D v (t y + (1 - t) z) \cdot (y - z) d t$ , hence $∣ v (y) - v (z) ∣ \leq ∣ y - z ∣ \int_{0}^{1} ∣ D v (t y + (1 - t) z) ∣ d t$ . Writing $S_{ρ} : = \partial B (z, ρ)$ for the sphere equipped with its surface measure, and using that the homothety $y \mapsto t y + (1 - t) z$ maps $S_{ρ}$ onto $S_{t ρ}$ with surface element scaled by $t^{n - 1}$ ; its image of $B \cap S_{ρ}$ is contained in $B \cap S_{t ρ}$ by convexity, so enlargement gives the inequality below (the surface measures are the polar measures of cones, so this is the linear change-of-variables property of [F1] and [F4]), $\int_{B \cap S_{ρ}} ∣ v (y) - v (z) ∣ d S (y) \leq ρ \int_{0}^{1} \int_{B \cap S_{ρ}} ∣ D v (t y + (1 - t) z) ∣ d S (y) d t \leq ρ \int_{0}^{1} t^{1 - n} \int_{B \cap S_{t ρ}} ∣ D v (w) ∣ d S (w) d t$ . Since $∣ w - z ∣ = t ρ$ on $S_{t ρ}$ , the inner integral equals $ρ^{n - 1} t^{n - 1} \int_{B \cap S_{t ρ}} ∣ D v (w) ∣ ∣ z - w ∣^{1 - n} d S (w)$ ; substituting $s = t ρ$ , so that $d t = d s / ρ$ , the last display becomes $ρ^{n - 1} \int_{0}^{ρ} \int_{B \cap S_{s}} ∣ D v (w) ∣ ∣ z - w ∣^{1 - n} d S (w) d s = ρ^{n - 1} \int_{B \cap B (z, ρ)} ∣ D v (w) ∣ ∣ z - w ∣^{1 - n} d w$ , the final equality being the polar-coordinate formula [F1] for the nonnegative function $w \mapsto ∣ D v (w) ∣ ∣ z - w ∣^{1 - n}$ on $B \cap B (z, ρ)$ (whose singularity at $w = z$ is integrable; a single point is null).

2.1F1F2F7step 1.1algebra

The oscillation bound for a smooth function. Let $v \in C^{\infty} (R^{n}; K)$ and keep $B = B (x, r)$ . Since $u_{B}$ is the normalized integral, $∣ v (z) - v_{B} ∣ = ∣ B ∣^{- 1} ∣ \int_{B} (v (z) - v (y)) d y ∣$ ; writing the integral over $B$ in polar coordinates around $z$ and using $B \subseteq B (z, 2 r)$ , step 1.1 gives $∣ v (z) - v_{B} ∣ \leq ∣ B ∣^{- 1} \int_{0}^{2 r} \int_{B \cap S_{ρ}} ∣ v (y) - v (z) ∣ d S (y) d ρ \leq ∣ B ∣^{- 1} \int_{0}^{2 r} ρ^{n - 1} d ρ \int_{B} ∣ D v (y) ∣ ∣ z - y ∣^{1 - n} d y$ for every $z \in B$ . By [F2], $∣ B ∣ = σ (S^{n - 1}) r^{n} / n$ and $\int_{0}^{2 r} ρ^{n - 1} d ρ = (2 r)^{n} / n$ , so $∣ B ∣^{- 1} \int_{0}^{2 r} ρ^{n - 1} d ρ = 2^{n} / σ (S^{n - 1}) = : c (n)$ ; hence $∣ v (z) - v_{B} ∣ \leq c (n) \int_{B} ∣ D v (y) ∣ ∣ z - y ∣^{1 - n} d y$ for every $z \in B$ .

3.1F5F6F8F9step 2.1algebra

First pass to the Sobolev class on an inner ball $B_{j} : = B (x, r (1 - 1 / j))$ , $j \geq 2$ . Its closure lies in $B$ , so [F6] supplies smooth mollifications $u_{i} \to u$ in $W^{1, p} (B_{j})$ . By [F8] their $B_{j}$ means converge. Apply step 2.1 on $B_{j}$ . The potential operator on $B_{j}$ satisfies [F5], and $∣ \int_{B_{j}} ∣ D u_{i} (y) ∣ ∣ z - y ∣^{1 - n} d y - \int_{B_{j}} ∣ D u (y) ∣ ∣ z - y ∣^{1 - n} d y ∣ \leq \int_{B_{j}} ∣ D u_{i} - D u ∣ (y) ∣ z - y ∣^{1 - n} d y$ tends to zero in $L^{p} (B_{j})$ by [F5]. Successive almost-everywhere subsequences from [F6] for $u_{i}$ and these potentials therefore give $∣ u (z) - u_{B_{j}} ∣ \leq c (n) \int_{B_{j}} ∣ D u (y) ∣ ∣ z - y ∣^{1 - n} d y$ for almost every $z \in B_{j}$ .

4.1F6F8step 3.1algebra∎

Take the union of the countably many exceptional null sets from step 3.1. For $z$ outside this union, $z \in B_{j}$ for every sufficiently large $j$ , and each right side is at most $c (n) \int_{B} ∣ D u (y) ∣ ∣ z - y ∣^{1 - n} d y$ . Since $u \in L^{1} (B)$ , dominated convergence [F6] gives $u_{B_{j}} \to u_{B}$ . Letting $j \to \infty$ proves the asserted inequality on $B$ , without any approximation claim at its boundary.

Source notes

The computation is Kinnunen's Lemma 5.22, printed pp. 133-135: the spherical change of variables $w = t y + (1 - t) z$ , the radius substitution $s = t ρ$ and the final polar-coordinate identity are reproduced with their justification, and the explicit constant $2^{n} / σ (S^{n - 1})$ is recorded. Kinnunen states the lemma for $C^{1} (R^{n})$ functions and then passes to $W_{l o c}^{1, p}$ by mollification and the $L^{p}$ bound for the Riesz potential of the gradient; the passage above uses the library's interior mollification and its truncated-kernel bound, which already carries the John-domain rescaling used later on the companion page.

Depends on

Used by

Morrey's inequality for p>n Theorem
The mean-zero Poincare inequality on bounded John domains Theorem

Dependency tree · two levels

130 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)
John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes) (standard reference, not scraped)