Multiplication by a smooth cutoff on W^{1,p}(Ω) #
The Leibniz rule of TauCeti/Analysis/Sobolev/Leibniz.lean says that ψ u is weakly
differentiable whenever u is and ψ is smooth. This file upgrades that from a statement about
weak derivatives to a statement about the Sobolev space itself: if ψ and ∇ψ are bounded by a
constant M, then
u ↦ ψ u
is a continuous linear operator on W^{1,p}(Ω) of norm at most 2 M, with value component ψ u
and gradient component ψ ∇u + u ∇ψ.
Boundedness of ψ and of ∇ψ on Ω is what the statement needs, and neither is automatic: for
ψ x = exp ‖x‖² on Ω = ℝⁿ, multiplication by ψ need not preserve Lᵖ. Both bounds are
therefore carried explicitly, through a single constant M, so that the operator norm is visible
rather than hidden behind an unquantified ∃ C; that is the convention the PDE roadmap asks for.
A cutoff built from ContDiffBump satisfies them, which is the intended use.
The operator and the milestone #
Multiplication by a cutoff is the localization device of Lane A of
TauCetiRoadmap/PDE/README.md: it is the first step of the Meyers--Serrin H = W density theorem
and of the extension operator (Lane A.2 and A.6), and it is what converts an interior estimate
into an estimate on a compactly contained subdomain. Having it as a bounded operator, rather
than as a pointwise membership statement, is what lets those arguments range over a family of
cutoffs while keeping uniform control of the resulting Sobolev norms.
The factor 2 in ‖ψ u‖ ≤ 2 M ‖u‖ is explicit, and it is the only shape the downstream
localization arguments need.
Main declarations #
TauCeti.W1p.contDiffSMul: the productψ u, as an element ofW^{1,p}(Ω).TauCeti.W1p.value_contDiffSMul_aeandTauCeti.W1p.gradient_contDiffSMul_ae: its two components,ψ uandψ ∇u + u ∇ψ.TauCeti.W1p.norm_contDiffSMul_le: the bound‖ψ u‖ ≤ 2 M ‖u‖.TauCeti.W1p.contDiffSMulL: the same map, bundled as a continuous linear operator.TauCeti.W1p.norm_gradient_contDiffSMul_sq_le: at exponent two, the weighted bound‖∇(ψ u)‖₂² ≤ 2 ∫ ψ² ‖∇u‖² + 2 ∫ ‖∇ψ‖² u².TauCeti.W1p.contDiffSMul_mem_w1p0Submodule: it preservesW^{1,p}_0(Ω), the closure ofC_c^∞(Ω).
References #
L. C. Evans, Partial Differential Equations, §5.2.3, Theorem 1(iv) and §5.3.3.
The two Lᵖ components #
The gradient of a smooth function is continuous. This is what makes the product below measurable.
The value component ψ u of the product is Lᵖ, because ψ is bounded.
The gradient component ψ ∇u + u ∇ψ of the product is Lᵖ, because ψ and ∇ψ are
bounded.
The product #
Multiplication by a smooth cutoff. If ψ is smooth with |ψ| ≤ M and ‖∇ψ‖ ≤ M on
Ω, the product ψ u of ψ with a Sobolev function u ∈ W^{1,p}(Ω) is again in W^{1,p}(Ω);
its weak gradient is ψ ∇u + u ∇ψ by the Leibniz rule.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value component of ψ u is ψ u.
The Leibniz rule in W^{1,p}(Ω): the weak gradient of ψ u is ψ ∇u + u ∇ψ.
Linearity and boundedness #
Multiplication by ψ is additive.
Multiplication by ψ commutes with scalars.
The operator bound. Multiplication by ψ increases the W^{1,p} norm by a factor of at
most 2 M, where M bounds both |ψ| and ‖∇ψ‖. The two bounds enter separately: M scales
the value and the ψ ∇u half of the gradient, while the second M pays for the Leibniz error
u ∇ψ, which is why a bound on ψ alone cannot suffice.
Multiplication by a smooth cutoff, as a continuous linear operator on W^{1,p}(Ω), of
norm at most 2 M.
Equations
- TauCeti.W1p.contDiffSMulL psi hpsi hM hpsiM hgradM = { toFun := TauCeti.W1p.contDiffSMul psi hpsi hM hpsiM hgradM, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (2 * M) ⋯
Instances For
The L² Leibniz estimate #
The L² Leibniz estimate. At exponent two, the gradient ψ ∇u + u ∇ψ of ψ u satisfies
‖∇(ψ u)‖₂² ≤ 2 ∫_Ω ψ² ‖∇u‖² + 2 ∫_Ω ‖∇ψ‖² u².
Unlike TauCeti.W1p.norm_contDiffSMul_le, the two terms keep their weights ψ² and ‖∇ψ‖²,
which is the form in which energy estimates such as Caccioppoli's inequality are applied to a
localized function.
The zero-boundary subspace is preserved #
Multiplying a test function by a smooth ψ gives the test function ψ φ, whichever of the
two orders — multiply then embed, or embed then multiply — is used.
W^{1,p}_0(Ω) is stable under multiplication by a smooth cutoff. Since ψ φ is again a
test function supported in Ω, the operator maps the generating test-function jets back into
W^{1,p}_0(Ω), and continuity extends that to their closure. This is the form the localization
arguments of Lane A use, because a cutoff must not create a boundary trace.
The operator norm of multiplication by ψ is at most 2 M.