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 Leibniz rule with a smooth factor
Statement
Assume Countable Choice. Let be open with , let , and let and . For , suppose that for every there is with weakly. Then has a weak -derivative, and its almost-everywhere class is where is the classical derivative and products are pointwise products of representatives. The resulting class does not depend on the representatives.
For and , if and for every , then and the same formula holds in for every . In particular, is a sufficient condition on the multiplier for this global conclusion.
For all classes are zero and the identity holds. The pairing convention is bilinear, with no complex conjugation.
Facts & Assumptions
Given: Countable Choice, an open , a scalar field , a smooth multiplier , a locally integrable , and a multi-index for which the weak derivatives through have locally integrable values.
The regular-distribution pairing is complex bilinear and depends only on the almost-everywhere class (Locally integrable functions as regular distributions).
A weak derivative is characterized by the signed test identity, which is the distributional derivative identity for the corresponding regular distributions (Weak derivative of a locally integrable function).
Distributional Leibniz holds for a smooth complex multiplier and every multi-index, in the bilinear convention and without a choice assumption (Leibniz rule for distributions).
Multiplication of distributions by smooth functions is defined by , with no conjugation, and is associative (Multiplication of a distribution by a smooth function).
A locally integrable weak derivative, if it exists, is unique as an almost-everywhere class under Countable Choice (Uniqueness of a weak derivative as an almost-everywhere class).
The class has an class for each weak derivative of order at most (Integer-order Sobolev spaces and their norms).
Real elements are almost-everywhere classes (The space as the quotient by null functions).
Complex elements are almost-everywhere classes and use pointwise complex products (Complex Lp classes and Euclidean test-function conventions).
Countable Choice asserts that every countable family of nonempty sets has a choice function (The Axiom of Countable Choice ()).
Choice accounting: Countable Choice is used only through [F5] to identify locally integrable derivative value classes, including at order zero; [F9] names this assumption. The test-identity transfers, distributional Leibniz identity, and finite algebraic expansion are choice-free. No full Axiom of Choice is assumed.
Proof
For every , the weak identity and [F2] give In particular, the derivative on the left is represented by a locally integrable function for each such .
Set The sum is finite. On each compact subset of , every smooth is bounded and every is integrable, so . Changing any selected representative on a null set changes each product only on a null set; hence defines a single almost-everywhere class.
Apply [F3] to and , then substitute the identities of step 1.1. By [F4], the left side is the th distributional derivative of , while each term on the right is the regular distribution of the corresponding summand in . Thus By the weak-derivative identity in [F2], is a locally integrable weak -derivative of . By [F5] it is the unique value class, which proves the asserted local formula.
Now suppose the global hypotheses hold. For each , the local result applies because all weak derivatives with are supplied by [F6]. For every , the factor is bounded, so is an class: for finite its modulus is bounded by almost everywhere, and for the same estimate bounds the essential supremum. The finite sum is therefore in . Taking also shows ; the local result for every now gives by its definition, and its weak derivative classes are exactly the displayed sums.
If , its support is compact in . Each derivative is continuous and vanishes off that compact support, so every derivative through order is bounded. Thus the preceding global argument applies. For the formula has only and says . When the same order-zero identity holds in the local assertion. For the zero input class, zero is a weak derivative at every order by the defining test identity, and [F5] makes each supplied derivative class zero; if , every summand is zero. On the empty domain every term is the zero class.
The argument treats real and complex values uniformly because all pairings and multiplier products are bilinear; no conjugation or additional choice principle enters.
Depends on
- Locally integrable functions as regular distributions
- Weak derivative of a locally integrable function
- Leibniz rule for distributions
- Multiplication of a distribution by a smooth function
- Uniqueness of a weak derivative as an almost-everywhere class
- Integer-order Sobolev spaces and their norms
- The space $L^p(\mu)$ as the quotient by null functions
- Complex Lp classes and Euclidean test-function conventions
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- Compactly supported smooth functions are dense in W^k,p(Rⁿ) Corollary
- Smooth interior data do not repair incompatible Dirichlet corner values Counterexample
- Subcritical W^1,p is not closed under multiplication Counterexample
- A Poisson-type extension and its local and global Sobolev traces Example
- The trace of a one-dimensional Sobolev function is the pair of endpoint values Example
- A bounded regular decomposition with both summands satisfying full Dirichlet conditions Lemma
- A conforming averaging companion for Crouzeix–Raviart functions Lemma
- Bounded restriction and cutoff localisation in Sobolev spaces Lemma
- Classical solutions satisfy the weak formulation Lemma
- Endpoint trace commutes with Sobolev truncation on an interval Lemma
- Exterior finite-energy functions have a trace controlled by their gradient Lemma
- Fractional face traces and cellwise Green identity on a simplex Lemma
- Inward mollification and smooth finite-rank approximation on Lipschitz domains Lemma
- Localisation of a weak solution up to a bounded first-order term Lemma
- Logarithmic Caccioppoli estimate for positive supersolutions Lemma
- Mean-zero Poincare estimate on bounded connected extension domains below the dimension Lemma
- Moser iteration for positive supersolutions: negative-power and logarithmic comparison Lemma
- Positive-part truncation calculus and admissible cut-off weak tests Lemma
- Scalar H1 and H2 extension across a bounded Lipschitz boundary Lemma
- Smooth functions are dense in finite-order Sobolev spaces on a reference simplex Lemma
- Smooth-boundary trace lifts and Sobolev Helmholtz layer extensions Lemma
- Sobolev pullback and Green identity on Lipschitz graphs Lemma
- The coordinate inequality ‖xⱼf‖₂‖Dⱼf‖₂≥1/2‖f‖₂² Lemma
- The cutoff difference-quotient commutator estimate Lemma
- The difference-quotient test function and its commutators Lemma
- The Euclidean trace quotient is the fixed-atlas H1/2 boundary space Lemma
- The H1 trace and lifting theorem on a compact Lipschitz boundary Lemma
- The nodal P1 interpolant preserves homogeneous boundary values Lemma
- The normal-boundary Hodge estimate on four-dimensional balls Lemma
- The trace commutes with smooth cutoffs and is chart local Lemma
- Weak tangential trace on a Lipschitz polyhedron Lemma
- Whole-space support and the zero-boundary Sobolev closure Lemma
- A bounded right inverse of the trace, supported in a prescribed collar Theorem
- A reference simplex is an integer-order Sobolev extension domain Theorem
- Bounded Cᵏ domains admit integer-order Sobolev extension Theorem
- Compactness of W^1,p(Ω)↪ Lᵖ(Ω) on bounded extension domains Theorem
- De Giorgi local boundedness of homogeneous subsolutions Theorem
- De Giorgi local boundedness with a scale-correct forcing term Theorem
- De Giorgi-Nash interior Holder regularity for divergence-form equations Theorem
- Higher-order Rellich--Kondrachov compactness Theorem
…and 12 more results.
Dependency tree · two levels
40 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 (2026) (standard reference, not scraped)
- John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)