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 #

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.

Instances For

    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.

    Equations
    • One or more equations did not get rendered due to their size.
    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.

      Equations
      Instances For
        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.

        Instances
          theorem ZeroAtInftyContinuousMapClass.zero_at_infty {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [TopologicalSpace α] [Zero β] [TopologicalSpace β] [FunLike F α β] [self : ZeroAtInftyContinuousMapClass F α β] (f : F) :

          Each member of the class tends to zero along the cocompact filter.

          Equations
          Equations
          • ZeroAtInftyContinuousMap.instCoeTC = { coe := fun (f : F) => { 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) :

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

          Equations
          • f.copy f' h = { toFun := f', continuous_toFun := , zero_at_infty' := }
          Instances For
            @[simp]
            theorem ZeroAtInftyContinuousMap.coe_copy {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (f' : αβ) (h : f' = f) :
            (f.copy f' h) = f'
            theorem ZeroAtInftyContinuousMap.copy_eq {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (f' : αβ) (h : f' = f) :
            f.copy f' h = 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
            @[simp]
            theorem ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_symm_apply {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [CompactSpace α] (f : ZeroAtInftyContinuousMap α β) :
            ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty.symm f = f

            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.
            Instances For

              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.

              Equations
              • ZeroAtInftyContinuousMap.instZero = { zero := { toContinuousMap := 0, zero_at_infty' := } }
              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
              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
              Equations
              Equations
              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
              Equations
              Equations
              • ZeroAtInftyContinuousMap.instSMul = { smul := fun (r : R) (f : ZeroAtInftyContinuousMap α β) => { 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
              Equations
              Equations
              Equations
              • ZeroAtInftyContinuousMap.instNeg = { neg := fun (f : ZeroAtInftyContinuousMap α β) => { toContinuousMap := -f, zero_at_infty' := } }
              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
              Equations
              Equations
              Equations
              Equations
              Equations
              • ZeroAtInftyContinuousMap.instModule = Function.Injective.module R { toFun := DFunLike.coe, map_zero' := , map_add' := }
              Equations
              Equations
              Equations
              Equations
              Equations
              Equations
              theorem ZeroAtInftyContinuousMap.uniformContinuous {F : Type u_1} {β : Type v} {γ : Type w} [UniformSpace β] [UniformSpace γ] [Zero γ] [FunLike F β γ] [ZeroAtInftyContinuousMapClass F β γ] (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} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] [FunLike F α β] [ZeroAtInftyContinuousMapClass F α β] (f : F) :
              ∃ (C : ), ∀ (x y : α), dist (f x) (f y) C
              @[instance 100]
              Equations
              • =
              @[simp]
              theorem ZeroAtInftyContinuousMap.toBCF_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (a : α) :
              f.toBCF a = f a
              @[simp]
              theorem ZeroAtInftyContinuousMap.toBCF_toFun {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : ZeroAtInftyContinuousMap α β) (a : α) :
              f.toBCF a = f a

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

              Equations
              • f.toBCF = { toContinuousMap := f, map_bounded' := }
              Instances For
                theorem ZeroAtInftyContinuousMap.toBCF_injective (α : Type u) (β : Type v) [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] :
                Function.Injective ZeroAtInftyContinuousMap.toBCF

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

                Equations

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

                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.

                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                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₀(α, β).

                Equations
                • ZeroAtInftyContinuousMap.instStar = { star := fun (f : ZeroAtInftyContinuousMap α β) => { toFun := fun (x : α) => star (f x), continuous_toFun := , zero_at_infty' := } }
                Equations
                instance ZeroAtInftyContinuousMap.instStarModule {α : Type u} {β : Type v} [TopologicalSpace α] {𝕜 : Type u_2} [Zero 𝕜] [Star 𝕜] [AddMonoid β] [StarAddMonoid β] [TopologicalSpace β] [ContinuousStar β] [SMulWithZero 𝕜 β] [ContinuousConstSMul 𝕜 β] [StarModule 𝕜 β] :
                Equations
                • =
                Equations
                • ZeroAtInftyContinuousMap.instStarRing = let __src := ZeroAtInftyContinuousMap.instStarAddMonoid; StarRing.mk

                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.

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

                Equations
                • f.comp g = { toContinuousMap := (f).comp g, zero_at_infty' := }
                Instances For
                  @[simp]
                  theorem ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun {β : Type v} {γ : Type w} {δ : Type u_2} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : ZeroAtInftyContinuousMap γ δ) (g : CocompactMap β γ) :
                  (f.comp g) = f g
                  @[simp]
                  theorem ZeroAtInftyContinuousMap.comp_id {γ : Type w} {δ : Type u_2} [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : ZeroAtInftyContinuousMap γ δ) :
                  f.comp (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 α β) :
                  (f.comp g).comp h = f.comp (g.comp h)

                  Composition as an additive monoid homomorphism.

                  Equations
                  Instances For

                    Composition as a semigroup homomorphism.

                    Equations
                    Instances For

                      Composition as a linear map.

                      Equations
                      Instances For

                        Composition as a non-unital algebra homomorphism.

                        Equations
                        Instances For