Coarse-graining support: Support.Sobolev.W1p.InwardMollificationGeometry

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Inward mollification on bounded convex domains

This file records the geometric version of global mollification used for zero-boundary Sobolev approximation. The convolution is evaluated after an outward affine dilation. Consequently, its support is a compact set strictly inside the original bounded open convex domain.

noncomputable def HCPolySupport.inwardMollification {d : ℕ} (ρ g : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) : Vec d → ℝ

Mollify a global field at scale ε * r and pull the result back by the outward affine map based at x0.

Equations

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

@[simp]

theorem HCPolySupport.inwardMollification_apply {d : ℕ} (ρ g : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : inwardMollification ρ g x0 r ε x = MeasureTheory.convolution (scaledConvexApproxKernel ρ (ε * r)) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume ((1 + ε) • x - ε • x0)

def HCPolySupport.inwardMollificationSupportSet {d : ℕ} (U : Set (Vec d)) (x0 : Vec d) (r ε : ℝ) : Set (Vec d)

The affine contraction toward x0 of the sum of the radius-ε r closed ball and closure U, used to contain the inward mollification's support.

Equations

• HCPolySupport.inwardMollificationSupportSet U x0 r ε = (fun (y : HCPolySupport.Vec d) => (1 + ε)⁻¹ • y + (ε * (1 + ε)⁻¹) • x0) '' (Metric.closedBall 0 (ε * r) + closure U)

theorem HCPolySupport.contDiff_inwardMollification {d : ℕ} {ρ g : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) {x0 : Vec d} {r ε : ℝ} (hr : 0 < r) (hε : 0 < ε) : ContDiff ℝ (↑⊤) (inwardMollification ρ g x0 r ε)

A compactly supported smooth kernel convolved with a locally integrable field is smooth after the inward affine pullback.

theorem HCPolySupport.tsupport_inwardMollification_subset {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {ρ g : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hg_support : tsupport g ⊆ closure U) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε : 0 < ε) : tsupport (inwardMollification ρ g x0 r ε) ⊆ U

The topological support of inward mollification lies strictly in the domain, provided the input field is supported in the domain closure.

theorem HCPolySupport.hasCompactSupport_inwardMollification {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {ρ g : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hg_support : tsupport g ⊆ closure U) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε : 0 < ε) : HasCompactSupport (inwardMollification ρ g x0 r ε)

Inward mollification has compact support under the bounded-domain support condition.

theorem HCPolySupport.H10Function.tsupport_zeroExtension_subset_closure {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : tsupport u.zeroExtension ⊆ closure U

The literal zero extension of an H¹₀ function is supported in the closure of its domain.

theorem HCPolySupport.H10Function.inwardMollification_unit_properties {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε : 0 < ε) : ContDiff ℝ (↑⊤) (inwardMollification unitConvexApproxKernel u.zeroExtension x0 r ε) ∧ HasCompactSupport (inwardMollification unitConvexApproxKernel u.zeroExtension x0 r ε) ∧ tsupport (inwardMollification unitConvexApproxKernel u.zeroExtension x0 r ε) ⊆ U

The inward mollification of the global zero extension of an H¹₀ function is globally smooth, compactly supported, and has topological support strictly inside the original bounded open convex domain.