Differentiability of superposition operators on bounded continuous functions

Let G : X → Y be a Lipschitz map between normed spaces over ℝ or ℂ. Postcomposition with G is the superposition (or Nemytskii) operator f ↦ G ∘ f on bounded continuous functions, BoundedContinuousFunction.comp G hG : (α →ᵇ X) → (α →ᵇ Y), for the sup norm. This file shows that it is continuously differentiable wherever G is, in the following uniform sense.

Suppose that G has derivative G' x at every point x of a set s, that G' : X → (X →L[𝕜] Y) is uniformly continuous on s, and that the values of f₀ stay a fixed distance δ > 0 inside s. Nothing is assumed about G' off s. Then the superposition operator is differentiable at f₀, and its derivative is pointwise application of the family of derivatives, h ↦ (t ↦ G' (f₀ t) (h t)), that is applyCLM Φ for the bounded continuous family Φ t = G' (f₀ t); the Lipschitz constant of G bounds G' on s, so this family is bounded. The derivative is moreover strict, and the operator is C¹ near f₀.

Uniform continuity of G' is what makes the remainder estimate hold with one constant at all the points f₀ t at once; nothing makes the range of f₀ compact, for instance for curves on [0, ∞). The distance δ allows G to be differentiable only on part of its domain, as when a smooth map is cut off outside a ball by a merely Lipschitz retraction.

This is the differentiability input to the Lyapunov--Perron construction of stable manifolds. Its integral operator acts on bounded continuous curves through the superposition by the nonlinearity of the differential equation, and the implicit function theorem turns a C¹ operator into C¹ dependence of its fixed points on parameters.

Main declarations

• BoundedContinuousFunction.exists_eq_comp: along a function with values in s, the derivatives t ↦ G' (f t) form a bounded continuous family.
• BoundedContinuousFunction.hasFDerivAt_comp: the superposition operator is differentiable at f₀, with derivative h ↦ (t ↦ G' (f₀ t) (h t)).
• BoundedContinuousFunction.hasStrictFDerivAt_comp: the derivative is strict.
• BoundedContinuousFunction.contDiffAt_comp: the superposition operator is C¹ near f₀.
• BoundedContinuousFunction.contDiff_comp: when G is differentiable everywhere with a derivative uniformly continuous on bounded sets, the superposition operator is C¹.

References

• J. Appell and P. P. Zabrejko, Nonlinear Superposition Operators, Cambridge Tracts in Mathematics 95, Cambridge University Press, 1990.

theorem BoundedContinuousFunction.exists_eq_comp {α : Type u_1} {𝕜 : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {G : X → Y} {C : NNReal} {G' : X → X →L[𝕜] Y} {s : Set X} (hG : LipschitzWith C G) (hGs : ∀ x ∈ s, HasFDerivAt G (G' x) x) (hG' : ContinuousOn G' s) {f : BoundedContinuousFunction α X} (hf : ∀ (t : α), f t ∈ s) : ∃ (Φ : BoundedContinuousFunction α (X →L[𝕜] Y)), ∀ (t : α), Φ t = G' (f t)

Along a function f with values in s, the derivatives t ↦ G' (f t) form a bounded continuous family: they are bounded by the Lipschitz constant of G. This supplies the family Φ in BoundedContinuousFunction.hasFDerivAt_comp and BoundedContinuousFunction.hasStrictFDerivAt_comp.

theorem BoundedContinuousFunction.hasFDerivAt_comp {α : Type u_1} {𝕜 : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {G : X → Y} {C : NNReal} {G' : X → X →L[𝕜] Y} {s : Set X} {f₀ : BoundedContinuousFunction α X} {δ : ℝ} {Φ : BoundedContinuousFunction α (X →L[𝕜] Y)} [IsRCLikeNormedField 𝕜] (hG : LipschitzWith C G) (hGs : ∀ x ∈ s, HasFDerivAt G (G' x) x) (hG' : UniformContinuousOn G' s) (hδ : 0 < δ) (hf₀ : ∀ (t : α), Metric.ball (f₀ t) δ ⊆ s) (hΦ : ∀ (t : α), Φ t = G' (f₀ t)) : HasFDerivAt (comp G hG) (applyCLM Φ) f₀

The derivative of a superposition operator. Let G be Lipschitz, with derivative G' x at every point x of s, where G' is uniformly continuous on s. If the values of f₀ stay a distance δ > 0 inside s, then f ↦ G ∘ f is differentiable at f₀ for the sup norm, with derivative h ↦ (t ↦ G' (f₀ t) (h t)), that is applyCLM Φ for the bounded continuous family Φ t = G' (f₀ t).

theorem BoundedContinuousFunction.hasStrictFDerivAt_comp {α : Type u_1} {𝕜 : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {G : X → Y} {C : NNReal} {G' : X → X →L[𝕜] Y} {s : Set X} {f₀ : BoundedContinuousFunction α X} {δ : ℝ} {Φ : BoundedContinuousFunction α (X →L[𝕜] Y)} [IsRCLikeNormedField 𝕜] (hG : LipschitzWith C G) (hGs : ∀ x ∈ s, HasFDerivAt G (G' x) x) (hG' : UniformContinuousOn G' s) (hδ : 0 < δ) (hf₀ : ∀ (t : α), Metric.ball (f₀ t) δ ⊆ s) (hΦ : ∀ (t : α), Φ t = G' (f₀ t)) : HasStrictFDerivAt (comp G hG) (applyCLM Φ) f₀

Strict differentiability of a superposition operator. Under the hypotheses of BoundedContinuousFunction.hasFDerivAt_comp, the derivative h ↦ (t ↦ G' (f₀ t) (h t)) of f ↦ G ∘ f at f₀ is strict.

theorem BoundedContinuousFunction.contDiffAt_comp {α : Type u_1} {𝕜 : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {G : X → Y} {C : NNReal} {G' : X → X →L[𝕜] Y} {s : Set X} {f₀ : BoundedContinuousFunction α X} {δ : ℝ} [IsRCLikeNormedField 𝕜] (hG : LipschitzWith C G) (hGs : ∀ x ∈ s, HasFDerivAt G (G' x) x) (hG' : UniformContinuousOn G' s) (hδ : 0 < δ) (hf₀ : ∀ (t : α), Metric.ball (f₀ t) δ ⊆ s) : ContDiffAt 𝕜 1 (comp G hG) f₀

A superposition operator is C¹. Let G be Lipschitz, with derivative G' x at every point x of s, where G' is uniformly continuous on s. If the values of f₀ stay a distance δ > 0 inside s, then the map f ↦ G ∘ f is continuously differentiable at f₀.

theorem BoundedContinuousFunction.contDiff_comp {α : Type u_1} {𝕜 : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {G : X → Y} {C : NNReal} {G' : X → X →L[𝕜] Y} [IsRCLikeNormedField 𝕜] (hG : LipschitzWith C G) (hGs : ∀ (x : X), HasFDerivAt G (G' x) x) (hG' : ∀ (r : ℝ), UniformContinuousOn G' (Metric.ball 0 r)) : ContDiff 𝕜 1 (comp G hG)

A superposition operator is C¹, global form. If G is Lipschitz and differentiable everywhere, with a derivative G' that is uniformly continuous on every ball about 0, then f ↦ G ∘ f is continuously differentiable on the bounded continuous functions. Since each bounded continuous f₀ takes values in a ball, uniform continuity of G' on bounded sets suffices; it holds for instance when X is finite-dimensional and G' is continuous.