Symmetry of iterated coordinate directional derivatives

theorem CIV.contDiffOn_foldr_axisDeriv (s : Set CKN.Foundation.Parabolic.Vec3) (hs : IsOpen s) (G : CKN.Foundation.Parabolic.Vec3 → ℝ) (hG : ContDiffOn ℝ (↑⊤) G s) (l : List (Fin 3)) : ContDiffOn ℝ (↑⊤) (List.foldr axisDeriv G l) s

Iterating axisDeriv preserves ContDiffOn ℝ ∞ on an open set.

theorem CIV.axisDeriv_axisDeriv_symm (s : Set CKN.Foundation.Parabolic.Vec3) (hs : IsOpen s) (G : CKN.Foundation.Parabolic.Vec3 → ℝ) (hG : ContDiffOn ℝ (↑⊤) G s) (a b : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) (hx : x ∈ s) : axisDeriv a (axisDeriv b G) x = axisDeriv b (axisDeriv a G) x

Symmetry of two consecutive axisDeriv applications on an open set.

Uses the symmetry of the second derivative (second_derivative_symmetric_of_eventually).

theorem CIV.axisDeriv_congr_on (s : Set CKN.Foundation.Parabolic.Vec3) (hs : IsOpen s) (F G : CKN.Foundation.Parabolic.Vec3 → ℝ) (a : Fin 3) (h : Set.EqOn F G s) : Set.EqOn (axisDeriv a F) (axisDeriv a G) s

If two functions agree on an open set s and both are ContDiffOn ℝ ∞ there, then their axisDeriv also agree on s.

theorem CIV.eqOn_foldr_axisDeriv_of_perm (s : Set CKN.Foundation.Parabolic.Vec3) (hs : IsOpen s) (G : CKN.Foundation.Parabolic.Vec3 → ℝ) (hG : ContDiffOn ℝ (↑⊤) G s) {l l' : List (Fin 3)} (hperm : l.Perm l') : Set.EqOn (List.foldr axisDeriv G l) (List.foldr axisDeriv G l') s

Iterated axisDeriv does not depend on the order of the directions.