Leibniz rule for a W^{1,∞} weight

EllipticPdes.Regularity.HasWeakDerivOn.mul_contDiff_left proves the weak-derivative product rule for a C¹ weight. Guo's hypothesis supplies no classical derivative, and this file replaces that route.

Smooth case

For a weight that is already C^∞, no mollification is needed at all and no product rule for weak derivatives has to be proved: b · φ is itself a smooth compactly supported test function supported where φ is, so it may be fed straight to HasWeakDerivOn, and the classical Leibniz rule splits the result. That is weakDerivOn_smul_test_contDiff below, the whole content of the mollified stage.

Entry point of the weak hypothesis

The mollification a ⋆ ρ_ε of a W^{1,∞} weight is C^∞, and its derivative is the mollification of the weak derivative (partialD_convolution_eq_of_hasWeakPartial). Feeding it to the smooth case gives the identity for every ε, and what remains is to pass to the limit.

Passing to the limit

The C¹ route mollifies and lets dominated convergence take the limit, which needs a ⋆ ρ_ε → a pointwise and so needs a continuous. A merely measurable weight has no such convergence, and the limit is taken in L² instead: the pairing is bounded by Cauchy-Schwarz (abs_setIntegral_mul_le), leaving ‖a ⋆ ρ_ε - a‖_{L²} on the support of the test function.

A bounded weight lies in no Lᵖ on the whole space, so the L² convergence of EllipticPdes.Embedding.tendsto_eLpNorm_convolution_sub does not apply to a itself. It applies to the truncation a · 1_B on a large ball, and convolution_congr_of_eqOn says the truncation changes the mollification nowhere near the test function once the kernel radius is below the margin. That is tendsto_setIntegral_mul_convolution_of_measurable, which replaces the C¹-weight dominated-convergence lemma and is applied three times, once per term.

Main declarations

• weakDerivOn_smul_test_contDiff: the identity for a C^∞ weight, with no mollification.
• abs_setIntegral_mul_le: Cauchy-Schwarz, with the second factor left as an eLpNorm.
• tendsto_setIntegral_mul_convolution_of_measurable: the mollification limit against an L² class, for a weight that is measurable and essentially bounded and nothing more.
• HasWeakDerivOn.mul_isWkInfty_left: the Leibniz rule for a W^{1,∞} weight.

theorem EllipticPdes.Regularity.memLp_two_restrict_of_continuous_hasCompactSupport {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {h : EuclideanSpace ℝ (Fin d) → ℝ} (hc : Continuous h) (hcs : HasCompactSupport h) : MeasureTheory.MemLp h 2 (MeasureTheory.volume.restrict V)

A continuous compactly supported function is in L² of any restricted Lebesgue measure.

theorem EllipticPdes.Regularity.weakDerivOn_smul_test_contDiff {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (ℓ : Fin d) {g g' : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict V))} (hg : HasWeakDerivOn V ℓ g g') {b : EuclideanSpace ℝ (Fin d) → ℝ} (hb : ContDiff ℝ (↑⊤) b) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφc : ContDiff ℝ (↑⊤) φ) (hφcs : HasCompactSupport φ) (hφV : tsupport φ ⊆ V) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑g x * (b x * Sobolev.partialD ℓ φ x) = -∫ (x : EuclideanSpace ℝ (Fin d)) in V, (↑↑g' x * b x + ↑↑g x * Sobolev.partialD ℓ b x) * φ x

Leibniz identity for a C^∞ weight. If g has weak ℓ-derivative g' on V and b is smooth, then for every test function φ supported in V,

∫_V g · (b · ∂_ℓφ) = - ∫_V (g' · b + g · ∂_ℓ b) · φ.

No mollification and no product rule for weak derivatives is involved: b · φ is a smooth compactly supported test function supported inside V, so HasWeakDerivOn applies to it directly, and the classical Leibniz rule splits the derivative of the product.

Pairing against an L² class

theorem EllipticPdes.Regularity.abs_setIntegral_mul_le {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (h : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict V))) {F : EuclideanSpace ℝ (Fin d) → ℝ} (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict V)) : |∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑h x * F x| ≤ ‖h‖ * (MeasureTheory.eLpNorm F 2 (MeasureTheory.volume.restrict V)).toReal

Cauchy-Schwarz on a restricted measure. The pairing of an L²(V) class with an L²(V) function is bounded by the product of the norms, with the second factor left as an eLpNorm so that a convergence statement about eLpNorm transfers to the pairing with no further work.

theorem EllipticPdes.Regularity.memLp_two_restrict_mul_of_ae_bound {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {c η : EuclideanSpace ℝ (Fin d) → ℝ} (hcm : Measurable c) {M : ℝ} (hcM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |c x| ≤ M) (hηc : Continuous η) (hηcs : HasCompactSupport η) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin d)) => c x * η x) 2 (MeasureTheory.volume.restrict V)

