Spatial mollification of Leray data

These definitions and estimates prepare the smooth approximation step in lem:J-weak-div.

noncomputable def CKN.spatialMollifyVec3 (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ε : ℝ) (hε : 0 < ε) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

Componentwise spatial mollification of a three-dimensional vector field.

Equations

• CKN.spatialMollifyVec3 a ε hε x i = CKN.mollify (fun (y : CKN.Vec 3) => a y i) ε hε x

theorem CKN.spatialMollifyVec3_contDiff {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {ε : ℝ} (hε : 0 < ε) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : ContDiff ℝ (↑⊤) (spatialMollifyVec3 a ε hε)

Spatial mollification makes every component smooth.

theorem CKN.spatialMollifyVec3_memLp {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {ε : ℝ} (hε : 0 < ε) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : MeasureTheory.MemLp (spatialMollifyVec3 a ε hε) 2 MeasureTheory.volume

Spatial mollification preserves square integrability componentwise.

theorem CKN.spatialMollifyVec3_tendsto_L2 {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (spatialMollifyVec3 a (1 / ↑(n + 1)) ⋯ - a) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

Spatial mollification converges in L² for vector fields in L².

theorem CKN.spatialMollifyVec3_divergence_eq_zero {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {ε : ℝ} (hε : 0 < ε) (ha : IsWeakDivFreeL2 a) (x : Foundation.Parabolic.Vec3) : ∑ i : Fin 3, spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => spatialMollifyVec3 a ε hε y i) i x = 0

Spatial mollification preserves weak divergence-freeness pointwise.