Iterated derivatives of a directional derivative

For a sufficiently smooth map f, the i-th iterated derivative of the directional derivative y ↦ Df(y) v is the derivative of the i-th iterated derivative of f in the direction v:

Dⁱ (y ↦ Df(y) v) (x) = D(Dⁱ f)(x) v.

The two sides place the direction v in the last and in the first slot of D^{i+1} f respectively, so the identity is a consequence of the symmetry of second derivatives. It is the form in which a fixed directional derivative commutes with all higher derivatives.

As an application, every derivative of the first-order Taylor remainder z ↦ f (z - h) - f z + Df(z) h of a compactly supported C^{i+1} map is o(‖h‖) uniformly on the whole space. This controls every derivative of the difference quotients of translates of a compactly supported smooth function at once. The same holds for the first-order Taylor remainder x ↦ g (p + h, x) - g (p, x) - Dg(p, x) (h, 0) of a compactly supported map g on a product in its first variable, with derivatives taken in the second: this controls the difference quotients of a smooth family of compactly supported functions with respect to a parameter.

Main declarations

• ContDiff.iteratedFDeriv_fderiv_apply: Dⁱ (y ↦ Df(y) v) = D(Dⁱ f)(·) v.
• ContDiff.norm_iteratedFDeriv_fderiv_apply_le: ‖Dⁱ (y ↦ Df(y) v)‖ ≤ ‖D^{i+1} f‖ ‖v‖.
• TauCeti.tsupport_sub_sub_add_fderiv_subset: the support of the first-order Taylor remainder.
• HasCompactSupport.exists_norm_iteratedFDeriv_sub_sub_add_fderiv_le: the uniform estimate on the derivatives of the first-order Taylor remainder.
• HasCompactSupport.exists_norm_iteratedFDeriv_prod_right_sub_sub_le: the same estimate for the Taylor remainder in a parameter.

theorem ContDiff.iteratedFDeriv_fderiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E → F} (hf : ContDiff 𝕜 n f) {i : ℕ} (hi : minSmoothness 𝕜 (↑i + 1) ≤ n) (v x : E) : iteratedFDeriv 𝕜 i (fun (y : E) => (fderiv 𝕜 f y) v) x = (fderiv 𝕜 (iteratedFDeriv 𝕜 i f) x) v

Iterated derivatives commute with a directional derivative. For a map which is C^{minSmoothness 𝕜 (i + 1)} (so C^{i+1} over ℝ or ℂ), the i-th iterated derivative of y ↦ Df(y) v is the derivative of Dⁱ f in the direction v.

theorem ContDiff.norm_iteratedFDeriv_fderiv_apply_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E → F} (hf : ContDiff 𝕜 n f) {i : ℕ} (hi : minSmoothness 𝕜 (↑i + 1) ≤ n) (v x : E) : ‖iteratedFDeriv 𝕜 i (fun (y : E) => (fderiv 𝕜 f y) v) x‖ ≤ ‖iteratedFDeriv 𝕜 (i + 1) f x‖ * ‖v‖

The i-th iterated derivative of a directional derivative y ↦ Df(y) v is bounded by the (i + 1)-th iterated derivative of f: ‖Dⁱ (y ↦ Df(y) v) (x)‖ ≤ ‖D^{i+1} f (x)‖ ‖v‖.

theorem TauCeti.tsupport_sub_sub_add_fderiv_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {h : E} {δ : ℝ} (hh : ‖h‖ ≤ δ) : (tsupport fun (z : E) => f (z - h) - f z + (fderiv 𝕜 f z) h) ⊆ Metric.cthickening δ (tsupport f)

The first-order Taylor remainder z ↦ f (z - h) - f z + Df(z) h is supported in every closed δ-thickening of the support of f with ‖h‖ ≤ δ.

theorem HasCompactSupport.exists_norm_iteratedFDeriv_sub_sub_add_fderiv_le {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : WithTop ℕ∞} {f : E → F} (hfc : HasCompactSupport f) (hf : ContDiff ℝ n f) {i : ℕ} (hi : ↑i + 1 ≤ n) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (h : E), ‖h‖ < δ → ∀ (y : E), ‖iteratedFDeriv ℝ i (fun (z : E) => f (z - h) - f z + (fderiv ℝ f z) h) y‖ ≤ ε * ‖h‖

Uniform first-order Taylor estimate for all derivatives. If f is C^{i+1} with compact support, then the i-th derivative of the first-order Taylor remainder z ↦ f (z - h) - f z + Df(z) h is o(‖h‖) as h → 0, uniformly on the whole space.

theorem HasCompactSupport.exists_norm_iteratedFDeriv_prod_right_sub_sub_le {P : Type u_4} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : WithTop ℕ∞} {g : P × E → F} (hgc : HasCompactSupport g) (hg : ContDiff ℝ n g) {i : ℕ} (hi : ↑i + 1 ≤ n) (p : P) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (h : P), ‖h‖ < δ → ∀ (y : E), ‖iteratedFDeriv ℝ i (fun (x : E) => g (p + h, x) - g (p, x) - (fderiv ℝ g (p, x)) (h, 0)) y‖ ≤ ε * ‖h‖

Uniform first-order Taylor estimate in a parameter. If g : P × E → F is C^{i+1} with compact support, then the i-th derivative in the second variable of the first-order Taylor remainder x ↦ g (p + h, x) - g (p, x) - Dg(p, x) (h, 0) in the first variable is o(‖h‖) as h → 0, uniformly on the whole space.