Kernel All Orders Open

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Iterated derivatives on an open subset of space

On an open set the global iterated Fréchet derivative agrees with the derivative computed within the set, so it only depends on the values of the function there and inherits differentiability and continuity from ContDiffOn. These are the local-to-global bridges used by the all-order kernel estimates of cor:CZ-harmonic.

theorem CKN.Foundation.Heat.iteratedFDeriv_eq_of_eqOn_isOpen {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : Parabolic.Vec3 → F} {U : Set Parabolic.Vec3} (hU : IsOpen U) (hfg : Set.EqOn f g U) (n : ℕ) {x : Parabolic.Vec3} (hx : x ∈ U) : iteratedFDeriv ℝ n f x = iteratedFDeriv ℝ n g x

Iterated derivatives at a point of an open set only depend on the function there.

theorem CKN.Foundation.Heat.differentiableAt_iteratedFDeriv_of_isOpen {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : Parabolic.Vec3 → F} {U : Set Parabolic.Vec3} (hU : IsOpen U) (n : ℕ) (hf : ContDiffOn ℝ (↑(n + 1)) f U) {x : Parabolic.Vec3} (hx : x ∈ U) : DifferentiableAt ℝ (iteratedFDeriv ℝ n f) x

A function of order n + 1 on an open set has a differentiable n-th derivative there.

theorem CKN.Foundation.Heat.continuousOn_iteratedFDeriv_of_isOpen {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : Parabolic.Vec3 → F} {U : Set Parabolic.Vec3} (hU : IsOpen U) (n : ℕ) (hf : ContDiffOn ℝ (↑n) f U) : ContinuousOn (iteratedFDeriv ℝ n f) U

A function of order n on an open set has a continuous n-th derivative there.