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

Poincare-Wirtinger on bounded connected extension domains by Rellich compactness

Statement

Assume the Axiom of Choice. Let $n \geq 1$ , let $Ω \subseteq R^{n}$ be a nonempty bounded connected extension domain, and let $1 \leq p < \infty$ . Then there is $C = C (Ω, p)$ such that every $u \in W^{1, p} (Ω; K)$ satisfies $∥ u - u_{Ω} ∥_{L^{p} (Ω)} \leq C ∥ D u ∥_{L^{p} (Ω)}, u_{Ω} : = ∣ Ω ∣^{- 1} \int_{Ω} u (x) d x .$

Facts & Assumptions

Given: the Axiom of Choice, a nonempty bounded connected extension domain $Ω \subseteq R^{n}$ of finite positive measure, $1 \leq p < \infty$ , and the mean $u_{Ω}$ of $u$ . Nonempty openness supplies a ball inside $Ω$ , and boundedness supplies a containing ball; thus $0 < ∣ Ω ∣ < \infty$ by Euclidean balls have positive finite Lebesgue measure.

[F1]

Rellich compactness. Every sequence bounded in $W^{1, p} (Ω)$ has a subsequence converging in $L^{p} (Ω)$ . (Compactness of $W^{1, p} (Ω) ↪ L^{p} (Ω)$ on bounded extension domains, Sobolev extension domains and extension operators)

[F2]

The mean is continuous for the $L^{p}$ norm. $∣ u_{Ω} ∣ \leq ∣ Ω ∣^{- 1 / p} ∥ u ∥_{L^{p}}$ and hence $∣ \int_{Ω} (u_{j} - u) ∣ \leq ∣ Ω ∣^{1 - 1 / p} ∥ u_{j} - u ∥_{L^{p} (Ω)}$ , by H"older's inequality on the finite-measure set $Ω$ . (Holder's inequality for integrals, including the endpoint cases, The space $L^{p} (μ)$ as the quotient by null functions)

[F3]

Weak gradients vanish when tested against convergent subsequences. If $u_{j} \to u$ in $L^{p} (Ω)$ and $∥ D u_{j} ∥_{L^{p} (Ω)} \to 0$ , then for every $φ \in C_{c}^{\infty} (Ω)$ and every coordinate $i$ , $\int_{Ω} u \partial_{i} φ = \lim_{j} \int_{Ω} u_{j} \partial_{i} φ = - \lim_{j} \int_{Ω} D_{i} u_{j} φ = 0$ . (Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions)

[F4]

Zero gradient implies constancy on components. If $u \in W_{l o c}^{1, p} (Ω)$ and $D_{i} u = 0$ almost everywhere for all $i$ , then $u$ is almost everywhere constant on each connected component of $Ω$ . (Zero weak gradient gives componentwise constants)

Proof

technique · suppose no constant exists, normalise a violating sequence, extract a strongly convergent subsequence by Rellich, and use the vanishing gradient to force the limit to be a constant, contradicting unit norm

1.1F2givenassume-contra

Suppose the assertion fails: for every $j \geq 1$ there is $v_{j} \in W^{1, p} (Ω)$ with $∥ v_{j} - (v_{j})_{Ω} ∥_{p} > j ∥ D v_{j} ∥_{p}$ , and $v_{j}$ is not almost everywhere constant. Put $u_{j} : = (v_{j} - (v_{j})_{Ω}) / ∥ v_{j} - (v_{j})_{Ω} ∥_{p}$ ; then the mean of $u_{j}$ is $0$ , $∥ u_{j} ∥_{L^{p}} = 1$ , and $∥ D u_{j} ∥_{p} \leq 1 / j$ , so $∥ u_{j} ∥_{W^{1, p} (Ω)} \leq (1 + n / j^{p})^{1 / p} \leq (1 + n)^{1 / p}$ for all $j$ .

2.1F1F2step 1.1

By [F1] there is a subsequence $u_{j_{k}} \to u$ in $L^{p} (Ω)$ . By [F2] and step 1.1 the means pass to the limit, so $\int_{Ω} u = 0$ ; and $∥ u ∥_{L^{p}} = 1$ because $∣ ∥ u_{j_{k}} ∥_{p} - ∥ u ∥_{p} ∣ \leq ∥ u_{j_{k}} - u ∥_{p} \to 0$ .

3.1F3F4step 2.1discharge-contradiction∎

By [F3] applied to the convergent subsequence of step 2.1 with $∥ D u_{j_{k}} ∥_{p} \leq 1 / j_{k} \to 0$ , $\int_{Ω} u \partial_{i} φ = 0$ for every test function $φ$ and every $i$ , so $D_{i} u = 0$ almost everywhere and $u \in W^{1, p} (Ω)$ ; [F4] then makes $u$ an almost everywhere constant on the connected $Ω$ , and since its mean is $0$ that constant is $0$ , contradicting $∥ u ∥_{L^{p}} = 1$ from step 2.1. Hence the constant $C$ exists. Countable Choice selects the violating sequence in step 1.1; the assumed Axiom of Choice also supplies [F1] and [F4].

Depends on

Used by

Dependency tree · two levels

69 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

Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, complete graduate notes) (standard reference, not scraped)
Juha Kinnunen, Sobolev Spaces (Aalto University, complete graduate lecture notes) (standard reference, not scraped)