# Continuous functions vanishing at infinity #

The type of continuous functions vanishing at infinity. When the domain is compact C(α, β) ≃ C₀(α, β) via the identity map. When the codomain is a metric space, every continuous map which vanishes at infinity is a bounded continuous function. When the domain is a locally compact space, this type has nice properties.

## TODO #

• Create more intances of algebraic structures (e.g., NonUnitalSemiring) once the necessary type classes (e.g., TopologicalRing) are sufficiently generalized.
• Relate the unitization of C₀(α, β) to the Alexandroff compactification.
structure ZeroAtInftyContinuousMap (α : Type u) (β : Type v) [] [Zero β] [] extends :
Type (max u v)

C₀(α, β) is the type of continuous functions α → β which vanish at infinity from a topological space to a metric space with a zero element.

When possible, instead of parametrizing results over (f : C₀(α, β)), you should parametrize over (F : Type*) [ZeroAtInftyContinuousMapClass F α β] (f : F).

When you extend this structure, make sure to extend ZeroAtInftyContinuousMapClass.

• toFun : αβ
• continuous_toFun : Continuous self.toFun
• zero_at_infty' : Filter.Tendsto self.toFun () (nhds 0)

The function tends to zero along the cocompact filter.

Instances For
theorem ZeroAtInftyContinuousMap.zero_at_infty' {α : Type u} {β : Type v} [] [Zero β] [] (self : ) :
Filter.Tendsto self.toFun () (nhds 0)

The function tends to zero along the cocompact filter.

C₀(α, β) is the type of continuous functions α → β which vanish at infinity from a topological space to a metric space with a zero element.

When possible, instead of parametrizing results over (f : C₀(α, β)), you should parametrize over (F : Type*) [ZeroAtInftyContinuousMapClass F α β] (f : F).

When you extend this structure, make sure to extend ZeroAtInftyContinuousMapClass.

Equations
• One or more equations did not get rendered due to their size.
Instances For

C₀(α, β) is the type of continuous functions α → β which vanish at infinity from a topological space to a metric space with a zero element.

When possible, instead of parametrizing results over (f : C₀(α, β)), you should parametrize over (F : Type*) [ZeroAtInftyContinuousMapClass F α β] (f : F).

When you extend this structure, make sure to extend ZeroAtInftyContinuousMapClass.

