Separated space-time tests

The test (y, s) ↦ k(x - y) θ(s), built from a smooth compact spatial kernel k and a smooth compact time test θ, is an admissible space-time test on ℝ³ × (a, τ). Its time derivative, spatial derivatives and spatial second derivatives are again separated. Testing the weak equation with it gives the time derivative of the spatial convolution in lem:localized-vorticity-energy of the Escauriaza–Seregin–Šverák manuscript.

def CKN.vlTest (k : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) (θ : ℝ → ℝ) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The separated test (y, s) ↦ k(x - y) θ(s).

Equations

• CKN.vlTest k x θ p = k (x - p.1) * θ p.2

theorem CKN.vlTest_contDiff {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (x : Foundation.Parabolic.Vec3) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) : ContDiff ℝ (↑⊤) (vlTest k x θ)

theorem CKN.vlTest_mem {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (x : Foundation.Parabolic.Vec3) {a τ : ℝ} {θ : ℝ → ℝ} (hθ : IsIntervalTest (Set.Ioo a τ) θ) : vlTest k x θ ∈ spaceTimeTestFunction Set.univ (Set.Ioo a τ)

theorem CKN.vlTest_timePartial {k : Foundation.Parabolic.Vec3 → ℝ} (x : Foundation.Parabolic.Vec3) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (p : Foundation.Parabolic.Vec3 × ℝ) : timePartial (vlTest k x θ) p = k (x - p.1) * deriv θ p.2

theorem CKN.vlTest_spatialPartial {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (x : Foundation.Parabolic.Vec3) (θ : ℝ → ℝ) (j : Fin 3) (p : Foundation.Parabolic.Vec3 × ℝ) : spatialPartial (vlTest k x θ) j p = -(vlDeriv k j (x - p.1) * θ p.2)

theorem CKN.vlTest_spatialSecondPartial {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (x : Foundation.Parabolic.Vec3) (θ : ℝ → ℝ) (j : Fin 3) (p : Foundation.Parabolic.Vec3 × ℝ) : spatialSecondPartial (vlTest k x θ) j j p = vlDeriv (vlDeriv k j) j (x - p.1) * θ p.2