Derivatives of a separated space-time product

For a function on space-time written as the separated product v ↦ g v.1 * h v.2 of a spatial factor g and a time factor h, this file records the smoothness of the product and expresses its factor-wise spatial and time derivatives through the derivatives of the two factors. It also places the support and the topological support of the product inside the product of the corresponding one-factor sets.

theorem CKN.Core.Endgame.contDiff_separatedProduct {g : Foundation.Parabolic.Vec3 → ℝ} {h : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hh : ContDiff ℝ (↑⊤) h) : ContDiff ℝ ↑⊤ fun (v : Foundation.Parabolic.Vec3 × ℝ) => g v.1 * h v.2

A product v ↦ g v.1 * h v.2 of a smooth spatial factor and a smooth time factor is smooth on space-time.

theorem CKN.Core.Endgame.support_separatedProduct_subset (g : Foundation.Parabolic.Vec3 → ℝ) (h : ℝ → ℝ) : (Function.support fun (v : Foundation.Parabolic.Vec3 × ℝ) => g v.1 * h v.2) ⊆ Function.support g ×ˢ Function.support h

The support of a separated product is contained in the product of the two factor supports.

theorem CKN.Core.Endgame.tsupport_separatedProduct_subset (g : Foundation.Parabolic.Vec3 → ℝ) (h : ℝ → ℝ) : (tsupport fun (v : Foundation.Parabolic.Vec3 × ℝ) => g v.1 * h v.2) ⊆ tsupport g ×ˢ tsupport h

The topological support of a separated product is contained in the product of the two factor topological supports.

theorem CKN.Core.Endgame.spatialPartial_separatedProduct {g : Foundation.Parabolic.Vec3 → ℝ} (h : ℝ → ℝ) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (w : Foundation.Parabolic.Vec3 × ℝ) : spatialPartial (fun (v : Foundation.Parabolic.Vec3 × ℝ) => g v.1 * h v.2) i w = spatialDeriv g i w.1 * h w.2

The spatial partial derivative of a separated product is the product of the spatial derivative of the spatial factor with the time factor.

theorem CKN.Core.Endgame.timePartial_separatedProduct (g : Foundation.Parabolic.Vec3 → ℝ) {h : ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (w : Foundation.Parabolic.Vec3 × ℝ) : timePartial (fun (v : Foundation.Parabolic.Vec3 × ℝ) => g v.1 * h v.2) w = g w.1 * deriv h w.2

The time partial derivative of a separated product is the product of the spatial factor with the ordinary derivative of the time factor.

theorem CKN.Core.Endgame.spatialSecondPartial_separatedProduct {g : Foundation.Parabolic.Vec3 → ℝ} (h : ℝ → ℝ) (hg : ContDiff ℝ (↑⊤) g) (i j : Fin 3) (w : Foundation.Parabolic.Vec3 × ℝ) : spatialSecondPartial (fun (v : Foundation.Parabolic.Vec3 × ℝ) => g v.1 * h v.2) i j w = mixedSecond g j i w.1 * h w.2

The second spatial partial derivative of a separated product is the product of the corresponding mixed second derivative of the spatial factor with the time factor.