Support Thickening

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Support, mollifier support, and thickening lemmas

These five results were previously private lemmas in CKN/Foundation/Euclidean/RieszSecondExterior.lean (the d = 3 versions) and CKN/Foundation/Sobolev/Mollify/LpApproximation.lean (the general d version of mollifier_tsupp_eq_closedBall). They are collected here as public theorems.

theorem CKN.support_subset_closure_of_zero_outside {b : Foundation.Parabolic.Vec3 → ℝ} {A : Set Foundation.Parabolic.Vec3} (hbA : ∀ y ∉ A, b y = 0) : Function.support b ⊆ closure A

If a function b vanishes outside a set A, then its support is contained in the closure of A.

theorem CKN.mollifier_tsupp_eq_closedBall {d : ℕ} {ε : ℝ} (hε : 0 < ε) : tsupport (mollifier ε hε) = Metric.closedBall 0 ε

The topological support of the normalized mollifier kernel of radius ε > 0 in any dimension d is exactly the closed ball of radius ε centred at 0.

theorem CKN.mollify_support_subset {b : Foundation.Parabolic.Vec3 → ℝ} {A : Set Foundation.Parabolic.Vec3} {δ ε : ℝ} (hε : 0 < ε) (hbA : ∀ y ∉ A, b y = 0) (hεA : ε ≤ δ) : Function.support (mollify b ε hε) ⊆ Metric.closedBall 0 δ + closure A

The support of mollify b ε hε is contained in the Minkowski sum of the closed ball of radius δ and the closure of A, provided b vanishes outside A and ε ≤ δ.

theorem CKN.thickening_compact {A : Set Foundation.Parabolic.Vec3} (hAb : Bornology.IsBounded A) {δ : ℝ} : IsCompact (Metric.closedBall 0 (δ / 12) + closure A)

The Minkowski sum of a closed ball of radius δ/12 and the closure of a bounded set A is compact.

theorem CKN.thickening_separated {A U : Set Foundation.Parabolic.Vec3} {δ : ℝ} (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Foundation.Parabolic.vec3EuclideanNorm (x - y)) (x : Foundation.Parabolic.Vec3) : x ∈ U → ∀ y ∈ Metric.closedBall 0 (δ / 12) + closure A, δ / 2 ≤ Foundation.Parabolic.vec3EuclideanNorm (x - y)

If points in U are at Euclidean distance at least δ from A, then every point of the thickening closed ball (δ/12) + closure A is at distance at least δ/2 from every point of U.