Multiplication in supercritical first-order Sobolev spaces

Let E have real dimension n and let p > n. Morrey's embedding gives every element of W^{1,p}(ℝⁿ) a canonical bounded continuous representative. Consequently the pointwise product of two Sobolev functions is again Sobolev, with the weak Leibniz rule

grad (u * v) = u * grad v + v * grad u.

This file packages that product on the whole-space Sobolev type, together with its representative- and gradient-level characterizations and its basic algebraic laws.

In dimension two this is the Sobolev multiplication input used for nonlinear Cauchy--Riemann operators on strips and surfaces. The dimension restriction is load-bearing: without an L^∞ bound on either factor, two L^p gradients cannot in general be multiplied by the other factor and remain in L^p.

Main declarations

• TauCeti.W1p.hasWeakFDerivOn_mul_morreyRepresentative: the weak Leibniz rule for the canonical Morrey representatives.
• TauCeti.W1p.mul: multiplication in W^{1,p}(ℝⁿ) for p > n.
• TauCeti.W1p.value_mul_ae and TauCeti.W1p.gradient_mul_ae: the characteristic formulas for the product.
• TauCeti.W1p.norm_mul_le: the multiplication estimate ‖u v‖ ≤ C ‖u‖ ‖v‖, with C three times the operator norm of Morrey's embedding.
• TauCeti.W1p.mulL: the product as a bounded bilinear map on W^{1,p}(ℝⁿ).

References

• R. A. Adams, J. J. F. Fournier, Sobolev Spaces, 2nd ed., Theorem 4.39.
• L. C. Evans, Partial Differential Equations, §5.6.3.

theorem TauCeti.W1p.hasWeakFDerivOn_mul_morreyRepresentative {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v : ↥(W1p mu ⊤ ↑p)) : HasWeakFDerivOn mu ⊤ (fun (x : E) => morreyRepresentative u hp x * morreyRepresentative v hp x) fun (x : E) => (innerSL ℝ) (morreyRepresentative u hp x • ↑↑(gradient v) x + morreyRepresentative v hp x • ↑↑(gradient u) x)

Weak Leibniz rule in the supercritical range. If p > dim E, the product of the canonical Morrey representatives of u and v has weak gradient u • ∇v + v • ∇u.

The statement uses the canonical continuous representatives because multiplication is not well-defined on arbitrary pointwise representatives of L^p classes.

noncomputable def TauCeti.W1p.mul {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v : ↥(W1p mu ⊤ ↑p)) : ↥(W1p mu ⊤ ↑p)

Multiplication of two whole-space W^{1,p} functions in the supercritical range p > dim E. The value is the pointwise product of their canonical Morrey representatives.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.W1p.value_mul_ae {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v : ↥(W1p mu ⊤ ↑p)) : ↑↑(value (mul hp u v)) =ᵐ[mu] fun (x : E) => morreyRepresentative u hp x * morreyRepresentative v hp x

The value of the supercritical Sobolev product is the pointwise product of the canonical Morrey representatives.

@[simp]

theorem TauCeti.W1p.morreyRepresentative_mul {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v : ↥(W1p mu ⊤ ↑p)) : morreyRepresentative (mul hp u v) hp = morreyRepresentative u hp * morreyRepresentative v hp

The canonical Morrey representative of a supercritical Sobolev product is the pointwise product of the representatives.

theorem TauCeti.W1p.gradient_mul_ae {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v : ↥(W1p mu ⊤ ↑p)) : ↑↑(gradient (mul hp u v)) =ᵐ[mu] fun (x : E) => morreyRepresentative u hp x • ↑↑(gradient v) x + morreyRepresentative v hp x • ↑↑(gradient u) x

The weak gradient of the supercritical Sobolev product satisfies the Leibniz rule.

theorem TauCeti.W1p.mul_comm {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v : ↥(W1p mu ⊤ ↑p)) : mul hp u v = mul hp v u

Supercritical Sobolev multiplication is commutative.

theorem TauCeti.W1p.mul_add {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v w : ↥(W1p mu ⊤ ↑p)) : mul hp u (v + w) = mul hp u v + mul hp u w

Supercritical Sobolev multiplication distributes over addition in the second factor.

theorem TauCeti.W1p.add_mul {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v w : ↥(W1p mu ⊤ ↑p)) : mul hp (u + v) w = mul hp u w + mul hp v w

Supercritical Sobolev multiplication distributes over addition in the first factor.

theorem TauCeti.W1p.mul_assoc {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v w : ↥(W1p mu ⊤ ↑p)) : mul hp (mul hp u v) w = mul hp u (mul hp v w)

Supercritical Sobolev multiplication is associative.

@[simp]

theorem TauCeti.W1p.mul_zero {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u : ↥(W1p mu ⊤ ↑p)) : mul hp u 0 = 0

Multiplication by zero on the right is zero.

@[simp]

theorem TauCeti.W1p.zero_mul {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u : ↥(W1p mu ⊤ ↑p)) : mul hp 0 u = 0

Multiplication by zero on the left is zero.

theorem TauCeti.W1p.mul_smul_comm {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (c : ℝ) (u v : ↥(W1p mu ⊤ ↑p)) : mul hp u (c • v) = c • mul hp u v

Scalar multiplication can be pulled out of the right factor.

theorem TauCeti.W1p.smul_mul_assoc {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (c : ℝ) (u v : ↥(W1p mu ⊤ ↑p)) : mul hp (c • u) v = c • mul hp u v

Scalar multiplication can be pulled out of the left factor.

The multiplication estimate

theorem TauCeti.W1p.norm_mul_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v : ↥(W1p mu ⊤ ↑p)) : ‖mul hp u v‖ ≤ 3 * ‖morreyEmbedding hp‖ * ‖u‖ * ‖v‖

The supercritical Sobolev multiplication estimate. The W^{1,p} norm of a product is at most three times the operator norm of Morrey's embedding times the product of the norms of the factors. The embedding norm is what enters because the only control on a factor outside L^p is the supremum norm of its Morrey representative.

noncomputable def TauCeti.W1p.mulL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) : ↥(W1p mu ⊤ ↑p) →L[ℝ] ↥(W1p mu ⊤ ↑p) →L[ℝ] ↥(W1p mu ⊤ ↑p)

Supercritical Sobolev multiplication as a bounded bilinear map on W^{1,p}(ℝⁿ). Its bound is TauCeti.W1p.norm_mul_le, and multiplication by a fixed factor is a bounded operator by TauCeti.W1p.norm_mulL_apply_le. This is the form the nonlinear estimates use, where a product must be differentiated and estimated in the Sobolev norm at once.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.W1p.mulL_apply {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u v : ↥(W1p mu ⊤ ↑p)) : ((mulL hp) u) v = mul hp u v

Evaluating the bundled multiplication recovers supercritical Sobolev multiplication.

theorem TauCeti.W1p.norm_mulL_apply_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u : ↥(W1p mu ⊤ ↑p)) : ‖(mulL hp) u‖ ≤ 3 * ‖morreyEmbedding hp‖ * ‖u‖

Multiplication by a fixed u is a bounded operator on W^{1,p}(ℝⁿ), of norm at most three times the operator norm of Morrey's embedding times ‖u‖.