Admissibility

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

noncomputable def CKN.backwardHeatCutoff (η : Foundation.Parabolic.Vec3 × ℝ → ℝ) (x₀ : Foundation.Parabolic.Vec3) (t₀ r : ℝ) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The globally defined product used for the backward heat test.

Equations

• CKN.backwardHeatCutoff η x₀ t₀ r z = η z * if z.2 - t₀ < r ^ 2 then CKN.Foundation.Heat.backwardHeatTestFunction r (z.1 - x₀) (z.2 - t₀) else 0

theorem CKN.backwardHeat_cutoff_testFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (η : Foundation.Parabolic.Vec3 × ℝ → ℝ) (x₀ : Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηΩI : tsupport η ⊆ spaceTimeSet Ω I) (hηtime : tsupport η ⊆ {z : Foundation.Parabolic.Vec3 × ℝ | z.2 < t₀ + r ^ 2}) (hηnonneg : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ η z) : backwardHeatCutoff η x₀ t₀ r ∈ spaceTimeTestFunction Ω I ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ backwardHeatCutoff η x₀ t₀ r z

The truncated backward heat product is an admissible nonnegative test function.

The hypotheses expose the cutoff properties supplied by the space-time cutoff construction: compact support, location in the domain, time support at or before t₀, and nonnegativity.