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.

def ContinuousMap.equivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : C(α, β) ≃ BoundedContinuousFunction α β

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

@[simp]

theorem ContinuousMap.equivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : ⇑(equivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact

@[simp]

theorem ContinuousMap.equivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : ⇑(equivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap

theorem ContinuousMap.isUniformInducing_equivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : IsUniformInducing ⇑(equivBoundedOfCompact α β)

theorem ContinuousMap.isUniformEmbedding_equivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : IsUniformEmbedding ⇑(equivBoundedOfCompact α β)

def ContinuousMap.addEquivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : C(α, β) ≃+ BoundedContinuousFunction α β

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

@[simp]

theorem ContinuousMap.addEquivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : ⇑(addEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact

@[simp]

theorem ContinuousMap.addEquivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : ⇑(addEquivBoundedOfCompact α β).symm = ⇑(BoundedContinuousFunction.toContinuousMapAddMonoidHom α β)

instance ContinuousMap.instPseudoMetricSpace (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : PseudoMetricSpace C(α, β)

instance ContinuousMap.instMetricSpace (α : Type u_1) [TopologicalSpace α] [CompactSpace α] {β : Type u_4} [MetricSpace β] : MetricSpace C(α, β)

def ContinuousMap.isometryEquivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : C(α, β) ≃ᵢ BoundedContinuousFunction α β

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

@[simp]

theorem ContinuousMap.isometryEquivBoundedOfCompact_toEquiv (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : (isometryEquivBoundedOfCompact α β).toEquiv = equivBoundedOfCompact α β

@[simp]

theorem ContinuousMap.isometryEquivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : ⇑(isometryEquivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap

@[simp]

theorem ContinuousMap.isometryEquivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] : ⇑(isometryEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact

@[simp]

theorem BoundedContinuousFunction.dist_mkOfCompact {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] (f g : C(α, β)) : dist (mkOfCompact f) (mkOfCompact g) = dist f g

@[simp]

theorem BoundedContinuousFunction.dist_toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] (f g : BoundedContinuousFunction α β) : dist f.toContinuousMap g.toContinuousMap = dist f g

theorem ContinuousMap.dist_apply_le_dist {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] {f 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 α] [PseudoMetricSpace β] {f 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 α] [PseudoMetricSpace β] {f 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 α] [PseudoMetricSpace β] {f 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 α] [PseudoMetricSpace β] {f 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 α] [PseudoMetricSpace β] {f g : C(α, β)} {C : ℝ} (C0 : 0 < C) : dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

theorem ContinuousMap.dist_eq_iSup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] {f g : C(α, β)} : dist f g = ⨆ (x : α), dist (f x) (g x)

theorem ContinuousMap.nndist_eq_iSup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] {f g : C(α, β)} : nndist f g = ⨆ (x : α), nndist (f x) (g x)

theorem ContinuousMap.edist_eq_iSup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] {f g : C(α, β)} : edist f g = ⨆ (x : α), edist (f x) (g x)

instance ContinuousMap.instIsBoundedSMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] {R : Type u_4} [Zero R] [Zero β] [PseudoMetricSpace R] [SMul R β] [IsBoundedSMul R β] : IsBoundedSMul R C(α, β)

instance ContinuousMap.instNorm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] : Norm C(α, E)

@[simp]

theorem BoundedContinuousFunction.norm_mkOfCompact {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] (f : C(α, E)) : ‖mkOfCompact f‖ = ‖f‖

@[simp]

theorem BoundedContinuousFunction.norm_toContinuousMap_eq {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] (f : BoundedContinuousFunction α E) : ‖f.toContinuousMap‖ = ‖f‖

instance ContinuousMap.instSeminormedAddCommGroup {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] : SeminormedAddCommGroup C(α, E)

instance ContinuousMap.instNormedAddCommGroup {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {E : Type u_4} [NormedAddCommGroup E] : NormedAddCommGroup C(α, E)

instance ContinuousMap.instNormOneClassOfNonempty {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] [Nonempty α] [One E] [NormOneClass E] : NormOneClass C(α, E)

theorem ContinuousMap.norm_coe_le_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] (f : C(α, E)) (x : α) : ‖f x‖ ≤ ‖f‖

theorem ContinuousMap.dist_le_two_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup 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 α] [SeminormedAddCommGroup 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 α] [SeminormedAddCommGroup 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 α] [SeminormedAddCommGroup 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 α] [SeminormedAddCommGroup 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 α] [SeminormedAddCommGroup 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 α] [SeminormedAddCommGroup 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 : α) : -‖f‖ ≤ f x

theorem ContinuousMap.nnnorm_eq_iSup_nnnorm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] (f : C(α, E)) : ‖f‖₊ = ⨆ (x : α), ‖f x‖₊

theorem ContinuousMap.norm_eq_iSup_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] (f : C(α, E)) : ‖f‖ = ⨆ (x : α), ‖f x‖

theorem ContinuousMap.enorm_eq_iSup_enorm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] (f : C(α, E)) : ‖f‖ₑ = ⨆ (x : α), ‖f x‖ₑ

