Smooth postcomposition in the uniform norm

Abstract

Nonlinear postcomposition preserves every finite differentiability order and smoothness on continuous maps from an arbitrary compact topological space.

ContinuousMap(K,E) denotes continuous maps with their existing sup norm. K is any compact topological space, including empty and infinite spaces. The field k is nontrivially normed; the differentiability results also assume IsRCLikeNormedField(k). E and F are normed k-spaces. The independent universe levels are a for K, b for k, u for E, and max(u,v) for F in the differentiability results. No completeness, finite dimension, Hausdorff assumption on K, globally bounded derivative, or linearity of f is required. The bilinear operator and its evaluation identity allow independent E and F universes.

Definition 1.1 (Bounded pointwise application).

$$\begin{array}{r}\forall K:\mathrm{Type}\left(a\right),[\mathrm{TopologicalSpace}\left(K\right)][\mathrm{CompactSpace}\left(K\right)]\\ \forall k:\mathrm{Type}\left(b\right),[\mathrm{NontriviallyNormedField}\left(k\right)]\\ \forall E:\mathrm{Type}\left(u\right),[\mathrm{NormedAddCommGroup}\left(E\right)][\mathrm{NormedSpace}\left(k,E\right)]\\ \forall F:\mathrm{Type}\left(v\right),[\mathrm{NormedAddCommGroup}\left(F\right)][\mathrm{NormedSpace}\left(k,F\right)]\\ \mathrm{applyContinuousLinearMap}\left(\right):\mathrm{ContinuousLinearMap}\left(k,\mathrm{ContinuousMap}\left(K,\mathrm{ContinuousLinearMap}\left(k,E,F\right)\right),\mathrm{ContinuousLinearMap}\left(k,\mathrm{ContinuousMap}\left(K,E\right),\mathrm{ContinuousMap}\left(K,F\right)\right)\right)\end{array}$$

Formalization. D5/S3/Topology/CompactSmoothPostcomposition.applyContinuousLinearMap (✓ std3).

Citation. The Tau Ceti contributors (2026). Calculus on spaces of continuous maps. URL: https://github.com/TauCetiProject/TauCeti/blob/3924e3ef4afb8102b6a8e9893043c2c1a303f0d1/TauCeti/Analysis/Calculus/ContinuousMap.lean.

Commentary.

For A a continuous family of continuous linear maps and g a continuous E-valued map, applyContinuousLinearMap(A)(g) sends x to A(x)(g(x)). The pointwise operator-norm estimate bounds its uniform norm by the product of the uniform norms of A and g. The resulting operator is continuous linear in A and continuous linear in g.

Theorem 1.2 (Evaluation of the bilinear operator).

