RemarkRemark: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Weak derivatives are represented distributional derivatives

Remark

Assume Countable Choice, as required by the cited regular-distribution injection, weak-derivative uniqueness, measure, and interval-FTC results. Let $Ω \subseteq R^{n}$ be open, $n \geq 1$ , let $u \in L_{l o c}^{1} (Ω)$ , and let $α \in N_{0}^{n}$ . Then $D^{α} u exists as a weak L_{l o c}^{1} derivative ⟺ \partial^{α} T_{u} \in {T_{h} : h \in L_{l o c}^{1} (Ω)} \subseteq D^{'} (Ω) .$ When such an $h$ exists, its almost-everywhere class is unique. Every distribution has distributional derivatives, but these derivatives need not lie in the image of the regular-distribution map. In particular, a locally integrable function can belong to every $L^{p}$ under consideration and still have no $L^{p}$ weak derivative.

Example of the obstruction. On $Ω = (- 1, 1)$ let $u = 1_{(0, 1)}$ . This function is in $L^{p} (Ω)$ for every $1 \leq p \leq \infty$ , but its distributional derivative is $δ_{0}$ . The delta distribution is not the regular distribution of any $h \in L_{l o c}^{1} ((- 1, 1))$ , so $u$ has no locally integrable weak derivative, and consequently no $L^{p}$ weak derivative.

Facts & Assumptions

Given: Countable Choice, an open set $Ω \subseteq R^{n}$ , $n \geq 1$ , $u \in L_{l o c}^{1} (Ω)$ , and $α \in N_{0}^{n}$ .

[F1]

The regular pairing $T_{f} (φ) = \int_{Ω} f φ$ defines a distribution for each $f \in L_{l o c}^{1} (Ω)$ ; under Countable Choice the map from almost-everywhere classes to distributions is injective (Locally integrable functions as regular distributions).

[F2]

The weak-derivative identity is equivalent to $\partial^{α} T_{u} = T_{v}$ (Weak derivative of a locally integrable function).

[F3]

A weak derivative, when it exists, is unique as an almost-everywhere class under Countable Choice (Uniqueness of a weak derivative as an almost-everywhere class).

[F4]

Distributional differentiation maps every distribution to a distribution, with the signed-transpose convention (Distributional derivative).

[F5]

A complex $L^{p}$ class is the quotient of measurable functions with finite $N_{p}$ (Complex Lp classes and Euclidean test-function conventions).

[F18]

For finite $p$ , $N_{p}$ is the $p$ th-root integral size; for $p = \infty$ , $N_{\infty}$ is the essential-supremum size (Complex Lp classes and Euclidean test-function conventions).

[F6]

The intervals $(0, 1)$ and $(- 1, 1)$ have measures one and two, respectively, and $[- ε, ε]$ has measure $2 ε$ for $0 < ε < 1 / 2$ (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).

[F7]

The nonnegative integral of an indicator equals the measure of its measurable set, and a nonnegative simple function has integral equal to its simple integral (The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions).

[F8]

Every compact subset of $R$ is measurable with finite measure under Countable Choice; the integral over a measurable set is the integral after restricting by its indicator, and the nonnegative integral is monotone (Lebesgue measure is sigma-finite, and every metrically bounded subset of $R^{n}$ has finite outer measure, Integral over a measurable subset, Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F9]

A complex function is integrable when its modulus has finite integral (Integrable real and complex functions, and their integrals).

[F10]

In one dimension there is a smooth $β : R \to [0, 1]$ equal to one on $[- 1 / 2, 1 / 2]$ and with support contained in $(- 1, 1)$ (A smooth bump between concentric Euclidean balls).

[F11]

If $h$ is integrable on a compact set, then its absolute integral over measurable subsets tends to zero as their measure tends to zero (Absolute continuity of the integral).

[F12]

For complex $C^{1}$ functions, the Lebesgue integral of the derivative on a compact interval is the endpoint increment, under Countable Choice (Complex integration by parts on intervals and decaying lines).

[F13]

For $a \in Ω$ , the Dirac distribution satisfies $δ_{a} (φ) = φ (a)$ (Dirac delta and its derivatives).

[F14]

For open $Ω$ , membership in $L_{l o c}^{1} (Ω)$ means integrability on every compact subset of $Ω$ (Regular distribution from a locally integrable function).

[F15]

A test function on an open set has compact support in that set, and its zero extension to $R^{n}$ is smooth with compact support (Test function space d of an open set).

[F16]

Composing a smooth one-variable function with $x \mapsto x / ε$ preserves smoothness; iterating the chain rule gives $(β (\cdot / ε))^{(m)} (x) = ε^{- m} β^{(m)} (x / ε)$ (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[F17]

Countable Choice asserts that every countably indexed family of nonempty sets has a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1F1F2F4given

For every test $φ \in C_{c}^{\infty} (Ω)$ , the identity $\partial^{α} T_{u} = T_{h}$ expands by [F1] and [F4] to $(- 1)^{∣ α ∣} \int_{Ω} u D^{α} φ d x = \int_{Ω} h φ d x$ ; since the sign squares to one, this is exactly the weak-derivative identity, and conversely that identity gives the distribution equality, proving both directions of the image criterion.

1.2F5F6F7F8F9F14F18given

On $Ω = (- 1, 1)$ , let $u = 1_{(0, 1)}$ ; [F6] gives $λ ((0, 1)) = 1$ and $λ (Ω) = 2$ , so [F7], [F5], and [F18] give $\int_{Ω} ∣ u ∣^{p} = 1$ for finite $p \geq 1$ and essential supremum one, hence $u \in L^{p} (Ω)$ for every $1 \leq p \leq \infty$ ; also $u \in L^{1} (Ω)$ by [F7] and [F9], and for every compact $K \subseteq Ω$ , [F8] gives $\int_{K} ∣ u ∣ \leq \int_{K} 1 d x = λ (K) < \infty$ , so $u \in L_{l o c}^{1} (Ω)$ by [F14].

1.3F1F2given

If $Ω = \emptyset$ , [F1] gives only the zero regular distribution and locally integrable class, so the image criterion holds and the weak test identity is vacuous.

2.1F3step 1.1given

If $h$ and $k$ both represent $\partial^{α} T_{u}$ , step 1.1 makes both weak $α$ -derivatives of $u$ , and Countable-Choice uniqueness [F3] gives $h = k$ almost everywhere.

2.2F1step 1.1given

If $α = 0$ , then $D^{0} u = u$ and $\partial^{0} T_{u} = T_{u}$ ; step 1.1 and the injection [F1] identify every representing class $h$ with $u$ almost everywhere.

2.3F4F12F13F15step 1.2given

For $φ \in C_{c}^{\infty} ((- 1, 1))$ , its zero extension $\tilde{φ}$ is smooth and vanishes at $1$ by [F15], so the signed derivative and complex FTC [F4, F12] give $⟨ \partial T_{u}, φ ⟩ = - \int_{0}^{1} {\tilde{φ}}^{'} (x) d x = \tilde{φ} (0) - \tilde{φ} (1) = φ (0) = δ_{0} (φ)$ by [F13]; hence $\partial T_{u} = δ_{0}$ .

2.4F1F6F10F11F13F14F15F16step 1.2given

If $δ_{0} = T_{h}$ for some $h \in L_{l o c}^{1} ((- 1, 1))$ , choose the bump $β$ from [F10] with $r = 1 / 2$ and $R = 1$ , and set $φ_{ε} (x) = β (x / ε)$ for $0 < ε < 1 / 2$ ; iterating the chain rule [F16] and scaling its compact support [F15] make this a test with value one at zero and $0 \leq φ_{ε} \leq 1$ , so [F1] and [F13] give $1 = ∣ T_{h} (φ_{ε}) ∣ \leq \int_{[- ε, ε]} ∣ h ∣$ . The function $h$ is integrable on $[- 1 / 2, 1 / 2]$ by [F14], while [F6] makes the interval measures tend to zero and absolute continuity [F11] makes the right side tend to zero, a contradiction. Thus $δ_{0}$ has no locally integrable representative, and step 1.2's $L^{p}$ function has no $L^{p}$ weak derivative.

3.1F1F4step 1.1step 2.1given

If $u = 0$ , [F1] gives $T_{u} = 0$ and [F4] gives $\partial^{α} T_{u} = 0 = T_{0}$ ; step 1.1 makes zero a weak derivative, and step 2.1 makes its class unique.

4.1F1F3F6F8F12F17given∎

Countable Choice is used only by the injection and uniqueness [F1, F3], interval and compact-measure facts [F6, F8], and complex interval FTC [F12]; the test-pairing equivalence and shrinking-test contradiction are direct, and no full Axiom of Choice is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

88 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

Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (2011) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)