Iterated derivatives of iterated derivatives

The i-th iterated derivative of the m-th iterated derivative of a function has the same norm as its (i + m)-th iterated derivative. This extends Mathlib's norm_iteratedFDeriv_fderiv, the case m = 1, and lets bounds on all iterated derivatives of a function transfer to its iterated derivative fields. The file also supplies the two-variable currying isometry used to identify continuous multilinear second derivatives with curried bilinear maps, and the corresponding exact comparison for differences of second derivatives, which transfers Hölder bounds between the two forms of the second derivative. Where a function ζ equals one on a neighbourhood of a point, every iterated derivative of ζ * u there is that of u (Filter.EventuallyEq.iteratedFDeriv_mul_eq).

noncomputable def TauCeti.continuousMultilinearCurryFin2 (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : (E [×2]→L[𝕜] F) ≃ₗᵢ[𝕜] E →L[𝕜] E →L[𝕜] F

The currying linear isometry from continuous multilinear maps on Fin 2 to continuous bilinear maps in curried form.

@[simp]

theorem TauCeti.continuousMultilinearCurryFin2_apply (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E [×2]→L[𝕜] F) (x y : E) : (((continuousMultilinearCurryFin2 𝕜 E F) f) x) y = f ![x, y]

The currying isometry evaluates a multilinear map on its two arguments in order.

@[simp]

theorem TauCeti.continuousMultilinearCurryFin2_symm_apply (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (g : E →L[𝕜] E →L[𝕜] F) (m : Fin 2 → E) : ((continuousMultilinearCurryFin2 𝕜 E F).symm g) m = (g (m 0)) (m 1)

The inverse currying isometry evaluates its arguments in their original order.

theorem TauCeti.continuousMultilinearCurryFin2_iteratedFDeriv_two {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) : (continuousMultilinearCurryFin2 𝕜 E F) (iteratedFDeriv 𝕜 2 f x) = fderiv 𝕜 (fderiv 𝕜 f) x

Currying the second iterated derivative gives the Fréchet derivative of the first Fréchet derivative, including at points where these derivatives are junk-valued.

theorem TauCeti.norm_fderiv_fderiv_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x y : E) : ‖fderiv 𝕜 (fderiv 𝕜 f) x - fderiv 𝕜 (fderiv 𝕜 f) y‖ = ‖iteratedFDeriv 𝕜 2 f x - iteratedFDeriv 𝕜 2 f y‖

Differences of curried second derivatives and multilinear second derivatives have exactly the same norm, without differentiability assumptions.

theorem TauCeti.holderOnWith_fderiv_fderiv_iff_iteratedFDeriv_two {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {C r : NNReal} {s : Set E} (f : E → F) : HolderOnWith C r (fderiv 𝕜 (fderiv 𝕜 f)) s ↔ HolderOnWith C r (iteratedFDeriv 𝕜 2 f) s

The curried second Fréchet derivative is r-Hölder with constant C on a set exactly when the second iterated derivative is, without differentiability assumptions: the two differ by the currying isometry.

theorem TauCeti.norm_iteratedFDeriv_iteratedFDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (i m : ℕ) (x : E) : ‖iteratedFDeriv 𝕜 i (iteratedFDeriv 𝕜 m f) x‖ = ‖iteratedFDeriv 𝕜 (i + m) f x‖

The i-th iterated derivative of the m-th iterated derivative of f has the same norm as the (i + m)-th iterated derivative of f.

theorem Filter.EventuallyEq.iteratedFDeriv_mul_eq {𝕜 : Type u_4} {F : Type u_5} {A : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedRing A] [NormedSpace 𝕜 A] {k : ℕ} {ζ u : F → A} {x : F} (hζ : ζ =ᶠ[nhds x] 1) : iteratedFDeriv 𝕜 k (ζ * u) x = iteratedFDeriv 𝕜 k u x

Where a function ζ equals one on a neighbourhood of x, every iterated derivative of ζ * u at x is that of u.