Serrin-style cutoff profiles for the interior estimates

Smooth radial and temporal cutoff functions used in the backward parabolic windows B(x, ρ) × [s - ρ², s] that appear in the proof of lem:aniso:annulus. Each profile is a smooth monotone function that transitions from 0 to 1 over a controlled interval and is identically constant outside it.

noncomputable def CIV.serrinSpaceBump (r : ℝ) : ℝ

Radial profile, equal to one on r ≤ 1/4 and to zero on r ≥ 1.

Equations

• CIV.serrinSpaceBump r = (4 * (1 - r) / 3).smoothTransition

noncomputable def CIV.serrinTimeBump (τ : ℝ) : ℝ

Time profile, equal to zero on τ ≤ -1 and to one on τ ≥ -1/2.

Equations

• CIV.serrinTimeBump τ = (2 * τ + 2).smoothTransition

noncomputable def CIV.serrinBallCutoff (x : CKN.Foundation.Parabolic.Vec3) (ρ : ℝ) (y : CKN.Foundation.Parabolic.Vec3) : ℝ

Ball cutoff at x of radius ρ for the Euclidean norm.

Equations

• CIV.serrinBallCutoff x ρ y = CIV.serrinSpaceBump ((∑ i : Fin 3, (y i - x i) ^ 2) / ρ ^ 2)

theorem CIV.serrinBallCutoff_mem_Icc (x : CKN.Foundation.Parabolic.Vec3) (ρ : ℝ) (y : CKN.Foundation.Parabolic.Vec3) : serrinBallCutoff x ρ y ∈ Set.Icc 0 1

theorem CIV.serrinBallCutoff_support (x : CKN.Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (y : CKN.Foundation.Parabolic.Vec3) : (CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ / 2 → serrinBallCutoff x ρ y = 1) ∧ (ρ ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) → serrinBallCutoff x ρ y = 0) ∧ ContDiff ℝ (↑⊤) (serrinBallCutoff x ρ)

theorem CIV.serrinTimeBump_support {s ρ : ℝ} (hρ : 0 < ρ) (s' : ℝ) : (s - ρ ^ 2 / 2 ≤ s' → serrinTimeBump ((s' - s) / ρ ^ 2) = 1) ∧ (s' ≤ s - ρ ^ 2 → serrinTimeBump ((s' - s) / ρ ^ 2) = 0) ∧ ContDiff ℝ (↑⊤) serrinTimeBump