The chain rule and the positive part in W^{1,p}(Ω) for p < ∞ #
For 1 ≤ p < ∞, W^{1,p}(Ω) is stable under composition with a Lipschitz C¹ function F
vanishing at 0, and the weak gradient obeys the classical chain rule
∇(F ∘ u) = F'(u) ∇u.
In the same exponent range, its limiting case is the truncation property:
u⁺ ∈ W^{1,p}(Ω), with
∇(u⁺) = 1_{u > 0} ∇u,
which is the starting point of the truncation arguments of elliptic regularity: the Caccioppoli
inequality for the truncations (u − k)⁺ of a subsolution, and the weak maximum principle for a
weak solution, both test the equation against a truncation of the solution itself.
The two limits #
Neither statement can be read off from the definition, because a weak derivative is only defined
by integration against test functions and F ∘ u has no reason to be smooth. Both are obtained
by approximation, and the order of the two limits matters.
- First,
uis approximated. On a subdomainVrelatively compact inΩ, test functions onΩare dense inW^{1,p}(V)(TauCeti.W1p.restrictL_mem_closure_range_ofTestFunctionₗ), the chain rule is classical for them, and it passes to the limit becauseVhas finite measure and weak derivatives are stable underL¹limits (TauCeti.hasWeakFDerivOn_of_tendsto_lintegral_enorm_sub). HereF'must be continuous: the convergenceF'(uₖ) → F'(u)is what carries the derivative. Locality of the weak derivative then returns the statement toΩ. - Only then is the nonlinearity approximated. The positive part is the limit of the
C¹functionsFδ t = ∫₀ᵗ χ(s / δ), whereχisReal.smoothTransition; the point of that choice is thatFδ' = χ(· / δ)vanishes identically on(−∞, 0], soFδ'(t) → 1_{t > 0}including att = 0. Taking the two limits in the other order would instead produce the factorFδ'(0), and the identification of the limit would need the separate fact that∇u = 0almost everywhere on{u = 0}.
Main declarations #
TauCeti.W1p.hasWeakFDerivOn_comp: the chain rule, as a weak-derivative statement.TauCeti.W1p.contDiffComp:F ∘ uas an element ofW^{1,p}(Ω).TauCeti.W1p.hasWeakFDerivOn_posPart: the weak gradient of the positive part.TauCeti.W1p.posPartAboveOfMemLp: the shifted truncation(u - k)⁺at an arbitrary level, assuming its value is globally inLᵖ.TauCeti.W1p.posPartAbove: the shifted truncation(u - k)⁺fork ≥ 0.TauCeti.W1p.posPart: the positive partu⁺as an element ofW^{1,p}(Ω), with its valueTauCeti.W1p.value_posPartand its weak gradientTauCeti.W1p.gradient_posPart_ae.
References #
- D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Lemma 7.6.
- L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, §4.2.2.
- H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Proposition 9.5.
The classical chain rule for a test function #
The chain rule in W^{1,p}(Ω) for p < ∞ #
The local chain rule for W^{1,p}(Ω) when 1 ≤ p < ∞. If F is C¹ with
derivative bounded by M, then F ∘ u has the weak gradient F'(u) ∇u on Ω. No boundary
regularity of Ω is needed: the statement is local, and the approximation happens on subdomains
relatively compact in Ω.
For 1 ≤ p < ∞, W^{1,p}(Ω) is stable under composition with a Lipschitz C¹ function
vanishing at 0. Its value and weak gradient are F ∘ u and F'(u) ∇u, by
TauCeti.W1p.value_contDiffComp_ae and TauCeti.W1p.gradient_contDiffComp_ae.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value of F ∘ u produced by W1p.contDiffComp agrees almost everywhere with the
pointwise composition.
The weak gradient of F ∘ u produced by W1p.contDiffComp is F'(u) ∇u almost
everywhere.
The positive part #
The positive part of a Sobolev function #
The pointwise truncation (u - k)⁺ is in Lᵖ when u is and k ≥ 0.
Raising the level of an Lᵖ positive truncation preserves its Lᵖ membership.
For 1 ≤ p < ∞, truncation above any real level is weakly differentiable, with
weak gradient 1_{u > k} ∇u.
For 1 ≤ p < ∞, the positive part of a Sobolev function is weakly differentiable, with
weak gradient 1_{u > 0} ∇u.
For 1 ≤ p < ∞, truncation above any level preserves W^{1,p}(Ω) whenever the
truncated value is globally in Lᵖ. Its weak gradient is 1_{u > k} ∇u.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value of W1p.posPartAboveOfMemLp hp k u hmem is (u - k)⁺ almost everywhere.
The weak gradient of an Lᵖ truncation (u - k)⁺ is 1_{u > k} ∇u almost
everywhere.
For 1 ≤ p < ∞, truncation above a nonnegative level preserves W^{1,p}(Ω).
The value of W1p.posPartAbove hp hk u is (u - k)⁺, and its weak gradient is
1_{u > k} ∇u.
Equations
- TauCeti.W1p.posPartAbove hp hk u = TauCeti.W1p.posPartAboveOfMemLp hp k u ⋯
Instances For
At a nonnegative level, the general Lᵖ truncation constructor agrees with
W1p.posPartAbove, independently of the supplied MemLp proof.
The value of W1p.posPartAbove hp hk u is (u - k)⁺ almost everywhere.
The weak gradient of (u - k)⁺ is 1_{u > k} ∇u almost everywhere.
For 1 ≤ p < ∞, the positive part u⁺ of a Sobolev function is again in
W^{1,p}(Ω). Its value is Mathlib's MeasureTheory.Lp.posPart of the value of u, and its
weak gradient is 1_{u > 0} ∇u (TauCeti.W1p.gradient_posPart_ae).
Equations
Instances For
The value of W1p.posPart hp u is the Lᵖ positive part of the value of u.
The weak gradient of u⁺ is 1_{u > 0} ∇u almost everywhere.
Truncation above zero is the positive part.