Bounded smooth multiplication in zero-boundary Sobolev spaces

Multiplication by a smooth scalar function whose derivatives through order k are bounded by M preserves W^{k,p}_0(Ω), with operator norm at most 2^(k+1) M. This holds for 1 ≤ p ≤ ∞ on any open domain, without boundary regularity. The estimate includes every recorded weak derivative in the iterated graph norm.

The underlying estimate, TauCeti.Wkp.norm_ofTestFunctionₗ_le_of_eqOn_mul, needs only that the multiplied function be a Cᵏ representative f of some u ∈ W^{k,p}(Ω): a test function equal to ψ f on Ω has norm at most 2^(k+1) M ‖u‖. It controls the error when a smooth approximation is multiplied by a fixed cutoff. Extending the resulting map on test functions to their closure gives the zero-boundary operator. This file does not assert multiplication on all of W^{k,p}(Ω).

References

L. C. Evans, Partial Differential Equations, §5.2.3 and §5.3.2.

Adapted from Tau Ceti contribution #12418, Bound smooth multiplication in higher-order zero-boundary Sobolev spaces.

theorem TauCeti.Wkp.norm_ofTestFunctionₗ_le_of_eqOn_mul {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ i ≤ k, ∀ x ∈ Omega, ‖iteratedFDeriv ℝ i psi x‖ ≤ M) (u : Wkp mu Omega p k) {f : E → ℝ} (hf : ContDiffOn ℝ (↑k) f ↑Omega) (hu : ↑↑(value k u) =ᵐ[mu.restrict ↑Omega] f) (Phi : TestFunction Omega ℝ ⊤) (hPhi : Set.EqOn (⇑Phi) (fun (x : E) => psi x * f x) ↑Omega) : ‖(ofTestFunctionₗ k) Phi‖ ≤ 2 ^ (k + 1) * M * ‖u‖

Let u ∈ W^{k,p}(Ω) have a representative f which is Cᵏ on Ω. If a test function Phi agrees on Ω with the product of f and a smooth scalar function whose derivatives through order k are bounded by M, then the full W^{k,p} norm of Phi is at most 2^(k+1) M ‖u‖.

theorem TauCeti.Wkp.norm_ofTestFunctionₗ_bilinLeftCLM_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ i ≤ k, ∀ x ∈ Omega, ‖iteratedFDeriv ℝ i psi x‖ ≤ M) (phi : TestFunction Omega ℝ ⊤) : ‖(ofTestFunctionₗ k) ((TestFunction.bilinLeftCLM (ContinuousLinearMap.lsmul ℝ ℝ) hpsi) phi)‖ ≤ 2 ^ (k + 1) * M * ‖(ofTestFunctionₗ k) phi‖

Multiplying a test function by a smooth scalar function with derivatives through order k bounded by M increases its full W^{k,p} norm by at most 2^(k+1) M.

noncomputable def TauCeti.Wkp0.contDiffSMulL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) : ↥(Wkp0 mu Omega p k) →L[ℝ] ↥(Wkp0 mu Omega p k)

A continuous linear endomorphism associated to a smooth scalar function on W^{k,p}_0(Ω). When the derivatives through order k are bounded on Ω, its action on test functions is characterized by contDiffSMulL_apply_ofTestFunction.

theorem TauCeti.Wkp0.contDiffSMulL_apply_ofTestFunction {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ i ≤ k, ∀ x ∈ Omega, ‖iteratedFDeriv ℝ i psi x‖ ≤ M) (phi : TestFunction Omega ℝ ⊤) : (contDiffSMulL k hpsi) ((ofTestFunctionₗ k) phi) = (ofTestFunctionₗ k) ((TestFunction.bilinLeftCLM (ContinuousLinearMap.lsmul ℝ ℝ) hpsi) phi)

On a test function, zero-boundary smooth multiplication is ordinary pointwise multiplication. The product remains a test function in the same domain.

theorem TauCeti.Wkp0.lowerOrderL_contDiffSMulL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ i ≤ k + 1, ∀ x ∈ Omega, ‖iteratedFDeriv ℝ i psi x‖ ≤ M) (u : ↥(Wkp0 mu Omega p (k + 1))) : (lowerOrderL k) ((contDiffSMulL (k + 1) hpsi) u) = (contDiffSMulL k hpsi) ((lowerOrderL k) u)

Smooth multiplication commutes with forgetting the highest weak derivative when the derivatives through order k + 1 are bounded on Ω.

theorem TauCeti.Wkp0.norm_contDiffSMulL_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ i ≤ k, ∀ x ∈ Omega, ‖iteratedFDeriv ℝ i psi x‖ ≤ M) : ‖contDiffSMulL k hpsi‖ ≤ 2 ^ (k + 1) * M

The norm of smooth multiplication on W^{k,p}_0(Ω) is bounded explicitly in terms of the Sobolev order and a common bound on the multiplier's derivatives.

theorem TauCeti.Wkp0.contDiffSMulL_unique {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ i ≤ k, ∀ x ∈ Omega, ‖iteratedFDeriv ℝ i psi x‖ ≤ M) (T : ↥(Wkp0 mu Omega p k) →L[ℝ] ↥(Wkp0 mu Omega p k)) (hT : ∀ (phi : TestFunction Omega ℝ ⊤), T ((ofTestFunctionₗ k) phi) = (ofTestFunctionₗ k) ((TestFunction.bilinLeftCLM (ContinuousLinearMap.lsmul ℝ ℝ) hpsi) phi)) : contDiffSMulL k hpsi = T

Smooth multiplication is the unique continuous linear endomorphism of W^{k,p}_0(Ω) with its stated action on test functions.

theorem TauCeti.Wkp0.value_contDiffSMulL_ae {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ i ≤ k, ∀ x ∈ Omega, ‖iteratedFDeriv ℝ i psi x‖ ≤ M) (u : ↥(Wkp0 mu Omega p k)) : ∀ᵐ (x : E) ∂mu.restrict ↑Omega, ↑↑(Wkp.value k ↑((contDiffSMulL k hpsi) u)) x = psi x * ↑↑(Wkp.value k ↑u) x

The value of zero-boundary smooth multiplication is represented almost everywhere by the pointwise product, at every order and including the infinite exponent.