Continuous functions on a compact space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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(α, β)
@[simp]
theorem
continuous_map.isometry_equiv_bounded_of_compact_to_equiv
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
def
continuous_map.isometry_equiv_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.isometry_equiv_bounded_of_compact α β = {to_equiv := continuous_map.equiv_bounded_of_compact α β _inst_3, isometry_to_fun := _}
@[simp]
theorem
continuous_map.isometry_equiv_bounded_of_compact_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[compact_space α]
[metric_space β] :
@[simp]
theorem
continuous_map.isometry_equiv_bounded_of_compact_symm_apply
(α : 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_add_comm_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_add_comm_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_add_comm_group E]
(f : bounded_continuous_function α E) :
@[protected, instance]
noncomputable
def
continuous_map.normed_add_comm_group
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_add_comm_group E] :
Equations
- continuous_map.normed_add_comm_group = {to_has_norm := {norm := has_norm.norm continuous_map.has_norm}, to_add_comm_group := {add := add_comm_group.add continuous_map.add_comm_group, add_assoc := _, zero := add_comm_group.zero continuous_map.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul continuous_map.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg continuous_map.add_comm_group, sub := add_comm_group.sub continuous_map.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul continuous_map.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, to_metric_space := {to_pseudo_metric_space := {to_has_dist := {dist := has_dist.dist pseudo_metric_space.to_has_dist}, dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist metric_space.to_pseudo_metric_space, edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space metric_space.to_pseudo_metric_space, uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology metric_space.to_pseudo_metric_space, cobounded_sets := _}, eq_of_dist_eq_zero := _}, dist_eq := _}
@[protected, instance]
def
continuous_map.norm_one_class
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_add_comm_group E]
[nonempty α]
[has_one E]
[norm_one_class E] :
theorem
continuous_map.norm_coe_le_norm
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_add_comm_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_add_comm_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.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_add_comm_group E]
(f : C(α, E)) :
theorem
continuous_map.norm_restrict_mono_set
{E : Type u_3}
[normed_add_comm_group E]
{X : Type u_1}
[topological_space X]
(f : C(X, E))
{K L : topological_space.compacts X}
(hKL : K ≤ L) :
@[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_add_comm_group.to_has_norm infer_instance, to_ring := {add := add_comm_group.add normed_add_comm_group.to_add_comm_group, add_assoc := _, zero := add_comm_group.zero normed_add_comm_group.to_add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul normed_add_comm_group.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg normed_add_comm_group.to_add_comm_group, sub := add_comm_group.sub normed_add_comm_group.to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul normed_add_comm_group.to_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast continuous_map.ring, nat_cast := ring.nat_cast continuous_map.ring, one := ring.one continuous_map.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul continuous_map.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow continuous_map.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_metric_space := normed_add_comm_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_add_comm_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_add_comm_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' := _}
noncomputable
def
continuous_map.eval_clm
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_add_comm_group E]
(𝕜 : Type u_4)
[normed_field 𝕜]
[normed_space 𝕜 E]
(x : α) :
The evaluation at a point, as a continuous linear map from C(α, 𝕜) to 𝕜.
@[simp]
theorem
continuous_map.linear_isometry_bounded_of_compact_symm_apply
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_add_comm_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_add_comm_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_isometry_equiv
{α : Type u_1}
{E : Type u_3}
[topological_space α]
[compact_space α]
[normed_add_comm_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_add_comm_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_add_comm_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_1, 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 < ε) :
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]
[nontrivially_normed_field 𝕜]
[normed_add_comm_group β]
[normed_space 𝕜 β]
[normed_add_comm_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]
[nontrivially_normed_field 𝕜]
[normed_add_comm_group β]
[normed_space 𝕜 β]
[normed_add_comm_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]
[nontrivially_normed_field 𝕜]
[normed_add_comm_group β]
[normed_space 𝕜 β]
[normed_add_comm_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]
[metric_space 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]
[metric_space 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]
[metric_space 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 := _}
theorem
continuous_map.comp_right_alg_hom_continuous
{X : Type u_1}
{Y : Type u_2}
(R : Type u_3)
(A : Type u_4)
[topological_space X]
[compact_space X]
[topological_space Y]
[compact_space Y]
[comm_semiring R]
[semiring A]
[metric_space A]
[topological_semiring A]
[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
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_add_comm_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
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
bounded_continuous_function.mk_of_compact_star
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[normed_add_comm_group β]
[star_add_monoid β]
[normed_star_group β]
[compact_space α]
(f : C(α, β)) :
@[protected, instance]
def
continuous_map.normed_star_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[normed_add_comm_group β]
[star_add_monoid β]
[normed_star_group β]
[compact_space α] :
@[protected, instance]
def
continuous_map.cstar_ring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[normed_ring β]
[star_ring β]
[compact_space α]
[cstar_ring β] :
cstar_ring C(α, β)