Bridge from curlComp to multiPartial language #
extends CIV.curlComp's definition (built from CKN's spatialPartial) with the smoothness
transfer, time-slice restriction, and one-derivative multiPartial-language translation that every
consumer of the genuine vorticity field ω := CIV.curlComp u needs, the missing static
(non-PDE) half of the bridge from the Cartesian curl to the multiPartial language used
throughout the induction on derivative order behind thm:analytic:interior (Kahane 1969,
Theorem 1.2).
theorem
CIV.contDiffOn_curlComp_public
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
(i : Fin 3)
:
ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => curlComp u i z) unitCylinder
theorem
CIV.contDiffOn_curlComp_slice_public
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
(i : Fin 3)
(s : ℝ)
(hs : s ∈ Set.Ioo (-1) 0)
:
ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => curlComp u i (x, s))
(CKN.Foundation.Parabolic.vec3Ball 0 1)
theorem
CIV.axisDeriv_curlComp_eq_multiPartial
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
(i k : Fin 3)
{t : ℝ}
(ht : t ∈ Set.Ioo (-1) 0)
{x : CKN.Foundation.Parabolic.Vec3}
(hx : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 1)
:
axisDeriv k (fun (y : CKN.Foundation.Parabolic.Vec3) => curlComp u i (y, t)) x = multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w (i + 2)) (Pi.single (i + 1) 1 + Pi.single k 1)
(x, t) - multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w (i + 1))
(Pi.single (i + 2) 1 + Pi.single k 1) (x, t)