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
ContinuousMap.equivBoundedOfCompact to move functions back and forth.
def
ContinuousMap.equivBoundedOfCompact
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
C(α, β) ≃ BoundedContinuousFunction α β
When α is compact, the bounded continuous maps α →ᵇ β are
equivalent to C(α, β).
Equations
- ContinuousMap.equivBoundedOfCompact α β = { toFun := BoundedContinuousFunction.mkOfCompact, invFun := BoundedContinuousFunction.toContinuousMap, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
theorem
ContinuousMap.equivBoundedOfCompact_symm_apply
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
@[simp]
theorem
ContinuousMap.equivBoundedOfCompact_apply
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
theorem
ContinuousMap.isUniformInducing_equivBoundedOfCompact
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
@[deprecated ContinuousMap.isUniformInducing_equivBoundedOfCompact (since := "2024-10-05")]
theorem
ContinuousMap.uniformInducing_equivBoundedOfCompact
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
Alias of ContinuousMap.isUniformInducing_equivBoundedOfCompact.
theorem
ContinuousMap.isUniformEmbedding_equivBoundedOfCompact
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
@[deprecated ContinuousMap.isUniformEmbedding_equivBoundedOfCompact (since := "2024-10-01")]
theorem
ContinuousMap.uniformEmbedding_equivBoundedOfCompact
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
Alias of ContinuousMap.isUniformEmbedding_equivBoundedOfCompact.
def
ContinuousMap.addEquivBoundedOfCompact
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
[AddMonoid β]
[LipschitzAdd β]
:
C(α, β) ≃+ BoundedContinuousFunction α β
When α is compact, the bounded continuous maps α →ᵇ 𝕜 are
additively equivalent to C(α, 𝕜).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMap.addEquivBoundedOfCompact_symm_apply
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
[AddMonoid β]
[LipschitzAdd β]
:
@[simp]
theorem
ContinuousMap.addEquivBoundedOfCompact_apply
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
[AddMonoid β]
[LipschitzAdd β]
:
instance
ContinuousMap.instPseudoMetricSpace
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
instance
ContinuousMap.instMetricSpace
(α : Type u_1)
[TopologicalSpace α]
[CompactSpace α]
{β : Type u_4}
[MetricSpace β]
:
MetricSpace C(α, β)
def
ContinuousMap.isometryEquivBoundedOfCompact
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
C(α, β) ≃ᵢ BoundedContinuousFunction α β
When α is compact, and β is a metric space, the bounded continuous maps α →ᵇ β are
isometric to C(α, β).
Equations
- ContinuousMap.isometryEquivBoundedOfCompact α β = { toEquiv := ContinuousMap.equivBoundedOfCompact α β, isometry_toFun := ⋯ }
Instances For
@[simp]
theorem
ContinuousMap.isometryEquivBoundedOfCompact_toEquiv
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
(ContinuousMap.isometryEquivBoundedOfCompact α β).toEquiv = ContinuousMap.equivBoundedOfCompact α β
@[simp]
theorem
ContinuousMap.isometryEquivBoundedOfCompact_apply
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
@[simp]
theorem
ContinuousMap.isometryEquivBoundedOfCompact_symm_apply
(α : Type u_1)
(β : Type u_2)
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
:
@[simp]
theorem
BoundedContinuousFunction.dist_mkOfCompact
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
(f g : C(α, β))
:
@[simp]
theorem
BoundedContinuousFunction.dist_toContinuousMap
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
(f g : BoundedContinuousFunction α β)
:
theorem
ContinuousMap.dist_apply_le_dist
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
{f g : C(α, β)}
(x : α)
:
The pointwise distance is controlled by the distance between functions, by definition.
theorem
ContinuousMap.dist_le
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
{f g : C(α, β)}
{C : ℝ}
(C0 : 0 ≤ C)
:
The distance between two functions is controlled by the supremum of the pointwise distances.
theorem
ContinuousMap.dist_le_iff_of_nonempty
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
{f g : C(α, β)}
{C : ℝ}
[Nonempty α]
:
theorem
ContinuousMap.dist_lt_iff_of_nonempty
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
{f g : C(α, β)}
{C : ℝ}
[Nonempty α]
:
theorem
ContinuousMap.dist_lt_of_nonempty
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
{f g : C(α, β)}
{C : ℝ}
[Nonempty α]
(w : ∀ (x : α), dist (f x) (g x) < C)
:
theorem
ContinuousMap.dist_lt_iff
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
{f g : C(α, β)}
{C : ℝ}
(C0 : 0 < C)
:
instance
ContinuousMap.instBoundedSMul
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
{R : Type u_4}
[Zero R]
[Zero β]
[PseudoMetricSpace R]
[SMul R β]
[BoundedSMul R β]
:
BoundedSMul R C(α, β)
instance
ContinuousMap.instNorm
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
:
@[simp]
theorem
BoundedContinuousFunction.norm_mkOfCompact
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
:
@[simp]
theorem
BoundedContinuousFunction.norm_toContinuousMap_eq
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : BoundedContinuousFunction α E)
:
instance
ContinuousMap.instSeminormedAddCommGroup
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
:
instance
ContinuousMap.instNormedAddCommGroup
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{E : Type u_4}
[NormedAddCommGroup E]
:
instance
ContinuousMap.instNormOneClassOfNonempty
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
[Nonempty α]
[One E]
[NormOneClass E]
:
NormOneClass C(α, E)
theorem
ContinuousMap.norm_coe_le_norm
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
(x : α)
:
theorem
ContinuousMap.dist_le_two_norm
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
(x y : α)
:
Distance between the images of any two points is at most twice the norm of the function.
theorem
ContinuousMap.norm_le
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
{C : ℝ}
(C0 : 0 ≤ C)
:
The norm of a function is controlled by the supremum of the pointwise norms.
theorem
ContinuousMap.norm_le_of_nonempty
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
[Nonempty α]
{M : ℝ}
:
theorem
ContinuousMap.norm_lt_iff
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
{M : ℝ}
(M0 : 0 < M)
:
theorem
ContinuousMap.nnnorm_lt_iff
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
{M : NNReal}
(M0 : 0 < M)
:
theorem
ContinuousMap.norm_lt_iff_of_nonempty
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
[Nonempty α]
{M : ℝ}
:
theorem
ContinuousMap.nnnorm_lt_iff_of_nonempty
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
[Nonempty α]
{M : NNReal}
:
theorem
ContinuousMap.apply_le_norm
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
(f : C(α, ℝ))
(x : α)
:
theorem
ContinuousMap.neg_norm_le_apply
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
(f : C(α, ℝ))
(x : α)
:
theorem
ContinuousMap.nnnorm_eq_iSup_nnnorm
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
:
theorem
ContinuousMap.norm_eq_iSup_norm
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(f : C(α, E))
:
instance
ContinuousMap.instCompactSpaceElemCoeCompacts
{X : Type u_4}
[TopologicalSpace X]
(K : TopologicalSpace.Compacts X)
:
CompactSpace ↑↑K
theorem
ContinuousMap.norm_restrict_mono_set
{E : Type u_3}
[SeminormedAddCommGroup E]
{X : Type u_4}
[TopologicalSpace X]
(f : C(X, E))
{K L : TopologicalSpace.Compacts X}
(hKL : K ≤ L)
:
‖ContinuousMap.restrict (↑K) f‖ ≤ ‖ContinuousMap.restrict (↑L) f‖
instance
ContinuousMap.instNonUnitalSeminormedRing
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
[NonUnitalSeminormedRing R]
:
instance
ContinuousMap.instNonUnitalSeminormedCommRing
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
[NonUnitalSeminormedCommRing R]
:
instance
ContinuousMap.instSeminormedRing
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
[SeminormedRing R]
:
Equations
instance
ContinuousMap.instSeminormedCommRing
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
[SeminormedCommRing R]
:
instance
ContinuousMap.instNonUnitalNormedRing
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
[NonUnitalNormedRing R]
:
Equations
instance
ContinuousMap.instNonUnitalNormedCommRing
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
[NonUnitalNormedCommRing R]
:
instance
ContinuousMap.instNormedRing
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
[NormedRing R]
:
NormedRing C(α, R)
Equations
instance
ContinuousMap.instNormedCommRing
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
[NormedCommRing R]
:
Equations
instance
ContinuousMap.normedSpace
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
{𝕜 : Type u_4}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
NormedSpace 𝕜 C(α, E)
Equations
def
ContinuousMap.linearIsometryBoundedOfCompact
(α : Type u_1)
(E : Type u_3)
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
(𝕜 : Type u_4)
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
When α is compact and 𝕜 is a normed field,
the 𝕜-algebra of bounded continuous maps α →ᵇ β is
𝕜-linearly isometric to C(α, β).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMap.linearIsometryBoundedOfCompact_symm_apply
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
{𝕜 : Type u_4}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
(f : BoundedContinuousFunction α E)
:
(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).symm f = f.toContinuousMap
@[simp]
theorem
ContinuousMap.linearIsometryBoundedOfCompact_apply_apply
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
{𝕜 : Type u_4}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
(f : C(α, E))
(a : α)
:
((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f) a = f a
@[simp]
theorem
ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
{𝕜 : Type u_4}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toIsometryEquiv = ContinuousMap.isometryEquivBoundedOfCompact α E
@[simp]
theorem
ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
{𝕜 : Type u_4}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
↑(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toLinearEquiv = ContinuousMap.addEquivBoundedOfCompact α E
@[simp]
theorem
ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv
{α : Type u_1}
{E : Type u_3}
[TopologicalSpace α]
[CompactSpace α]
[SeminormedAddCommGroup E]
{𝕜 : Type u_4}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toEquiv = ContinuousMap.equivBoundedOfCompact α E
@[simp]
theorem
ContinuousMap.nnnorm_smul_const
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
{β : Type u_5}
[NormedAddCommGroup β]
[NormedDivisionRing R]
[Module R β]
[BoundedSMul R β]
(f : C(α, R))
(b : β)
:
@[simp]
theorem
ContinuousMap.norm_smul_const
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{R : Type u_4}
{β : Type u_5}
[NormedAddCommGroup β]
[NormedDivisionRing R]
[Module R β]
[BoundedSMul R β]
(f : C(α, R))
(b : β)
:
instance
ContinuousMap.instNormedAlgebra
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
{𝕜 : Type u_4}
{γ : Type u_5}
[NormedField 𝕜]
[SeminormedRing γ]
[NormedAlgebra 𝕜 γ]
:
NormedAlgebra 𝕜 C(α, γ)
Equations
We now set up some declarations making it convenient to use uniform continuity.
theorem
ContinuousMap.uniform_continuity
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
(f : C(α, β))
(ε : ℝ)
(h : 0 < ε)
:
def
ContinuousMap.modulus
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
(f : C(α, β))
(ε : ℝ)
(h : 0 < ε)
:
An arbitrarily chosen modulus of uniform continuity for a given function f and ε > 0.
Equations
- f.modulus ε h = Classical.choose ⋯
Instances For
theorem
ContinuousMap.modulus_pos
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
(f : C(α, β))
{ε : ℝ}
{h : 0 < ε}
:
0 < f.modulus ε h
theorem
ContinuousMap.dist_lt_of_dist_lt_modulus
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[CompactSpace α]
[PseudoMetricSpace β]
(f : C(α, β))
(ε : ℝ)
(h : 0 < ε)
{a b : α}
(w : dist a b < f.modulus ε h)
:
def
ContinuousLinearMap.compLeftContinuousCompact
(X : Type u_1)
{𝕜 : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[TopologicalSpace X]
[CompactSpace X]
[NontriviallyNormedField 𝕜]
[SeminormedAddCommGroup β]
[NormedSpace 𝕜 β]
[SeminormedAddCommGroup γ]
[NormedSpace 𝕜 γ]
(g : β →L[𝕜] γ)
:
Postcomposition of continuous functions into a normed module by a continuous linear map is a
continuous linear map.
Transferred version of ContinuousLinearMap.compLeftContinuousBounded,
upgraded version of ContinuousLinearMap.compLeftContinuous,
similar to LinearMap.compLeft.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousLinearMap.toLinear_compLeftContinuousCompact
(X : Type u_1)
{𝕜 : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[TopologicalSpace X]
[CompactSpace X]
[NontriviallyNormedField 𝕜]
[SeminormedAddCommGroup β]
[NormedSpace 𝕜 β]
[SeminormedAddCommGroup γ]
[NormedSpace 𝕜 γ]
(g : β →L[𝕜] γ)
:
@[simp]
theorem
ContinuousLinearMap.compLeftContinuousCompact_apply
(X : Type u_1)
{𝕜 : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[TopologicalSpace X]
[CompactSpace X]
[NontriviallyNormedField 𝕜]
[SeminormedAddCommGroup β]
[NormedSpace 𝕜 β]
[SeminormedAddCommGroup γ]
[NormedSpace 𝕜 γ]
(g : β →L[𝕜] γ)
(f : C(X, β))
(x : X)
:
((ContinuousLinearMap.compLeftContinuousCompact X g) f) x = g (f x)
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
ContinuousMap.summable_of_locally_summable_norm
{X : Type u_1}
[TopologicalSpace X]
[LocallyCompactSpace X]
{E : Type u_2}
[NormedAddCommGroup E]
[CompleteSpace E]
{ι : Type u_3}
{F : ι → C(X, E)}
(hF : ∀ (K : TopologicalSpace.Compacts X), Summable fun (i : ι) => ‖ContinuousMap.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
BoundedContinuousFunction.mkOfCompact_star
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
[StarAddMonoid β]
[NormedStarGroup β]
[CompactSpace α]
(f : C(α, β))
:
instance
ContinuousMap.instNormedStarGroup
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
[StarAddMonoid β]
[NormedStarGroup β]
[CompactSpace α]
:
instance
ContinuousMap.instCStarRing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[CompactSpace α]
[NonUnitalNormedRing β]
[StarRing β]
[CStarRing β]
: