Multiplying an iterated weak derivative by a W^{k,∞} weight

The datum of the differentiated equation is a sum of products, each a coefficient against a derivative of the solution. Feeding that datum back into the induction of Guo, Partial Differential Equations I and II (Course Lecture Notes), Theorem VIII.3.2 (p. 65) needs weak derivatives of the product up to order k, with a bound. This file supplies them.

Recursion

HasWeakDerivOn.mul_isWkInfty_left gives one derivative of a·g, namely (∂_ℓ a)·g + a·(∂_ℓ g). Both summands are again products of a W^{k,∞} weight with a function with k weak derivatives, so the statement recurses on its own conclusion. The family for a·g at order k + 1 is therefore assembled rather than written down: the empty list is the product itself, and a list ℓ :: α reads the order-k family built for the ℓ-derivative.

No Leibniz formula over subsets of the index list appears, and none is needed. Naming the derivative of each order through the recursion avoids the combinatorial statement altogether, with a constant that is existentially quantified rather than computed. The estimate of Theorem VIII.3.2 quantifies its constant before the solution and the datum and says nothing about its size, so nothing is lost.

Main declarations

• HasWeakDerivOn.add, HasIteratedWeakDerivOn.add: sums.
• mulL2: a bounded measurable weight acting on an L²(V) class.
• exists_iteratedWeakDeriv_mul: the product has k weak derivatives, with a bound linear in the bound on the family of g.

Sums

theorem EllipticPdes.Regularity.HasWeakDerivOn.add {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {ℓ : Fin d} {g g' h h' : Sobolev.L2D V} (hg : HasWeakDerivOn V ℓ g g') (hh : HasWeakDerivOn V ℓ h h') : HasWeakDerivOn V ℓ (g + h) (g' + h')

A weak derivative of a sum is the sum of the weak derivatives.

noncomputable def EllipticPdes.Regularity.HasIteratedWeakDerivOn.add {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {g h : Sobolev.L2D V} (hg : HasIteratedWeakDerivOn V k g) (hh : HasIteratedWeakDerivOn V k h) : HasIteratedWeakDerivOn V k (g + h)

The order-k family of a sum, entry by entry.

Equations

• hg.add hh = { D := fun (α : List (Fin d)) => hg.D α + hh.D α, D_nil := ⋯, D_step := ⋯ }

Bounded weight acting on an L² class

noncomputable def EllipticPdes.Regularity.mulL2 {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {a : EuclideanSpace ℝ (Fin d) → ℝ} (ham : Measurable a) {M : ℝ} (haM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |a x| ≤ M) (g : Sobolev.L2D V) : Sobolev.L2D V

Bounded measurable weight acting on L²(V). The bound is asked on the whole space rather than on V, which is the form every W^{k,∞} bundle has.

Equations

• EllipticPdes.Regularity.mulL2 ham haM g = (EllipticPdes.Sobolev.mulCoeffL ham ⋯) g

theorem EllipticPdes.Regularity.mulL2_coeFn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {a : EuclideanSpace ℝ (Fin d) → ℝ} (ham : Measurable a) {M : ℝ} (haM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |a x| ≤ M) (g : Sobolev.L2D V) : ↑↑(mulL2 ham haM g) =ᵐ[MeasureTheory.volume.restrict V] fun (x : EuclideanSpace ℝ (Fin d)) => a x * ↑↑g x

The pointwise a.e. representative of the weighted class.

theorem EllipticPdes.Regularity.norm_le_of_ae_mul {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {a : EuclideanSpace ℝ (Fin d) → ℝ} (ham : Measurable a) {M : ℝ} (haM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |a x| ≤ M) {g ag : Sobolev.L2D V} (hag : ↑↑ag =ᵐ[MeasureTheory.volume.restrict V] fun (x : EuclideanSpace ℝ (Fin d)) => a x * ↑↑g x) : ‖ag‖ ≤ M * ‖g‖

Any class representing the product is bounded by the weight's bound. Stated for an arbitrary representative rather than for mulL2 itself, because the consumers of the product rule name their own class.

Product rule at every order

theorem EllipticPdes.Regularity.exists_iteratedWeakDeriv_mul {d : ℕ} (k : ℕ) {a : EuclideanSpace ℝ (Fin d) → ℝ} : ∀ (a✝ : IsWkInfty a k), ∃ (K : ℝ), 0 ≤ K ∧ ∀ {V : Set (EuclideanSpace ℝ (Fin d))} {g ag : Sobolev.L2D V} (hg : HasIteratedWeakDerivOn V k g), (↑↑ag =ᵐ[MeasureTheory.volume.restrict V] fun (x : EuclideanSpace ℝ (Fin d)) => a x * ↑↑g x) → ∀ {M : ℝ}, IteratedL2Bound hg M → ∃ (H : HasIteratedWeakDerivOn V k ag), IteratedL2Bound H (K * M)

Preservation of k weak derivatives by a W^{k,∞} weight. For a ∈ W^{k,∞} there is a constant K, depending on the bundle alone, such that whenever g has weak derivatives to order k on V bounded by M, every class representing a·g has weak derivatives to order k bounded by K·M.

The induction is on k. The step applies HasWeakDerivOn.mul_isWkInfty_left once to obtain ∂_ℓ(a·g) = (∂_ℓ a)·g + a·(∂_ℓ g), then the induction hypothesis to each summand, the first with the weight ∂_ℓ a ∈ W^{k,∞} and the second with the function ∂_ℓ g, whose order-k family is HasIteratedWeakDerivOn.deriv.