An essentially bounded measurable function times a continuous compactly supported one is in L² of any restricted Lebesgue measure. The bound is not assumed non-negative, so the proof compares against max M 0.

Mollification limit for a measurable weight

theorem EllipticPdes.Regularity.tendsto_setIntegral_mul_convolution_of_measurable {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (φ : ℕ → ContDiffBump 0) (hφ : Filter.Tendsto (fun (n : ℕ) => (φ n).rOut) Filter.atTop (nhds 0)) (hφK : ∀ (n : ℕ), (φ n).rOut ≤ 2 * (φ n).rIn) {c : EuclideanSpace ℝ (Fin d) → ℝ} (hcm : Measurable c) {Mc : ℝ} (hcM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |c x| ≤ Mc) (h : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict V))) {η : EuclideanSpace ℝ (Fin d) → ℝ} (hηc : Continuous η) (hηcs : HasCompactSupport η) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑h x * (MeasureTheory.convolution c ((φ n).normed MeasureTheory.volume) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x * η x)) Filter.atTop (nhds (∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑h x * (c x * η x)))

Mollification limit against an L² class. For a measurable, essentially bounded c, an L²(V) class h and a continuous compactly supported η,

∫_V h · ((c ⋆ ρ_ε) · η) → ∫_V h · (c · η).

Continuity of c is not assumed, so c ⋆ ρ_ε → c pointwise is unavailable and the limit is taken in L². Cauchy-Schwarz leaves ‖(c ⋆ ρ_ε - c) · η‖_{L²}, which sees c only on the compact support of η. Replacing c there by its truncation to a large closed ball, which convolution_congr_of_eqOn shows to change nothing once the kernel radius is under the margin, puts the difference inside the reach of tendsto_eLpNorm_convolution_sub.

Leibniz rule

theorem EllipticPdes.Regularity.HasWeakDerivOn.mul_isWkInfty_left {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (ℓ : Fin d) {g g' : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict V))} (hg : HasWeakDerivOn V ℓ g g') {a a' : EuclideanSpace ℝ (Fin d) → ℝ} (ham : Measurable a) (ha'm : Measurable a') (ha : HasWeakPartial ℓ a a') {Ma Mda : ℝ} (haM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |a x| ≤ Ma) (hdaM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |a' x| ≤ Mda) (ag : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict V))) (hag : ↑↑ag =ᵐ[MeasureTheory.volume.restrict V] fun (x : EuclideanSpace ℝ (Fin d)) => a x * ↑↑g x) (dag : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict V))) (hdag : ↑↑dag =ᵐ[MeasureTheory.volume.restrict V] fun (x : EuclideanSpace ℝ (Fin d)) => a' x * ↑↑g x + a x * ↑↑g' x) : HasWeakDerivOn V ℓ ag dag

Weak-derivative Leibniz with a W^{1,∞} weight. If g has weak ℓ-derivative g' on V, and a is measurable and essentially bounded with an essentially bounded weak ℓ-derivative a', then a·g has weak ℓ-derivative a'·g + a·g' on V.

This is HasWeakDerivOn.mul_contDiff_left with the C¹ hypothesis on the weight removed, which is what Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) asks for. The weight is mollified, the smooth case weakDerivOn_smul_test_contDiff gives the identity at every radius, and tendsto_setIntegral_mul_convolution_of_measurable sends each of the three terms to its limit.