instance ContinuousMap.instCompactSpaceElemCoeCompacts {X : Type u_4} [TopologicalSpace X] (K : TopologicalSpace.Compacts X) : CompactSpace ↑↑K

theorem ContinuousMap.norm_restrict_mono_set {E : Type u_3} [SeminormedAddCommGroup E] {X : Type u_4} [TopologicalSpace X] (f : C(X, E)) {K L : TopologicalSpace.Compacts X} (hKL : K ≤ L) : ‖restrict (↑K) f‖ ≤ ‖restrict (↑L) f‖

instance ContinuousMap.instNonUnitalSeminormedRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [NonUnitalSeminormedRing R] : NonUnitalSeminormedRing C(α, R)

instance ContinuousMap.instNonUnitalSeminormedCommRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [NonUnitalSeminormedCommRing R] : NonUnitalSeminormedCommRing C(α, R)

instance ContinuousMap.instSeminormedRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [SeminormedRing R] : SeminormedRing C(α, R)

instance ContinuousMap.instSeminormedCommRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [SeminormedCommRing R] : SeminormedCommRing C(α, R)

instance ContinuousMap.instNonUnitalNormedRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [NonUnitalNormedRing R] : NonUnitalNormedRing C(α, R)

instance ContinuousMap.instNonUnitalNormedCommRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [NonUnitalNormedCommRing R] : NonUnitalNormedCommRing C(α, R)

instance ContinuousMap.instNormedRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [NormedRing R] : NormedRing C(α, R)

instance ContinuousMap.instNormedCommRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [NormedCommRing R] : NormedCommRing C(α, R)

instance ContinuousMap.normedSpace {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 E] : NormedSpace 𝕜 C(α, E)

def ContinuousMap.linearIsometryBoundedOfCompact (α : Type u_1) (E : Type u_3) [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] (𝕜 : Type u_4) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : C(α, E) ≃ₗᵢ[𝕜] BoundedContinuousFunction α E

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

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_symm_apply {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] {𝕜 : Type u_4} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : BoundedContinuousFunction α E) : (linearIsometryBoundedOfCompact α E 𝕜).symm f = f.toContinuousMap

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_apply_apply {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] {𝕜 : Type u_4} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : C(α, E)) (a : α) : ((linearIsometryBoundedOfCompact α E 𝕜) f) a = f a

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] {𝕜 : Type u_4} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : (linearIsometryBoundedOfCompact α E 𝕜).toIsometryEquiv = isometryEquivBoundedOfCompact α E

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] {𝕜 : Type u_4} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : ↑(linearIsometryBoundedOfCompact α E 𝕜).toLinearEquiv = addEquivBoundedOfCompact α E

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] {𝕜 : Type u_4} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : (linearIsometryBoundedOfCompact α E 𝕜).toEquiv = equivBoundedOfCompact α E

@[simp]

theorem ContinuousMap.nnnorm_smul_const {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} {β : Type u_5} [SeminormedAddCommGroup β] [SeminormedRing R] [Module R β] [NormSMulClass R β] (f : C(α, R)) (b : β) : ‖f • const α b‖₊ = ‖f‖₊ * ‖b‖₊

@[simp]

theorem ContinuousMap.norm_smul_const {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} {β : Type u_5} [SeminormedAddCommGroup β] [SeminormedRing R] [Module R β] [NormSMulClass R β] (f : C(α, R)) (b : β) : ‖f • const α b‖ = ‖f‖ * ‖b‖

instance ContinuousMap.instNormedAlgebra {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {𝕜 : Type u_4} {γ : Type u_5} [NormedField 𝕜] [SeminormedRing γ] [NormedAlgebra 𝕜 γ] : NormedAlgebra 𝕜 C(α, γ)

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

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

def ContinuousMap.modulus {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [CompactSpace α] [PseudoMetricSpace β] (f : C(α, β)) (ε : ℝ) (h : 0 < ε) : ℝ

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

theorem ContinuousMap.modulus_pos {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [CompactSpace α] [PseudoMetricSpace β] (f : C(α, β)) {ε : ℝ} {h : 0 < ε} : 0 < f.modulus ε h

theorem ContinuousMap.dist_lt_of_dist_lt_modulus {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [CompactSpace α] [PseudoMetricSpace β] (f : C(α, β)) (ε : ℝ) (h : 0 < ε) {a b : α} (w : dist a b < f.modulus ε h) : dist (f a) (f b) < ε

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} [TopologicalSpace X] [LocallyCompactSpace X] {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] {ι : Type u_3} {F : ι → C(X, E)} (hF : ∀ (K : TopologicalSpace.Compacts X), Summable fun (i : ι) => ‖restrict (↑K) (F i)‖) : Summable F

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} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] [CompactSpace α] (f : C(α, β)) : mkOfCompact (star f) = star (mkOfCompact f)

instance ContinuousMap.instNormedStarGroup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] [CompactSpace α] : NormedStarGroup C(α, β)

instance ContinuousMap.instCStarRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [NonUnitalNormedRing β] [StarRing β] [CStarRing β] : CStarRing C(α, β)