LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A Poincare bound on a slab-bounded domain

Statement

Let $Ω \subset R^{d}$ be open and satisfy $a < x \cdot e < b$ for a unit vector $e$ and all $x \in Ω$ , with $a < b$ . Then every $v \in H_{0}^{1} (Ω)$ satisfies $∥ v ∥_{L^{2} (Ω)} \leq (b - a) ∥ \nabla v ∥_{L^{2} (Ω)} .$ The argument assumes Countable Choice through the stated Sobolev, product-measure, and affine change-of-variables interfaces; it does not use the Axiom of Choice.

Facts & Assumptions

Given: Countable Choice, an open domain contained in the slab $a < x \cdot e < b$ , and $v \in H_{0}^{1} (Ω)$ , where $H_{0}^{1}$ is the $W^{1, 2}$ -closure of $C_{c}^{\infty} (Ω)$ .

[F1]

The vector-valued fundamental theorem of calculus applies to smooth functions on a compact interval. (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)

[F2]

Countable Choice gives Tonelli/Fubini for nonnegative integrands on the Euclidean product spaces used below. (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability, The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F3]

For an orthogonal matrix $Q$ , $Q^{T} Q = I$ and $∣ \det Q ∣ = 1$ ; the linear affine map $y \mapsto Q y$ is a $C^{1}$ diffeomorphism, so change of variables preserves integrals of nonnegative measurable functions. (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions)

[F4]

Holder's inequality with exponents $2, 2$ gives $∣ \int_{I} f g ∣ \leq ∥ f ∥_{L^{2} (I)} ∥ g ∥_{L^{2} (I)}$ and, in particular, $∣ \int_{a}^{t} g ∣^{2} \leq (t - a) \int_{a}^{t} ∣ g ∣^{2}$ . (Holder's inequality for integrals, including the endpoint cases)

Proof

1.1F1F4givenalgebra

First let $φ \in C_{c}^{\infty} (Ω)$ and extend it by zero to $R^{d}$ . Write $x = x_{⊥} + t e$ with $x_{⊥} ⊥ e$ . For fixed $x_{⊥}$ and $a < t < b$ , the fundamental theorem [F1] gives $φ (x_{⊥} + t e) = \int_{a}^{t} \partial_{e} φ (x_{⊥} + s e) d s$ , since the zero extension vanishes at $t = a$ . Holder's inequality [F4], applied on $(a, t)$ and then enlarged to $(a, b)$ , yields $∣ φ (x_{⊥} + t e) ∣^{2} \leq (b - a) \int_{a}^{b} ∣ \partial_{e} φ (x_{⊥} + s e) ∣^{2} d s$ .

2.1F2F3step 1.1algebra

Integrate step 1.1 over $t \in (a, b)$ and $x_{⊥} \in e^{⊥}$ . Choose an orthonormal basis of $e^{⊥}$ and let $Q$ have those basis vectors followed by $e$ as its columns. Then $T (y) = Q y$ sends $(y_{⊥}, t)$ to $x_{⊥} + t e$ ; Tonelli [F2] and $Q^{T} Q = I$ , $∣ \det Q ∣ = 1$ in [F3] give the coordinate integral over the slab. The zero extension of $φ$ and its derivative vanish off $Ω$ , so those slab integrals equal their integrals over $Ω$ . Thus $∥ φ ∥_{L^{2} (Ω)}^{2} \leq (b - a)^{2} ∥ \partial_{e} φ ∥_{L^{2} (Ω)}^{2} \leq (b - a)^{2} ∥ \nabla φ ∥_{L^{2} (Ω)}^{2}$ .

3.1F4givenstep 2.1algebra∎

Let $δ > 0$ . By the closure definition of $H_{0}^{1} (Ω)$ , choose a single $φ \in C_{c}^{\infty} (Ω)$ with $∥ v - φ ∥_{H^{1}} < δ$ . The $L^{2}$ triangle inequality follows by expanding $∥ f + g ∥_{2}^{2}$ and applying [F4] to the cross term; hence [F4] and step 2.1 give $∥ v ∥_{2} \leq ∥ φ ∥_{2} + δ \leq (b - a) ∥ \nabla φ ∥_{2} + δ \leq (b - a) ∥ \nabla v ∥_{2} + (b - a + 1) δ$ . This holds for every $δ > 0$ , so letting $δ ↓ 0$ proves the statement without selecting a sequence of approximants.

Depends on

Used by

Dependency tree · two levels

68 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

Jean-Luc Guermond, MATH 661 Fall 2025, Chapter 3, Traces and Poincare inequalities (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations, Chapter 3 (standard reference, not scraped)