Continuous families with a common compact spatial support give continuous paths in the space of bounded continuous functions, equipped with the uniform norm.

def EulerComparator.boundedOfCompactSupport {E : Type u_2} {V : Type u_3} [TopologicalSpace E] [NormedAddCommGroup V] (f : E → V) (hf : Continuous f) (hs : HasCompactSupport f) : BoundedContinuousFunction E V

A continuous, compactly supported function, regarded as a bounded continuous function.

Equations

• EulerComparator.boundedOfCompactSupport f hf hs = { toFun := f, continuous_toFun := hf, map_bounded' := ⋯ }

@[simp]

theorem EulerComparator.boundedOfCompactSupport_apply {E : Type u_2} {V : Type u_3} [TopologicalSpace E] [NormedAddCommGroup V] (f : E → V) (hf : Continuous f) (hs : HasCompactSupport f) (x : E) : (boundedOfCompactSupport f hf hs) x = f x

theorem EulerComparator.continuous_boundedOfCompactSupport {A : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace A] [TopologicalSpace E] [NormedAddCommGroup V] (u : A × E → V) (hu : Continuous u) (K : Set E) (hK : IsCompact K) (hs : ∀ (t : A), (tsupport fun (x : E) => u (t, x)) ⊆ K) : Continuous fun (t : A) => boundedOfCompactSupport (fun (x : E) => u (t, x)) ⋯ ⋯

Uniformly compact spatial support upgrades joint continuity to continuity in the bounded-continuous-function norm. No compactness assumption on the parameter space is needed.

def EulerComparator.compactSupportBoundedPath {A : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace A] [TopologicalSpace E] [NormedAddCommGroup V] (u : A × E → V) (hu : Continuous u) (K : Set E) (hK : IsCompact K) (hs : ∀ (t : A), (tsupport fun (x : E) => u (t, x)) ⊆ K) : C(A, BoundedContinuousFunction E V)

A continuous family with one common compact spatial support, bundled as a continuous path of bounded continuous functions.

Equations

• EulerComparator.compactSupportBoundedPath u hu K hK hs = { toFun := fun (t : A) => EulerComparator.boundedOfCompactSupport (fun (x : E) => u (t, x)) ⋯ ⋯, continuous_toFun := ⋯ }

@[simp]

theorem EulerComparator.compactSupportBoundedPath_apply {A : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace A] [TopologicalSpace E] [NormedAddCommGroup V] (u : A × E → V) (hu : Continuous u) (K : Set E) (hK : IsCompact K) (hs : ∀ (t : A), (tsupport fun (x : E) => u (t, x)) ⊆ K) (t : A) (x : E) : ((compactSupportBoundedPath u hu K hK hs) t) x = u (t, x)