Scalar Test Function Lift

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.contDiff_smul_basisVec_of_contDiff {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z • CKN.basisVec i

If ψ is smooth then ψ • basisVec i is also smooth, because scalar multiplication by a constant vector is a smooth operation on Vec3.

theorem CIV.hasCompactSupport_smul_basisVec_of_hasCompactSupport {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψc : HasCompactSupport ψ) (i : Fin 3) : HasCompactSupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z • CKN.basisVec i

If ψ has compact support then ψ • basisVec i also has compact support, since support (ψ • basisVec i) ⊆ support ψ (the basis vector is non-zero, so ψ z • basisVec i = 0 only when ψ z = 0).

theorem CIV.smul_basisVec_mem_spaceTimeTestFunction {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ CKN.spaceTimeTestFunction Ω I) (i : Fin 3) : (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z • CKN.basisVec i) ∈ CKN.spaceTimeTestFunction Ω I

A scalar test function ψ lifts to a vector test function ψ • basisVec i in spaceTimeTestFunction (V := Vec3) Ω I. This is the technical lemma that licenses isolating the i-th scalar component of the vector momentum equation by testing against φ := ψ • basisVec i.