Compactly supported smooth approximation for whole-space Sobolev families

Finite families of whole-space Sobolev functions admit smooth compactly supported approximations in every derivative represented by the family.

noncomputable def CKN.localSobolevMollifyProfile : Foundation.Parabolic.Vec3 → ℝ

A smooth cutoff equal to one on the unit ball and supported in the ball of radius two.

Equations

• CKN.localSobolevMollifyProfile = Classical.choose CKN.localSobolevMollifyProfile._proof_4

noncomputable def CKN.localSobolevMollifyScale (n : ℕ) : ℝ

The inverse scale for cutoffs exhausting the whole spatial domain.

Equations

• CKN.localSobolevMollifyScale n = (2 * (↑n + 1))⁻¹

noncomputable def CKN.localSobolevMollifyCutoff (n : ℕ) : Foundation.Parabolic.Vec3 → ℝ

The scaled cutoff used in the compactly supported Sobolev approximants.

Equations

• CKN.localSobolevMollifyCutoff n x = CKN.localSobolevMollifyProfile (CKN.localSobolevMollifyScale n • x)

noncomputable def CKN.localSobolevMollifyFamily {ι : Type u_1} (f : ι → Foundation.Parabolic.Vec3 → ℝ) (ε : ℝ) (hε : 0 < ε) : Foundation.Parabolic.Vec3 → ι → ℝ

Coordinatewise mollification of the vector-valued family.

Equations

• CKN.localSobolevMollifyFamily f ε hε x i = CKN.mollify (f i) ε hε x

def CKN.localSobolevMollifyTail (n : ℕ) : Set Foundation.Parabolic.Vec3

The exterior region controlling the error of the spatial cutoff.

Equations

• CKN.localSobolevMollifyTail n = {x : CKN.Foundation.Parabolic.Vec3 | ↑n + 1 < CKN.Foundation.Parabolic.vec3EuclideanNorm x}

noncomputable def CKN.localSobolevMollifyRemainder (n : ℕ) : Foundation.Parabolic.Vec3 → ℝ

The complementary cutoff measuring the part removed from each approximant.

Equations

• CKN.localSobolevMollifyRemainder n = (fun (x : CKN.Foundation.Parabolic.Vec3) => 1) - CKN.localSobolevMollifyCutoff n

theorem CKN.sobolevFamily_smooth_approx {ι : Type u_1} [Fintype ι] {m : ℕ} {f : ι → Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → ι → Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (i : ι), IsSobolevFamilyOn m Set.univ (f i) fun (x : List (Fin 3)) => D x i) : ∃ (g : ℕ → ι → Foundation.Parabolic.Vec3 → ℝ), (∀ (n : ℕ) (i : ι), ContDiff ℝ (↑⊤) (g n i)) ∧ (∀ (n : ℕ) (i : ι), HasCompactSupport (g n i)) ∧ (∀ (i : ι) (α : List (Fin 3)), α.length ≤ m → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (wordDeriv α (g n i) - D α i) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ ∀ (M : ℝ), (∀ᵐ (x : Foundation.Parabolic.Vec3), √(∑ i : ι, f i x ^ 2) ≤ M) → ∀ (n : ℕ) (x : Foundation.Parabolic.Vec3), √(∑ i : ι, g n i x ^ 2) ≤ M

Every finite whole-space Sobolev family has smooth compactly supported approximations in all represented derivatives, with the same vector-valued essential supremum bound.