Support and compact support of spatial derivatives

theorem CKN.support_spatialDeriv_subset {f : Foundation.Parabolic.Vec3 → ℝ} (i : Fin 3) : Function.support (spatialDeriv f i) ⊆ tsupport f

The support of a spatial derivative is contained in the support of the function.

theorem CKN.tsupport_spatialDeriv_subset {f : Foundation.Parabolic.Vec3 → ℝ} (i : Fin 3) : tsupport (spatialDeriv f i) ⊆ tsupport f

The topological support of a spatial derivative is contained in the topological support of the function.

theorem CKN.hasCompactSupport_spatialDeriv {f : Foundation.Parabolic.Vec3 → ℝ} (hf : HasCompactSupport f) (i : Fin 3) : HasCompactSupport (spatialDeriv f i)

A function with compact support has a spatial derivative with compact support.

theorem CKN.support_mixedSecond_subset {f : Foundation.Parabolic.Vec3 → ℝ} (i j : Fin 3) : Function.support (mixedSecond f i j) ⊆ tsupport f

The support of a mixed second derivative is contained in the topological support of the function.

theorem CKN.tsupport_mixedSecond_subset {f : Foundation.Parabolic.Vec3 → ℝ} (i j : Fin 3) : tsupport (mixedSecond f i j) ⊆ tsupport f

The topological support of a mixed second derivative is contained in the topological support of the function.

theorem CKN.hasCompactSupport_mixedSecond {f : Foundation.Parabolic.Vec3 → ℝ} (hf : HasCompactSupport f) (i j : Fin 3) : HasCompactSupport (mixedSecond f i j)

A function with compact support has a mixed second derivative with compact support.

theorem CKN.support_spatialLaplacian_subset {f : Foundation.Parabolic.Vec3 → ℝ} : Function.support (spatialLaplacian f) ⊆ tsupport f

The support of the spatial Laplacian is contained in the topological support of the function.

theorem CKN.tsupport_spatialLaplacian_subset {f : Foundation.Parabolic.Vec3 → ℝ} : tsupport (spatialLaplacian f) ⊆ tsupport f

The topological support of the spatial Laplacian is contained in the topological support of the function.

theorem CKN.hasCompactSupport_spatialLaplacian {f : Foundation.Parabolic.Vec3 → ℝ} (hf : HasCompactSupport f) : HasCompactSupport (spatialLaplacian f)

A function with compact support has a spatial Laplacian with compact support.