The order-shift composition law for multiPartial/axisDeriv #
One further coordinate derivative of a multi-index derivative on a time slice
is again a multi-index derivative, at the multi-index incremented by the new
direction — the bookkeeping step needed to differentiate the momentum equation's
multiPartial-language form (CIV.laplacian_eq_of_isClassicalSolutionOn) one
further time for the inductive derivative estimates behind
thm:analytic:interior (Kahane 1969).
theorem
CIV.contDiffOn_multiPartial_slice
{h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{s : Set CKN.Foundation.Parabolic.Vec3}
(hs : IsOpen s)
(t : ℝ)
(hG : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) s)
(α : Fin 3 → ℕ)
:
ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => multiPartial h α (x, t)) s
theorem
CIV.axisDeriv_multiPartial_slice_eq
{h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{s : Set CKN.Foundation.Parabolic.Vec3}
(hs : IsOpen s)
(t : ℝ)
(hG : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) s)
(α : Fin 3 → ℕ)
(k : Fin 3)
{x : CKN.Foundation.Parabolic.Vec3}
(hx : x ∈ s)
:
axisDeriv k (fun (y : CKN.Foundation.Parabolic.Vec3) => multiPartial h α (y, t)) x = multiPartial h (α + Pi.single k 1) (x, t)
theorem
CIV.axisDeriv_axisDeriv_multiPartial_slice_eq
{h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{s : Set CKN.Foundation.Parabolic.Vec3}
(hs : IsOpen s)
(t : ℝ)
(hG : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) s)
(α : Fin 3 → ℕ)
(k l : Fin 3)
{x : CKN.Foundation.Parabolic.Vec3}
(hx : x ∈ s)
:
axisDeriv k
(fun (y : CKN.Foundation.Parabolic.Vec3) =>
axisDeriv l (fun (z : CKN.Foundation.Parabolic.Vec3) => multiPartial h α (z, t)) y)
x = multiPartial h (α + Pi.single k 1 + Pi.single l 1) (x, t)
theorem
CIV.axisDeriv_axisDeriv_multiPartial_slice_eq_single
{h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{s : Set CKN.Foundation.Parabolic.Vec3}
(hs : IsOpen s)
(t : ℝ)
(hG : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) s)
(α : Fin 3 → ℕ)
(k : Fin 3)
{x : CKN.Foundation.Parabolic.Vec3}
(hx : x ∈ s)
:
axisDeriv k
(fun (y : CKN.Foundation.Parabolic.Vec3) =>
axisDeriv k (fun (z : CKN.Foundation.Parabolic.Vec3) => multiPartial h α (z, t)) y)
x = multiPartial h (α + Pi.single k 2) (x, t)