TheoremStatement: 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.

Poincare inequality on a ball

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $n \geq 1$ , $B = B (x_{0}, r) \subseteq R^{n}$ with $r > 0$ , $1 \leq p < \infty$ , and $u \in W^{1, p} (B; K)$ with ball average $u_{B} = ∣ B ∣^{- 1} \int_{B} u$ . Then $∥ u - u_{B} ∥_{L^{p} (B)} \leq C (n, p) r ∥ D u ∥_{L^{p} (B)}$ .

Facts & Assumptions

Given: The Axiom of Choice; an integer $n \geq 1$ ; a ball $B = B (x_{0}, r) \subseteq R^{n}$ with $r > 0$ ; an exponent $1 \leq p < \infty$ ; a field $K \in {R, C}$ ; and a class $u \in W^{1, p} (B; K)$ .

[F1]

The convex-domain Poincare-Wirtinger estimate: for every open bounded convex nonempty $Ω$ and every $v \in W^{1, p} (Ω; K)$ , $∥ v - v_{Ω} ∥_{L^{p} (Ω)} \leq C (n) diam (Ω) ∥ D v ∥_{L^{p} (Ω)}$ with $C (n) = 2 (2^{n} - 1) / n$ , where $v_{Ω} = ∣ Ω ∣^{- 1} \int_{Ω} v$ (Poincare-Wirtinger on bounded convex domains by the direct pairwise argument).

[F2]

The ball average $u_{B} = ∣ B ∣^{- 1} \int_{B} u$ is the mean of $u$ over $B$ ; it is defined because every ball has positive finite Lebesgue measure (The average of a locally integrable function over a Euclidean ball, Euclidean balls have positive finite Lebesgue measure).

[F3]

$W^{1, p} (B; K)$ consists of the $L^{p}$ classes with weak first derivatives in $L^{p}$ , and $L^{p}$ consists of almost-everywhere classes (Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions).

Proof

technique · direct

1.1F2F3givenalgebra

The ball is admissible for [F1]. The ball $B = B (x_{0}, r)$ is open, bounded, convex and nonempty, and its diameter is $diam (B) = 2 r$ ; the class $u$ lies in $W^{1, p} (B; K)$ by hypothesis. Its mean over $B$ as a convex set is exactly the ball average $u_{B} = ∣ B ∣^{- 1} \int_{B} u$ of [F2], because both are $∣ B ∣^{- 1} \int_{B} u$ ; the value is a finite element of $K$ by [F2] and [F3].

2.1F1step 1.1algebra∎

Applying the convex-domain estimate. By [F1] applied to $Ω = B$ and $v = u$ , $∥ u - u_{B} ∥_{L^{p} (B)} \leq C (n) diam (B) ∥ D u ∥_{L^{p} (B)} = 2 C (n) r ∥ D u ∥_{L^{p} (B)}$ . Hence the asserted inequality holds with the dimension-and-exponent constant $C (n, p) : = 2 C (n) = 4 (2^{n} - 1) / n$ , which depends only on $n$ and $p$ .

Source notes

Kinnunen proves the ball case by the pointwise potential estimate and the maximal-function bound; Laugesen records it as an exercise with a constant linear in $r$ . The proof above derives the ball statement from the more general convex-domain Poincare-Wirtinger corollary proved earlier on this page, with the explicit constant $4 (2^{n} - 1) / n$ , which is not sharp but is dimension-only and linear in $r$ as asserted.

Depends on

Used by

Dependency tree · two levels

35 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)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, complete 158-page graduate notes) (standard reference, not scraped)