Bounded uniformly continuous functions

BoundedContinuousFunction.uniformContinuousSubmodule is the closed vector subspace of bounded continuous functions consisting of uniformly continuous functions. Its norm is the inherited supremum norm, and its carrier is a Banach space whenever the target is complete. This is the natural space for initial data whose diffusion evolution attains its trace in supremum norm; bounded continuity alone does not imply uniform attainment on a noncompact domain.

theorem BoundedContinuousFunction.isClosed_setOf_uniformContinuous {X : Type u_1} {F : Type u_2} [UniformSpace X] [PseudoMetricSpace F] : IsClosed {f : BoundedContinuousFunction X F | UniformContinuous ⇑f}

Uniformly continuous bounded functions form a closed subset for the supremum metric.

def BoundedContinuousFunction.uniformContinuousSubmodule (𝕜 : Type u_3) (X : Type u_4) (F : Type u_5) [NormedField 𝕜] [UniformSpace X] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : ClosedSubmodule 𝕜 (BoundedContinuousFunction X F)

The closed vector subspace of bounded uniformly continuous functions, with the inherited supremum norm. Its carrier is complete when F is complete.

@[simp]

theorem BoundedContinuousFunction.mem_uniformContinuousSubmodule {X : Type u_1} {F : Type u_2} [UniformSpace X] {𝕜 : Type u_3} [NormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : BoundedContinuousFunction X F) : f ∈ uniformContinuousSubmodule 𝕜 X F ↔ UniformContinuous ⇑f

Membership in the bounded uniformly continuous subspace.