Iterated derivatives under a linear change of variables

For a continuous linear equivalence e, the iterated derivative of f ∘ e at y is the iterated derivative of f at e y precomposed with e in every slot. Hence the norm of the i-th derivative of f ∘ e at y is at most ‖e‖ ^ i times that of f at e y, and the norm of the i-th derivative of f at e y is at most ‖e⁻¹‖ ^ i times that of f ∘ e at y. A Hölder bound for the i-th derivative of f ∘ e transfers to one for the i-th derivative of f, at the cost of the factor ‖e⁻¹‖ ^ (i + r). The second Fréchet derivative of f ∘ e at y, applied to v and w, is that of f at e y applied to e v and e w; when e takes values in the scalar field, it is e v * e w times the second derivative of f. No differentiability of f is needed.

In particular, for a rescaling z ↦ f (a • z) the i-th derivative at x is a ^ i times that of f at a • x, again without any differentiability of f (TauCeti.iteratedFDeriv_comp_const_smul_apply). A Hölder bound on a set t for the i-th derivative of f transfers to the rescaled map on any set that rescaling maps into t (HolderOnWith.iteratedFDeriv_comp_const_smul).

theorem ContinuousLinearEquiv.iteratedFDeriv_comp_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : G ≃L[𝕜] E) (f : E → F) (x : G) (i : ℕ) : iteratedFDeriv 𝕜 i (f ∘ ⇑e) x = (iteratedFDeriv 𝕜 i f (e x)).compContinuousLinearMap fun (x : Fin i) => ↑e

Iterated derivatives under a linear change of variables. For a continuous linear equivalence e, the i-th derivative of f ∘ e at x is the i-th derivative of f at e x precomposed with e in every slot. Unlike ContinuousLinearMap.iteratedFDeriv_comp_right, no differentiability of f is needed.

theorem ContinuousLinearEquiv.fderiv_fderiv_comp_right_apply_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : G ≃L[𝕜] E) (f : E → F) (z v w : G) : ((fderiv 𝕜 (fderiv 𝕜 (f ∘ ⇑e)) z) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) (e z)) (e v)) (e w)

Second derivatives under a linear change of variables. For a continuous linear equivalence e, the second derivative of f ∘ e at z, applied to v and w, is the second derivative of f at e z applied to e v and e w. No differentiability of f is needed.

theorem ContinuousLinearEquiv.fderiv_fderiv_comp_right_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : G ≃L[𝕜] 𝕜) (f : 𝕜 → F) (z v w : G) : ((fderiv 𝕜 (fderiv 𝕜 (f ∘ ⇑e)) z) v) w = (e v * e w) • deriv (deriv f) (e z)

Second derivatives along a one-dimensional linear change of variables. For a continuous linear equivalence e onto the scalar field and a function f of one variable, the second derivative of f ∘ e at z, applied to v and w, is e v * e w times the second derivative of f at e z. For instance, e may be the coordinate PiLp.equivOfUnique p 𝕜 fun _ : ι ↦ 𝕜 of a one-dimensional L^p space such as EuclideanSpace ℝ (Fin 1). No differentiability of f is needed.

theorem ContinuousLinearEquiv.norm_iteratedFDeriv_comp_right_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : G ≃L[𝕜] E) (f : E → F) (y : G) (i : ℕ) : ‖iteratedFDeriv 𝕜 i (f ∘ ⇑e) y‖ ≤ ‖↑e‖ ^ i * ‖iteratedFDeriv 𝕜 i f (e y)‖

Under a linear change of variables e, the i-th derivative of f ∘ e at y is bounded by ‖e‖ ^ i times the i-th derivative of f at e y.

theorem ContinuousLinearEquiv.norm_iteratedFDeriv_le_pow_mul_norm_iteratedFDeriv_comp_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : G ≃L[𝕜] E) (f : E → F) (y : G) (i : ℕ) : ‖iteratedFDeriv 𝕜 i f (e y)‖ ≤ ‖↑e.symm‖ ^ i * ‖iteratedFDeriv 𝕜 i (f ∘ ⇑e) y‖

Under a linear change of variables e, the i-th derivative of f at e y is bounded by ‖e⁻¹‖ ^ i times the i-th derivative of f ∘ e at y.

