Multi Partial Linearity

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.axisDeriv_add {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 + axisDeriv k G x

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

theorem CIV.multiPartial_add {h₁ 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) (hG₂ : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h₂ (x, t)) s) (α : Fin 3 → ℕ) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ s) : multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => h₁ z + h₂ z) α (x, t) = multiPartial h₁ α (x, t) + multiPartial h₂ α (x, t)

theorem CIV.multiPartial_const_smul {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 → ℕ) (c : ℝ) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ s) : multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => c * h z) α (x, t) = c * multiPartial h α (x, t)