Mollifying a W^{1,∞} weight

EllipticPdes.Regularity.HasWeakDerivOn.mul_contDiff_left proves the weak-derivative Leibniz rule for a C¹ weight, by mollifying the weight and differentiating the mollification classically. Guo's hypothesis supplies no classical derivative, so that route is closed and the mollification has to take the weak derivative instead. This file rebuilds the two facts about mollification the Leibniz rule needs, with continuity of the weight dropped throughout.

• The sup bound survives with measurability alone. EllipticPdes.Regularity already had this for a continuous weight; continuity entered only through the integrability of the convolution integrand, which an essential bound supplies just as well.
• The derivative of the mollification is the mollification of the weak derivative. This is where the weak hypothesis does the work: the classical proof moves the derivative from the kernel back onto the weight by integration by parts, and HasWeakPartial is that integration-by-parts identity, applied to the reflected kernel t ↦ ρ (x - t), which is a legitimate test function. The weak version is shorter than the C¹ version it replaces.

Main declarations

• abs_convolution_le_of_measurable: a mollification inherits an essential sup bound, at every point.
• partialD_convolution_eq_of_hasWeakPartial: ∂_ℓ (a ⋆ ρ) = a' ⋆ ρ when a' is the weak ℓ-derivative of a.

theorem EllipticPdes.Regularity.convolution_lsmul_apply {d : ℕ} (F K : EuclideanSpace ℝ (Fin d) → ℝ) (y : EuclideanSpace ℝ (Fin d)) : MeasureTheory.convolution F K (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume y = ∫ (t : EuclideanSpace ℝ (Fin d)), F t * K (y - t)

The scalar convolution written as an integral. convolution_def states it with the lsmul action; over ℝ that action is multiplication.

Sup bound with no continuity assumed

theorem EllipticPdes.Regularity.abs_convolution_le_of_measurable {d : ℕ} {ρ : EuclideanSpace ℝ (Fin d) → ℝ} (hρ0 : 0 ≤ ρ) (hρc : Continuous ρ) (hρcs : HasCompactSupport ρ) (hρ1 : ∫ (y : EuclideanSpace ℝ (Fin d)), ρ y = 1) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hhm : Measurable h) {M : ℝ} (hM : ∀ᵐ (t : EuclideanSpace ℝ (Fin d)), |h t| ≤ M) (x : EuclideanSpace ℝ (Fin d)) : |MeasureTheory.convolution h ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x| ≤ M

Sup bound for a mollification of an essentially bounded weight. If h is measurable and bounded by M almost everywhere, and ρ is a non-negative continuous compactly supported kernel of unit mass, then h ⋆ ρ is bounded by M at every point.

Continuity of h is unused. It entered the C¹ version only to make the integrand |h t| · ρ (x - t) integrable, and domination by M · ρ (x - t) does that under an essential bound alone.

theorem EllipticPdes.Regularity.convolution_congr_of_eqOn {d : ℕ} {a b ρ : EuclideanSpace ℝ (Fin d) → ℝ} {x : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hρsupp : ∀ (y : EuclideanSpace ℝ (Fin d)), r ≤ ‖y‖ → ρ y = 0) (heq : ∀ (t : EuclideanSpace ℝ (Fin d)), ‖x - t‖ < r → a t = b t) : MeasureTheory.convolution a ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x = MeasureTheory.convolution b ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Locality of a mollification. If the kernel vanishes outside the ball of radius r and two weights agree on the ball of radius r about x, their mollifications agree at x. This is what lets a globally bounded weight, which lies in no Lᵖ on the whole space, be replaced near a compact set by a truncation that does, without changing the mollification there.

Derivative of a mollification from the weak derivative

theorem EllipticPdes.Regularity.contDiff_reflect {d : ℕ} {ρ : EuclideanSpace ℝ (Fin d) → ℝ} (hρcd : ContDiff ℝ (↑⊤) ρ) (x : EuclideanSpace ℝ (Fin d)) : ContDiff ℝ ↑⊤ fun (t : EuclideanSpace ℝ (Fin d)) => ρ (x - t)

Reflected kernel as a test function. For a smooth compactly supported ρ, the map t ↦ ρ (x - t) is smooth with compact support, so HasWeakPartial may be applied to it.

theorem EllipticPdes.Regularity.partialD_reflect {d : ℕ} {ρ : EuclideanSpace ℝ (Fin d) → ℝ} (hρcd : ContDiff ℝ (↑⊤) ρ) (ℓ : Fin d) (x t : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD ℓ (fun (s : EuclideanSpace ℝ (Fin d)) => ρ (x - s)) t = -Sobolev.partialD ℓ ρ (x - t)

The classical partial derivative of the reflected kernel is the reflection of the partial derivative, with a sign: ∂_ℓ (t ↦ ρ (x - t)) = -(∂_ℓ ρ) (x - t).

theorem EllipticPdes.Regularity.partialD_convolution_eq_of_hasWeakPartial {d : ℕ} {ℓ : Fin d} {a a' : EuclideanSpace ℝ (Fin d) → ℝ} (haLI : MeasureTheory.LocallyIntegrable a MeasureTheory.volume) (ha : HasWeakPartial ℓ a a') {ρ : EuclideanSpace ℝ (Fin d) → ℝ} (hρcd : ContDiff ℝ (↑⊤) ρ) (hρcs : HasCompactSupport ρ) : Sobolev.partialD ℓ (MeasureTheory.convolution a ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) = MeasureTheory.convolution a' ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

Derivative of a mollified W^{1,∞} weight is the mollification of its weak derivative. For a with weak ℓ-derivative a' and a smooth compactly supported kernel ρ, ∂_ℓ (a ⋆ ρ) = a' ⋆ ρ.

The derivative first passes to the kernel, ∂_ℓ (a ⋆ ρ) = a ⋆ ∂_ℓ ρ, which needs only local integrability of a. Moving it back onto a is where the C¹ proof integrates by parts, and here it is the hypothesis: HasWeakPartial applied to the reflected kernel t ↦ ρ (x - t) states exactly that identity, and partialD_reflect supplies the sign.