Iterated FDeriv Tuples

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

theorem CIV.eqOn_iteratedFDeriv_basis (s : Set CKN.Foundation.Parabolic.Vec3) (hs : IsOpen s) (G : CKN.Foundation.Parabolic.Vec3 → ℝ) (hG : ContDiffOn ℝ (↑⊤) G s) (n : ℕ) (v : Fin n → Fin 3) : Set.EqOn (fun (x : CKN.Foundation.Parabolic.Vec3) => (iteratedFDeriv ℝ n G x) fun (i : Fin n) => CKN.basisVec (v i)) (List.foldr axisDeriv G (List.ofFn v)) s

On an open set, the n-th iterated Fréchet derivative evaluated at a tuple of coordinate basis vectors agrees with the corresponding iteration of axisDeriv in the order the tuple lists them.