Ordered derivatives of smooth products

The classical coordinate derivatives of the regularized transport tensor obey the Leibniz family used by the integer Sobolev norms in Part III. This is the algebraic first step of the H^m transport estimate in eq:lps-Hm-energy.

theorem ESS.lps_wordDeriv_sub {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (α : List (Fin 3)) : (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => f x - g x) = fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.wordDeriv α f x - CKN.wordDeriv α g x

Ordered derivatives distribute over a smooth scalar difference (eq:lps-regularized-Hm-identity).

theorem ESS.lps_wordDeriv_mul_leibniz {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (α : List (Fin 3)) : (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) = CKN.sobolevLeibnizFamily α (fun (β : List (Fin 3)) => CKN.wordDeriv β f) fun (β : List (Fin 3)) => CKN.wordDeriv β g

The classical ordered derivative of a smooth scalar product is the ordered Leibniz family (eq:lps-Hm-energy).

theorem ESS.lps_transport_divergence (v u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ∀ (j : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (hdiv : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) j x = 0) (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : ∑ j : Fin 3, v x j * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) j x = ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j * u y i) j x

For a smooth solenoidal advecting field, convection is the divergence of its tensor product (eq:lps-Hm-energy).

theorem ESS.lps_ordered_transport_divergence (v u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ∀ (j : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (hdiv : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) j x = 0) (α : List (Fin 3)) (i : Fin 3) : (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, v x j * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) j x) = fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.spatialDeriv (CKN.sobolevLeibnizFamily α (fun (β : List (Fin 3)) => CKN.wordDeriv β fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) fun (β : List (Fin 3)) => CKN.wordDeriv β fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) j x

Every ordered derivative of smooth solenoidal convection retains a divergence-form tensor product (eq:lps-Hm-energy).