# 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_apply (α : Type u_1) (β : Type u_2) [] [] [] :
= BoundedContinuousFunction.mkOfCompact
@[simp]
theorem ContinuousMap.equivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [] [] [] :
().symm = BoundedContinuousFunction.toContinuousMap
def ContinuousMap.equivBoundedOfCompact (α : Type u_1) (β : Type u_2) [] [] [] :

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

Instances For
def ContinuousMap.addEquivBoundedOfCompact (α : Type u_1) (β : Type u_2) [] [] [] [] [] :

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

Instances For
@[simp]
theorem ContinuousMap.addEquivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [] [] [] [] [] :
@[simp]
theorem ContinuousMap.addEquivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [] [] [] [] [] :
= BoundedContinuousFunction.mkOfCompact
instance ContinuousMap.metricSpace (α : Type u_1) (β : Type u_2) [] [] [] :
@[simp]
theorem ContinuousMap.isometryEquivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [] [] [] :
= BoundedContinuousFunction.toContinuousMap
@[simp]
theorem ContinuousMap.isometryEquivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [] [] [] :
= BoundedContinuousFunction.mkOfCompact
@[simp]
theorem ContinuousMap.isometryEquivBoundedOfCompact_toEquiv (α : Type u_1) (β : Type u_2) [] [] [] :
def ContinuousMap.isometryEquivBoundedOfCompact (α : Type u_1) (β : Type u_2) [] [] [] :

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

Instances For
@[simp]
theorem BoundedContinuousFunction.dist_mkOfCompact {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) (g : C(α, β)) :
@[simp]
theorem BoundedContinuousFunction.dist_toContinuousMap {α : Type u_1} {β : Type u_2} [] [] [] (f : ) (g : ) :
dist f.toContinuousMap g.toContinuousMap = dist f g
theorem ContinuousMap.dist_apply_le_dist {α : Type u_1} {β : Type u_2} [] [] [] {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} [] [] [] {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} [] [] [] {f : C(α, β)} {g : C(α, β)} {C : } [] :
dist f g C ∀ (x : α), dist (f x) (g x) C
theorem ContinuousMap.dist_lt_iff_of_nonempty {α : Type u_1} {β : Type u_2} [] [] [] {f : C(α, β)} {g : C(α, β)} {C : } [] :
dist f g < C ∀ (x : α), dist (f x) (g x) < C
theorem ContinuousMap.dist_lt_of_nonempty {α : Type u_1} {β : Type u_2} [] [] [] {f : C(α, β)} {g : C(α, β)} {C : } [] (w : ∀ (x : α), dist (f x) (g x) < C) :
dist f g < C
theorem ContinuousMap.dist_lt_iff {α : Type u_1} {β : Type u_2} [] [] [] {f : C(α, β)} {g : C(α, β)} {C : } (C0 : 0 < C) :
dist f g < C ∀ (x : α), dist (f x) (g x) < C
theorem ContinuousMap.continuous_eval {α : Type u_1} {β : Type u_2} [] [] [] :
Continuous fun p => p.fst p.snd

See also ContinuousMap.continuous_eval'.

@[simp]
theorem BoundedContinuousFunction.norm_mkOfCompact {α : Type u_1} {E : Type u_3} [] [] (f : C(α, E)) :
@[simp]
theorem BoundedContinuousFunction.norm_toContinuousMap_eq {α : Type u_1} {E : Type u_3} [] [] (f : ) :
f.toContinuousMap = f
theorem ContinuousMap.norm_coe_le_norm {α : Type u_1} {E : Type u_3} [] [] (f : C(α, E)) (x : α) :
theorem ContinuousMap.dist_le_two_norm {α : Type u_1} {E : Type u_3} [] [] (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} [] [] (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} [] [] (f : C(α, E)) [] {M : } :
f M ∀ (x : α), f x M
theorem ContinuousMap.norm_lt_iff {α : Type u_1} {E : Type u_3} [] [] (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} [] [] (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} [] [] (f : C(α, E)) [] {M : } :
f < M ∀ (x : α), f x < M
theorem ContinuousMap.nnnorm_lt_iff_of_nonempty {α : Type u_1} {E : Type u_3} [] [] (f : C(α, E)) [] {M : NNReal} :
f‖₊ < M ∀ (x : α), f x‖₊ < M
theorem ContinuousMap.apply_le_norm {α : Type u_1} [] [] (f : ) (x : α) :
f x f
theorem ContinuousMap.neg_norm_le_apply {α : Type u_1} [] [] (f : ) (x : α) :
-f f x
theorem ContinuousMap.norm_eq_iSup_norm {α : Type u_1} {E : Type u_3} [] [] (f : C(α, E)) :
f = ⨆ (x : α), f x
theorem ContinuousMap.norm_restrict_mono_set {E : Type u_3} {X : Type u_4} [] (f : C(X, E)) {K : } {L : } (hKL : K L) :
instance ContinuousMap.normedSpace {α : Type u_1} {E : Type u_3} [] [] {𝕜 : Type u_4} [] [] :
NormedSpace 𝕜 C(α, E)
def ContinuousMap.linearIsometryBoundedOfCompact (α : Type u_1) (E : Type u_3) [] [] (𝕜 : Type u_4) [] [] :

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

