ExampleConstruction: AI-adaptedVerification: 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 on an interval: the length dependence is linear

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $I = (0, L)$ with $L > 0$ and let $1 \leq p < \infty$ . For every $u \in W^{1, p} (I)$ with mean $u_{I} = ∣ I ∣^{- 1} \int_{I} u$ one has $∥ u - u_{I} ∥_{L^{p} (I)} \leq L ∥ u^{'} ∥_{L^{p} (I)} .$ The dependence on $L$ cannot be improved below a positive multiple of $L$ : for $u (x) = x - \frac{L}{2}$ the weak derivative is $u^{'} \equiv 1$ , the mean vanishes, and $∥ u - u_{I} ∥_{L^{p} (I)} = L^{1 + 1 / p} 2^{- 1} (p + 1)^{- 1 / p}, ∥ u^{'} ∥_{L^{p} (I)} = L^{1 / p},$ so the ratio $∥ u - u_{I} ∥_{L^{p}} / ∥ u^{'} ∥_{L^{p}}$ equals $c_{p} L$ with $c_{p} = \frac{1}{2} (p + 1)^{- 1 / p} > 0$ . Consequently every admissible constant for this family is at least $c_{p} L$ , while the inequality above shows that $L$ itself is admissible: the optimal constant is of order $L$ .

Facts & Assumptions

Given: The Axiom of Choice (used only through the cited absolutely-continuous-representative interface); reals $0 < L < \infty$ and $1 \leq p < \infty$ ; the interval $I = (0, L)$ ; and a class $u \in W^{1, p} (I; K)$ with $K \in {R, C}$ .

[F1]

Every $u \in W^{1, p} (I)$ has exactly one continuous locally absolutely continuous representative $u^{*}$ with $u^{*} (x) - u^{*} (y) = \int_{y}^{x} u^{'}$ for all $x, y \in I$ , and $u^{*} = u$ almost everywhere (One-dimensional $W^{1, p}$ functions have unique absolutely continuous representatives).

[F2]

$W^{1, p}$ consists of the $L^{p}$ classes whose weak derivative exists as an $L^{p}$ class, and equality of classes is equality almost everywhere (Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions).

[F3]

On a finite measure space $L^{r}$ includes into $L^{1}$ for $1 \leq r < \infty$ , so $u \in L^{1} (I)$ and the mean $u_{I} = ∣ I ∣^{- 1} \int_{I} u$ is a well-defined scalar (Finite-measure $L^{r}$ includes into $L^{p}$ for $p < r$ ); the interval has $∣ I ∣ = L$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[F4]

Holder's inequality gives $\int_{I} ∣ g ∣ \leq ∣ I ∣^{1 - 1 / p} ∥ g ∥_{L^{p} (I)}$ for $g \in L^{p} (I)$ and $1 < p < \infty$ , while for $p = 1$ the same display holds with $∣ I ∣^{0} = 1$ (Holder's inequality for integrals, including the endpoint cases).

[F5]

A function with $C^{k}$ real and imaginary parts has its classical partial derivatives as weak derivatives (Classical derivatives agree with weak derivatives).

[F6]

