The spatial mollifier of lem:aniso:comparison

The comparison argument mollifies in space with the standard family η_ε = ε^{-m} η(·/ε), where η is a fixed smooth nonnegative kernel of unit mass supported in the unit ball. The profile η is the normalized bump kernel of the ambient library, and the family is obtained from it by the explicit rescaling, so that the scaling identities below are available.

The bounds recorded here are the two that the commutator estimate of DiPerna and Lions needs: the kernel has unit mass and is supported in the ball of radius ε, and the integral of the length of its gradient is C_η/ε with C_η the corresponding integral for the profile. The ball is the one of the sup norm of Vec m, which is the norm carried by that type.

The fixed profile

noncomputable def CIV.mollifierProfile (m : ℕ) : CKN.Vec m → ℝ

The fixed mollifier profile η: the normalized smooth bump of radius one on Vec m.

Equations

• CIV.mollifierProfile m = CKN.mollifier 1 CIV.mollifierProfile._proof_1

theorem CIV.mollifierProfile_nonneg {m : ℕ} (x : CKN.Vec m) : 0 ≤ mollifierProfile m x

theorem CIV.contDiff_mollifierProfile {m : ℕ} : ContDiff ℝ (↑⊤) (mollifierProfile m)

theorem CIV.differentiable_mollifierProfile {m : ℕ} : Differentiable ℝ (mollifierProfile m)

theorem CIV.integral_mollifierProfile {m : ℕ} : ∫ (x : CKN.Vec m), mollifierProfile m x = 1

theorem CIV.hasCompactSupport_mollifierProfile {m : ℕ} : HasCompactSupport (mollifierProfile m)

theorem CIV.support_mollifierProfile {m : ℕ} : Function.support (mollifierProfile m) = Metric.ball 0 1

The profile is supported in the unit ball.

theorem CIV.mollifierProfile_eq_zero {m : ℕ} {x : CKN.Vec m} (hx : 1 ≤ ‖x‖) : mollifierProfile m x = 0

The rescaled family

noncomputable def CIV.mollifierKernel (m : ℕ) (ε : ℝ) : CKN.Vec m → ℝ

The rescaled kernel η_ε(x) = ε^{-m} η(x/ε).

Equations

• CIV.mollifierKernel m ε x = (ε ^ m)⁻¹ * CIV.mollifierProfile m (ε⁻¹ • x)

theorem CIV.mollifierKernel_nonneg {m : ℕ} {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) : 0 ≤ mollifierKernel m ε x

theorem CIV.contDiff_mollifierKernel {m : ℕ} (ε : ℝ) : ContDiff ℝ (↑⊤) (mollifierKernel m ε)

theorem CIV.differentiable_mollifierKernel {m : ℕ} (ε : ℝ) : Differentiable ℝ (mollifierKernel m ε)

theorem CIV.mollifierKernel_eq_zero {m : ℕ} {ε : ℝ} (hε : 0 < ε) {x : CKN.Vec m} (hx : ε ≤ ‖x‖) : mollifierKernel m ε x = 0

The kernel η_ε vanishes outside the ball of radius ε.

theorem CIV.hasCompactSupport_mollifierKernel {m : ℕ} {ε : ℝ} (hε : 0 < ε) : HasCompactSupport (mollifierKernel m ε)

theorem CIV.integrable_mollifierKernel {m : ℕ} {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (mollifierKernel m ε) MeasureTheory.volume

theorem CIV.integral_mollifierKernel {m : ℕ} {ε : ℝ} (hε : 0 < ε) : ∫ (x : CKN.Vec m), mollifierKernel m ε x = 1

The kernel η_ε has unit mass.

The gradient of the kernel

noncomputable def CIV.mollifierGradConst (m : ℕ) : ℝ

The gradient constant C_η = ∫ ∑_i |∂_iη| of the fixed profile.

Equations

• CIV.mollifierGradConst m = ∫ (x : CKN.Vec m), ∑ i : Fin m, |(fderiv ℝ (CIV.mollifierProfile m) x) (CKN.basisVec i)|

theorem CIV.mollifierGradConst_nonneg {m : ℕ} : 0 ≤ mollifierGradConst m

theorem CIV.fderiv_mollifierKernel_apply {m : ℕ} (ε : ℝ) (x v : CKN.Vec m) : (fderiv ℝ (mollifierKernel m ε) x) v = (ε ^ m)⁻¹ * (ε⁻¹ * (fderiv ℝ (mollifierProfile m) (ε⁻¹ • x)) v)

theorem CIV.integral_sum_abs_fderiv_mollifierKernel {m : ℕ} {ε : ℝ} (hε : 0 < ε) : ∫ (x : CKN.Vec m), ∑ i : Fin m, |(fderiv ℝ (mollifierKernel m ε) x) (CKN.basisVec i)| = mollifierGradConst m / ε

The scaling of the gradient integral: ∫ |∇η_ε| = C_η/ε.

theorem CIV.fderiv_mollifierKernel_eq_zero {m : ℕ} {ε : ℝ} (hε : 0 < ε) {w : CKN.Vec m} (hw : ε < ‖w‖) (v : CKN.Vec m) : (fderiv ℝ (mollifierKernel m ε) w) v = 0

The gradient of η_ε vanishes outside the ball of radius ε.

theorem CIV.continuous_fderiv_mollifierKernel {m : ℕ} (ε : ℝ) (v : CKN.Vec m) : Continuous fun (w : CKN.Vec m) => (fderiv ℝ (mollifierKernel m ε) w) v

theorem CIV.hasCompactSupport_fderiv_mollifierKernel {m : ℕ} {ε : ℝ} (hε : 0 < ε) (v : CKN.Vec m) : HasCompactSupport fun (w : CKN.Vec m) => (fderiv ℝ (mollifierKernel m ε) w) v

theorem CIV.integrable_sum_abs_fderiv_mollifierKernel {m : ℕ} {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (fun (w : CKN.Vec m) => ∑ i : Fin m, |(fderiv ℝ (mollifierKernel m ε) w) (CKN.basisVec i)|) MeasureTheory.volume