LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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 product rule for a bounded coefficient with bounded weak derivative

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $d \geq 1$ and let $a \in L^{\infty} (R^{d}; C)$ be a class having weak first derivatives $D_{j} a \in L^{\infty} (R^{d}; C)$ for every $j \in {1, \dots, d}$ , in the sense of Weak derivative of a locally integrable function. Let $u \in W^{1, 2} (R^{d}; C)$ (Integer-order Sobolev spaces and their norms). Then $a u \in W^{1, 2} (R^{d}; C)$ and, for every $j$ , $D_{j} (a u) = a D_{j} u + (D_{j} a) u as L^{2} classes,$ with pointwise products of chosen representatives. No boundedness of $u$ is assumed.

Facts & Assumptions

Given: a class $a \in L^{\infty}$ with weak derivatives $D_{j} a \in L^{\infty}$ , and a class $u \in W^{1, 2}$ .

[F1]

$u \in W^{1, 2}$ means $u \in L^{2}$ and each weak derivative $D_{j} u$ is an $L^{2}$ class satisfying $\int u D_{j} φ = - \int (D_{j} u) φ$ for every $φ \in C_{c}^{\infty}$ ; the pairing is bilinear and the weak derivative class is unique (Integer-order Sobolev spaces and their norms, Weak derivative of a locally integrable function, Uniqueness of a weak derivative as an almost-everywhere class).

[F2]

The same identity $\int a D_{j} ψ = - \int (D_{j} a) ψ$ holds for every $ψ \in C_{c}^{\infty}$ because $D_{j} a$ is the weak derivative of $a$ ; both sides are finite since $a$ and $D_{j} a$ are bounded and $ψ$ is compactly supported.

[F3]

$C_{c}^{\infty} (R^{d}; C)$ is dense in $W^{1, 2} (R^{d}; C)$ in the $W^{1, 2}$ norm (Compactly supported smooth functions are dense in W^{k,p}(R^n)).

[F4]

Classical partial derivatives of complex smooth functions are weak derivatives (Classical derivatives agree with weak derivatives). The product rule of Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ is stated for real functions of one real variable; its use for complex partial derivatives is reduced to that case in step 1.1.

Proof

1.1givenF1F2F4algebra

[Compactly supported smooth case] Let $v, φ \in C_{c}^{\infty} (R^{d}; C)$ , and fix $j$ . Write $v = v_{1} + i v_{2}$ , $φ = φ_{1} + i φ_{2}$ with real smooth components. Holding all coordinates except $x_{j}$ fixed gives smooth real functions of one variable. Applying [F4]'s real product and sum rules to $v_{1} φ_{1} - v_{2} φ_{2} + i (v_{1} φ_{2} + v_{2} φ_{1})$ gives $D_{j} (v φ) = (D_{j} v) φ + v D_{j} φ$ . Iterating these rules proves smoothness of $v φ$ , whose support lies in the intersection of the two compact supports. Its classical derivative is its weak derivative by [F4], so [F2] with $ψ : = v φ$ gives $\int a ((D_{j} v) φ + v D_{j} φ) = - \int (D_{j} a) v φ$ . Rearranging, $\int a v D_{j} φ = - \int (a D_{j} v + (D_{j} a) v) φ$ . Boundedness of $a, D_{j} a$ and square integrability of $v, D_{j} v$ imply $a v, a D_{j} v + (D_{j} a) v \in L^{2}$ . Since $j$ and the test $φ$ were arbitrary, [F1] gives $a v \in W^{1, 2}$ with these weak derivatives.

1.2givenF1F3algebra

[Approximation] By [F3] choose $v_{n} \in C_{c}^{\infty} (R^{d})$ with $∥ v_{n} - u ∥_{W^{1, 2}} \to 0$ ; then $v_{n} \to u$ and $D_{j} v_{n} \to D_{j} u$ in $L^{2}$ . Put $M : = \max {∥ a ∥_{\infty}, ∥ D_{j} a ∥_{\infty}} < \infty$ . Then $∥ a v_{n} - a u ∥_{2} \leq M ∥ v_{n} - u ∥_{2} \to 0$ , $∥ a D_{j} v_{n} - a D_{j} u ∥_{2} \leq M ∥ D_{j} v_{n} - D_{j} u ∥_{2} \to 0$ , and $∥ (D_{j} a) v_{n} - (D_{j} a) u ∥_{2} \leq M ∥ v_{n} - u ∥_{2} \to 0$ : all three convergences hold in $L^{2}$ .

2.1step 1.1step 1.2F1algebra∎

[Passage to the limit] Fix $φ \in C_{c}^{\infty} (R^{d})$ . By step 1.1, $\int a v_{n} D_{j} φ = - \int (a D_{j} v_{n} + (D_{j} a) v_{n}) φ$ for every $n$ . As $n \to \infty$ , the left side tends to $\int a u D_{j} φ$ and the right side to $- \int (a D_{j} u + (D_{j} a) u) φ$ , because $a v_{n} \to a u$ , $a D_{j} v_{n} \to a D_{j} u$ and $(D_{j} a) v_{n} \to (D_{j} a) u$ in $L^{2}$ by step 1.2 while $D_{j} φ$ and $φ$ are bounded with compact support. Hence $\int a u D_{j} φ = - \int (a D_{j} u + (D_{j} a) u) φ$ for every test function $φ$ . The class $a D_{j} u + (D_{j} a) u$ lies in $L^{2}$ by step 1.2's estimates, so by [F1] the class $a u$ has weak $j$ -derivative $a D_{j} u + (D_{j} a) u$ and $a u \in W^{1, 2}$ .

Weak product rule for a bounded coefficient with bounded weak derivative

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources