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.
The difference-quotient characterisation of for
Statement
Assume Countable Choice. Let be open, , and ; write and for the difference-quotient and gradient vectors, with (1) If and , then for every and every coordinate direction , At the vector estimate has constant one. The coordinate bound also holds on any open for a fixed for which every segment , , stays in ; compact containment is unnecessary. In particular, for tangential directions on a half-space . (2) Conversely, if , and there is with for every coordinate and all , then with , , and weakly in as . For , tangential quotients on also converge strongly: in as . Both parts are identities of classes and hold without any regularity of . At the converse in (2) is deliberately not asserted; the companion remark records why only a measure derivative survives there.
Facts & Assumptions
Given: Countable Choice; an open set with ; an open ; a scalar field ; the exponent range for part (1) and for part (2); a class in part (1) or a class with uniform difference-quotient bound in part (2); and a coordinate direction .
Difference quotients: on ; for one has , and for the class lies in with ; the definition depends only on the class of . (Difference quotients on a shrunken domain, The space as the quotient by null functions)
Sobolev classes: consists of the classes whose first weak derivatives lie in , and ; convergence in means convergence in of and of every . (Integer-order Sobolev spaces and their norms, The notation and the reserved zero-boundary symbol, Weak derivative of a locally integrable function)
Smooth approximation: is dense in for . (Meyers–Serrin density on an arbitrary open set)
Fundamental theorem of calculus and chain rule: for smooth and , the map is differentiable with derivative , so . (The second fundamental theorem: if is differentiable on with and is integrable, then , The chain rule for total derivatives: )
Jensen's inequality: on a probability space and for a convex , ; the normalized restriction of Lebesgue measure to , , is a probability measure, and is convex on . (Jensen's integral inequality for a probability measure)
Fubini for nonnegative integrands and translation invariance of Lebesgue measure: for measurable one has , and for one has and . (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L^1 functions on a sigma-finite product, Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions)
Hölder's inequality with conjugate exponents on , and the triangle inequality in for . (Conjugate exponents, including the endpoint conventions, Holder's inequality for integrals, including the endpoint cases, Minkowski's inequality for integrals, including )
The weak-limit lemma: a uniform bound for and , , , gives , and for every . (Uniformly bounded difference quotients represent a weak derivative)
Translations are strongly continuous on for under Countable Choice. ( in as , for )
Proof
Let and . Take first and fix ; by [F4] and the convexity of , Jensen's inequality [F5] for the probability measure gives For the same computation applies with the segment from to and the average taken over .
For part (2), choose a finite with ; when and the distance is infinite, take ; the hypothesis is exactly the uniform bound required by the weak-limit lemma [F8], which gives with and the convergence for every ; by [F7] the latter is precisely weak convergence in .
Integrating the estimate of step 1.1 over and applying Fubini and the translation invariance of [F6] (every point with , between and , satisfies because ) gives, for either sign of , so .
Let now and and choose with , as [F3] permits. For fixed with , [F1] applied to gives , and by [F2]; step 2.1 applied to each and passage to the limit (norms are continuous) yield .
The coordinate argument in steps 1.1--3.1 works on any open with the segment condition: each translated set lies in , so Tonelli and change of variables bound its integral by the gradient norm on . For , fix a compact . The union of its segments is compact in , so choose a bounded open tube containing that union. For each finite , the same coordinate argument applied to gives . If the quotient exceeded this essential bound by on a positive-measure subset of , its norm would exceed , a contradiction as . Exhausting by compact sets proves the coordinate bound.
Tangential strong convergence. For a tangential direction on , smooth approximation [F3] and the fixed- translation bounds pass the segment formula to : as classes. Indeed Jensen and tangential change of variables bound the error between the averages of two gradient approximations by their distance. Extend by zero as an class on ; tangential shifts preserve , so [F9] gives uniformly for as . Jensen and Tonelli applied to the segment formula therefore give .
Vector estimate. Put and . Step 3.1 gives for each coordinate. If , the finite-dimensional inequalities yield . If , the triangle inequality in gives . For , step 4.1 gives a.e., hence . These finite-dimensional comparisons follow from Hölder applied to the finite sum. Thus the stated vector constant is valid, and equals one at . Each component uses its own coordinate segment; no common translated gradient vector is asserted.
Steps 3.1--4.1 prove (1) for every , and step 1.2 proves (2) for ; no step used any regularity of , only the containedness and the shrunken-domain definition of the quotients, so both assertions are identities of classes on arbitrary open sets.
Source notes
Hunter's Theorem 4.53 (printed pp. 125-126) states (1) with the mean value formula and (2) by weak compactness; Laugesen's Proposition 5.7 (printed pp. 110-111) and Simon's Lemma 7 record the same two directions. The companion remark on this page records the failure of (2) at . The scaffold dependency on def-sobolev-conjugate-exponent was replaced by Conjugate exponents, including the endpoint conventions: the exponents in Hölder's inequality are conjugate exponents, while the Sobolev conjugate is a different object.
Depends on
Difference quotients on a shrunken domain
Difference-quotient calculus: integration by parts, product rule, commutation
Uniformly bounded difference quotients represent a weak derivative
Integer-order Sobolev spaces and their norms
Conjugate exponents, including the endpoint conventions
Dominated convergence
The Axiom of Countable Choice ()
Meyers–Serrin density on an arbitrary open set
Jensen's integral inequality for a probability measure
Fubini's theorem for L^1 functions on a sigma-finite product
Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation
A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions
The second fundamental theorem: if is differentiable on with and is integrable, then
The chain rule for total derivatives:
Weak derivative of a locally integrable function
The notation and the reserved zero-boundary symbol
The space as the quotient by null functions
Holder's inequality for integrals, including the endpoint cases
Minkowski's inequality for integrals, including
Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
in as , for
Dependency tree · 2 levels
Sources
- John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter graduate notes)
- Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes)
- Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan)