Spatial cutoffs of growing radius

Smooth cutoffs equal to one on balls of radius n + 1, with values in [0, 1] and gradients of size O(1 / (n + 1)). They localize the mollified cross pairing in lem:pv-serrin-uniqueness.

def ESS.serrinBump : ContDiffBump 0

The fixed bump profile equal to one on the unit ball.

Equations

• ESS.serrinBump = { rIn := 1, rOut := 2, rIn_pos := ESS.serrinBump._proof_2, rIn_lt_rOut := ESS.serrinBump._proof_3 }

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

The cutoff of radius n + 1.

Equations

• ESS.serrinCutoff n x = ↑ESS.serrinBump ((1 / (↑n + 1)) • x)

theorem ESS.serrinCutoff_contDiff (n : ℕ) : ContDiff ℝ (↑⊤) (serrinCutoff n)

theorem ESS.serrinCutoff_hasCompactSupport (n : ℕ) : HasCompactSupport (serrinCutoff n)

theorem ESS.serrinCutoff_nonneg (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) : 0 ≤ serrinCutoff n x

theorem ESS.serrinCutoff_le_one (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) : serrinCutoff n x ≤ 1

theorem ESS.serrinCutoff_abs_le_one (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) : |serrinCutoff n x| ≤ 1

theorem ESS.serrinCutoff_tendsto_one (x : CKN.Foundation.Parabolic.Vec3) : Filter.Tendsto (fun (n : ℕ) => serrinCutoff n x) Filter.atTop (nhds 1)

theorem ESS.serrinCutoff_deriv_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3), |CKN.spatialDeriv (serrinCutoff n) j x| ≤ C * (1 / (↑n + 1))

The gradient of the cutoff of radius n + 1 is uniformly O(1 / (n + 1)).