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) [TopologicalSpace α] [Zero β] [TopologicalSpace β] extends ContinuousMap :

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 (Filter.cocompact α) (nhds 0)
The function tends to zero along the cocompact filter.

Instances For

def ZeroAtInfty.«termC₀(_,_)» :

Lean.ParserDescr

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.

def ZeroAtInfty.«term_→C₀_» :

Lean.TrailingParserDescr

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.

class ZeroAtInftyContinuousMapClass (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [TopologicalSpace α] [Zero β] [TopologicalSpace β] [FunLike F α β] extends ContinuousMapClass :

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), Continuous ⇑f
zero_at_infty : ∀ (f : F), Filter.Tendsto (⇑f) (Filter.cocompact α) (nhds 0)
Each member of the class tends to zero along the cocompact filter.

Instances

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

FunLike (ZeroAtInftyContinuousMap α β) α β

Equations

ZeroAtInftyContinuousMap.instFunLike = { coe := fun (f : ZeroAtInftyContinuousMap α β) => f.toFun, coe_injective' := ⋯ }

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

ZeroAtInftyContinuousMapClass (ZeroAtInftyContinuousMap α β) α β

Equations

⋯ = ⋯

instance ZeroAtInftyContinuousMap.instCoeTC {F : Type u_1} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [FunLike F α β] [ZeroAtInftyContinuousMapClass F α β] :

CoeTC F (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instCoeTC = { coe := fun (f : F) => { toContinuousMap := { toFun := ⇑f, continuous_toFun := ⋯ }, zero_at_infty' := ⋯ } }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_toContinuousMap {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) :

⇑f.toContinuousMap = ⇑f

theorem ZeroAtInftyContinuousMap.ext {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {f : ZeroAtInftyContinuousMap α β} {g : ZeroAtInftyContinuousMap α β} (h : ∀ (x : α), f x = g x) :

f = g

def ZeroAtInftyContinuousMap.copy {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (f' : α → β) (h : f' = ⇑f) :

ZeroAtInftyContinuousMap α β

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

Equations

ZeroAtInftyContinuousMap.copy f f' h = { toContinuousMap := { toFun := f', continuous_toFun := ⋯ }, zero_at_infty' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_copy {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (f' : α → β) (h : f' = ⇑f) :

⇑(ZeroAtInftyContinuousMap.copy f f' h) = f'

theorem ZeroAtInftyContinuousMap.copy_eq {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (f' : α → β) (h : f' = ⇑f) :

ZeroAtInftyContinuousMap.copy f f' h = f

theorem ZeroAtInftyContinuousMap.eq_of_empty {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [IsEmpty α] (f : ZeroAtInftyContinuousMap α β) (g : ZeroAtInftyContinuousMap α β) :

f = g

@[simp]

theorem ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_symm_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [CompactSpace α] (f : ZeroAtInftyContinuousMap α β) :

ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty.symm f = ↑f

@[simp]

theorem ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_apply_toFun {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [CompactSpace α] (f : C(α, β)) (a : α) :

(ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty f) a = f a

def ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [CompactSpace α] :

C(α, β) ≃ ZeroAtInftyContinuousMap α β

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.

theorem ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass.ofCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {G : Type u_2} [FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α] :

ZeroAtInftyContinuousMapClass 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} [TopologicalSpace α] [TopologicalSpace β] [Zero β] :

Zero (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instZero = { zero := { toContinuousMap := 0, zero_at_infty' := ⋯ } }

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

Inhabited (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instInhabited = { default := 0 }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_zero {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] :

⇑0 = 0

theorem ZeroAtInftyContinuousMap.zero_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] (x : α) [Zero β] :

0 x = 0

instance ZeroAtInftyContinuousMap.instMul {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [MulZeroClass β] [ContinuousMul β] :

Mul (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instMul = { mul := fun (f g : ZeroAtInftyContinuousMap α β) => { toContinuousMap := ↑f * ↑g, zero_at_infty' := ⋯ } }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_mul {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [MulZeroClass β] [ContinuousMul β] (f : ZeroAtInftyContinuousMap α β) (g : ZeroAtInftyContinuousMap α β) :

⇑(f * g) = ⇑f * ⇑g

theorem ZeroAtInftyContinuousMap.mul_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] (x : α) [MulZeroClass β] [ContinuousMul β] (f : ZeroAtInftyContinuousMap α β) (g : ZeroAtInftyContinuousMap α β) :

(f * g) x = f x * g x

instance ZeroAtInftyContinuousMap.instMulZeroClass {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [MulZeroClass β] [ContinuousMul β] :

MulZeroClass (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instMulZeroClass = Function.Injective.mulZeroClass (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instSemigroupWithZero {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [SemigroupWithZero β] [ContinuousMul β] :

SemigroupWithZero (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instSemigroupWithZero = Function.Injective.semigroupWithZero (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instAdd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] :

Add (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instAdd = { add := fun (f g : ZeroAtInftyContinuousMap α β) => { toContinuousMap := ↑f + ↑g, zero_at_infty' := ⋯ } }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_add {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (f : ZeroAtInftyContinuousMap α β) (g : ZeroAtInftyContinuousMap α β) :

⇑(f + g) = ⇑f + ⇑g

theorem ZeroAtInftyContinuousMap.add_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] (x : α) [AddZeroClass β] [ContinuousAdd β] (f : ZeroAtInftyContinuousMap α β) (g : ZeroAtInftyContinuousMap α β) :

(f + g) x = f x + g x

instance ZeroAtInftyContinuousMap.instAddZeroClass {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] :

AddZeroClass (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instAddZeroClass = Function.Injective.addZeroClass (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯

@[simp]

theorem ZeroAtInftyContinuousMap.coe_nsmulRec {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : ZeroAtInftyContinuousMap α β) (n : ℕ) :

⇑(nsmulRec n f) = n • ⇑f

instance ZeroAtInftyContinuousMap.instNatSMul {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] :

SMul ℕ (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instNatSMul = { smul := fun (n : ℕ) (f : ZeroAtInftyContinuousMap α β) => { toContinuousMap := n • ↑f, zero_at_infty' := ⋯ } }

instance ZeroAtInftyContinuousMap.instAddMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] :

AddMonoid (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instAddMonoid = Function.Injective.addMonoid (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instAddCommMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] :

AddCommMonoid (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instAddCommMonoid = Function.Injective.addCommMonoid (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instNeg {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] :

Neg (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instNeg = { neg := fun (f : ZeroAtInftyContinuousMap α β) => { toContinuousMap := -↑f, zero_at_infty' := ⋯ } }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_neg {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : ZeroAtInftyContinuousMap α β) :

⇑(-f) = -⇑f

theorem ZeroAtInftyContinuousMap.neg_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] (x : α) [AddGroup β] [TopologicalAddGroup β] (f : ZeroAtInftyContinuousMap α β) :

(-f) x = -f x

instance ZeroAtInftyContinuousMap.instSub {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] :

Sub (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instSub = { sub := fun (f g : ZeroAtInftyContinuousMap α β) => { toContinuousMap := ↑f - ↑g, zero_at_infty' := ⋯ } }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_sub {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : ZeroAtInftyContinuousMap α β) (g : ZeroAtInftyContinuousMap α β) :

⇑(f - g) = ⇑f - ⇑g

theorem ZeroAtInftyContinuousMap.sub_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] (x : α) [AddGroup β] [TopologicalAddGroup β] (f : ZeroAtInftyContinuousMap α β) (g : ZeroAtInftyContinuousMap α β) :

(f - g) x = f x - g x

@[simp]

theorem ZeroAtInftyContinuousMap.coe_zsmulRec {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : ZeroAtInftyContinuousMap α β) (z : ℤ) :

⇑(zsmulRec z f) = z • ⇑f

instance ZeroAtInftyContinuousMap.instIntSMul {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] :

SMul ℤ (ZeroAtInftyContinuousMap α β)

Equations

One or more equations did not get rendered due to their size.

instance ZeroAtInftyContinuousMap.instAddGroup {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] :

AddGroup (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instAddGroup = Function.Injective.addGroup (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] :

AddCommGroup (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instAddCommGroup = Function.Injective.addCommGroup (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instSMul {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_2} [Zero R] [SMulWithZero R β] [ContinuousConstSMul R β] :

SMul R (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instSMul = { smul := fun (r : R) (f : ZeroAtInftyContinuousMap α β) => { toContinuousMap := { toFun := r • ⇑f, continuous_toFun := ⋯ }, zero_at_infty' := ⋯ } }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_smul {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_2} [Zero R] [SMulWithZero R β] [ContinuousConstSMul R β] (r : R) (f : ZeroAtInftyContinuousMap α β) :

⇑(r • f) = r • ⇑f

theorem ZeroAtInftyContinuousMap.smul_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_2} [Zero R] [SMulWithZero R β] [ContinuousConstSMul R β] (r : R) (f : ZeroAtInftyContinuousMap α β) (x : α) :

(r • f) x = r • f x

instance ZeroAtInftyContinuousMap.instIsCentralScalar {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_2} [Zero R] [SMulWithZero R β] [SMulWithZero Rᵐᵒᵖ β] [ContinuousConstSMul R β] [IsCentralScalar R β] :

IsCentralScalar R (ZeroAtInftyContinuousMap α β)

Equations

⋯ = ⋯

instance ZeroAtInftyContinuousMap.instSMulWithZero {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_2} [Zero R] [SMulWithZero R β] [ContinuousConstSMul R β] :

SMulWithZero R (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instSMulWithZero = Function.Injective.smulWithZero { toFun := DFunLike.coe, map_zero' := ⋯ } ⋯ ⋯

instance ZeroAtInftyContinuousMap.instMulActionWithZero {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_2} [MonoidWithZero R] [MulActionWithZero R β] [ContinuousConstSMul R β] :

MulActionWithZero R (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instMulActionWithZero = Function.Injective.mulActionWithZero { toFun := DFunLike.coe, map_zero' := ⋯ } ⋯ ⋯

instance ZeroAtInftyContinuousMap.instModule {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {R : Type u_2} [Semiring R] [Module R β] [ContinuousConstSMul R β] :

Module R (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instModule = Function.Injective.module R { toZeroHom := { toFun := DFunLike.coe, map_zero' := ⋯ }, map_add' := ⋯ } ⋯ ⋯

instance ZeroAtInftyContinuousMap.instNonUnitalNonAssocSemiring {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] :

NonUnitalNonAssocSemiring (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instNonUnitalNonAssocSemiring = Function.Injective.nonUnitalNonAssocSemiring (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instNonUnitalSemiring {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalSemiring β] [TopologicalSemiring β] :

NonUnitalSemiring (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instNonUnitalSemiring = Function.Injective.nonUnitalSemiring (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instNonUnitalCommSemiring {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommSemiring β] [TopologicalSemiring β] :

NonUnitalCommSemiring (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instNonUnitalCommSemiring = Function.Injective.nonUnitalCommSemiring (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instNonUnitalNonAssocRing {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocRing β] [TopologicalRing β] :

NonUnitalNonAssocRing (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instNonUnitalNonAssocRing = Function.Injective.nonUnitalNonAssocRing (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instNonUnitalRing {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalRing β] [TopologicalRing β] :

NonUnitalRing (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instNonUnitalRing = Function.Injective.nonUnitalRing (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instNonUnitalCommRing {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommRing β] [TopologicalRing β] :

NonUnitalCommRing (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing (fun (f : ZeroAtInftyContinuousMap α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ZeroAtInftyContinuousMap.instIsScalarTower {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] [Module R β] [ContinuousConstSMul R β] [IsScalarTower R β β] :

IsScalarTower R (ZeroAtInftyContinuousMap α β) (ZeroAtInftyContinuousMap α β)

Equations

⋯ = ⋯

instance ZeroAtInftyContinuousMap.instSMulCommClass {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] [Module R β] [ContinuousConstSMul R β] [SMulCommClass R β β] :

SMulCommClass R (ZeroAtInftyContinuousMap α β) (ZeroAtInftyContinuousMap α β)

Equations

⋯ = ⋯

theorem ZeroAtInftyContinuousMap.uniformContinuous {F : Type u_1} {β : Type v} {γ : Type w} [UniformSpace β] [UniformSpace γ] [Zero γ] [FunLike F β γ] [ZeroAtInftyContinuousMapClass F β γ] (f : F) :

UniformContinuous ⇑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} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] [FunLike F α β] [ZeroAtInftyContinuousMapClass F α β] (f : F) :

∃ (C : ℝ), ∀ (x y : α), dist (f x) (f y) ≤ C

theorem ZeroAtInftyContinuousMap.isBounded_range {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) :

Bornology.IsBounded (Set.range ⇑f)

theorem ZeroAtInftyContinuousMap.isBounded_image {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (s : Set α) :

Bornology.IsBounded (⇑f '' s)

instance ZeroAtInftyContinuousMap.instBoundedContinuousMapClass {F : Type u_1} {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] [FunLike F α β] [ZeroAtInftyContinuousMapClass F α β] :

BoundedContinuousMapClass F α β

Equations

⋯ = ⋯

@[simp]

theorem ZeroAtInftyContinuousMap.toBCF_toFun {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (a : α) :

(ZeroAtInftyContinuousMap.toBCF f) a = f a

@[simp]

theorem ZeroAtInftyContinuousMap.toBCF_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (a : α) :

(ZeroAtInftyContinuousMap.toBCF f) a = f a

def ZeroAtInftyContinuousMap.toBCF {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) :

BoundedContinuousFunction α β

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

Equations

ZeroAtInftyContinuousMap.toBCF f = { toContinuousMap := ↑f, map_bounded' := ⋯ }

theorem ZeroAtInftyContinuousMap.toBCF_injective (α : Type u) (β : Type v) [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] :

Function.Injective ZeroAtInftyContinuousMap.toBCF

noncomputable instance ZeroAtInftyContinuousMap.instPseudoMetricSpace {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] :

PseudoMetricSpace (ZeroAtInftyContinuousMap α β)

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

Equations

ZeroAtInftyContinuousMap.instPseudoMetricSpace = PseudoMetricSpace.induced ZeroAtInftyContinuousMap.toBCF inferInstance

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

MetricSpace (ZeroAtInftyContinuousMap α β)

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} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] {f : ZeroAtInftyContinuousMap α β} {g : ZeroAtInftyContinuousMap α β} :

dist (ZeroAtInftyContinuousMap.toBCF f) (ZeroAtInftyContinuousMap.toBCF g) = dist f g

theorem ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] {ι : Type u_2} {F : ι → ZeroAtInftyContinuousMap α β} {f : ZeroAtInftyContinuousMap α β} {l : Filter ι} :

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} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] :

Isometry ZeroAtInftyContinuousMap.toBCF

theorem ZeroAtInftyContinuousMap.isClosed_range_toBCF {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] :

IsClosed (Set.range ZeroAtInftyContinuousMap.toBCF)

@[deprecated ZeroAtInftyContinuousMap.isClosed_range_toBCF]

theorem ZeroAtInftyContinuousMap.closed_range_toBCF {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] :

IsClosed (Set.range ZeroAtInftyContinuousMap.toBCF)

Alias of ZeroAtInftyContinuousMap.isClosed_range_toBCF.

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

CompleteSpace (ZeroAtInftyContinuousMap α β)

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} [TopologicalSpace α] [SeminormedAddCommGroup β] :

SeminormedAddCommGroup (ZeroAtInftyContinuousMap α β)

Equations

One or more equations did not get rendered due to their size.

noncomputable instance ZeroAtInftyContinuousMap.instNormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] :

NormedAddCommGroup (ZeroAtInftyContinuousMap α β)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem ZeroAtInftyContinuousMap.norm_toBCF_eq_norm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] {f : ZeroAtInftyContinuousMap α β} :

‖ZeroAtInftyContinuousMap.toBCF f‖ = ‖f‖

instance ZeroAtInftyContinuousMap.instNormedSpaceZeroAtInftyContinuousMapToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstSeminormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] {𝕜 : Type u_2} [NormedField 𝕜] [NormedSpace 𝕜 β] :

NormedSpace 𝕜 (ZeroAtInftyContinuousMap α β)

Equations

One or more equations did not get rendered due to their size.

noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalSeminormedRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalSeminormedRing β] :

NonUnitalSeminormedRing (ZeroAtInftyContinuousMap α β)

Equations

One or more equations did not get rendered due to their size.

noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalNormedRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalNormedRing β] :

NonUnitalNormedRing (ZeroAtInftyContinuousMap α β)

Equations

One or more equations did not get rendered due to their size.

noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalSeminormedCommRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalSeminormedCommRing β] :

NonUnitalSeminormedCommRing (ZeroAtInftyContinuousMap α β)

Equations

One or more equations did not get rendered due to their size.

noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalNormedCommRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalNormedCommRing β] :

NonUnitalNormedCommRing (ZeroAtInftyContinuousMap α β)

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} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] :

Star (ZeroAtInftyContinuousMap α β)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_star {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] (f : ZeroAtInftyContinuousMap α β) :

⇑(star f) = star ⇑f

theorem ZeroAtInftyContinuousMap.star_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] (f : ZeroAtInftyContinuousMap α β) (x : α) :

(star f) x = star (f x)

instance ZeroAtInftyContinuousMap.instStarAddMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] [ContinuousAdd β] :

StarAddMonoid (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instStarAddMonoid = StarAddMonoid.mk ⋯

instance ZeroAtInftyContinuousMap.instNormedStarGroup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] :

NormedStarGroup (ZeroAtInftyContinuousMap α β)

Equations

⋯ = ⋯

instance ZeroAtInftyContinuousMap.instStarModule {α : Type u} {β : Type v} [TopologicalSpace α] {𝕜 : Type u_2} [Zero 𝕜] [Star 𝕜] [AddMonoid β] [StarAddMonoid β] [TopologicalSpace β] [ContinuousStar β] [SMulWithZero 𝕜 β] [ContinuousConstSMul 𝕜 β] [StarModule 𝕜 β] :

StarModule 𝕜 (ZeroAtInftyContinuousMap α β)

Equations

⋯ = ⋯

instance ZeroAtInftyContinuousMap.instStarRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalSemiring β] [StarRing β] [TopologicalSpace β] [ContinuousStar β] [TopologicalSemiring β] :

StarRing (ZeroAtInftyContinuousMap α β)

Equations

ZeroAtInftyContinuousMap.instStarRing = let __src := ZeroAtInftyContinuousMap.instStarAddMonoid; StarRing.mk ⋯

instance ZeroAtInftyContinuousMap.instCstarRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalNormedRing β] [StarRing β] [CstarRing β] :

CstarRing (ZeroAtInftyContinuousMap α β)

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} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : ZeroAtInftyContinuousMap γ δ) (g : CocompactMap β γ) :

ZeroAtInftyContinuousMap β δ

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

Equations

ZeroAtInftyContinuousMap.comp f g = { toContinuousMap := ContinuousMap.comp ↑f ↑g, zero_at_infty' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun {β : Type v} {γ : Type w} {δ : Type u_2} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : ZeroAtInftyContinuousMap γ δ) (g : CocompactMap β γ) :

⇑(ZeroAtInftyContinuousMap.comp f g) = ⇑f ∘ ⇑g

@[simp]

theorem ZeroAtInftyContinuousMap.comp_id {γ : Type w} {δ : Type u_2} [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : ZeroAtInftyContinuousMap γ δ) :

ZeroAtInftyContinuousMap.comp f (CocompactMap.id γ) = f

@[simp]

theorem ZeroAtInftyContinuousMap.comp_assoc {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] {δ : Type u_2} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : ZeroAtInftyContinuousMap γ δ) (g : CocompactMap β γ) (h : CocompactMap α β) :

ZeroAtInftyContinuousMap.comp (ZeroAtInftyContinuousMap.comp f g) h = ZeroAtInftyContinuousMap.comp f (CocompactMap.comp g h)

@[simp]

theorem ZeroAtInftyContinuousMap.zero_comp {β : Type v} {γ : Type w} {δ : Type u_2} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (g : CocompactMap β γ) :

ZeroAtInftyContinuousMap.comp 0 g = 0

def ZeroAtInftyContinuousMap.compAddMonoidHom {β : Type v} {γ : Type w} {δ : Type u_2} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [AddMonoid δ] [ContinuousAdd δ] (g : CocompactMap β γ) :

ZeroAtInftyContinuousMap γ δ →+ ZeroAtInftyContinuousMap β δ

Composition as an additive monoid homomorphism.

Equations

One or more equations did not get rendered due to their size.

def ZeroAtInftyContinuousMap.compMulHom {β : Type v} {γ : Type w} {δ : Type u_2} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [MulZeroClass δ] [ContinuousMul δ] (g : CocompactMap β γ) :

ZeroAtInftyContinuousMap γ δ →ₙ* ZeroAtInftyContinuousMap β δ

Composition as a semigroup homomorphism.

Equations

ZeroAtInftyContinuousMap.compMulHom g = { toFun := fun (f : ZeroAtInftyContinuousMap γ δ) => ZeroAtInftyContinuousMap.comp f g, map_mul' := ⋯ }

def ZeroAtInftyContinuousMap.compLinearMap {β : Type v} {γ : Type w} {δ : Type u_2} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [AddCommMonoid δ] [ContinuousAdd δ] {R : Type u_3} [Semiring R] [Module R δ] [ContinuousConstSMul R δ] (g : CocompactMap β γ) :

ZeroAtInftyContinuousMap γ δ →ₗ[R] ZeroAtInftyContinuousMap β δ

Composition as a linear map.

Equations

ZeroAtInftyContinuousMap.compLinearMap g = { toAddHom := { toFun := fun (f : ZeroAtInftyContinuousMap γ δ) => ZeroAtInftyContinuousMap.comp f g, map_add' := ⋯ }, map_smul' := ⋯ }

def ZeroAtInftyContinuousMap.compNonUnitalAlgHom {β : Type v} {γ : Type w} {δ : Type u_2} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {R : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring δ] [TopologicalSemiring δ] [Module R δ] [ContinuousConstSMul R δ] (g : CocompactMap β γ) :

ZeroAtInftyContinuousMap γ δ →ₙₐ[R] ZeroAtInftyContinuousMap β δ

Composition as a non-unital algebra homomorphism.

Equations

One or more equations did not get rendered due to their size.