Linearity of multi-partial derivatives over finite sums #
The Finset-indexed generalization of multiPartial_add / multiPartial_const_smul, the
shape needed whenever thm:analytic:interior (Kahane 1969, Theorem 1.2) differentiates a finite
linear combination of several coupled unknowns — for instance velocity, vorticity, and an
adjoined force term — rather than just two fields.
theorem
CIV.multiPartial_finset_sum
{ι : Type u_1}
{h : ι → CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{u : Finset ι}
{s : Set CKN.Foundation.Parabolic.Vec3}
(hs : IsOpen s)
(t : ℝ)
(hG : ∀ j ∈ u, ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h j (x, t)) s)
(α : Fin 3 → ℕ)
{x : CKN.Foundation.Parabolic.Vec3}
(hx : x ∈ s)
:
multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j ∈ u, h j z) α (x, t) = ∑ j ∈ u, multiPartial (h j) α (x, t)
theorem
CIV.multiPartial_fin3_sum
{h : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{s : Set CKN.Foundation.Parabolic.Vec3}
(hs : IsOpen s)
(t : ℝ)
(hG : ∀ (j : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h j (x, t)) s)
(α : Fin 3 → ℕ)
{x : CKN.Foundation.Parabolic.Vec3}
(hx : x ∈ s)
:
multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, h j z) α (x, t) = ∑ j : Fin 3, multiPartial (h j) α (x, t)
theorem
CIV.multiPartial_finset_sum_const_smul
{ι : Type u_1}
{h : ι → CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{c : ι → ℝ}
{u : Finset ι}
{s : Set CKN.Foundation.Parabolic.Vec3}
(hs : IsOpen s)
(t : ℝ)
(hG : ∀ j ∈ u, ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h j (x, t)) s)
(α : Fin 3 → ℕ)
{x : CKN.Foundation.Parabolic.Vec3}
(hx : x ∈ s)
:
multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j ∈ u, c j * h j z) α (x, t) = ∑ j ∈ u, c j * multiPartial (h j) α (x, t)
theorem
CIV.abs_multiPartial_finset_sum_le
{ι : Type u_1}
{h : ι → CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{u : Finset ι}
{s : Set CKN.Foundation.Parabolic.Vec3}
(hs : IsOpen s)
(t : ℝ)
(hG : ∀ j ∈ u, ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h j (x, t)) s)
(α : Fin 3 → ℕ)
{x : CKN.Foundation.Parabolic.Vec3}
(hx : x ∈ s)
:
|multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j ∈ u, h j z) α (x, t)| ≤ ∑ j ∈ u, |multiPartial (h j) α (x, t)|