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.

@[simp]

theorem continuous_map.equiv_bounded_of_compact_apply (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) :

⇑(continuous_map.equiv_bounded_of_compact α β) f = bounded_continuous_function.mk_of_compact f

@[simp]

theorem continuous_map.equiv_bounded_of_compact_symm_apply (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (ᾰ : α →ᵇ β) :

⇑((continuous_map.equiv_bounded_of_compact α β).symm) ᾰ = bounded_continuous_function.forget_boundedness α β ᾰ

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

continuous_map.equiv_bounded_of_compact α β = {to_fun := bounded_continuous_function.mk_of_compact _inst_2, inv_fun := bounded_continuous_function.forget_boundedness α β normed_group.to_metric_space, left_inv := _, right_inv := _}

@[simp]

theorem continuous_map.add_equiv_bounded_of_compact_symm_apply (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (ᾰ : α →ᵇ β) :

⇑((continuous_map.add_equiv_bounded_of_compact α β).symm) ᾰ = bounded_continuous_function.forget_boundedness α β ᾰ

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

continuous_map.add_equiv_bounded_of_compact α β = {to_fun := (bounded_continuous_function.forget_boundedness_add_hom α β).to_fun, inv_fun := (continuous_map.equiv_bounded_of_compact α β).symm.inv_fun, left_inv := _, right_inv := _, map_add' := _}.symm

@[simp]

theorem continuous_map.add_equiv_bounded_of_compact_apply_to_continuous_map (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (ᾰ : C(α, β)) :

(⇑(continuous_map.add_equiv_bounded_of_compact α β) ᾰ).to_continuous_map = ᾰ

@[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 : α) :

⇑(⇑(continuous_map.add_equiv_bounded_of_compact α β) f) a = ⇑f a

@[simp]

theorem continuous_map.add_equiv_bounded_of_compact_to_equiv (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :

(continuous_map.add_equiv_bounded_of_compact α β).to_equiv = continuous_map.equiv_bounded_of_compact α β

@[instance]

def continuous_map.metric_space (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :

metric_space C(α, β)

Equations

continuous_map.metric_space α β = metric_space.induced ⇑(continuous_map.equiv_bounded_of_compact α β) _ bounded_continuous_function.metric_space

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

continuous_map.isometric_bounded_of_compact α β = {to_equiv := continuous_map.equiv_bounded_of_compact α β _inst_3, isometry_to_fun := _}

@[simp]

theorem continuous_map.isometric_bounded_of_compact_to_equiv (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :

(continuous_map.isometric_bounded_of_compact α β).to_equiv = continuous_map.equiv_bounded_of_compact α β

@[instance]

def continuous_map.has_norm (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :

has_norm C(α, β)

Equations

continuous_map.has_norm α β = {norm := λ (x : C(α, β)), dist x 0}

@[instance]

def continuous_map.normed_group (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] :

normed_group C(α, β)

Equations

continuous_map.normed_group α β = {to_has_norm := continuous_map.has_norm α β _inst_3, to_add_comm_group := continuous_map.add_comm_group _, to_metric_space := continuous_map.metric_space α β _inst_3, dist_eq := _}

theorem continuous_map.norm_coe_le_norm {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) (x : α) :

∥⇑f x∥ ≤ ∥f∥

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 : α) :

⇑f x ≤ ∥f∥

theorem continuous_map.neg_norm_le_apply {α : Type u_1} [topological_space α] [compact_space α] (f : C(α, ℝ )) (x : α) :

-∥f∥ ≤ ⇑f x

@[simp]

theorem bounded_continuous_function.norm_forget_boundedness_eq {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : α →ᵇ β) :

∥bounded_continuous_function.forget_boundedness α β f∥ = ∥f∥

theorem continuous_map.norm_eq_supr_norm {α : Type u_1} {β : Type u_2} [topological_space α] [compact_space α] [normed_group β] (f : C(α, β)) :

∥f∥ = ⨆ (x : α), ∥⇑f x∥

@[instance]

def continuous_map.normed_ring (α : Type u_1) [topological_space α] [compact_space α] {R : Type u_3} [normed_ring R] :

normed_ring C(α, R)

Equations

continuous_map.normed_ring α = {to_has_norm := normed_group.to_has_norm infer_instance, to_ring := continuous_map.ring continuous_map.normed_ring._proof_1, to_metric_space := normed_group.to_metric_space infer_instance, dist_eq := _, norm_mul := _}

@[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

continuous_map.normed_space α β = {to_module := continuous_map.module _, norm_smul_le := _}

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

continuous_map.linear_isometry_bounded_of_compact α β 𝕜 = {to_linear_equiv := {to_fun := (continuous_map.add_equiv_bounded_of_compact α β).to_fun, map_add' := _, map_smul' := _, inv_fun := (continuous_map.add_equiv_bounded_of_compact α β).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}

@[simp]

theorem continuous_map.linear_isometry_bounded_of_compact_symm_apply (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (𝕜 : Type u_3) [normed_field 𝕜] [normed_space 𝕜 β] (f : α →ᵇ β) :

⇑((continuous_map.linear_isometry_bounded_of_compact α β 𝕜).symm) f = bounded_continuous_function.forget_boundedness α β f

@[simp]

theorem continuous_map.linear_isometry_bounded_of_compact_apply_apply (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (𝕜 : Type u_3) [normed_field 𝕜] [normed_space 𝕜 β] (f : C(α, β)) (a : α) :

⇑(⇑(continuous_map.linear_isometry_bounded_of_compact α β 𝕜) f) a = ⇑f a

@[simp]

theorem continuous_map.linear_isometry_bounded_of_compact_to_isometric (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (𝕜 : Type u_3) [normed_field 𝕜] [normed_space 𝕜 β] :

(continuous_map.linear_isometry_bounded_of_compact α β 𝕜).to_isometric = continuous_map.isometric_bounded_of_compact α β

@[simp]

theorem continuous_map.linear_isometry_bounded_of_compact_to_add_equiv (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (𝕜 : Type u_3) [normed_field 𝕜] [normed_space 𝕜 β] :

(continuous_map.linear_isometry_bounded_of_compact α β 𝕜).to_linear_equiv.to_add_equiv = continuous_map.add_equiv_bounded_of_compact α β

@[simp]

theorem continuous_map.linear_isometry_bounded_of_compact_of_compact_to_equiv (α : Type u_1) (β : Type u_2) [topological_space α] [compact_space α] [normed_group β] (𝕜 : Type u_3) [normed_field 𝕜] [normed_space 𝕜 β] :

(continuous_map.linear_isometry_bounded_of_compact α β 𝕜).to_linear_equiv.to_equiv = continuous_map.equiv_bounded_of_compact α β

@[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 α] :

normed_algebra 𝕜 C(α, γ)

Equations

continuous_map.normed_algebra α = {to_algebra := continuous_map.algebra continuous_map.normed_algebra._proof_2, norm_algebra_map_eq := _}

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

f.modulus ε h = classical.some _

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) < ε

def continuous_linear_map.comp_left_continuous_compact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space X] [compact_space X] [nondiscrete_normed_field 𝕜] [normed_group β] [normed_space 𝕜 β] [normed_group γ] [normed_space 𝕜 γ] (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 continuous_linear_map.comp_left_continuous_bounded, upgraded version of continuous_linear_map.comp_left_continuous, similar to linear_map.comp_left.

Equations

continuous_linear_map.comp_left_continuous_compact X g = (continuous_map.linear_isometry_bounded_of_compact X γ 𝕜).symm.to_linear_isometry.to_continuous_linear_map.comp ((continuous_linear_map.comp_left_continuous_bounded X g).comp (continuous_map.linear_isometry_bounded_of_compact X β 𝕜).to_linear_isometry.to_continuous_linear_map)

@[simp]

theorem continuous_linear_map.to_linear_comp_left_continuous_compact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space X] [compact_space X] [nondiscrete_normed_field 𝕜] [normed_group β] [normed_space 𝕜 β] [normed_group γ] [normed_space 𝕜 γ] (g : β →L[𝕜] γ) :

↑(continuous_linear_map.comp_left_continuous_compact X g) = continuous_linear_map.comp_left_continuous 𝕜 X g

@[simp]

theorem continuous_linear_map.comp_left_continuous_compact_apply (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space X] [compact_space X] [nondiscrete_normed_field 𝕜] [normed_group β] [normed_space 𝕜 β] [normed_group γ] [normed_space 𝕜 γ] (g : β →L[𝕜] γ) (f : C(X, β)) (x : X) :

⇑(⇑(continuous_linear_map.comp_left_continuous_compact X g) f) x = ⇑g (⇑f x)

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:

comp_right_continuous_map, the bundled continuous map (for this we need X Y compact).
comp_right_homeomorph, when we precompose by a homeomorphism.
comp_right_alg_hom, when T = R is a topological ring.

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)) :

C(C(Y, T), C(X, T))

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

Equations

continuous_map.comp_right_continuous_map T f = {to_fun := λ (g : C(Y, T)), g.comp f, continuous_to_fun := _}

@[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)) :

⇑(continuous_map.comp_right_continuous_map T f) g = g.comp f

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) :

C(Y, T) ≃ₜ C(X, T)

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

Equations

continuous_map.comp_right_homeomorph T f = {to_equiv := {to_fun := ⇑(continuous_map.comp_right_continuous_map T f.to_continuous_map), inv_fun := ⇑(continuous_map.comp_right_continuous_map T f.symm.to_continuous_map), left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

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)) :

C(Y, R) →ₐ[R] C(X, R)

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

Equations

continuous_map.comp_right_alg_hom R f = {to_fun := λ (g : C(Y, R)), g.comp f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[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)) :

⇑(continuous_map.comp_right_alg_hom R f) g = g.comp f

theorem continuous_map.comp_right_alg_hom_continuous {X : Type u_1} {Y : Type u_2} (R : Type u_3) [topological_space X] [compact_space X] [topological_space Y] [compact_space Y] [normed_comm_ring R] (f : C(X, Y)) :

continuous ⇑(continuous_map.comp_right_alg_hom R f)