Higher differentials

Glöckner–Neeb, Infinite-Dimensional Lie Groups (arXiv:2602.12362), §1.3.

The k-th differential of f : E → F is d^(k) f (x, y₁, …, yₖ) = (D_{yₖ} ⋯ D_{y₁} f)(x) (iteratedDMB). We show:

• Proposition 1.3.10: f is C^k in the recursive sense of ContDiffMBOn if and only if f is continuous and the differentials d^(j) f exist and are continuous on U × E^j for j ≤ k (the original definition of Bastiani and Neeb, HasContIterDerivOn).
• Remark 1.3.13: if f is C^r, then d^(k) f is C^{r-k} on U × E^k.
• Proposition 1.3.17 (Schwarz): for f of class C^k, d^(k) f (x, ·) is a continuous, symmetric k-linear map.

def LCAnalysis.iteratedDMB {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (k : ℕ) : (E → F) → E × (Fin k → E) → F

The k-th differential d^(k) f (x, y) = (D_{y (k-1)} ⋯ D_{y 0} f)(x) (junk values where the derivatives do not exist).

Equations

• LCAnalysis.iteratedDMB 0 x✝ p = x✝ p.1
• LCAnalysis.iteratedDMB k.succ x✝ p = LCAnalysis.dMB (fun (z : E) => LCAnalysis.iteratedDMB k x✝ (z, Fin.init p.2)) (p.1, p.2 (Fin.last k))

def LCAnalysis.HasContIterDerivOn {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (k : ℕ) (f : E → F) (U : Set E) : Prop

Neeb's definition of C^k maps: the iterated directional derivatives d^(j) f exist for j ≤ k and are continuous on U × E^j (for j = 0, this is the continuity of f).

Equations

• One or more equations did not get rendered due to their size.

Algebraic identities

theorem LCAnalysis.iteratedDMB_zero {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : E → F) (p : E × (Fin 0 → E)) : iteratedDMB 0 f p = f p.1

theorem LCAnalysis.iteratedDMB_one {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : E → F) (x : E) (v : Fin 1 → E) : iteratedDMB 1 f (x, v) = dMB f (x, v 0)

theorem LCAnalysis.iteratedDMB_succ {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (k : ℕ) (f : E → F) (x : E) (v : Fin (k + 1) → E) : iteratedDMB (k + 1) f (x, v) = dMB (fun (z : E) => iteratedDMB k f (z, Fin.init v)) (x, v (Fin.last k))

theorem LCAnalysis.iteratedDMB_cons {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (k : ℕ) (f : E → F) (y x : E) (v : Fin k → E) : iteratedDMB (k + 1) f (x, Fin.cons y v) = iteratedDMB k (fun (z : E) => dMB f (z, y)) (x, v)

Peeling off the first direction: d^(k+1) f (x, y, v) = d^(k) (df(·, y)) (x, v).

theorem LCAnalysis.dMB_slice {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_1} [AddCommGroup E'] [Module ℝ E'] (g : E × E' → F) (x h : E) (a : E') : dMB g ((x, a), h, 0) = dMB (fun (z : E) => g (z, a)) (x, h)

theorem LCAnalysis.dMB_slice₂ {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_1} [AddCommGroup E'] [Module ℝ E'] (g : E × E' → F) (x : E) (a b : E') : dMB g ((x, a), 0, b) = dMB (fun (w : E') => g (x, w)) (a, b)

Derivatives in directions (0, b) are derivatives of the second slice.

theorem LCAnalysis.hasDirDerivAt_slice {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_1} [AddCommGroup E'] [Module ℝ E'] {g : E × E' → F} {x h : E} {a : E'} {y : F} : HasDirDerivAt g (x, a) (h, 0) y ↔ HasDirDerivAt (fun (z : E) => g (z, a)) x h y

theorem LCAnalysis.iteratedDMB_slice {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_1} [AddCommGroup E'] [Module ℝ E'] [TopologicalSpace E'] (k : ℕ) (g : E × E' → F) (a : E') (x : E) (v : Fin k → E) : iteratedDMB k (fun (z : E) => g (z, a)) (x, v) = iteratedDMB k g ((x, a), fun (i : Fin k) => (v i, 0))

Differentials of a slice z ↦ g (z, a) are differentials of g in directions (y, 0).

theorem LCAnalysis.iteratedDMB_succ_eq_dMB {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (k : ℕ) (f : E → F) (x : E) (v : Fin (k + 1) → E) : iteratedDMB (k + 1) f (x, v) = iteratedDMB k (dMB f) ((x, v 0), fun (i : Fin k) => (v i.succ, 0))

Glöckner–Neeb (1.36): d^(k+1) f (x, y₀, …, yₖ) = d^(k) (df) ((x, y₀), (y₁, 0), …, (yₖ, 0)).

Proposition 1.3.10, first half

theorem LCAnalysis.ContinuousOn.iteratedDMB_zero {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : E → F} {U : Set E} (hf : ContinuousOn f U) : ContinuousOn (iteratedDMB 0 f) (U ×ˢ Set.univ)

theorem LCAnalysis.ContDiffMBOn.hasContIterDerivOn {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {k : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] {f : E₁ → F} {U : Set E₁} : ContDiffMBOn k f U → HasContIterDerivOn k f U

A C^k map has continuous differentials d^(j) f for j ≤ k.

theorem LCAnalysis.hasDirDerivAt_slice₂ {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_1} [AddCommGroup E'] [Module ℝ E'] {g : E × E' → F} {x : E} {a h : E'} {y : F} : HasDirDerivAt g (x, a) (0, h) y ↔ HasDirDerivAt (fun (w : E') => g (x, w)) a h y

theorem LCAnalysis.hasDirDerivAt_of_multilinear {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {ℓ : ℕ} {M : (Fin ℓ → E) → F} [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] (hM : Continuous M) (hadd : ∀ (w : Fin ℓ → E) (i : Fin ℓ) (a b : E), M (Function.update w i (a + b)) = M (Function.update w i a) + M (Function.update w i b)) (hsmul : ∀ (w : Fin ℓ → E) (i : Fin ℓ) (c : ℝ) (a : E), M (Function.update w i (c • a)) = c • M (Function.update w i a)) (w h : Fin ℓ → E) : HasDirDerivAt M w h (∑ i : Fin ℓ, M (Function.update w i (h i)))

The directional derivative of a continuous map that is additive and homogeneous in each variable separately: D_h M (w) = ∑ᵢ M (w₁, …, hᵢ, …, wₗ).

theorem LCAnalysis.HasDirDerivAt.add {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E₁ : Type u_1} [AddCommGroup E₁] [Module ℝ E₁] [IsTopologicalAddGroup F] {f g : E₁ → F} {x h : E₁} {a b : F} (hf : HasDirDerivAt f x h a) (hg : HasDirDerivAt g x h b) : HasDirDerivAt (fun (y : E₁) => f y + g y) x h (a + b)

theorem LCAnalysis.HasDirDerivAt.const_smul {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] {E₁ : Type u_1} [AddCommGroup E₁] [Module ℝ E₁] {f : E₁ → F} {x h : E₁} {a : F} (hf : HasDirDerivAt f x h a) (c : ℝ) : HasDirDerivAt (fun (y : E₁) => c • f y) x h (c • a)

Proposition 1.3.10, second half

theorem LCAnalysis.contDiffMBOn_const {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T2Space F] (k : ℕ) {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] (c : F) (U : Set E₁) : ContDiffMBOn k (fun (x : E₁) => c) U

theorem LCAnalysis.ContDiffMBOn.add {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {k : ℕ} {f g : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn k f U) (hg : ContDiffMBOn k g U) : ContDiffMBOn k (fun (x : E) => f x + g x) U

theorem LCAnalysis.ContDiffMBOn.sum {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {k : ℕ} {ι : Type u_1} (s : Finset ι) {f : ι → E → F} {U : Set E} (hU : IsOpen U) (hf : ∀ i ∈ s, ContDiffMBOn k (f i) U) : ContDiffMBOn k (fun (x : E) => ∑ i ∈ s, f i x) U

theorem LCAnalysis.contDiffMBOn_of_multilinear {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {U : Set E} (hU : IsOpen U) (r ℓ : ℕ) (f : E × (Fin ℓ → E) → F) : (∀ x ∈ U, ∀ (w : Fin ℓ → E) (i : Fin ℓ) (a b : E), f (x, Function.update w i (a + b)) = f (x, Function.update w i a) + f (x, Function.update w i b)) → (∀ x ∈ U, ∀ (w : Fin ℓ → E) (i : Fin ℓ) (c : ℝ) (a : E), f (x, Function.update w i (c • a)) = c • f (x, Function.update w i a)) → (∀ j < r, ∀ x ∈ U, ∀ (w : Fin ℓ → E) (v : Fin (j + 1) → E), HasDirDerivAt (fun (z : E) => iteratedDMB j (fun (z' : E) => f (z', w)) (z, Fin.init v)) x (v (Fin.last j)) (iteratedDMB (j + 1) (fun (z' : E) => f (z', w)) (x, v))) → (∀ j ≤ r, ContinuousOn (fun (q : (E × (Fin ℓ → E)) × (Fin j → E)) => iteratedDMB j (fun (z : E) => f (z, q.1.2)) (q.1.1, q.2)) ((U ×ˢ Set.univ) ×ˢ Set.univ)) → ContDiffMBOn r f (U ×ˢ Set.univ)

Glöckner–Neeb, Lemma 1.3.12: a map f : U × E^ℓ → F that is ℓ-linear in the second variable and has continuous differentials d^(j) in the first variable for j ≤ r is C^r.

theorem LCAnalysis.HasContIterDerivOn.contDiffMBOn {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {k : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) (hf : HasContIterDerivOn k f U) : ContDiffMBOn k f U

Glöckner–Neeb, Proposition 1.3.10: Neeb's definition of C^k implies the recursive one.

theorem LCAnalysis.contDiffMBOn_iff_hasContIterDerivOn {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {k : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) : ContDiffMBOn k f U ↔ HasContIterDerivOn k f U

Glöckner–Neeb, Proposition 1.3.10: the recursive definition of C^k agrees with Neeb's.

Remark 1.3.13: the differentials of a C^r map are C^{r-k}

theorem LCAnalysis.ContDiffMBOn.contDiffMBOn_iteratedDMB {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T2Space F] (k : ℕ) {r : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] {f : E₁ → F} {U : Set E₁} : IsOpen U → ContDiffMBOn (k + r) f U → ContDiffMBOn r (iteratedDMB k f) (U ×ˢ Set.univ)

theorem LCAnalysis.ContDiffMBOn.contDiffMBOn_iteratedDMB_slice {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {k r : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn (k + r) f U) (w : Fin k → E) : ContDiffMBOn r (fun (z : E) => iteratedDMB k f (z, w)) U

For fixed directions w, the map x ↦ d^(k) f (x, w) is C^r if f is C^{k+r}.

Proposition 1.3.17: Schwarz's theorem

theorem LCAnalysis.dMB_congr_of_eventuallyEq {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) (v : E) : dMB f₁ (x, v) = dMB f₂ (x, v)

theorem LCAnalysis.iteratedDMB_add_two {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (k : ℕ) (f : E → F) (x : E) (v : Fin (k + 2) → E) : iteratedDMB (k + 2) f (x, v) = dMB (dMB fun (z : E) => iteratedDMB k f (z, Fin.init (Fin.init v))) ((x, v (Fin.last k).castSucc), v (Fin.last (k + 1)), 0)

theorem LCAnalysis.ContDiffMBOn.iteratedDMB_swap {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {m : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn m f U) (k : ℕ) : k + 1 ≤ m → ∀ x ∈ U, ∀ (v : Fin (k + 1) → E) (i : Fin k), iteratedDMB (k + 1) f (x, v ∘ ⇑(Equiv.swap i.castSucc i.succ)) = iteratedDMB (k + 1) f (x, v)

Swapping two adjacent directions does not change d^(k+1) f.

theorem LCAnalysis.ContDiffMBOn.iteratedDMB_perm {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {m k : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn m f U) (hk : k ≤ m) {x : E} (hx : x ∈ U) (v : Fin k → E) (σ : Equiv.Perm (Fin k)) : iteratedDMB k f (x, v ∘ ⇑σ) = iteratedDMB k f (x, v)

Proposition 1.3.17: d^(k) f (x, ·) is symmetric.

theorem LCAnalysis.ContDiffMBOn.iteratedDMB_snoc_add {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {m k : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn m f U) (hk : k + 1 ≤ m) {x : E} (hx : x ∈ U) (v : Fin k → E) (a b : E) : iteratedDMB (k + 1) f (x, Fin.snoc v (a + b)) = iteratedDMB (k + 1) f (x, Fin.snoc v a) + iteratedDMB (k + 1) f (x, Fin.snoc v b)

Linearity of d^(k+1) f (x, ·) in the last direction.

theorem LCAnalysis.ContDiffMBOn.iteratedDMB_snoc_smul {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {m k : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn m f U) (hk : k + 1 ≤ m) {x : E} (hx : x ∈ U) (v : Fin k → E) (c : ℝ) (a : E) : iteratedDMB (k + 1) f (x, Fin.snoc v (c • a)) = c • iteratedDMB (k + 1) f (x, Fin.snoc v a)

theorem LCAnalysis.ContDiffMBOn.exists_iteratedDMB_multilinear {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {k : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn k f U) {x : E} (hx : x ∈ U) : ∃ (M : E [×k]→L[ℝ] F), (∀ (v : Fin k → E), M v = iteratedDMB k f (x, v)) ∧ ∀ (σ : Equiv.Perm (Fin k)) (v : Fin k → E), M (v ∘ ⇑σ) = M v

Proposition 1.3.17: for f of class C^k and x ∈ U, d^(k) f (x, ·) is a continuous symmetric k-linear map.