Product rules for the spatial part of the first Caccioppoli term.

theorem CKN.caccioppoli_spatialSecondDeriv_mul {η φ : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hφ : ContDiff ℝ (↑⊤) φ) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : mixedSecond (fun (y : Foundation.Parabolic.Vec3) => η y * φ y) i j x = mixedSecond η i j x * φ x + spatialDeriv η j x * spatialDeriv φ i x + spatialDeriv η i x * spatialDeriv φ j x + η x * mixedSecond φ i j x

theorem CKN.caccioppoli_spatialLaplacian_mul {η φ : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hφ : ContDiff ℝ (↑⊤) φ) : (spatialLaplacian fun (x : Foundation.Parabolic.Vec3) => η x * φ x) = fun (x : Foundation.Parabolic.Vec3) => η x * spatialLaplacian φ x + 2 * spatialGradDot η φ x + φ x * spatialLaplacian η x