The absolute value has a weak first derivative

Given: Countable Choice, a bounded open interval $I$ with $0\in I$, and $u(x)=\mathrm{\mid }x\mathrm{\mid }$.

The exact assumption is Countable Choice, denoted ${\mathrm{A}\mathrm{C}}_{\omega }$ (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)).

The test space is $C_c^{\mathrm{\infty }}(I;\mathbb{C})$ and its members are actual smooth functions with compact support (Test function space d of an open set).

A locally integrable $v$ is the weak first derivative of $u$ exactly when ${\int }_{I}u{\phi }^{\mathrm{\prime }}=-{\int }_{I}v\phi$ for every test (Weak derivative of a locally integrable function).

Membership in $W^{1,p}(I;\mathbb{R})$ requires an $L^p$ class for $u$ and an $L^p$ class for its weak derivative, with the zero-order derivative equal to $u$ (Integer-order Sobolev spaces and their norms).

Changing locally integrable representatives on a null set preserves the weak-derivative identity; $L^p$ objects are almost-everywhere classes (Weak differentiation ignores null-set changes).

Write $I=(a,b)$. Boundedness and openness give finite endpoints $a<b$; $0\in I$ gives $a<0<b$ (Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length).

Under Countable Choice, $[a,b]$ is measurable with measure $b-a$, and every singleton is a zero-length box of measure zero (A box in ${\mathbb{R}}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure ${\prod }_{i<n}(b_i-a_i)$, whichever of its faces are included).

Continuous real functions are Borel measurable, and Borel sets are Lebesgue measurable under Countable Choice (Continuous functions on Euclidean spaces are Borel measurable, Assuming countable choice, every Borel subset of ${\mathbb{R}}^n$ is Lebesgue measurable). The piecewise-constant function $v_0$ below is Borel because its level sets are intervals and a singleton.

For each finite $p\ge 1$, $t\mapsto t^p$ is nondecreasing on $[0,\mathrm{\infty })$. For $0<x<y$, the mean value theorem and $(t^p)\mathrm{\prime }=p{t}^{p-1}>0$ on $(0,\mathrm{\infty })$ give $x^p<y^p$; at zero, $0^p=0$ and positive-base powers are positive (The mean value theorem, as the case $g(x)=x$ of Cauchy's: for $f$ continuous on $[a,b]$ with $a<b$ and differentiable on $(a,b)$ there is $c\in (a,b)$ with $f(b)-f(a)=f^{\mathrm{\prime }}(c)(b-a)$, Continuity and derivatives of positive-base real powers, Real powers for positive bases, with the zero-base positive-exponent convention, The exponential is positive and satisfies $\exp (-x)=1\mathrm{/}\exp (x)$).

For finite $p$, membership in $L^p$ means measurability and finiteness of ${\int }_I\mathrm{\mid }f{\mathrm{\mid }}^p$ (Complex Lp classes and Euclidean test-function conventions).

Integration over a measurable set is integration after multiplication by its indicator. The nonnegative integral is monotone and homogeneous, and a nonnegative simple function integrates by its simple-integral formula (Integral over a measurable subset, Monotonicity and nonnegative homogeneity of the nonnegative integral, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions).

A nonnegative measurable function has integral zero over a measurable null set (A nonnegative integral over a null set vanishes).

The product rule holds for differentiable real functions (Sums, scalar multiples, products and quotients: $(f+g{)}^{\mathrm{\prime }}(c)=f^{\mathrm{\prime }}(c)+g^{\mathrm{\prime }}(c)$, $(\alpha f{)}^{\mathrm{\prime }}(c)=\alpha f^{\mathrm{\prime }}(c)$, $(fg{)}^{\mathrm{\prime }}(c)=f^{\mathrm{\prime }}(c)g(c)+f(c)g^{\mathrm{\prime }}(c)$, and $(f\mathrm{/}g{)}^{\mathrm{\prime }}(c)=(f^{\mathrm{\prime }}(c)g(c)-f(c)g^{\mathrm{\prime }}(c))\mathrm{/}g(c{)}^2$ when $g(c)\mathrm{\ne }0$).

Every bounded function on a closed interval that is continuous except at finitely many points is Riemann integrable (A bounded function on $[a,b]$ that is continuous except at finitely many points is Riemann integrable).

Newton–Leibniz holds for a continuous function whose interior derivative has a Riemann-integrable extension; finitely many exceptional interior points are allowed (Newton–Leibniz remains valid across finitely many exceptional interior points when the primitive is continuous).

Riemann integration on a closed interval is linear (Integrable functions on $[a,b]$ form a set closed under sums and scalar multiples, and ${\int }_a^b(\lambda f+\mu g)=\lambda {\int }_a^{b}f+\mu {\int }_a^{b}g$).

Under Countable Choice, a bounded Riemann-integrable function on a closed interval is Lebesgue measurable and its Lebesgue and Riemann integrals agree (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

The defining requirement for an $L^p$ class uses the measurable function and integral conventions in [F10]; for a bounded measurable $f$ on $I$, the majorant $C^p{\mathbf{1}}_I$ is simple, has integral $C^p(b-a)$, and bounds ${\int }_I\mathrm{\mid }f{\mathrm{\mid }}^p$ whenever $\mathrm{\mid }f\mathrm{\mid }\le C$ (derived from [F7], [F9], [F10], [F11]).

Complex test pairings are bilinear and use no conjugation (Test function space d of an open set).

Complex integrals are defined componentwise (Complex Lp classes and Euclidean test-function conventions).

For $p=\mathrm{\infty }$, a finite almost-everywhere bound is sufficient for $L^{\mathrm{\infty }}$ membership (Complex Lp classes and Euclidean test-function conventions).

Nonnegative powers of nonnegative measurable functions are measurable (Complex Lp classes and Euclidean test-function conventions).

Boundedness gives a finite $M>0$ with $\mathrm{\mid }x\mathrm{\mid }\le M$ on $I$ (Lower bound, bounded below, bounded set, Basic properties of the absolute value).

Choice use. The declared principle is exactly ${\mathrm{A}\mathrm{C}}_{\omega }$. It is used through the Sobolev definition, representative-independence lemma, interval measure formula, Borel-to-Lebesgue measurability, and Riemann-to-Lebesgue integral comparison. The explicit piecewise calculation itself is choice-free; no full Axiom of Choice or Dependent Choice is invoked.