Compactness Mollifier Support

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.eventually_reflected_mollifier_supported_in_open {K W : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hW : IsOpen W) (hKW : K ⊆ W) : ∃ (m₀ : ℕ), ∀ m ≥ m₀, ∀ x ∈ K, ∀ (y : Foundation.Parabolic.Vec3), mollifier (sliceRadius m) ⋯ (x - y) ≠ 0 → y ∈ W

On a compact subset of an open spatial neighborhood, all sufficiently small reflected mollifiers are supported inside that neighborhood.