Michal–Bastiani C^{k+1} maps between normed spaces are Fréchet C^k

Neeb–Glöckner, Infinite-Dimensional Lie Groups (arXiv:2602.12362), Proposition 2.3.17 (b). Their proof goes through the compact-open topology on L(E, F) and the exponential law (Theorem 1.7.30). Here we give a proof that stays in normed spaces: derivatives are tracked as continuous multilinear maps with the operator norm. We show, by induction on k and for all m simultaneously:

if g : U → L^m(E; F) is such that (x, v₁, …, vₘ) ↦ g x (v₁, …, vₘ) is C^{k+1} in the sense of Michal–Bastiani, then g is Fréchet C^k.

The derivative of g is curryLeft ∘ B, where B y (w, v) = d(ĝ)((y, v), (w, 0)) is (m + 1)-multilinear and is handled by the case (k, m + 1). For m = 0 we get the result for maps f : U → F.

def LCAnalysis.unc {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (g : E → E [×m]→L[ℝ] F) : E × (Fin m → E) → F

The uncurried version (x, v) ↦ g x v of g : E → L^m(E; F).

Equations

• LCAnalysis.unc g p = (g p.1) p.2

noncomputable def LCAnalysis.secondB {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (g : E → E [×m]→L[ℝ] F) (y : E) (u : Fin (m + 1) → E) : F

B y u = d(ĝ)((y, tail u), (u 0, 0)): the derivative of ĝ in the base direction u 0.

Equations

• LCAnalysis.secondB g y u = LCAnalysis.dMB (LCAnalysis.unc g) ((y, Fin.tail u), u 0, 0)

Comparison with Fréchet differentiability (Remark I.2.2)

On normed spaces, C^{k+1}_{MB} ⇒ C^k (Fréchet) ⇒ C^k_{MB}; in particular both notions of smoothness agree.

theorem HasFDerivAt.hasDirDerivAt {F' : Type v} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {E₁ : Type u_1} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] {f : E₁ → F'} {L : E₁ →L[ℝ] F'} {x : E₁} (hf : HasFDerivAt f L x) (h : E₁) : LCAnalysis.HasDirDerivAt f x h (L h)

A Fréchet derivative gives the directional derivatives.

theorem LCAnalysis.ContDiffOn.contDiffMBOn {F' : Type v} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {k : ℕ} {E₁ : Type u} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] {f : E₁ → F'} {U : Set E₁} : IsOpen U → ContDiffOn ℝ (↑k) f U → ContDiffMBOn k f U

Remark I.2.2: Fréchet C^k maps are C^k in the sense of Michal–Bastiani.

theorem LCAnalysis.unc_line {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} (y w : E) (V : Fin m → E) (t : ℝ) : unc g ((y, V) + t • (w, 0)) = (g (y + t • w)) V

theorem LCAnalysis.hasDirDerivAt_unc_add {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} {y w : E} {V V₁ V₂ : Fin m → E} {a b : F} (h : ∀ (z : E), (g z) V = (g z) V₁ + (g z) V₂) (h₁ : HasDirDerivAt (unc g) (y, V₁) (w, 0) a) (h₂ : HasDirDerivAt (unc g) (y, V₂) (w, 0) b) : HasDirDerivAt (unc g) (y, V) (w, 0) (a + b)

theorem LCAnalysis.hasDirDerivAt_unc_smul {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} {y w : E} {V V₁ : Fin m → E} {a : F} (c : ℝ) (h : ∀ (z : E), (g z) V = c • (g z) V₁) (h₁ : HasDirDerivAt (unc g) (y, V₁) (w, 0) a) : HasDirDerivAt (unc g) (y, V) (w, 0) (c • a)

noncomputable def LCAnalysis.secondBML {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} {U : Set E} (hU : IsOpen U) (hg : ContDiffMBOn 1 (unc g) (U ×ˢ Set.univ)) {y : E} (hy : y ∈ U) : MultilinearMap ℝ (fun (x : Fin (m + 1)) => E) F

For y ∈ U, secondB g y is (m + 1)-multilinear.

Equations

• LCAnalysis.secondBML hU hg hy = { toFun := LCAnalysis.secondB g y, map_update_add' := ⋯, map_update_smul' := ⋯ }

theorem LCAnalysis.secondBML_apply {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} {U : Set E} (hU : IsOpen U) (hg : ContDiffMBOn 1 (unc g) (U ×ˢ Set.univ)) {y : E} (hy : y ∈ U) (u : Fin (m + 1) → E) : (secondBML hU hg hy) u = secondB g y u

theorem LCAnalysis.continuousOn_secondB {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} {U : Set E} (hg : ContDiffMBOn 1 (unc g) (U ×ˢ Set.univ)) : ContinuousOn (fun (p : E × (Fin (m + 1) → E)) => secondB g p.1 p.2) (U ×ˢ Set.univ)

theorem LCAnalysis.secondB_bound {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} {U : Set E} (hU : IsOpen U) (hg : ContDiffMBOn 1 (unc g) (U ×ˢ Set.univ)) {x : E} (hx : x ∈ U) : ∃ δ > 0, ∃ C ≥ 0, ∀ (y : E), ‖y - x‖ < δ → y ∈ U ∧ ∀ (u : Fin (m + 1) → E), ‖secondB g y u‖ ≤ C * ∏ i : Fin (m + 1), ‖u i‖

Local uniform bound for secondB.

theorem LCAnalysis.hasDirDerivAt_unc_base {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} {U : Set E} (hg : ContDiffMBOn 1 (unc g) (U ×ˢ Set.univ)) {p : E} (hp : p ∈ U) (V : Fin m → E) (w : E) : HasDirDerivAt (fun (z : E) => (g z) V) p w (secondB g p (Fin.cons w V))

theorem LCAnalysis.norm_prod_cons {E : Type u} [NormedAddCommGroup E] {m : ℕ} (w : E) (V : Fin m → E) : ∏ i : Fin (m + 1), ‖Fin.cons w V i‖ = ‖w‖ * ∏ i : Fin m, ‖V i‖

theorem LCAnalysis.lipschitz_of_unc {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {g : E → E [×m]→L[ℝ] F} {U : Set E} (hU : IsOpen U) (hg : ContDiffMBOn 1 (unc g) (U ×ˢ Set.univ)) {x : E} (hx : x ∈ U) : ∃ δ > 0, ∃ C ≥ 0, ∀ (y : E), ‖y - x‖ < δ → y ∈ U ∧ ‖g y - g x‖ ≤ C * ‖y - x‖

g is locally Lipschitz in the operator norm.

theorem LCAnalysis.contDiffOn_of_unc {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] (k m : ℕ) {g : E → E [×m]→L[ℝ] F} {U : Set E} : IsOpen U → ContDiffMBOn (k + 1) (unc g) (U ×ˢ Set.univ) → ContDiffOn ℝ (↑k) g U

The main induction: if (x, v) ↦ g x v is C^{k+1} in the sense of Michal–Bastiani, then g : U → L^m(E; F) is Fréchet C^k.

theorem LCAnalysis.ContDiffMBOn.contDiffOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn (k + 1) f U) : ContDiffOn ℝ (↑k) f U

Neeb–Glöckner, Proposition 2.3.17 (b): C^{k+1} maps in the sense of Michal–Bastiani between open subsets of normed spaces are Fréchet C^k.

theorem LCAnalysis.smoothMBOn_iff_contDiffOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {U : Set E} (hU : IsOpen U) : SmoothMBOn f U ↔ ContDiffOn ℝ (↑⊤) f U

Smoothness in the sense of Michal–Bastiani and Fréchet agree on normed spaces (Neeb–Glöckner, Proposition 2.3.17).

C^2 maps are Fréchet C^1 (Neeb–Glöckner, Prop. 2.3.17 (b) for k = 1)

theorem LCAnalysis.ContDiffMBOn.d2_smul_right {E' : Type u} {F' : Type v} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {f : E' → F'} {U : Set E'} (hf : ContDiffMBOn 2 f U) {y : E'} (hy : y ∈ U) (v w : E') (c : ℝ) : dMB (dMB f) ((y, v), c • w, 0) = c • dMB (dMB f) ((y, v), w, 0)

theorem LCAnalysis.ContDiffMBOn.d2_smul_left {E' : Type u} {F' : Type v} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {f : E' → F'} {U : Set E'} (hU : IsOpen U) (hf : ContDiffMBOn 2 f U) {y : E'} (hy : y ∈ U) (v w : E') (c : ℝ) : dMB (dMB f) ((y, c • v), w, 0) = c • dMB (dMB f) ((y, v), w, 0)

theorem LCAnalysis.ContDiffMBOn.exists_d2_bound {E' : Type u} {F' : Type v} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {f : E' → F'} {U : Set E'} (hU : IsOpen U) (hf : ContDiffMBOn 2 f U) {x : E'} (hx : x ∈ U) : ∃ δ > 0, ∃ C ≥ 0, ∀ (z : E'), ‖z - x‖ < δ → z ∈ U ∧ ∀ (v w : E'), ‖dMB (dMB f) ((z, v), w, 0)‖ ≤ C * ‖v‖ * ‖w‖

Local bilinear bound for the second derivative.

theorem LCAnalysis.ContDiffMBOn.dMB_sub_le {E' : Type u} {F' : Type v} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {f : E' → F'} {U : Set E'} (hU : IsOpen U) (hf : ContDiffMBOn 2 f U) {x : E'} (hx : x ∈ U) : ∃ δ > 0, ∃ C ≥ 0, ∀ (y : E'), ‖y - x‖ < δ → y ∈ U ∧ ∀ (v : E'), ‖dMB f (y, v) - dMB f (x, v)‖ ≤ C * ‖v‖ * ‖y - x‖

Lipschitz estimate for x ↦ df(x)(v).

theorem LCAnalysis.ContDiffMBOn.contDiffOn_one {E' : Type u} {F' : Type v} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {f : E' → F'} {U : Set E'} (hU : IsOpen U) (hf : ContDiffMBOn 2 f U) : ContDiffOn ℝ 1 f U

Neeb–Glöckner, Proposition 2.3.17 (b) for k = 1: a C^2 map in the sense of Michal–Bastiani between open subsets of normed spaces is continuously Fréchet differentiable.