Bridge from spatialPartial/spatialSecondPartial to multiPartial

These lemmas translate the momentum equation (eq:nse:forced) from the spatialPartial/spatialSecondPartial/timePartial operators used in the classical formulation into the multiPartial language of AnalyticBoundOn, eq:analytic:interior:force — the shape the real-analytic estimates behind thm:analytic:interior (Kahane 1969) need to state the induction on derivative order.

theorem CIV.spatialPartial_eq_multiPartial_single (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : CKN.spatialPartial g i (x, t) = multiPartial g (Pi.single i 1) (x, t)

theorem CIV.spatialSecondPartial_eq_multiPartial_single (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : CKN.spatialSecondPartial g j j (x, t) = multiPartial g (Pi.single j 2) (x, t)

theorem CIV.sum_spatialSecondPartial_eq_sum_multiPartial (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ∑ j : Fin 3, CKN.spatialSecondPartial g j j (x, t) = ∑ j : Fin 3, multiPartial g (Pi.single j 2) (x, t)

theorem CIV.laplacian_eq_of_isClassicalSolutionOn {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (hsol : IsClassicalSolutionOn u p f S) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hz : (x, t) ∈ S) (i : Fin 3) : ∑ j : Fin 3, multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) (Pi.single j 2) (x, t) = CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) (x, t) + ∑ j : Fin 3, u (x, t) j * multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) (Pi.single j 1) (x, t) + multiPartial p (Pi.single i 1) (x, t) - f (x, t) i