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 α]
[metric_space β] :
@[simp]
theorem
continuous_map.equiv_bounded_of_compact_symm_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
def
continuous_map.equiv_bounded_of_compact
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
C(α, β) ≃ bounded_continuous_function α β
When α is compact, the bounded continuous maps α →ᵇ β are
equivalent to C(α, β).
Equations
theorem
continuous_map.uniform_inducing_equiv_bounded_of_compact
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
theorem
continuous_map.uniform_embedding_equiv_bounded_of_compact
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
@[simp]
theorem
continuous_map.add_equiv_bounded_of_compact_symm_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β]
[add_monoid β]
[has_lipschitz_add β] :
@[simp]
theorem
continuous_map.add_equiv_bounded_of_compact_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β]
[add_monoid β]
[has_lipschitz_add β] :
noncomputable
def
continuous_map.add_equiv_bounded_of_compact
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β]
[add_monoid β]
[has_lipschitz_add β] :
C(α, β) ≃+ bounded_continuous_function α β
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.to_continuous_map_add_hom α β).to_fun, inv_fun := (continuous_map.equiv_bounded_of_compact α β).symm.inv_fun, left_inv := _, right_inv := _, map_add' := _}.symm
@[protected, instance]
noncomputable
def
continuous_map.metric_space
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
metric_space C(α, β)
def
continuous_map.isometric_bounded_of_compact
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
C(α, β) ≃ᵢ bounded_continuous_function α β
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_symm_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
@[simp]
theorem
continuous_map.isometric_bounded_of_compact_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
@[simp]
theorem
continuous_map.isometric_bounded_of_compact_to_equiv
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
@[simp]
theorem
bounded_continuous_function.dist_mk_of_compact
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
(f g : C(α, β)) :
@[simp]
theorem
bounded_continuous_function.dist_to_continuous_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
(f g : bounded_continuous_function α β) :
theorem
continuous_map.dist_apply_le_dist
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
{f g : C(α, β)}
(x : α) :
has_dist.dist (⇑f x) (⇑g x) ≤ has_dist.dist f g
The pointwise distance is controlled by the distance between functions, by definition.
theorem
continuous_map.dist_le
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
{f g : C(α, β)}
{C : ℝ}
(C0 : 0 ≤ C) :
has_dist.dist f g ≤ C ↔ ∀ (x : α), has_dist.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 α]
[metric_space β]
{f g : C(α, β)}
{C : ℝ}
[nonempty α] :
has_dist.dist f g ≤ C ↔ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C
theorem
continuous_map.dist_lt_iff_of_nonempty
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
{f g : C(α, β)}
{C : ℝ}
[nonempty α] :
has_dist.dist f g < C ↔ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) < C
theorem
continuous_map.dist_lt_of_nonempty
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
{f g : C(α, β)}
{C : ℝ}
[nonempty α]
(w : ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) < C) :
has_dist.dist f g < C
theorem
continuous_map.dist_lt_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
{f g : C(α, β)}
{C : ℝ}
(C0 : 0 < C) :
has_dist.dist f g < C ↔ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) < C
@[protected, instance]
def
continuous_map.complete_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
[complete_space β] :
@[continuity]
theorem
continuous_map.continuous_eval
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β] :
See also continuous_map.continuous_eval'
@[continuity]
theorem
continuous_map.continuous_eval_const
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β]
(x : α) :
continuous (λ (f : C(α, β)), ⇑f x)
See also continuous_map.continuous_eval_const
theorem
continuous_map.continuous_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[compact_space α]
[metric_space β] :
See also continuous_map.continuous_coe'
@[protected, instance]
noncomputable
def
continuous_map.has_norm
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E] :
Equations
- continuous_map.has_norm = {norm := λ (x : C(α, E)), has_dist.dist x 0}
@[simp]
theorem
bounded_continuous_function.norm_mk_of_compact
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : C(α, E)) :
@[simp]
theorem
bounded_continuous_function.norm_to_continuous_map_eq
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : bounded_continuous_function α E) :
@[protected, instance]
noncomputable
def
continuous_map.normed_group
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E] :
normed_group C(α, E)
Equations
- continuous_map.normed_group = {to_has_norm := continuous_map.has_norm _inst_4, to_add_comm_group := continuous_map.add_comm_group continuous_map.normed_group._proof_1, to_metric_space := continuous_map.metric_space α E normed_group.to_metric_space, dist_eq := _}
theorem
continuous_map.norm_coe_le_norm
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : C(α, E))
(x : α) :
theorem
continuous_map.dist_le_two_norm
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : C(α, E))
(x y : α) :
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}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : C(α, E))
{C : ℝ}
(C0 : 0 ≤ 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}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : C(α, E))
[nonempty α]
{M : ℝ} :
theorem
continuous_map.norm_lt_iff
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : C(α, E))
{M : ℝ}
(M0 : 0 < M) :
theorem
continuous_map.norm_lt_iff_of_nonempty
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : C(α, E))
[nonempty α]
{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 : α) :
theorem
continuous_map.norm_eq_supr_norm
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
(f : C(α, E)) :
@[protected, instance]
noncomputable
def
continuous_map.normed_ring
{α : Type u_1}
[topological_space α]
[compact_space α]
{R : Type u_4}
[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 := _}
@[protected, instance]
def
continuous_map.normed_space
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
{𝕜 : Type u_4}
[normed_field 𝕜]
[normed_space 𝕜 E] :
normed_space 𝕜 C(α, E)
Equations
- continuous_map.normed_space = {to_module := continuous_map.module continuous_map.normed_space._proof_2, norm_smul_le := _}
noncomputable
def
continuous_map.linear_isometry_bounded_of_compact
(α : Type u_1)
(E : Type u_3)
[topological_space α]
[compact_space α]
[normed_group E]
(𝕜 : Type u_4)
[normed_field 𝕜]
[normed_space 𝕜 E] :
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 α E 𝕜 = {to_linear_equiv := {to_fun := (continuous_map.add_equiv_bounded_of_compact α E).to_fun, map_add' := _, map_smul' := _, inv_fun := (continuous_map.add_equiv_bounded_of_compact α E).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
continuous_map.linear_isometry_bounded_of_compact_symm_apply
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
{𝕜 : Type u_4}
[normed_field 𝕜]
[normed_space 𝕜 E]
(f : bounded_continuous_function α E) :
@[simp]
theorem
continuous_map.linear_isometry_bounded_of_compact_apply_apply
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
{𝕜 : Type u_4}
[normed_field 𝕜]
[normed_space 𝕜 E]
(f : C(α, E))
(a : α) :
⇑(⇑(continuous_map.linear_isometry_bounded_of_compact α E 𝕜) f) a = ⇑f a
@[simp]
theorem
continuous_map.linear_isometry_bounded_of_compact_to_isometric
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
{𝕜 : Type u_4}
[normed_field 𝕜]
[normed_space 𝕜 E] :
@[simp]
theorem
continuous_map.linear_isometry_bounded_of_compact_to_add_equiv
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
{𝕜 : Type u_4}
[normed_field 𝕜]
[normed_space 𝕜 E] :
@[simp]
theorem
continuous_map.linear_isometry_bounded_of_compact_of_compact_to_equiv
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_group E]
{𝕜 : Type u_4}
[normed_field 𝕜]
[normed_space 𝕜 E] :
@[protected, instance]
def
continuous_map.normed_algebra
{α : Type u_1}
[topological_space α]
[compact_space α]
{𝕜 : Type u_4}
{γ : Type u_5}
[normed_field 𝕜]
[normed_ring γ]
[normed_algebra 𝕜 γ] :
normed_algebra 𝕜 C(α, γ)
Equations
- continuous_map.normed_algebra = {to_algebra := continuous_map.algebra continuous_map.normed_algebra._proof_2, norm_smul_le := _}
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 : α}, has_dist.dist x y < δ → has_dist.dist (⇑f x) (⇑f y) < ε
noncomputable
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 < ε} :
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 : has_dist.dist a b < f.modulus ε h) :
has_dist.dist (⇑f a) (⇑f b) < ε
@[protected]
noncomputable
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[𝕜] γ) :
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[𝕜] γ) :
@[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) :
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 needX Ycompact).comp_right_homeomorph, when we precompose by a homeomorphism.comp_right_alg_hom, whenT = Ris 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)) :
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) :
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)) :
Precomposition of functions into a normed ring by continuous map is an algebra homomorphism.
@[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)) :
theorem
continuous_map.summable_of_locally_summable_norm
{X : Type u_1}
[topological_space X]
[t2_space X]
[locally_compact_space X]
{E : Type u_2}
[normed_group E]
[complete_space E]
{ι : Type u_3}
{F : ι → C(X, E)}
(hF : ∀ (K : topological_space.compacts X), summable (λ (i : ι), ∥continuous_map.restrict ↑K (F i)∥)) :
summable F