# Documentation

Mathlib.Topology.ContinuousFunction.ZeroAtInfty

# 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)
• toFun : αβ
• continuous_toFun : Continuous s.toFun
• zero_at_infty' : Filter.Tendsto s.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.

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.

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.

Instances For
class ZeroAtInftyContinuousMapClass (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [] [Zero β] [] extends :
Type (max (max u_2 u_3) u_4)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• 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.

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.

Instances
instance ZeroAtInftyContinuousMap.instCoeFun {α : Type u} {β : Type v} [] [] [Zero β] :
CoeFun () fun x => αβ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun directly.

instance ZeroAtInftyContinuousMap.instCoeTC {F : Type u_1} {α : Type u} {β : Type v} [] [] [Zero β] [] :
@[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.

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

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

Instances For
def ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass.ofCompact {α : Type u} {β : Type v} [] [] [Zero β] {G : Type u_2} [] [] :

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.

Instances For

### 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 β] :
instance ZeroAtInftyContinuousMap.instInhabited {α : Type u} {β : Type v} [] [] [Zero β] :
@[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} [] [] [] [] :
@[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} [] [] [] [] :
instance ZeroAtInftyContinuousMap.instSemigroupWithZero {α : Type u} {β : Type v} [] [] [] :
instance ZeroAtInftyContinuousMap.instAdd {α : Type u} {β : Type v} [] [] [] [] :
@[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} [] [] [] [] :
@[simp]
theorem ZeroAtInftyContinuousMap.coe_nsmulRec {α : Type u} {β : Type v} [] [] [] [] (f : ) (n : ) :
↑(nsmulRec n f) = n f
instance ZeroAtInftyContinuousMap.instNatSMul {α : Type u} {β : Type v} [] [] [] [] :
instance ZeroAtInftyContinuousMap.instAddMonoid {α : Type u} {β : Type v} [] [] [] [] :
instance ZeroAtInftyContinuousMap.instAddCommMonoid {α : Type u} {β : Type v} [] [] [] [] :
instance ZeroAtInftyContinuousMap.instNeg {α : Type u} {β : Type v} [] [] [] :
@[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} [] [] [] :
@[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
@[simp]
theorem ZeroAtInftyContinuousMap.coe_zsmulRec {α : Type u} {β : Type v} [] [] [] (f : ) (z : ) :
↑(zsmulRec z f) = z f
instance ZeroAtInftyContinuousMap.instIntSMul {α : Type u} {β : Type v} [] [] [] :
instance ZeroAtInftyContinuousMap.instAddGroup {α : Type u} {β : Type v} [] [] [] :
instance ZeroAtInftyContinuousMap.instAddCommGroup {α : Type u} {β : Type v} [] [] [] :
instance ZeroAtInftyContinuousMap.instSMul {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [Zero R] [] [] :
SMul R ()
@[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.instIsCentralScalar {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [Zero R] [] [] [] [] :
instance ZeroAtInftyContinuousMap.instSMulWithZero {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [Zero R] [] [] :
instance ZeroAtInftyContinuousMap.instMulActionWithZero {α : Type u} {β : Type v} [] [] [Zero β] {R : Type u_2} [] [] [] :
instance ZeroAtInftyContinuousMap.instModule {α : Type u} {β : Type v} [] [] [] [] {R : Type u_2} [] [Module R β] [] :
instance ZeroAtInftyContinuousMap.instNonUnitalRing {α : Type u} {β : Type v} [] [] [] [] :
instance ZeroAtInftyContinuousMap.instNonUnitalCommRing {α : Type u} {β : Type v} [] [] [] :
instance ZeroAtInftyContinuousMap.instIsScalarTower {α : Type u} {β : Type v} [] [] {R : Type u_2} [] [Module R β] [] [] :
instance ZeroAtInftyContinuousMap.instSMulCommClass {α : Type u} {β : Type v} [] [] {R : Type u_2} [] [Module R β] [] [] :
theorem ZeroAtInftyContinuousMap.uniformContinuous {F : Type u_1} {β : Type v} {γ : Type w} [] [] [Zero γ] [] (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 β] [] (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 ZeroAtInftyContinuousMap.instBoundedContinuousMapClass {F : Type u_1} {α : Type u} {β : Type v} [] [] [Zero β] [] :
@[simp]
theorem ZeroAtInftyContinuousMap.toBcf_apply {α : Type u} {β : Type v} [] [] [Zero β] (f : ) (a : α) :
= f a
@[simp]
theorem ZeroAtInftyContinuousMap.toBcf_toFun {α : Type u} {β : Type v} [] [] [Zero β] (f : ) (a : α) :
= f a
def ZeroAtInftyContinuousMap.toBcf {α : Type u} {β : Type v} [] [] [Zero β] (f : ) :

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

Instances For
theorem ZeroAtInftyContinuousMap.toBcf_injective (α : Type u) (β : Type v) [] [] [Zero β] :
Function.Injective ZeroAtInftyContinuousMap.toBcf
noncomputable instance ZeroAtInftyContinuousMap.instMetricSpace {α : 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 metric space.

@[simp]
theorem ZeroAtInftyContinuousMap.dist_toBcf_eq_dist {α : Type u} {β : Type v} [] [] [Zero β] {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.closed_range_toBcf {α : Type u} {β : Type v} [] [] [Zero β] :
IsClosed (Set.range ZeroAtInftyContinuousMap.toBcf)
instance ZeroAtInftyContinuousMap.instCompleteSpace {α : Type u} {β : Type v} [] [] [Zero β] [] :

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

### 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.instNormedAddCommGroup {α : Type u} {β : Type v} [] :
@[simp]
theorem ZeroAtInftyContinuousMap.norm_toBcf_eq_norm {α : Type u} {β : Type v} [] {f : } :
noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalNormedRing {α : Type u} {β : Type v} [] :

### 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} [] [] [] [] [] :
@[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} [] [] [] [] [] [] :
instance ZeroAtInftyContinuousMap.instNormedStarGroup {α : Type u} {β : Type v} [] [] [] :
instance ZeroAtInftyContinuousMap.instStarModule {α : Type u} {β : Type v} [] {𝕜 : Type u_2} [Zero 𝕜] [Star 𝕜] [] [] [] [] [] [] [] :
instance ZeroAtInftyContinuousMap.instStarRing {α : Type u} {β : Type v} [] [] [] [] :
instance ZeroAtInftyContinuousMap.instCstarRing {α : Type u} {β : Type v} [] [] [] :

### 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.

Instances For
@[simp]
theorem ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [Zero δ] (f : ) (g : ) :
= f g
@[simp]
theorem ZeroAtInftyContinuousMap.comp_id {γ : Type w} {δ : Type u_2} [] [] [Zero δ] (f : ) :
@[simp]
theorem ZeroAtInftyContinuousMap.comp_assoc {α : Type u} {β : Type v} {γ : Type w} [] {δ : Type u_2} [] [] [] [Zero δ] (f : ) (g : ) (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.

Instances For
def ZeroAtInftyContinuousMap.compMulHom {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [] [] (g : ) :

Composition as a semigroup homomorphism.

Instances For
def ZeroAtInftyContinuousMap.compLinearMap {β : Type v} {γ : Type w} {δ : Type u_2} [] [] [] [] [] {R : Type u_3} [] [Module R δ] [] (g : ) :

Composition as a linear map.

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.

Instances For