mathlib documentation

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 #

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

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.coe_zero {α : Type u} {β : Type v} [topological_space α] [topological_space β] [has_zero β] :
0 = 0
theorem zero_at_infty_continuous_map.zero_apply {α : Type u} {β : Type v} [topological_space α] [topological_space β] (x : α) [has_zero β] :
0 x = 0
@[simp]
theorem zero_at_infty_continuous_map.mul_apply {α : Type u} {β : Type v} [topological_space α] [topological_space β] (x : α) [mul_zero_class β] [has_continuous_mul β] (f g : zero_at_infty_continuous_map α β) :
(f * g) x = f x * g x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem zero_at_infty_continuous_map.add_apply {α : Type u} {β : Type v} [topological_space α] [topological_space β] (x : α) [add_zero_class β] [has_continuous_add β] (f g : zero_at_infty_continuous_map α β) :
(f + g) x = f x + g x
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem zero_at_infty_continuous_map.neg_apply {α : Type u} {β : Type v} [topological_space α] [topological_space β] (x : α) [add_group β] [topological_add_group β] (f : zero_at_infty_continuous_map α β) :
(-f) x = -f x
@[simp]
theorem zero_at_infty_continuous_map.sub_apply {α : Type u} {β : Type v} [topological_space α] [topological_space β] (x : α) [add_group β] [topological_add_group β] (f g : zero_at_infty_continuous_map α β) :
(f - g) x = f x - g x
@[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.coe_smul {α : 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 α β) :
(r f) = r f
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
theorem zero_at_infty_continuous_map.bounded_image {α : Type u} {β : Type v} [topological_space α] [metric_space β] [has_zero β] (f : zero_at_infty_continuous_map α β) (s : set α) :

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]
noncomputable def zero_at_infty_continuous_map.metric_space {α : Type u} {β : Type v} [topological_space α] [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
theorem zero_at_infty_continuous_map.tendsto_iff_tendsto_uniformly {α : Type u} {β : Type v} [topological_space α] [metric_space β] [has_zero β] {ι : Type u_1} {F : ι → zero_at_infty_continuous_map α β} {f : zero_at_infty_continuous_map α β} {l : filter ι} :
filter.tendsto F l (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.

The natural inclusion to_bcf : C₀(α, β) → (α →ᵇ β) realized as an additive monoid homomorphism.

Equations
@[protected, instance]
Equations
@[protected, instance]
def zero_at_infty_continuous_map.normed_space {α : Type u} {β : Type v} [topological_space α] [normed_group β] {𝕜 : Type u_2} [normed_field 𝕜] [normed_space 𝕜 β] :
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]
def zero_at_infty_continuous_map.star_module {α : Type u} {β : Type v} [topological_space α] {𝕜 : Type u_2} [has_zero 𝕜] [has_star 𝕜] [add_monoid β] [star_add_monoid β] [topological_space β] [has_continuous_star β] [smul_with_zero 𝕜 β] [has_continuous_const_smul 𝕜 β] [star_module 𝕜 β] :
@[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} [topological_space β] [topological_space γ] [topological_space δ] [has_zero δ] (f : zero_at_infty_continuous_map γ δ) (g : cocompact_map β γ) :

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

Equations
@[simp]
@[simp]
theorem zero_at_infty_continuous_map.comp_id {γ : Type w} {δ : Type u_2} [topological_space γ] [topological_space δ] [has_zero δ] (f : zero_at_infty_continuous_map γ δ) :
@[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

Composition as an additive monoid homomorphism.

Equations

Composition as a semigroup homomorphism.

Equations