# mathlibdocumentation

topology.continuous_function.zero_at_infty

# 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., non_unital_semiring) once the necessary type classes (e.g., topological_ring) are sufficiently generalized.
• Relate the unitization of C₀(α, β) to the Alexandroff compactification.
structure zero_at_infty_continuous_map (α : Type u) (β : Type v) [has_zero β]  :
Type (max u v)
• to_continuous_map : C(α, β)
• zero_at_infty' : (nhds 0)

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*) [zero_at_infty_continuous_map_class F α β] (f : F).

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

Instances for zero_at_infty_continuous_map
@[class]
structure zero_at_infty_continuous_map_class (F : Type u_2) (α : out_param (Type u_3)) (β : out_param (Type u_4)) [has_zero β]  :
Type (max u_2 u_3 u_4)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_continuous : (f : F),
• zero_at_infty : (f : F), (nhds 0)

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

You should also extend this typeclass when you extend zero_at_infty_continuous_map.

Instances of this typeclass
Instances of other typeclasses for zero_at_infty_continuous_map_class
• zero_at_infty_continuous_map_class.has_sizeof_inst
@[instance]
def zero_at_infty_continuous_map_class.to_continuous_map_class (F : Type u_2) (α : out_param (Type u_3)) (β : out_param (Type u_4)) [has_zero β] [self : β] :
β
@[protected, instance]
def zero_at_infty_continuous_map.has_coe_to_fun {α : Type u} {β : Type v} [has_zero β] :
(λ (_x : , α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[protected, instance]
def zero_at_infty_continuous_map.has_coe_t {F : Type u_1} {α : Type u} {β : Type v} [has_zero β]  :
Equations
@[simp]
@[ext]
theorem zero_at_infty_continuous_map.ext {α : Type u} {β : Type v} [has_zero β] {f g : β} (h : (x : α), f x = g x) :
f = g
@[protected]
def zero_at_infty_continuous_map.copy {α : Type u} {β : Type v} [has_zero β] (f : β) (f' : α β) (h : f' = f) :

Copy of a zero_at_infinity_continuous_map with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_copy {α : Type u} {β : Type v} [has_zero β] (f : β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem zero_at_infty_continuous_map.copy_eq {α : Type u} {β : Type v} [has_zero β] (f : β) (f' : α β) (h : f' = f) :
f.copy f' h = f
theorem zero_at_infty_continuous_map.eq_of_empty {α : Type u} {β : Type v} [has_zero β] [is_empty α] (f g : β) :
f = g

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

Equations
@[simp]

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.

Equations
@[simp]
theorem zero_at_infty_continuous_map.zero_at_infty_continuous_map_class.of_compact_coe {α : Type u} {β : Type v} [has_zero β] {G : Type u_1} [ β] (g : G) (a : α) :

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_zero {α : Type u} {β : Type v} [has_zero β] :
0 = 0
theorem zero_at_infty_continuous_map.zero_apply {α : Type u} {β : Type v} (x : α) [has_zero β] :
0 x = 0
@[protected, instance]
def zero_at_infty_continuous_map.has_mul {α : Type u} {β : Type v}  :
Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_mul {α : Type u} {β : Type v} (f g : β) :
(f * g) = f * g
theorem zero_at_infty_continuous_map.mul_apply {α : Type u} {β : Type v} (x : α) (f g : β) :
(f * g) x = f x * g x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def zero_at_infty_continuous_map.has_add {α : Type u} {β : Type v}  :
Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_add {α : Type u} {β : Type v} (f g : β) :
(f + g) = f + g
theorem zero_at_infty_continuous_map.add_apply {α : Type u} {β : Type v} (x : α) (f g : β) :
(f + g) x = f x + g x
@[protected, instance]
Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_nsmul_rec {α : Type u} {β : Type v} [add_monoid β] (f : β) (n : ) :
f) = n f
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def zero_at_infty_continuous_map.has_neg {α : Type u} {β : Type v} [add_group β]  :
Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_neg {α : Type u} {β : Type v} [add_group β] (f : β) :
theorem zero_at_infty_continuous_map.neg_apply {α : Type u} {β : Type v} (x : α) [add_group β] (f : β) :
(-f) x = -f x
@[protected, instance]
def zero_at_infty_continuous_map.has_sub {α : Type u} {β : Type v} [add_group β]  :
Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_sub {α : Type u} {β : Type v} [add_group β] (f g : β) :
(f - g) = f - g
theorem zero_at_infty_continuous_map.sub_apply {α : Type u} {β : Type v} (x : α) [add_group β] (f g : β) :
(f - g) x = f x - g x
@[simp]
theorem zero_at_infty_continuous_map.coe_zsmul_rec {α : Type u} {β : Type v} [add_group β] (f : β) (z : ) :
f) = z f
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def zero_at_infty_continuous_map.has_smul {α : Type u} {β : Type v} [has_zero β] {R : Type u_1} [has_zero R] [ β]  :
Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_smul {α : Type u} {β : Type v} [has_zero β] {R : Type u_1} [has_zero R] [ β] (r : R) (f : β) :
(r f) = r f
theorem zero_at_infty_continuous_map.smul_apply {α : Type u} {β : Type v} [has_zero β] {R : Type u_1} [has_zero R] [ β] (r : R) (f : β) (x : α) :
(r f) x = r f x
@[protected, instance]
def zero_at_infty_continuous_map.is_central_scalar {α : Type u} {β : Type v} [has_zero β] {R : Type u_1} [has_zero R] [ β] [ β] [ β] :
@[protected, instance]
def zero_at_infty_continuous_map.smul_with_zero {α : Type u} {β : Type v} [has_zero β] {R : Type u_1} [has_zero R] [ β]  :
Equations
@[protected, instance]
def zero_at_infty_continuous_map.mul_action_with_zero {α : Type u} {β : Type v} [has_zero β] {R : Type u_1} [ β]  :
Equations
@[protected, instance]
def zero_at_infty_continuous_map.module {α : Type u} {β : Type v} {R : Type u_1} [semiring R] [ β]  :
Equations
@[protected, instance]
Equations
• zero_at_infty_continuous_map.non_unital_non_assoc_semiring = zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_2 zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_3 zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_4 zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_5 zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_6
@[protected, instance]
Equations
• zero_at_infty_continuous_map.non_unital_semiring = zero_at_infty_continuous_map.non_unital_semiring._proof_4 zero_at_infty_continuous_map.non_unital_semiring._proof_5 zero_at_infty_continuous_map.non_unital_semiring._proof_6 zero_at_infty_continuous_map.non_unital_semiring._proof_7 zero_at_infty_continuous_map.non_unital_semiring._proof_8
@[protected, instance]
Equations
• zero_at_infty_continuous_map.non_unital_comm_semiring = zero_at_infty_continuous_map.non_unital_comm_semiring._proof_4 zero_at_infty_continuous_map.non_unital_comm_semiring._proof_5 zero_at_infty_continuous_map.non_unital_comm_semiring._proof_6 zero_at_infty_continuous_map.non_unital_comm_semiring._proof_7 zero_at_infty_continuous_map.non_unital_comm_semiring._proof_8
@[protected, instance]
Equations
• zero_at_infty_continuous_map.non_unital_non_assoc_ring = zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_5 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_6 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_7 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_8 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_9 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_10 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_11 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_12
@[protected, instance]
Equations
• zero_at_infty_continuous_map.non_unital_ring = zero_at_infty_continuous_map.non_unital_ring._proof_7 zero_at_infty_continuous_map.non_unital_ring._proof_8 zero_at_infty_continuous_map.non_unital_ring._proof_9 zero_at_infty_continuous_map.non_unital_ring._proof_10 zero_at_infty_continuous_map.non_unital_ring._proof_11 zero_at_infty_continuous_map.non_unital_ring._proof_12 zero_at_infty_continuous_map.non_unital_ring._proof_13 zero_at_infty_continuous_map.non_unital_ring._proof_14
@[protected, instance]
Equations
• zero_at_infty_continuous_map.non_unital_comm_ring = zero_at_infty_continuous_map.non_unital_comm_ring._proof_7 zero_at_infty_continuous_map.non_unital_comm_ring._proof_8 zero_at_infty_continuous_map.non_unital_comm_ring._proof_9 zero_at_infty_continuous_map.non_unital_comm_ring._proof_10 zero_at_infty_continuous_map.non_unital_comm_ring._proof_11 zero_at_infty_continuous_map.non_unital_comm_ring._proof_12 zero_at_infty_continuous_map.non_unital_comm_ring._proof_13 zero_at_infty_continuous_map.non_unital_comm_ring._proof_14
@[protected, instance]
def zero_at_infty_continuous_map.is_scalar_tower {α : Type u} {β : Type v} {R : Type u_1} [semiring R] [ β] [ β] :
@[protected, instance]
def zero_at_infty_continuous_map.smul_comm_class {α : Type u} {β : Type v} {R : Type u_1} [semiring R] [ β] [ β] :
theorem zero_at_infty_continuous_map.uniform_continuous {F : Type u_1} {β : Type v} {γ : Type w} [has_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 zero_at_infty_continuous_map.to_bcf : 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.

@[protected]
theorem zero_at_infty_continuous_map.bounded {F : Type u_1} {α : Type u} {β : Type v} [metric_space β] [has_zero β] (f : F) :
(C : ), (x y : α), has_dist.dist (f x) (f y) C
theorem zero_at_infty_continuous_map.bounded_range {α : Type u} {β : Type v} [metric_space β] [has_zero β] (f : β) :
theorem zero_at_infty_continuous_map.bounded_image {α : Type u} {β : Type v} [metric_space β] [has_zero β] (f : β) (s : set α) :
@[protected, instance]
Equations
def zero_at_infty_continuous_map.to_bcf {α : Type u} {β : Type v} [metric_space β] [has_zero β] (f : β) :

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

Equations
@[simp]
theorem zero_at_infty_continuous_map.to_bcf_apply {α : Type u} {β : Type v} [metric_space β] [has_zero β] (f : β) (a : α) :
(f.to_bcf) a = f a
@[simp]
theorem zero_at_infty_continuous_map.to_bcf_to_continuous_map {α : Type u} {β : Type v} [metric_space β] [has_zero β] (f : β) :
@[protected, instance]
noncomputable def zero_at_infty_continuous_map.metric_space {α : Type u} {β : Type v} [metric_space β] [has_zero β] :

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

Equations
@[simp]
theorem zero_at_infty_continuous_map.dist_to_bcf_eq_dist {α : Type u} {β : Type v} [metric_space β] [has_zero β] {f g : β} :
=
theorem zero_at_infty_continuous_map.tendsto_iff_tendsto_uniformly {α : Type u} {β : Type v} [metric_space β] [has_zero β] {ι : Type u_1} {F : ι } {f : β} {l : filter ι} :
(nhds f) tendsto_uniformly (λ (i : ι), (F i)) f l

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

@[protected, instance]

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 to_bcf : C₀(α, β) → (α →ᵇ b), viewed as an additive monoid homomorphism. Then C₀(α, β) is naturally a normed space over a normed field 𝕜 whenever β is as well.

@[protected, instance]
noncomputable def zero_at_infty_continuous_map.normed_add_comm_group {α : Type u} {β : Type v}  :
Equations
@[simp]
@[protected, instance]
def zero_at_infty_continuous_map.normed_space {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [ β] :
Equations
@[protected, instance]
noncomputable def zero_at_infty_continuous_map.non_unital_normed_ring {α : Type u} {β : Type v}  :
Equations

### 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 star_add_monoid is close enough.

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

@[protected, instance]
Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_star {α : Type u} {β : Type v} [add_monoid β] (f : β) :
theorem zero_at_infty_continuous_map.star_apply {α : Type u} {β : Type v} [add_monoid β] (f : β) (x : α) :
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def zero_at_infty_continuous_map.star_module {α : Type u} {β : Type v} {𝕜 : Type u_2} [has_zero 𝕜] [has_star 𝕜] [add_monoid β] [ β] [ β] :
@[protected, instance]
Equations
@[protected, instance]

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

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

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

Equations
@[simp]
theorem zero_at_infty_continuous_map.coe_comp_to_continuous_fun {β : Type v} {γ : Type w} {δ : Type u_2} [has_zero δ] (f : δ) (g : γ) :
@[simp]
theorem zero_at_infty_continuous_map.comp_id {γ : Type w} {δ : Type u_2} [has_zero δ] (f : δ) :
f.comp = f
@[simp]
theorem zero_at_infty_continuous_map.comp_assoc {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [has_zero δ] (f : δ) (g : γ) (h : β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem zero_at_infty_continuous_map.zero_comp {β : Type v} {γ : Type w} {δ : Type u_2} [has_zero δ] (g : γ) :
0.comp g = 0
def zero_at_infty_continuous_map.comp_add_monoid_hom {β : Type v} {γ : Type w} {δ : Type u_2} [add_monoid δ] (g : γ) :

Composition as an additive monoid homomorphism.

Equations
def zero_at_infty_continuous_map.comp_mul_hom {β : Type v} {γ : Type w} {δ : Type u_2} (g : γ) :

Composition as a semigroup homomorphism.

Equations
def zero_at_infty_continuous_map.comp_linear_map {β : Type v} {γ : Type w} {δ : Type u_2} {R : Type u_1} [semiring R] [ δ] (g : γ) :

Composition as a linear map.

Equations
def zero_at_infty_continuous_map.comp_non_unital_alg_hom {β : Type v} {γ : Type w} {δ : Type u_2} {R : Type u_1} [semiring R] [ δ] (g : γ) :

Composition as a non-unital algebra homomorphism.

Equations