Gaussian collar covers in the velocity carrier

The bounded-overlap cover is first constructed in L2Vec3; this file transports it to the explicit Vec3 carrier used by the weak derivatives.

def ESS.buGaussianCoverCenterMap (p : Fin (Besicovitch.multiplicity CKN.BUGaussianSpace) × CKN.BUGaussianSpace) : Fin (Besicovitch.multiplicity CKN.BUGaussianSpace) × CKN.Foundation.Parabolic.Vec3

Transport a labeled Gaussian cover center from the Euclidean carrier to Vec3.

Equations

• ESS.buGaussianCoverCenterMap p = (p.1, CKN.Foundation.Parabolic.vec3Homeomorph.symm p.2)

theorem ESS.exists_buGaussian_transition_cover_vec3 (ρ r : ℝ) (hρ : 4 < ρ) (hr : 0 < r) (hrle : r ≤ 1 / 16) : ∃ (Y : Finset (Fin (Besicovitch.multiplicity CKN.BUGaussianSpace) × CKN.Foundation.Parabolic.Vec3)), (∀ p ∈ Y, CKN.Foundation.Parabolic.vec3EuclideanNorm p.2 ≤ ρ - 1 / 2) ∧ (∀ p ∈ Y, 13 * ρ / 20 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm p.2) ∧ (∀ (y : CKN.Foundation.Parabolic.Vec3), 13 * ρ / 20 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y → CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ 3 * ρ / 4 → ∃ p ∈ Y, y ∈ CKN.Foundation.Parabolic.vec3Ball p.2 r) ∧ (∀ p ∈ Y, CKN.Foundation.Parabolic.vec3Ball p.2 (2 * r) ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ) ∧ ∀ (z : CKN.Foundation.Parabolic.Vec3), {p ∈ Y | z ∈ CKN.Foundation.Parabolic.vec3Ball p.2 (2 * r)}.card ≤ Besicovitch.multiplicity CKN.BUGaussianSpace ^ 2

The transition annulus has a finite cover by Vec3 balls with doubled-ball containment and the spatial overlap inherited from Besicovitch. (eq:bu-gaussian-collar)