Space-time cutoffs

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This independent module combines the ball cutoff with a smooth one-dimensional time cutoff in the CKN namespace.

Main definitions

• timeCutoff: a smooth cutoff equal to one on the backward time interval [t₀ - r², t₀].
• spaceTimeCutoff: the product η(x) χ(t).

Main results

• timeCutoff_smooth, timeCutoff_eq_one_on, and timeCutoff_support_subset give the temporal cutoff properties.
• timeCutoff_abs_deriv_le gives the explicit bound 32 / (R² - r²).
• spaceTimeCutoff_smooth, spaceTimeCutoff_eq_one_on, and spaceTimeCutoff_support_subset give the product cutoff properties.

def CKN.timeGap (r R : ℝ) : ℝ

Gap between the squared inner and outer radii in the temporal cutoff.

Equations

• CKN.timeGap r R = R ^ 2 - r ^ 2

noncomputable def CKN.timeCutoffLeft (t₀ r R t : ℝ) : ℝ

Rising temporal cutoff at the backward end of the cylinder.

Equations

• CKN.timeCutoffLeft t₀ r R t = CKN.smoothTransitionProfile ((t - (t₀ - R ^ 2 + CKN.timeGap r R / 2)) / (CKN.timeGap r R / 2))

noncomputable def CKN.timeCutoffRight (t₀ r R t : ℝ) : ℝ

Falling temporal cutoff extending slightly beyond the cylinder's terminal time.

Equations

• CKN.timeCutoffRight t₀ r R t = CKN.smoothTransitionProfile ((t₀ + CKN.timeGap r R / 2 - t) / (CKN.timeGap r R / 2))

noncomputable def CKN.timeCutoff (t₀ r R t : ℝ) : ℝ

A smooth temporal cutoff with an interior support collar.

Equations

• CKN.timeCutoff t₀ r R t = CKN.timeCutoffLeft t₀ r R t * CKN.timeCutoffRight t₀ r R t

theorem CKN.timeCutoff_smooth {t₀ r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) : ContDiff ℝ (↑⊤) (timeCutoff t₀ r R)

The temporal cutoff is smooth to every order.

theorem CKN.timeCutoff_nonneg (t₀ r R t : ℝ) : 0 ≤ timeCutoff t₀ r R t

The temporal cutoff is nonnegative.

theorem CKN.timeCutoff_le_one (t₀ r R t : ℝ) : timeCutoff t₀ r R t ≤ 1

The temporal cutoff is at most one.

theorem CKN.timeCutoff_eq_one_on {t₀ r R t : ℝ} (hr : 0 ≤ r) (hrR : r < R) (ht : t ∈ Set.Icc (t₀ - r ^ 2) t₀) : timeCutoff t₀ r R t = 1

The temporal cutoff equals one on [t₀ - r², t₀].

theorem CKN.timeCutoff_support_subset {t₀ r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) : Function.support (timeCutoff t₀ r R) ⊆ Set.Ioo (t₀ - R ^ 2) (t₀ + (R ^ 2 - r ^ 2))

The temporal support lies strictly inside the prescribed time interval.

theorem CKN.timeCutoff_abs_deriv_le {t₀ r R t : ℝ} (hr : 0 ≤ r) (hrR : r < R) : |deriv (timeCutoff t₀ r R) t| ≤ 32 / (R ^ 2 - r ^ 2)

The temporal derivative obeys |χ'| ≤ 32 / (R² - r²).

noncomputable def CKN.spaceTimeCutoff {d : ℕ} (x₀ : Vec d) (t₀ r R : ℝ) (z : Vec d × ℝ) : ℝ

The product of the spatial and temporal cutoffs.

Equations

• CKN.spaceTimeCutoff x₀ t₀ r R z = CKN.canonicalBallCutoff x₀ r R z.1 * CKN.timeCutoff t₀ r R z.2

theorem CKN.spaceTimeCutoff_smooth {d : ℕ} (x₀ : Vec d) (t₀ r R : ℝ) (hr : 0 ≤ r) (hrR : r < R) : ContDiff ℝ (↑⊤) (spaceTimeCutoff x₀ t₀ r R)

The space-time cutoff is smooth to every order.

theorem CKN.spaceTimeCutoff_eq_one_on {d : ℕ} {x₀ : Vec d} {t₀ r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) {z : Vec d × ℝ} (hx : z.1 ∈ euclideanBall x₀ r) (ht : z.2 ∈ Set.Icc (t₀ - r ^ 2) t₀) : spaceTimeCutoff x₀ t₀ r R z = 1

The space-time cutoff equals one on the spatial-temporal plateau.

theorem CKN.spaceTimeCutoff_support_subset {d : ℕ} {x₀ : Vec d} {t₀ r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) : Function.support (spaceTimeCutoff x₀ t₀ r R) ⊆ euclideanBall x₀ R ×ˢ Set.Ioo (t₀ - R ^ 2) (t₀ + (R ^ 2 - r ^ 2))

The support lies in the spatial outer ball and the open time interval.