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.
When α
is compact, the bounded continuous maps α →ᵇ β
are
equivalent to C(α, β)
.
Equations
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
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 := _}
The pointwise distance is controlled by the distance between functions, by definition.
The distance between two functions is controlled by the supremum of the pointwise distances
See also continuous_map.continuous_eval'
See also continuous_map.continuous_eval_const
See also continuous_map.continuous_coe'
Equations
- continuous_map.has_norm = {norm := λ (x : C(α, E)), has_dist.dist x 0}
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 := _}
Distance between the images of any two points is at most twice the norm of the function.
The norm of a function is controlled by the supremum of the pointwise norms
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 := _}
Equations
- continuous_map.normed_space = {to_module := continuous_map.module continuous_map.normed_space._proof_2, norm_smul_le := _}
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' := _}
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.
An arbitrarily chosen modulus of uniform continuity for a given function f
and ε > 0
.
Equations
- f.modulus ε h = classical.some _
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)
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 Y
compact).comp_right_homeomorph
, when we precompose by a homeomorphism.comp_right_alg_hom
, whenT = R
is a topological ring.
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 := _}
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 := _}
Precomposition of functions into a normed ring by continuous map is an algebra homomorphism.