mathlib documentation

topology.continuous_function.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 bounded_continuous_function.equiv_continuous_map_of_compact to move functions back and forth.

def continuous_map.equiv_bounded_of_compact (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :
C(α, β) →ᵇ β)

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

Equations
def continuous_map.add_equiv_bounded_of_compact (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :
C(α, β) ≃+ →ᵇ β)

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

Equations
@[simp]
theorem continuous_map.add_equiv_bounded_of_compact_apply_apply (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) (a : α) :
theorem continuous_map.dist_le {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (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 continuous_map.dist_le_iff_of_nonempty {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f g : C(α, β)) {C : } [nonempty α] :
dist f g C ∀ (x : α), dist (f x) (g x) C
theorem continuous_map.dist_lt_of_nonempty {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f g : C(α, β)) {C : } [nonempty α] (w : ∀ (x : α), dist (f x) (g x) < C) :
dist f g < C
theorem continuous_map.dist_lt_iff {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f g : C(α, β)) {C : } (C0 : 0 < C) :
dist f g < C ∀ (x : α), dist (f x) (g x) < C
theorem continuous_map.dist_lt_iff_of_nonempty {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f g : C(α, β)) {C : } [nonempty α] :
dist f g < C ∀ (x : α), dist (f x) (g x) < C
def continuous_map.isometric_bounded_of_compact (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :
C(α, β) ≃ᵢ →ᵇ β)

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

Equations
@[instance]
def continuous_map.has_norm (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :
Equations
theorem continuous_map.norm_coe_le_norm {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) (x : α) :
theorem continuous_map.dist_le_two_norm {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) (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 continuous_map.norm_le {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) {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 continuous_map.norm_le_of_nonempty {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) [nonempty α] {M : } :
f M ∀ (x : α), f x M
theorem continuous_map.norm_lt_iff {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) {M : } (M0 : 0 < M) :
f < M ∀ (x : α), f x < M
theorem continuous_map.norm_lt_iff_of_nonempty {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) [nonempty α] {M : } :
f < M ∀ (x : α), f x < M
theorem continuous_map.apply_le_norm {α : Type u_1} [topological_space α] [compact_space α] (f : C(α, )) (x : α) :
theorem continuous_map.neg_norm_le_apply {α : Type u_1} [topological_space α] [compact_space α] (f : C(α, )) (x : α) :
@[instance]
def continuous_map.normed_space (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] {𝕜 : Type u_3} [normed_field 𝕜] [normed_space 𝕜 β] :
normed_space 𝕜 C(α, β)
Equations
def continuous_map.linear_isometry_bounded_of_compact (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (𝕜 : Type u_3) [normed_field 𝕜] [normed_space 𝕜 β] :
C(α, β) ≃ₗᵢ[𝕜] α →ᵇ β

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

Equations
@[instance]
def continuous_map.normed_algebra (α : Type u_1) [topological_space α] [compact_space α] {𝕜 : Type u_3} {γ : Type u_4} [normed_field 𝕜] [normed_ring γ] [normed_algebra 𝕜 γ] [nonempty α] :
Equations

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

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

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

Equations
theorem continuous_map.modulus_pos {α : Type u_1} {β : Type u_2} [metric_space α] [compact_space α] [metric_space β] (f : C(α, β)) {ε : } {h : 0 < ε} :
0 < f.modulus ε h
theorem continuous_map.dist_lt_of_dist_lt_modulus {α : Type u_1} {β : Type u_2} [metric_space α] [compact_space α] [metric_space β] (f : C(α, β)) (ε : ) (h : 0 < ε) {a b : α} (w : dist a b < f.modulus ε h) :
dist (f a) (f b) < ε

We now setup variations on comp_right_* 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:

def continuous_map.comp_right_continuous_map {X : Type u_1} {Y : Type u_2} (T : Type u_3) [topological_space X] [compact_space X] [topological_space Y] [compact_space Y] [normed_group T] (f : C(X, Y)) :

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

Equations
@[simp]
theorem continuous_map.comp_right_continuous_map_apply {X : Type u_1} {Y : Type u_2} (T : Type u_3) [topological_space X] [compact_space X] [topological_space Y] [compact_space Y] [normed_group T] (f : C(X, Y)) (g : C(Y, T)) :
def continuous_map.comp_right_homeomorph {X : Type u_1} {Y : Type u_2} (T : Type u_3) [topological_space X] [compact_space X] [topological_space Y] [compact_space Y] [normed_group T] (f : X ≃ₜ Y) :

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

Equations
def continuous_map.comp_right_alg_hom {X : Type u_1} {Y : Type u_2} (R : Type u_3) [topological_space X] [topological_space Y] [normed_comm_ring R] (f : C(X, Y)) :

Precomposition of functions into a normed ring by continuous map is an algebra homomorphism.

Equations
@[simp]
theorem continuous_map.comp_right_alg_hom_apply {X : Type u_1} {Y : Type u_2} (R : Type u_3) [topological_space X] [topological_space Y] [normed_comm_ring R] (f : C(X, Y)) (g : C(Y, R)) :