Product rule for the coordinate directional derivative

axisDeriv is the directional derivative along a coordinate axis on a spatial slice. This file establishes the Leibniz product rule for axisDeriv, its smoothness counterpart, and a Finset-indexed sum-of-products corollary used in the convective-term estimates of the inductive derivative bounds behind thm:analytic:interior.

theorem CIV.axisDeriv_mul {F G : CKN.Foundation.Parabolic.Vec3 → ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (k : Fin 3) : axisDeriv k (fun (y : CKN.Foundation.Parabolic.Vec3) => F y * G y) x = axisDeriv k F x * G x + F x * axisDeriv k G x

The Leibniz product rule for axisDeriv: differentiating a product along a coordinate axis splits into the derivative of the first factor times the second, plus the first times the derivative of the second.

theorem CIV.axisDeriv_mul_of_contDiffOn {F G : CKN.Foundation.Parabolic.Vec3 → ℝ} {s : Set CKN.Foundation.Parabolic.Vec3} (hs : IsOpen s) (hF : ContDiffOn ℝ (↑⊤) F s) (hG : ContDiffOn ℝ (↑⊤) G s) (k : Fin 3) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ s) : axisDeriv k (fun (y : CKN.Foundation.Parabolic.Vec3) => F y * G y) x = axisDeriv k F x * G x + F x * axisDeriv k G x

axisDeriv_mul with ContDiffOn ℝ ⊤ hypotheses on an open set, matching the regularity used in the interior analyticity argument.

theorem CIV.contDiffOn_mul_of_contDiffOn {F G : CKN.Foundation.Parabolic.Vec3 → ℝ} {s : Set CKN.Foundation.Parabolic.Vec3} (hF : ContDiffOn ℝ (↑⊤) F s) (hG : ContDiffOn ℝ (↑⊤) G s) : ContDiffOn ℝ (↑⊤) (fun (y : CKN.Foundation.Parabolic.Vec3) => F y * G y) s

ContDiffOn is preserved under pointwise products of real-valued functions.

theorem CIV.axisDeriv_sum_mul_of_contDiffOn {ι : Type u_1} (u : Finset ι) {F G : ι → CKN.Foundation.Parabolic.Vec3 → ℝ} {s : Set CKN.Foundation.Parabolic.Vec3} (hs : IsOpen s) (hF : ∀ i ∈ u, ContDiffOn ℝ (↑⊤) (F i) s) (hG : ∀ i ∈ u, ContDiffOn ℝ (↑⊤) (G i) s) (k : Fin 3) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ s) : axisDeriv k (fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ i ∈ u, F i y * G i y) x = ∑ i ∈ u, (axisDeriv k (F i) x * G i x + F i x * axisDeriv k (G i) x)

Finset-indexed sum-of-products corollary of the Leibniz rule, matching the convective term ∑_j g_j(x) ∂_j h(x) that appears when differentiating the momentum equation in the inductive derivative estimates behind thm:analytic:interior.