$$\begin{array}{r}\forall K:\mathrm{Type}\left(a\right),[\mathrm{TopologicalSpace}\left(K\right)][\mathrm{CompactSpace}\left(K\right)]\\ \forall k:\mathrm{Type}\left(b\right),[\mathrm{NontriviallyNormedField}\left(k\right)]\\ \forall E:\mathrm{Type}\left(u\right),[\mathrm{NormedAddCommGroup}\left(E\right)][\mathrm{NormedSpace}\left(k,E\right)]\\ \forall F:\mathrm{Type}\left(v\right),[\mathrm{NormedAddCommGroup}\left(F\right)][\mathrm{NormedSpace}\left(k,F\right)]\\ \forall A:\mathrm{ContinuousMap}\left(K,\mathrm{ContinuousLinearMap}\left(k,E,F\right)\right),\forall g:\mathrm{ContinuousMap}\left(K,E\right),\forall x:K,\\ \mathrm{apply}\left(\mathrm{applyContinuousLinearMap}\left(A\right),g,x\right)=\mathrm{apply}\left(\mathrm{apply}\left(A,x\right),\mathrm{apply}\left(g,x\right)\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Topology/CompactSmoothPostcomposition.applyContinuousLinearMap_apply (✓ std3). ∎

Citation. The Tau Ceti contributors (2026). Calculus on spaces of continuous maps. URL: https://github.com/TauCetiProject/TauCeti/blob/3924e3ef4afb8102b6a8e9893043c2c1a303f0d1/TauCeti/Analysis/Calculus/ContinuousMap.lean.

Commentary.

Evaluation at every x agrees with actual application of A(x) to g(x). This identity identifies the pointwise derivative in the uniform remainder estimate.

Theorem 1.3 (Frechet derivative of nonlinear postcomposition).

$$\begin{array}{r}\forall K:\mathrm{Type}\left(a\right),[\mathrm{TopologicalSpace}\left(K\right)][\mathrm{CompactSpace}\left(K\right)]\\ \forall k:\mathrm{Type}\left(b\right),[\mathrm{NontriviallyNormedField}\left(k\right)][\mathrm{IsRCLikeNormedField}\left(k\right)]\\ \forall E:\mathrm{Type}\left(u\right),[\mathrm{NormedAddCommGroup}\left(E\right)][\mathrm{NormedSpace}\left(k,E\right)]\\ \forall F:\mathrm{Type}\left(\max \left(u,v\right)\right),[\mathrm{NormedAddCommGroup}\left(F\right)][\mathrm{NormedSpace}\left(k,F\right)]\\ \forall f:\mathrm{ContinuousMap}\left(E,F\right),\mathrm{ContDiff}\left(k,1,f\right)\Rightarrow \\ \forall g:\mathrm{ContinuousMap}\left(K,E\right),\mathrm{HasFDerivAt}\left(g\mapsto \mathrm{comp}\left(f,g\right),\mathrm{applyContinuousLinearMap}\left(\mathrm{comp}\left(\mathrm{bundle}\left(\mathrm{fderiv}\left(k,f\right)\right),g\right)\right),g\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Topology/CompactSmoothPostcomposition.hasFDerivAt_postcomp (✓ std3). ∎

Citation. The Tau Ceti contributors (2026). Calculus on spaces of continuous maps. URL: https://github.com/TauCetiProject/TauCeti/blob/3924e3ef4afb8102b6a8e9893043c2c1a303f0d1/TauCeti/Analysis/Calculus/ContinuousMap.lean.

Commentary.

In this formula bundle(fderiv(k,f)) is the continuous map from E to continuous linear maps E to F, with continuity supplied by ContDiff(k,1,f). The derivative at g applies fderiv(k,f,g(x)) to the increment at x. Compactness of the image of g and continuity of fderiv give a common neighborhood on which the derivative varies by at most any prescribed positive c. The segment mean-value estimate gives the nonlinear remainder bound c times the uniform input distance. This is the Frechet little-o criterion.

Theorem 1.4 (Full nonlinear smooth-superposition theorem).

$$\begin{array}{r}\forall K:\mathrm{Type}\left(a\right),[\mathrm{TopologicalSpace}\left(K\right)][\mathrm{CompactSpace}\left(K\right)]\\ \forall k:\mathrm{Type}\left(b\right),[\mathrm{NontriviallyNormedField}\left(k\right)][\mathrm{IsRCLikeNormedField}\left(k\right)]\\ \forall E:\mathrm{Type}\left(u\right),[\mathrm{NormedAddCommGroup}\left(E\right)][\mathrm{NormedSpace}\left(k,E\right)]\\ \forall F:\mathrm{Type}\left(\max \left(u,v\right)\right),[\mathrm{NormedAddCommGroup}\left(F\right)][\mathrm{NormedSpace}\left(k,F\right)]\\ \forall n:\mathrm{NatInfinity}\left(\right),\forall f:\mathrm{ContinuousMap}\left(E,F\right),\\ \mathrm{ContDiff}\left(k,\mathrm{toOrder}\left(n\right),f\right)\Rightarrow \mathrm{ContDiff}\left(k,\mathrm{toOrder}\left(n\right),g\mapsto \mathrm{comp}\left(f,g\right)\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Topology/CompactSmoothPostcomposition.contDiff_postcomp (✓ std3). ∎

Citation. The Tau Ceti contributors (2026). Calculus on spaces of continuous maps. URL: https://github.com/TauCetiProject/TauCeti/blob/3924e3ef4afb8102b6a8e9893043c2c1a303f0d1/TauCeti/Analysis/Calculus/ContinuousMap.lean.

Commentary.

NatInfinity consists of the natural orders and infinity; toOrder is its canonical inclusion into NatInfinityOmega, the order type used by ContDiff. The lambda variable g ranges over ContinuousMap(K,E), so Post is a map into ContinuousMap(K,F). Order zero follows from continuity of postcomposition. For a successor order, apply the finite-order induction to the continuous derivative family, then compose with the bounded pointwise application operator. The displayed Frechet derivative identifies this derivative with that of postcomposition. The all-finite-orders criterion gives the infinite case. The max(u,v) codomain universe retains the derivative family at the same universe level.

These are the original selected proofs of the cited source. The nonlinear theorem is a supplier for smooth Picard residuals. It asserts no ODE existence, global-flow, half-density group, strong-continuity, generator, transport-equation or self-adjointness result.

References

• Truth anchor: D5/S3/Topology/CompactSmoothPostcomposition.applyContinuousLinearMap
• Truth anchor: D5/S3/Topology/CompactSmoothPostcomposition.applyContinuousLinearMap_apply
• Truth anchor: D5/S3/Topology/CompactSmoothPostcomposition.contDiff_postcomp
• Truth anchor: D5/S3/Topology/CompactSmoothPostcomposition.hasFDerivAt_postcomp