Equations
Instances For
class ZeroAtInftyContinuousMapClass (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [] [Zero β] [] [FunLike F α β] extends :

ZeroAtInftyContinuousMapClass F α β states that F is a type of continuous maps which vanish at infinity.

You should also extend this typeclass when you extend ZeroAtInftyContinuousMap.

• map_continuous : ∀ (f : F),
• zero_at_infty : ∀ (f : F), Filter.Tendsto (f) () (nhds 0)

Each member of the class tends to zero along the cocompact filter.

Instances
theorem ZeroAtInftyContinuousMapClass.zero_at_infty {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [] [Zero β] [] [FunLike F α β] [self : ] (f : F) :
Filter.Tendsto (f) () (nhds 0)

Each member of the class tends to zero along the cocompact filter.

instance ZeroAtInftyContinuousMap.instFunLike {α : Type u} {β : Type v} [] [] [Zero β] :
FunLike () α β
Equations
• ZeroAtInftyContinuousMap.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
Equations
• =
instance ZeroAtInftyContinuousMap.instCoeTC {F : Type u_1} {α : Type u} {β : Type v} [] [] [Zero β] [FunLike F α β] [] :
Equations
• ZeroAtInftyContinuousMap.instCoeTC = { coe := fun (f : F) => { toFun := f, continuous_toFun := , zero_at_infty' := } }
@[simp]
theorem ZeroAtInftyContinuousMap.coe_toContinuousMap {α : Type u} {β : Type v} [] [] [Zero β] (f : ) :
f.toContinuousMap = f
theorem ZeroAtInftyContinuousMap.ext {α : Type u} {β : Type v} [] [] [Zero β] {f : } {g : } (h : ∀ (x : α), f x = g x) :
f = g
def ZeroAtInftyContinuousMap.copy {α : Type u} {β : Type v} [] [] [Zero β] (f : ) (f' : αβ) (h : f' = f) :

Copy of a ZeroAtInftyContinuousMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• f.copy f' h = { toFun := f', continuous_toFun := , zero_at_infty' := }
Instances For
@[simp]
theorem ZeroAtInftyContinuousMap.coe_copy {α : Type u} {β : Type v} [] [] [Zero β] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem ZeroAtInftyContinuousMap.copy_eq {α : Type u} {β : Type v} [] [] [Zero β] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
theorem ZeroAtInftyContinuousMap.eq_of_empty {α : Type u} {β : Type v} [] [] [Zero β] [] (f : ) (g : ) :
f = g
@[simp]
theorem ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_apply_toFun {α : Type u} {β : Type v} [] [] [Zero β] [] (f : C(α, β)) (a : α) :
(ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty f) a = f a
@[simp]
theorem ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_symm_apply {α : Type u} {β : Type v} [] [] [Zero β] [] (f : ) :
ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty.symm f = f

A continuous function on a compact space is automatically a continuous function vanishing at infinity.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass.ofCompact {α : Type u} {β : Type v} [] [] [Zero β] {G : Type u_2} [FunLike G α β] [] [] :

A continuous function on a compact space is automatically a continuous function vanishing at infinity. This is not an instance to avoid type class loops.

### Algebraic structure #

Whenever β has suitable algebraic structure and a compatible topological structure, then C₀(α, β) inherits a corresponding algebraic structure. The primary exception to this is that C₀(α, β) will not have a multiplicative identity.

instance ZeroAtInftyContinuousMap.instZero {α : Type u} {β : Type v} [] [] [Zero β] :
Equations
• ZeroAtInftyContinuousMap.instZero = { zero := { toContinuousMap := 0, zero_at_infty' := } }
instance ZeroAtInftyContinuousMap.instInhabited {α : Type u} {β : Type v} [] [] [Zero β] :
Equations
• ZeroAtInftyContinuousMap.instInhabited = { default := 0 }
@[simp]
theorem ZeroAtInftyContinuousMap.coe_zero {α : Type u} {β : Type v} [] [] [Zero β] :
0 = 0
theorem ZeroAtInftyContinuousMap.zero_apply {α : Type u} {β : Type v} [] [] (x : α) [Zero β] :
0 x = 0
instance ZeroAtInftyContinuousMap.instMul {α : Type u} {β : Type v} [] [] [] [] :
Equations
• ZeroAtInftyContinuousMap.instMul = { mul := fun (f g : ) => { toContinuousMap := f * g, zero_at_infty' := } }
@[simp]
theorem ZeroAtInftyContinuousMap.coe_mul {α : Type u} {β : Type v} [] [] [] [] (f : ) (g : ) :
(f * g) = f * g
theorem ZeroAtInftyContinuousMap.mul_apply {α : Type u} {β : Type v} [] [] (x : α) [] [] (f : ) (g : ) :
(f * g) x = f x * g x
instance ZeroAtInftyContinuousMap.instMulZeroClass {α : Type u} {β : Type v} [] [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instSemigroupWithZero {α : Type u} {β : Type v} [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instAdd {α : Type u} {β : Type v} [] [] [] [] :
Equations
• ZeroAtInftyContinuousMap.instAdd = { add := fun (f g : ) => { toContinuousMap := f + g, zero_at_infty' := } }
@[simp]
theorem ZeroAtInftyContinuousMap.coe_add {α : Type u} {β : Type v} [] [] [] [] (f : ) (g : ) :
(f + g) = f + g
theorem ZeroAtInftyContinuousMap.add_apply {α : Type u} {β : Type v} [] [] (x : α) [] [] (f : ) (g : ) :
(f + g) x = f x + g x
instance ZeroAtInftyContinuousMap.instAddZeroClass {α : Type u} {β : Type v} [] [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instSMul {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [Zero R] [] [] :
SMul R ()
Equations
• ZeroAtInftyContinuousMap.instSMul = { smul := fun (r : R) (f : ) => { toFun := r f, continuous_toFun := , zero_at_infty' := } }
@[simp]
theorem ZeroAtInftyContinuousMap.coe_smul {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [Zero R] [] [] (r : R) (f : ) :
(r f) = r f
theorem ZeroAtInftyContinuousMap.smul_apply {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [Zero R] [] [] (r : R) (f : ) (x : α) :
(r f) x = r f x
instance ZeroAtInftyContinuousMap.instAddMonoid {α : Type u} {β : Type v} [] [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instAddCommMonoid {α : Type u} {β : Type v} [] [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instNeg {α : Type u} {β : Type v} [] [] [] :
Equations
• ZeroAtInftyContinuousMap.instNeg = { neg := fun (f : ) => { toContinuousMap := -f, zero_at_infty' := } }
@[simp]
theorem ZeroAtInftyContinuousMap.coe_neg {α : Type u} {β : Type v} [] [] [] (f : ) :
(-f) = -f
theorem ZeroAtInftyContinuousMap.neg_apply {α : Type u} {β : Type v} [] [] (x : α) [] (f : ) :
(-f) x = -f x
instance ZeroAtInftyContinuousMap.instSub {α : Type u} {β : Type v} [] [] [] :
Equations
• ZeroAtInftyContinuousMap.instSub = { sub := fun (f g : ) => { toContinuousMap := f - g, zero_at_infty' := } }
@[simp]
theorem ZeroAtInftyContinuousMap.coe_sub {α : Type u} {β : Type v} [] [] [] (f : ) (g : ) :
(f - g) = f - g
theorem ZeroAtInftyContinuousMap.sub_apply {α : Type u} {β : Type v} [] [] (x : α) [] (f : ) (g : ) :
(f - g) x = f x - g x
instance ZeroAtInftyContinuousMap.instAddGroup {α : Type u} {β : Type v} [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instAddCommGroup {α : Type u} {β : Type v} [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instIsCentralScalar {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [Zero R] [] [] [] [] :
Equations
• =
instance ZeroAtInftyContinuousMap.instSMulWithZero {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [Zero R] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instMulActionWithZero {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instModule {α : Type u} {β : Type v} [] [] [] [] {R : Type u_2} [] [Module R β] [] :
Equations
• ZeroAtInftyContinuousMap.instModule = Function.Injective.module R { toFun := DFunLike.coe, map_zero' := , map_add' := }
Equations
instance ZeroAtInftyContinuousMap.instNonUnitalSemiring {α : Type u} {β : Type v} [] [] :
Equations
Equations
instance ZeroAtInftyContinuousMap.instNonUnitalNonAssocRing {α : Type u} {β : Type v} [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instNonUnitalRing {α : Type u} {β : Type v} [] [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instNonUnitalCommRing {α : Type u} {β : Type v} [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instIsScalarTower {α : Type u} {β : Type v} [] [] {R : Type u_2} [] [Module R β] [] [] :
Equations
• =
instance ZeroAtInftyContinuousMap.instSMulCommClass {α : Type u} {β : Type v} [] [] {R : Type u_2} [] [Module R β] [] [] :
Equations
• =
theorem ZeroAtInftyContinuousMap.uniformContinuous {F : Type u_1} {β : Type v} {γ : Type w} [] [] [Zero γ] [FunLike F β γ] [] (f : F) :

### Metric structure #

When β is a metric space, then every element of C₀(α, β) is bounded, and so there is a natural inclusion map ZeroAtInftyContinuousMap.toBCF : C₀(α, β) → (α →ᵇ β). Via this map C₀(α, β) inherits a metric as the pullback of the metric on α →ᵇ β. Moreover, this map has closed range in α →ᵇ β and consequently C₀(α, β) is a complete space whenever β is complete.

theorem ZeroAtInftyContinuousMap.bounded {F : Type u_1} {α : Type u} {β : Type v} [] [Zero β] [FunLike F α β] [] (f : F) :
∃ (C : ), ∀ (x y : α), dist (f x) (f y) C
theorem ZeroAtInftyContinuousMap.isBounded_range {α : Type u} {β : Type v} [] [Zero β] (f : ) :
theorem ZeroAtInftyContinuousMap.isBounded_image {α : Type u} {β : Type v} [] [Zero β] (f : ) (s : Set α) :
@[instance 100]
instance ZeroAtInftyContinuousMap.instBoundedContinuousMapClass {F : Type u_1} {α : Type u} {β : Type v} [] [Zero β] [FunLike F α β] [] :
Equations
• =
@[simp]
theorem ZeroAtInftyContinuousMap.toBCF_apply {α : Type u} {β : Type v} [] [Zero β] (f : ) (a : α) :
f.toBCF a = f a
@[simp]
theorem ZeroAtInftyContinuousMap.toBCF_toFun {α : Type u} {β : Type v} [] [Zero β] (f : ) (a : α) :
f.toBCF a = f a
def ZeroAtInftyContinuousMap.toBCF {α : Type u} {β : Type v} [] [Zero β] (f : ) :

Construct a bounded continuous function from a continuous function vanishing at infinity.

Equations
• f.toBCF = { toContinuousMap := f, map_bounded' := }
Instances For
theorem ZeroAtInftyContinuousMap.toBCF_injective (α : Type u) (β : Type v) [] [Zero β] :
Function.Injective ZeroAtInftyContinuousMap.toBCF
noncomputable instance ZeroAtInftyContinuousMap.instPseudoMetricSpace {α : Type u} {β : Type v} [] [Zero β] :

The type of continuous functions vanishing at infinity, with the uniform distance induced by the inclusion ZeroAtInftyContinuousMap.toBCF, is a pseudo-metric space.

Equations
noncomputable instance ZeroAtInftyContinuousMap.instMetricSpace {α : Type u} [] {β : Type u_2} [] [Zero β] :

The type of continuous functions vanishing at infinity, with the uniform distance induced by the inclusion ZeroAtInftyContinuousMap.toBCF, is a metric space.

Equations
• ZeroAtInftyContinuousMap.instMetricSpace = MetricSpace.induced ZeroAtInftyContinuousMap.toBCF inferInstance
@[simp]
theorem ZeroAtInftyContinuousMap.dist_toBCF_eq_dist {α : Type u} {β : Type v} [] [Zero β] {f : } {g : } :
dist f.toBCF g.toBCF = dist f g
theorem ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly {α : Type u} {β : Type v} [] [Zero β] {ι : Type u_2} {F : ι} {f : } {l : } :
Filter.Tendsto F l (nhds f) TendstoUniformly (fun (i : ι) => (F i)) (f) l

Convergence in the metric on C₀(α, β) is uniform convergence.

theorem ZeroAtInftyContinuousMap.isometry_toBCF {α : Type u} {β : Type v} [] [Zero β] :
Isometry ZeroAtInftyContinuousMap.toBCF
theorem ZeroAtInftyContinuousMap.isClosed_range_toBCF {α : Type u} {β : Type v} [] [Zero β] :
IsClosed (Set.range ZeroAtInftyContinuousMap.toBCF)
@[deprecated ZeroAtInftyContinuousMap.isClosed_range_toBCF]
theorem ZeroAtInftyContinuousMap.closed_range_toBCF {α : Type u} {β : Type v} [] [Zero β] :
IsClosed (Set.range ZeroAtInftyContinuousMap.toBCF)

Alias of ZeroAtInftyContinuousMap.isClosed_range_toBCF.

instance ZeroAtInftyContinuousMap.instCompleteSpace {α : Type u} {β : Type v} [] [Zero β] [] :

Continuous functions vanishing at infinity taking values in a complete space form a complete space.

Equations
• =

### Normed space #

The norm structure on C₀(α, β) is the one induced by the inclusion toBCF : C₀(α, β) → (α →ᵇ b), viewed as an additive monoid homomorphism. Then C₀(α, β) is naturally a normed space over a normed field 𝕜 whenever β is as well.

noncomputable instance ZeroAtInftyContinuousMap.instSeminormedAddCommGroup {α : Type u} {β : Type v} [] :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance ZeroAtInftyContinuousMap.instNormedAddCommGroup {α : Type u} {β : Type v} [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem ZeroAtInftyContinuousMap.norm_toBCF_eq_norm {α : Type u} {β : Type v} [] {f : } :
f.toBCF = f
instance ZeroAtInftyContinuousMap.instNormedSpace {α : Type u} {β : Type v} [] {𝕜 : Type u_2} [] [] :
Equations
• ZeroAtInftyContinuousMap.instNormedSpace =
noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalSeminormedRing {α : Type u} {β : Type v} [] :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalNormedRing {α : Type u} {β : Type v} [] :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalSeminormedCommRing {α : Type u} {β : Type v} [] :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalNormedCommRing {α : Type u} {β : Type v} [] :
Equations
• One or more equations did not get rendered due to their size.

### Star structure #

It is possible to equip C₀(α, β) with a pointwise star operation whenever there is a continuous star : β → β for which star (0 : β) = 0. We don't have quite this weak a typeclass, but StarAddMonoid is close enough.

The StarAddMonoid and NormedStarGroup classes on C₀(α, β) are inherited from their counterparts on α →ᵇ β. Ultimately, when β is a C⋆-ring, then so is C₀(α, β).

instance ZeroAtInftyContinuousMap.instStar {α : Type u} {β : Type v} [] [] [] [] [] :
Equations
• ZeroAtInftyContinuousMap.instStar = { star := fun (f : ) => { toFun := fun (x : α) => star (f x), continuous_toFun := , zero_at_infty' := } }
@[simp]
theorem ZeroAtInftyContinuousMap.coe_star {α : Type u} {β : Type v} [] [] [] [] [] (f : ) :
(star f) = star f
theorem ZeroAtInftyContinuousMap.star_apply {α : Type u} {β : Type v} [] [] [] [] [] (f : ) (x : α) :
(star f) x = star (f x)
instance ZeroAtInftyContinuousMap.instStarAddMonoid {α : Type u} {β : Type v} [] [] [] [] [] [] :
Equations
instance ZeroAtInftyContinuousMap.instNormedStarGroup {α : Type u} {β : Type v} [] [] [] :
Equations
• =
instance ZeroAtInftyContinuousMap.instStarModule {α : Type u} {β : Type v} [] {𝕜 : Type u_2} [Zero 𝕜] [Star 𝕜] [] [] [] [] [] [] [] :
Equations
• =
instance ZeroAtInftyContinuousMap.instStarRing {α : Type u} {β : Type v} [] [] [] [] :
Equations
• ZeroAtInftyContinuousMap.instStarRing = let __src := ZeroAtInftyContinuousMap.instStarAddMonoid;
instance ZeroAtInftyContinuousMap.instCstarRing {α : Type u} {β : Type v} [] [] [] :
Equations
• =

### C₀ as a functor #

For each β with sufficient structure, there is a contravariant functor C₀(-, β) from the category of topological spaces with morphisms given by CocompactMaps.

def ZeroAtInftyContinuousMap.comp {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [Zero δ] (f : ) (g : ) :

Composition of a continuous function vanishing at infinity with a cocompact map yields another continuous function vanishing at infinity.

Equations
• f.comp g = { toContinuousMap := (f).comp g, zero_at_infty' := }
Instances For
@[simp]
theorem ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [Zero δ] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem ZeroAtInftyContinuousMap.comp_id {γ : Type w} {δ : Type u_2} [] [] [Zero δ] (f : ) :
f.comp () = f
@[simp]
theorem ZeroAtInftyContinuousMap.comp_assoc {α : Type u} {β : Type v} {γ : Type w} [] {δ : Type u_2} [] [] [] [Zero δ] (f : ) (g : ) (h : ) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem ZeroAtInftyContinuousMap.zero_comp {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [Zero δ] (g : ) :
def ZeroAtInftyContinuousMap.compAddMonoidHom {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [] [] (g : ) :

Composition as an additive monoid homomorphism.

Equations
• = { toFun := fun (f : ) => f.comp g, map_zero' := , map_add' := }
Instances For
def ZeroAtInftyContinuousMap.compMulHom {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [] [] (g : ) :

Composition as a semigroup homomorphism.

Equations
• = { toFun := fun (f : ) => f.comp g, map_mul' := }
Instances For
def ZeroAtInftyContinuousMap.compLinearMap {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [] [] {R : Type u_3} [] [Module R δ] [] (g : ) :

Composition as a linear map.

Equations
• = { toFun := fun (f : ) => f.comp g, map_add' := , map_smul' := }
Instances For
def ZeroAtInftyContinuousMap.compNonUnitalAlgHom {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] {R : Type u_3} [] [Module R δ] [] (g : ) :

Composition as a non-unital algebra homomorphism.

Equations
• = { toFun := fun (f : ) => f.comp g, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For