mathlib3 documentation

topology.continuous_function.zero_at_infty

Continuous functions vanishing at infinity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

structure zero_at_infty_continuous_map (α : Type u) (β : Type v) [topological_space α] [has_zero β] [topological_space β] :
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*) [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)) [topological_space α] [has_zero β] [topological_space β] :
Type (max u_2 u_3 u_4)

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
@[protected, instance]

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

Equations
@[ext]
theorem zero_at_infty_continuous_map.ext {α : Type u} {β : Type v} [topological_space α] [topological_space β] [has_zero β] {f g : zero_at_infty_continuous_map α β} (h : (x : α), f x = g x) :
f = g
@[protected]

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} [topological_space α] [topological_space β] [has_zero β] (f : zero_at_infty_continuous_map α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem zero_at_infty_continuous_map.copy_eq {α : Type u} {β : Type v} [topological_space α] [topological_space β] [has_zero β] (f : zero_at_infty_continuous_map α β) (f' : α β) (h : f' = f) :
f.copy f' h = f

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

Equations

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

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.

@[simp]
theorem zero_at_infty_continuous_map.zero_apply {α : Type u} {β : Type v} [topological_space α] [topological_space β] (x : α) [has_zero β] :
0 x = 0
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
  • zero_at_infty_continuous_map.add_comm_group = function.injective.add_comm_group coe_fn zero_at_infty_continuous_map.add_comm_group._proof_3 zero_at_infty_continuous_map.add_comm_group._proof_4 zero_at_infty_continuous_map.add_comm_group._proof_5 zero_at_infty_continuous_map.add_comm_group._proof_6 zero_at_infty_continuous_map.add_comm_group._proof_7 zero_at_infty_continuous_map.add_comm_group._proof_8 zero_at_infty_continuous_map.add_comm_group._proof_9
@[simp]
theorem zero_at_infty_continuous_map.smul_apply {α : Type u} {β : Type v} [topological_space α] [topological_space β] [has_zero β] {R : Type u_1} [has_zero R] [smul_with_zero R β] [has_continuous_const_smul R β] (r : R) (f : zero_at_infty_continuous_map α β) (x : α) :
(r f) x = r f x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
  • zero_at_infty_continuous_map.non_unital_non_assoc_ring = function.injective.non_unital_non_assoc_ring coe_fn 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 = function.injective.non_unital_ring coe_fn 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 = function.injective.non_unital_comm_ring coe_fn 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

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} [topological_space α] [metric_space β] [has_zero β] [zero_at_infty_continuous_map_class F α β] (f : F) :
(C : ), (x y : α), has_dist.dist (f x) (f y) C

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} [topological_space α] [metric_space β] [has_zero β] (f : zero_at_infty_continuous_map α β) (a : α) :
(f.to_bcf) a = f a
@[protected, instance]

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

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]
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]

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.

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.comp_assoc {α : Type u} {β : Type v} {γ : Type w} [topological_space α] {δ : Type u_2} [topological_space β] [topological_space γ] [topological_space δ] [has_zero δ] (f : zero_at_infty_continuous_map γ δ) (g : cocompact_map β γ) (h : cocompact_map α β) :
(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} [topological_space β] [topological_space γ] [topological_space δ] [has_zero δ] (g : cocompact_map β γ) :
0.comp g = 0