theorem ContinuousLinearEquiv.holderOnWith_iteratedFDeriv_of_comp_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : G ≃L[𝕜] E) {f : E → F} {s : Set E} {C r : NNReal} {i : ℕ} (h : HolderOnWith C r (iteratedFDeriv 𝕜 i (f ∘ ⇑e)) (⇑e ⁻¹' s)) : HolderOnWith (C * ‖↑e.symm‖₊ ^ i * ‖↑e.symm‖₊ ^ ↑r) r (iteratedFDeriv 𝕜 i f) s

Hölder continuity of iterated derivatives under a linear change of variables. If the i-th derivative of f ∘ e is r-Hölder with constant C on e ⁻¹' s, then the i-th derivative of f is r-Hölder on s with constant C ‖e⁻¹‖ ^ i ‖e⁻¹‖ ^ r.

theorem TauCeti.iteratedFDeriv_comp_const_smul_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (a : 𝕜) (x : E) (i : ℕ) : iteratedFDeriv 𝕜 i (fun (z : E) => f (a • z)) x = a ^ i • iteratedFDeriv 𝕜 i f (a • x)

Iterated derivatives of a rescaling. The i-th derivative of z ↦ f (a • z) at x is a ^ i times the i-th derivative of f at a • x. Unlike Mathlib's iteratedFDeriv_comp_const_smul, no differentiability of f is needed.

theorem TauCeti.norm_iteratedFDeriv_comp_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (a : 𝕜) (x : E) (i : ℕ) : ‖iteratedFDeriv 𝕜 i (fun (z : E) => f (a • z)) x‖ = ‖a‖ ^ i * ‖iteratedFDeriv 𝕜 i f (a • x)‖

The norm of the i-th derivative of z ↦ f (a • z) at x is ‖a‖ ^ i times that of the i-th derivative of f at a • x. No differentiability of f is needed.

theorem HolderOnWith.iteratedFDeriv_comp_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {i : ℕ} {C r : NNReal} {s t : Set E} (hf : HolderOnWith C r (iteratedFDeriv 𝕜 i f) t) (a : 𝕜) (hst : Set.MapsTo (fun (x : E) => a • x) s t) : HolderOnWith (‖a‖₊ ^ i * (C * ‖a‖₊ ^ ↑r)) r (iteratedFDeriv 𝕜 i fun (z : E) => f (a • z)) s

If the i-th derivative of f is r-Hölder with constant C on t and rescaling by a maps s into t, then the i-th derivative of z ↦ f (a • z) is r-Hölder on s with constant ‖a‖ ^ i C ‖a‖ ^ r. No differentiability of f is needed.

theorem LinearIsometryEquiv.norm_iteratedFDeriv_sub_comp {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {F' : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (e : E' ≃ₗᵢ[𝕜] E) (t : F ≃ₗᵢ[𝕜] F') (f : E → F) (j : ℕ) (x y : E') : ‖iteratedFDeriv 𝕜 j (⇑t ∘ f ∘ ⇑e) x - iteratedFDeriv 𝕜 j (⇑t ∘ f ∘ ⇑e) y‖ = ‖iteratedFDeriv 𝕜 j f (e x) - iteratedFDeriv 𝕜 j f (e y)‖

Linear isometries on either side preserve differences of iterated derivative fields, without any differentiability assumption on the function.

theorem LinearIsometryEquiv.holderOnWith_iteratedFDeriv_comp {E : Type u_1} {E' : Type u_2} {T : Type u_3} {Tu : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup T] [NormedSpace ℝ T] [NormedAddCommGroup Tu] [NormedSpace ℝ Tu] (e : E' ≃ₗᵢ[ℝ] E) (t : T ≃ₗᵢ[ℝ] Tu) (v : E → T) {C α : NNReal} (j : ℕ) {S : Set E} (hv : HolderOnWith C α (iteratedFDeriv ℝ j v) S) : HolderOnWith C α (iteratedFDeriv ℝ j (⇑t ∘ v ∘ ⇑e)) (⇑e ⁻¹' S)

Composing with linear isometries preserves a local Hölder bound on an actual derivative field, including at points where the function need not be differentiable.