The Leibniz rule for the heat operator

The heat operator ∂ₜ - Δ obeys a product rule on any open set where both factors are jointly smooth: (∂ₜ - Δ)(χ w) = χ (∂ₜ - Δ) w + w (∂ₜ - Δ) χ - 2 ∇χ · ∇w. This is the pointwise identity that expands the cutoff-and-heat-kernel product in the interior estimates of the proof of lem:aniso:annulus, before the divergence term coming from w's own equation is substituted in.

theorem CIV.HB2a_heat_operator_mul {χ w : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {O : Set CKN.Foundation.Parabolic.ParabolicPoint} (hO : IsOpen O) (hχ : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => χ z) O) (hw : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => w z) O) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ O → CKN.timePartial (fun (v : CKN.Foundation.Parabolic.ParabolicPoint) => χ v * w v) z - ∑ i : Fin 3, CKN.spatialSecondPartial (fun (v : CKN.Foundation.Parabolic.ParabolicPoint) => χ v * w v) i i z = χ z * (CKN.timePartial w z - ∑ i : Fin 3, CKN.spatialSecondPartial w i i z) + w z * (CKN.timePartial χ z - ∑ i : Fin 3, CKN.spatialSecondPartial χ i i z) - 2 * ∑ i : Fin 3, CKN.spatialPartial χ i z * CKN.spatialPartial w i z

The Leibniz rule for the heat operator ∂ₜ - Δ applied to a product of two functions that are jointly smooth on a common open set (the corresponding statement, the cutoff-decomposition step of the proof of lem:aniso:annulus).