Closed derivative graphs for bounded continuous functions

The Fréchet derivative identity is closed under uniform convergence of bounded continuous value and derivative fields. The derivative field may be read through a uniformly continuous map. These results supply the closed graph used to construct complete spaces of differentiable maps. The corresponding one-dimensional graph on a closed interval includes the one-sided derivatives at both endpoints.

The proofs use Mathlib's hasFDerivAt_of_tendstoUniformly.

theorem TauCeti.isClosed_setOf_hasFDerivAt_comp {𝕜 : Type u_1} {E : Type u} {Y : Type u_2} {Z : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [PseudoMetricSpace Z] (L : Z → E →L[𝕜] Y) (hL : UniformContinuous L) : IsClosed {J : BoundedContinuousFunction E Y × BoundedContinuousFunction E Z | ∀ (x : E), HasFDerivAt (⇑J.1) (L (J.2 x)) x}

The set of bounded continuous fields satisfying a Fréchet derivative identity, with the derivative read off the second field through a uniformly continuous map, is closed.

theorem TauCeti.isClosed_setOf_hasFDerivAt {𝕜 : Type u_1} {E : Type u} {Y : Type v} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] : IsClosed {J : BoundedContinuousFunction E Y × BoundedContinuousFunction E (E →L[𝕜] Y) | ∀ (x : E), HasFDerivAt (⇑J.1) (J.2 x) x}

The set of bounded continuous fields satisfying the Fréchet derivative identity is closed.

theorem TauCeti.isClosed_setOf_hasDerivWithinAt_Icc {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} (hab : a < b) : IsClosed {J : BoundedContinuousFunction (↑(Set.Icc a b)) F × BoundedContinuousFunction (↑(Set.Icc a b)) F | ∀ (t : ↑(Set.Icc a b)), HasDerivWithinAt (fun (s : ℝ) => J.1 (Set.projIcc a b ⋯ s)) (J.2 t) (Set.Icc a b) ↑t}

The derivative graph of bounded continuous fields on a nondegenerate closed interval is closed, including the one-sided derivative identities at its endpoints. The value field is extended outside the interval by projection onto the interval.