Newton-Leibniz with finitely many exceptional points: if $G$ is continuous on $[a, b]$ , differentiable off a finite set, and $f$ is Riemann integrable with $f = G^{'}$ off that set, then $\int_{a}^{b} f = G (b) - G (a)$ (Newton–Leibniz remains valid across finitely many exceptional interior points when the primitive is continuous).

[F7]

A bounded Riemann integrable function on $[a, b]$ is Lebesgue integrable there and its Lebesgue integral equals its Riemann integral (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

[F8]

For real $α$ the function $x \mapsto x^{α}$ is differentiable on $(0, \infty)$ with derivative $α x^{α - 1}$ (Continuity and derivatives of positive-base real powers).

Verification

technique · direct

1.1F1F2F3givenalgebra

By [F1] the class $u$ has a continuous representative $u^{*}$ on $I$ that is locally absolutely continuous and satisfies $u^{*} (x) - u^{*} (y) = \int_{y}^{x} u^{'}$ for all $x, y \in I$ , and $u^{*} = u$ almost everywhere. Since $u \in L^{p} (I)$ and $∣ I ∣ = L < \infty$ , [F3] gives $u \in L^{1} (I)$ , so $u_{I} = ∣ I ∣^{- 1} \int_{I} u$ is well defined and equals $L^{- 1} \int_{I} u^{*}$ by [F2]; the norms $∥ u - u_{I} ∥_{L^{p} (I)} = ∥ u^{*} - u_{I} ∥_{L^{p} (I)}$ agree because the two integrands coincide almost everywhere.

1.2F3F5F6F7F8givenalgebra

The linear function attains the scaling. Let $u (x) = x - \frac{L}{2}$ on $I$ . Its real and imaginary parts are $C^{\infty}$ , so by [F5] $u \in W^{1, p} (I)$ with weak derivative $u^{'} \equiv 1$ , and $∥ u^{'} ∥_{L^{p} (I)} = (L)^{1 / p} = L^{1 / p}$ by [F3]. The antiderivative $G (x) = \frac{x^{2}}{2} - \frac{L x}{2}$ is continuous and $G^{'} = u$ on $I$ , so [F6], [F7] and [F3] give $u_{I} = L^{- 1} (G (L) - G (0)) = L^{- 1} (L^{2} / 2 - L^{2} / 2) = 0$ . Finally $∣ u ∣^{p}$ has the continuous majorant-free antiderivative identity $\int_{0}^{L / 2} s^{p} d s = (L / 2)^{p + 1} / (p + 1)$ by [F6], [F7] and [F8] (the derivative of $s^{p + 1} / (p + 1)$ is $s^{p}$ on $(0, L / 2)$ and the endpoint values are limits), so $\int_{I} ∣ u - u_{I} ∣^{p} d x = 2 \int_{0}^{L / 2} s^{p} d s = 2 (L / 2)^{p + 1} / (p + 1) = L^{p + 1} 2^{- p} (p + 1)^{- 1}$ . Taking $p$ -th roots gives $∥ u - u_{I} ∥_{L^{p} (I)} = L^{1 + 1 / p} 2^{- 1} (p + 1)^{- 1 / p}$ .

2.1F4step 1.1algebra

Oscillation bound. For all $x, y \in I$ the representative satisfies $∣ u^{*} (x) - u^{*} (y) ∣ = ∣ \int_{y}^{x} u^{'} ∣ \leq \int_{I} ∣ u^{'} ∣$ ; by [F4], applied to $g = u^{'}$ , this is at most $L^{1 - 1 / p} ∥ u^{'} ∥_{L^{p} (I)}$ for $1 < p < \infty$ and at most $∥ u^{'} ∥_{L^{1} (I)}$ for $p = 1$ , that is, at most $L^{1 - 1 / p} ∥ u^{'} ∥_{L^{p} (I)}$ in both cases.

3.1F4step 1.1step 2.1algebra

The mean-zero bound. For every $x \in I$ the identity $u^{*} (x) - u_{I} = L^{- 1} \int_{I} (u^{*} (x) - u^{*} (y)) d y$ and [F4] with $g (y) = u^{*} (x) - u^{*} (y)$ give $∣ u^{*} (x) - u_{I} ∣^{p} \leq L^{- 1} \int_{I} ∣ u^{*} (x) - u^{*} (y) ∣^{p} d y$ ; by step 2.1 the integrand is at most $(L^{1 - 1 / p} ∥ u^{'} ∥_{L^{p} (I)})^{p} = L^{p - 1} ∥ u^{'} ∥_{L^{p} (I)}^{p}$ for every $y$ . Integrating over $x \in I$ therefore yields $\int_{I} ∣ u - u_{I} ∣^{p} \leq L \cdot L^{p - 1} ∥ u^{'} ∥_{L^{p} (I)}^{p} = L^{p} ∥ u^{'} ∥_{L^{p} (I)}^{p}$ , and taking $p$ -th roots gives the asserted inequality.

4.1step 3.1step 1.2givenalgebra∎

Sharpness. Dividing the two norms computed in step 1.2 gives $∥ u - u_{I} ∥_{L^{p} (I)} / ∥ u^{'} ∥_{L^{p} (I)} = L \cdot \frac{1}{2} (p + 1)^{- 1 / p} = c_{p} L$ with $c_{p} = \frac{1}{2} (p + 1)^{- 1 / p} > 0$ . Hence for every $L > 0$ there is a class in $W^{1, p} (I)$ for which the ratio of the left side to $∥ u^{'} ∥_{L^{p} (I)}$ equals $c_{p} L$ , so no constant smaller than $c_{p} L$ can be admissible for all $u \in W^{1, p} (I)$ ; combined with step 3.1 the optimal constant for this family lies between $c_{p} L$ and $L$ , and in particular is a positive multiple of $L$ .

Source notes

The upper bound is the one-dimensional instance of the Poincare inequality for $W^{1, p}$ functions on bounded open sets; Kinnunen, Theorem 3.12 treats cube mean oscillations (an interval when $n = 1$ ); the present proof works directly on the given interval, and Hunter's Theorem 4.9 gives the related p=2 zero-boundary slab estimate; here the cited one-dimensional representative supplier gives the mean-zero interval argument for all finite p. The computation of the extremal ratio for the affine function is included to fix the linear dependence on the interval length, which the statement of the companion theorem does not quantify; no claim about the exact optimal constant beyond the two-sided order $c_{p} L \leq C^{*} (L) \leq L$ is made.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

74 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)