Documentation

Mathlib.Topology.ContinuousFunction.Compact

Continuous functions on a compact space #

Continuous functions C(α, β) from a compact space α to a metric space β are automatically bounded, and so acquire various structures inherited from α →ᵇ β.

This file transfers these structures, and restates some lemmas characterising these structures.

If you need a lemma which is proved about α →ᵇ β but not for C(α, β) when α is compact, you should restate it here. You can also use ContinuousMap.equivBoundedOfCompact to move functions back and forth.

@[simp]
theorem ContinuousMap.equivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :
(ContinuousMap.equivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap
@[simp]
theorem ContinuousMap.equivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :
(ContinuousMap.equivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact

When α is compact, the bounded continuous maps α →ᵇ β are equivalent to C(α, β).

Equations
  • ContinuousMap.equivBoundedOfCompact α β = { toFun := BoundedContinuousFunction.mkOfCompact, invFun := BoundedContinuousFunction.toContinuousMap, left_inv := , right_inv := }
Instances For

    When α is compact, the bounded continuous maps α →ᵇ 𝕜 are additively equivalent to C(α, 𝕜).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem ContinuousMap.addEquivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] [AddMonoid β] [LipschitzAdd β] :
      (ContinuousMap.addEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact
      @[simp]
      theorem ContinuousMap.isometryEquivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :
      (ContinuousMap.isometryEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact
      @[simp]
      theorem ContinuousMap.isometryEquivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :
      (ContinuousMap.isometryEquivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap

      When α is compact, and β is a metric space, the bounded continuous maps α →ᵇ β are isometric to C(α, β).

      Equations
      Instances For
        @[simp]
        theorem BoundedContinuousFunction.dist_toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) :
        dist f.toContinuousMap g.toContinuousMap = dist f g
        theorem ContinuousMap.dist_apply_le_dist {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} (x : α) :
        dist (f x) (g x) dist f g

        The pointwise distance is controlled by the distance between functions, by definition.

        theorem ContinuousMap.dist_le {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : } (C0 : 0 C) :
        dist f g C ∀ (x : α), dist (f x) (g x) C

        The distance between two functions is controlled by the supremum of the pointwise distances.

        theorem ContinuousMap.dist_le_iff_of_nonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : } [Nonempty α] :
        dist f g C ∀ (x : α), dist (f x) (g x) C
        theorem ContinuousMap.dist_lt_iff_of_nonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : } [Nonempty α] :
        dist f g < C ∀ (x : α), dist (f x) (g x) < C
        theorem ContinuousMap.dist_lt_of_nonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : } [Nonempty α] (w : ∀ (x : α), dist (f x) (g x) < C) :
        dist f g < C
        theorem ContinuousMap.dist_lt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : } (C0 : 0 < C) :
        dist f g < C ∀ (x : α), dist (f x) (g x) < C
        instance ContinuousMap.instNorm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] :
        Equations
        • ContinuousMap.instNorm = { norm := fun (x : C(α, E)) => dist x 0 }
        Equations
        theorem ContinuousMap.norm_coe_le_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) (x : α) :
        theorem ContinuousMap.dist_le_two_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) (x : α) (y : α) :
        dist (f x) (f y) 2 * f

        Distance between the images of any two points is at most twice the norm of the function.

        theorem ContinuousMap.norm_le {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) {C : } (C0 : 0 C) :
        f C ∀ (x : α), f x C

        The norm of a function is controlled by the supremum of the pointwise norms.

        theorem ContinuousMap.norm_le_of_nonempty {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : } :
        f M ∀ (x : α), f x M
        theorem ContinuousMap.norm_lt_iff {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) {M : } (M0 : 0 < M) :
        f < M ∀ (x : α), f x < M
        theorem ContinuousMap.nnnorm_lt_iff {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) {M : NNReal} (M0 : 0 < M) :
        f‖₊ < M ∀ (x : α), f x‖₊ < M
        theorem ContinuousMap.norm_lt_iff_of_nonempty {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : } :
        f < M ∀ (x : α), f x < M
        theorem ContinuousMap.nnnorm_lt_iff_of_nonempty {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : NNReal} :
        f‖₊ < M ∀ (x : α), f x‖₊ < M
        theorem ContinuousMap.apply_le_norm {α : Type u_1} [TopologicalSpace α] [CompactSpace α] (f : C(α, )) (x : α) :
        f x f
        theorem ContinuousMap.neg_norm_le_apply {α : Type u_1} [TopologicalSpace α] [CompactSpace α] (f : C(α, )) (x : α) :
        theorem ContinuousMap.norm_eq_iSup_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) :
        f = ⨆ (x : α), f x
        Equations
        instance ContinuousMap.normedSpace {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 E] :
        NormedSpace 𝕜 C(α, E)
        Equations

        When α is compact and 𝕜 is a normed field, the 𝕜-algebra of bounded continuous maps α →ᵇ β is 𝕜-linearly isometric to C(α, β).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def ContinuousMap.evalCLM {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (𝕜 : Type u_4) [NormedField 𝕜] [NormedSpace 𝕜 E] (x : α) :
          C(α, E) →L[𝕜] E

          The evaluation at a point, as a continuous linear map from C(α, 𝕜) to 𝕜.

          Equations
          Instances For
            @[simp]
            theorem ContinuousMap.linearIsometryBoundedOfCompact_apply_apply {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) (a : α) :
            instance ContinuousMap.instNormedAlgebra {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {𝕜 : Type u_4} {γ : Type u_5} [NormedField 𝕜] [NormedRing γ] [NormedAlgebra 𝕜 γ] :
            Equations

            We now set up some declarations making it convenient to use uniform continuity.

            theorem ContinuousMap.uniform_continuity {α : Type u_1} {β : Type u_2} [MetricSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) (ε : ) (h : 0 < ε) :
            δ > 0, ∀ {x y : α}, dist x y < δdist (f x) (f y) < ε
            def ContinuousMap.modulus {α : Type u_1} {β : Type u_2} [MetricSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) (ε : ) (h : 0 < ε) :

            An arbitrarily chosen modulus of uniform continuity for a given function f and ε > 0.

            Equations
            Instances For
              theorem ContinuousMap.modulus_pos {α : Type u_1} {β : Type u_2} [MetricSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) {ε : } {h : 0 < ε} :
              0 < f.modulus ε h
              theorem ContinuousMap.dist_lt_of_dist_lt_modulus {α : Type u_1} {β : Type u_2} [MetricSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) (ε : ) (h : 0 < ε) {a : α} {b : α} (w : dist a b < f.modulus ε h) :
              dist (f a) (f b) < ε
              def ContinuousLinearMap.compLeftContinuousCompact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] [NormedAddCommGroup γ] [NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) :
              C(X, β) →L[𝕜] C(X, γ)

              Postcomposition of continuous functions into a normed module by a continuous linear map is a continuous linear map. Transferred version of ContinuousLinearMap.compLeftContinuousBounded, upgraded version of ContinuousLinearMap.compLeftContinuous, similar to LinearMap.compLeft.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem ContinuousLinearMap.compLeftContinuousCompact_apply (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] [NormedAddCommGroup γ] [NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) (f : C(X, β)) (x : X) :

                We now setup variations on compRight* f, where f : C(X, Y) (that is, precomposition by a continuous map), as a morphism C(Y, T) → C(X, T), respecting various types of structure.

                In particular:

                Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.

                Equations
                Instances For

                  Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Local normal convergence #

                    A sum of continuous functions (on a locally compact space) is "locally normally convergent" if the sum of its sup-norms on any compact subset is summable. This implies convergence in the topology of C(X, E) (i.e. locally uniform convergence).

                    Star structures #

                    In this section, if β is a normed ⋆-group, then so is the space of continuous functions from α to β, by using the star operation pointwise.

                    Furthermore, if α is compact and β is a C⋆-ring, then C(α, β) is a C⋆-ring.

                    instance ContinuousMap.instCStarRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [NormedRing β] [StarRing β] [CompactSpace α] [CStarRing β] :
                    Equations
                    • =