Instances For
def ContinuousMap.evalClm {α : Type u_1} {E : Type u_3} [] [] (𝕜 : Type u_4) [] [] (x : α) :
C(α, E) →L[𝕜] E

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

Instances For
@[simp]
theorem ContinuousMap.linearIsometryBoundedOfCompact_symm_apply {α : Type u_1} {E : Type u_3} [] [] {𝕜 : Type u_4} [] [] (f : ) :
= f.toContinuousMap
@[simp]
theorem ContinuousMap.linearIsometryBoundedOfCompact_apply_apply {α : Type u_1} {E : Type u_3} [] [] {𝕜 : Type u_4} [] [] (f : C(α, E)) (a : α) :
↑() a = f a
@[simp]
theorem ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv {α : Type u_1} {E : Type u_3} [] [] {𝕜 : Type u_4} [] [] :
@[simp]
theorem ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv {α : Type u_1} {E : Type u_3} [] [] {𝕜 : Type u_4} [] [] :
().toLinearEquiv =
@[simp]
theorem ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv {α : Type u_1} {E : Type u_3} [] [] {𝕜 : Type u_4} [] [] :
LinearEquiv.toEquiv ().toLinearEquiv =

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

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

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

Instances For
theorem ContinuousMap.modulus_pos {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) {ε : } {h : 0 < ε} :
0 <
theorem ContinuousMap.dist_lt_of_dist_lt_modulus {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) (ε : ) (h : 0 < ε) {a : α} {b : α} (w : dist a b < ) :
dist (f a) (f b) < ε
def ContinuousLinearMap.compLeftContinuousCompact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] (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.

Instances For
@[simp]
theorem ContinuousLinearMap.toLinear_compLeftContinuousCompact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] (g : β →L[𝕜] γ) :
@[simp]
theorem ContinuousLinearMap.compLeftContinuousCompact_apply (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] (g : β →L[𝕜] γ) (f : C(X, β)) (x : X) :
↑() x = g (f 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:

• compRightContinuousMap, the bundled continuous map (for this we need X Y compact).
• compRightHomeomorph, when we precompose by a homeomorphism.
• compRightAlgHom, when T = R is a topological ring.
def ContinuousMap.compRightContinuousMap {X : Type u_1} {Y : Type u_2} (T : Type u_3) [] [] [] [] [] (f : C(X, Y)) :

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

Instances For
@[simp]
theorem ContinuousMap.compRightContinuousMap_apply {X : Type u_1} {Y : Type u_2} (T : Type u_3) [] [] [] [] [] (f : C(X, Y)) (g : C(Y, T)) :
def ContinuousMap.compRightHomeomorph {X : Type u_1} {Y : Type u_2} (T : Type u_3) [] [] [] [] [] (f : X ≃ₜ Y) :

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

Instances For
theorem ContinuousMap.compRightAlgHom_continuous {X : Type u_1} {Y : Type u_2} (R : Type u_3) (A : Type u_4) [] [] [] [] [] [] [] [Algebra R A] (f : C(X, Y)) :

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

theorem ContinuousMap.summable_of_locally_summable_norm {X : Type u_1} [] {E : Type u_2} [] {ι : Type u_3} {F : ιC(X, E)} (hF : ∀ (K : ), Summable fun i => ContinuousMap.restrict (K) (F i)) :

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

theorem BoundedContinuousFunction.mkOfCompact_star {α : Type u_1} {β : Type u_2} [] [] [] [] (f : C(α, β)) :