Integration by parts against a C¹ test function

HasWeakGradOn asks for the integration-by-parts identity against smooth test functions. The extension operator needs it against a C¹ one: a boundary chart of a C¹ domain is C¹, so a smooth test function pulled back through it is C¹ and no better.

Mollification supplies the smooth test functions. The mollification of a C¹ class of compact support is smooth, its support sits in a closed thickening of the original, its partial derivatives are the mollified partial derivatives, and both stay bounded by the suprema of the originals while converging pointwise. Dominated convergence passes the identity.

Main declarations

• EllipticPdes.Extension.partialD_convolution_normed: the partial derivative of a mollification is the mollification of the partial derivative.
• EllipticPdes.Extension.norm_convolution_normed_le: a mollification is bounded by the supremum of what it mollifies.
• EllipticPdes.Extension.hasWeakGradOn_contDiffOne: the identity of a weak gradient, against a C¹ test function.

theorem EllipticPdes.Extension.partialD_convolution_normed {d : ℕ} (ρ : ContDiffBump 0) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hψ : ContDiff ℝ 1 ψ) (hψcs : HasCompactSupport ψ) (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD k (MeasureTheory.convolution (ρ.normed MeasureTheory.volume) ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) x = MeasureTheory.convolution (ρ.normed MeasureTheory.volume) (Sobolev.partialD k ψ) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Partial derivative of a mollification. For ψ of class C¹ with compact support, ρ ⋆ ψ is differentiable and its partial derivatives are the mollified partial derivatives.

theorem EllipticPdes.Extension.norm_convolution_normed_le {d : ℕ} (ρ : ContDiffBump 0) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hc : Continuous h) (hcs : HasCompactSupport h) {M : ℝ} (hM : ∀ (y : EuclideanSpace ℝ (Fin d)), ‖h y‖ ≤ M) (x : EuclideanSpace ℝ (Fin d)) : ‖MeasureTheory.convolution (ρ.normed MeasureTheory.volume) h (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x‖ ≤ M

Bound on a mollification by what it mollifies. The normed bump is a probability density, so the convolution is an average and inherits the bound.

theorem EllipticPdes.Extension.hasWeakGradOn_contDiffOne {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} (hBopen : IsOpen B) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u B MeasureTheory.volume) (hgi : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g k) B MeasureTheory.volume) (hwg : Embedding.HasWeakGradOn B u g) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hψ : ContDiff ℝ 1 ψ) (hψcs : HasCompactSupport ψ) (hψs : tsupport ψ ⊆ B) (k : Fin d) : ∫ (x : EuclideanSpace ℝ (Fin d)) in B, u x * Sobolev.partialD k ψ x = -∫ (x : EuclideanSpace ℝ (Fin d)) in B, g k x * ψ x

Integration by parts against a C¹ test function. A weak gradient on an open set satisfies its defining identity against every C¹ function of compact support inside the set, and not only against the smooth ones the definition names.