mathlib3 documentation

topology.continuous_function.bounded

Bounded continuous functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The type of bounded continuous functions taking values in a metric space, with the uniform distance.

structure bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [pseudo_metric_space β] :
Type (max u v)

α →ᵇ β is the type of bounded continuous functions α → β from a topological space to a metric space.

When possible, instead of parametrizing results over (f : α →ᵇ β), you should parametrize over (F : Type*) [bounded_continuous_map_class F α β] (f : F).

When you extend this structure, make sure to extend bounded_continuous_map_class.

Instances for bounded_continuous_function
@[class]
structure bounded_continuous_map_class (F : Type u_2) (α : Type u_3) (β : Type u_4) [topological_space α] [pseudo_metric_space β] :
Type (max u_2 u_3 u_4)

bounded_continuous_map_class F α β states that F is a type of bounded continuous maps.

You should also extend this typeclass when you extend bounded_continuous_function.

Instances of this typeclass
Instances of other typeclasses for bounded_continuous_map_class
  • bounded_continuous_map_class.has_sizeof_inst
@[protected, instance]

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
@[protected]
theorem bounded_continuous_function.bounded {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : bounded_continuous_function α β) :
(C : ), (x y : α), has_dist.dist (f x) (f y) C
@[ext]
theorem bounded_continuous_function.ext {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} (h : (x : α), f x = g x) :
f = g
def bounded_continuous_function.mk_of_bound {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : C(α, β)) (C : ) (h : (x y : α), has_dist.dist (f x) (f y) C) :

A continuous function with an explicit bound is a bounded continuous function.

Equations
@[simp]
theorem bounded_continuous_function.mk_of_bound_coe {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f : C(α, β)} {C : } {h : (x y : α), has_dist.dist (f x) (f y) C} :

A continuous function on a compact space is automatically a bounded continuous function.

Equations
@[simp]
theorem bounded_continuous_function.mk_of_discrete_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [discrete_topology α] (f : α β) (C : ) (h : (x y : α), has_dist.dist (f x) (f y) C) (ᾰ : α) :
@[simp]
def bounded_continuous_function.mk_of_discrete {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [discrete_topology α] (f : α β) (C : ) (h : (x y : α), has_dist.dist (f x) (f y) C) :

If a function is bounded on a discrete space, it is automatically continuous, and therefore gives rise to an element of the type of bounded continuous functions

Equations
@[protected, instance]

The uniform distance between two bounded continuous functions

Equations

The pointwise distance is controlled by the distance between functions, by definition.

theorem bounded_continuous_function.dist_le {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} {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

@[protected, instance]

The type of bounded continuous functions, with the uniform distance, is a pseudometric space.

Equations
@[protected, instance]

The type of bounded continuous functions, with the uniform distance, is a metric space.

Equations

On an empty space, bounded continuous functions are at distance 0

The topology on α →ᵇ β is exactly the topology induced by the natural map to α →ᵤ β.

Constant as a continuous bounded function.

Equations
@[protected, instance]

If the target space is inhabited, so is the space of bounded continuous functions

Equations
@[continuity]

When x is fixed, (f : α →ᵇ β) ↦ f x is continuous

@[continuity]

The evaluation map is continuous, as a joint function of u and x

@[protected, instance]

Bounded continuous functions taking values in a complete space form a complete space.

Composition of a bounded continuous function and a continuous function.

Equations
@[simp]
theorem bounded_continuous_function.comp_continuous_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_1} [topological_space δ] (f : bounded_continuous_function α β) (g : C(δ, α)) (x : δ) :
(f.comp_continuous g) x = f (g x)

Restrict a bounded continuous function to a set.

Equations
@[simp]

Composition (in the target) of a bounded continuous function with a Lipschitz map again gives a bounded continuous function

Equations

The composition operator (in the target) with a Lipschitz map is Lipschitz

The composition operator (in the target) with a Lipschitz map is uniformly continuous

The composition operator (in the target) with a Lipschitz map is continuous

Restriction (in the target) of a bounded continuous function taking values in a subset

Equations

A version of function.extend for bounded continuous maps. We assume that the domain has discrete topology, so we only need to verify boundedness.

Equations

First version, with pointwise equicontinuity and range in a compact space

theorem bounded_continuous_function.arzela_ascoli₂ {α : Type u} {β : Type v} [topological_space α] [compact_space α] [pseudo_metric_space β] (s : set β) (hs : is_compact s) (A : set (bounded_continuous_function α β)) (closed : is_closed A) (in_s : (f : bounded_continuous_function α β) (x : α), f A f x s) (H : equicontinuous coe_fn) :

Second version, with pointwise equicontinuity and range in a compact subset

theorem bounded_continuous_function.arzela_ascoli {α : Type u} {β : Type v} [topological_space α] [compact_space α] [pseudo_metric_space β] [t2_space β] (s : set β) (hs : is_compact s) (A : set (bounded_continuous_function α β)) (in_s : (f : bounded_continuous_function α β) (x : α), f A f x s) (H : equicontinuous coe_fn) :

Third (main) version, with pointwise equicontinuity and range in a compact subset, but without closedness. The closure is then compact

@[simp]
@[protected, instance]

The pointwise sum of two bounded continuous functions is again bounded continuous.

Equations
@[simp]
theorem bounded_continuous_function.nsmul_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] (r : ) (f : bounded_continuous_function α β) (v : α) :
(r f) v = r f v
@[protected, instance]
Equations
@[simp]
theorem bounded_continuous_function.coe_sum {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [add_comm_monoid β] [has_lipschitz_add β] {ι : Type u_1} (s : finset ι) (f : ι bounded_continuous_function α β) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
theorem bounded_continuous_function.sum_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [add_comm_monoid β] [has_lipschitz_add β] {ι : Type u_1} (s : finset ι) (f : ι bounded_continuous_function α β) (a : α) :
(s.sum (λ (i : ι), f i)) a = s.sum (λ (i : ι), (f i) a)

The norm of a bounded continuous function is the supremum of ‖f x‖. We use Inf to ensure that the definition works if α has no elements.

When the domain is non-empty, we do not need the 0 ≤ C condition in the formula for ‖f‖ as an Inf.

theorem bounded_continuous_function.dist_le_two_norm' {β : Type v} {γ : Type w} [seminormed_add_comm_group β] {f : γ β} {C : } (hC : (x : γ), f x C) (x y : γ) :
has_dist.dist (f x) (f y) 2 * C

Distance between the images of any two points is at most twice the norm of the function.

theorem bounded_continuous_function.norm_le {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] {f : bounded_continuous_function α β} {C : } (C0 : 0 C) :
f C (x : α), f x C

The norm of a function is controlled by the supremum of the pointwise norms

Norm of const α b is less than or equal to ‖b‖. If α is nonempty, then it is equal to ‖b‖.

Constructing a bounded continuous function from a uniformly bounded continuous function taking values in a normed group.

Equations

Constructing a bounded continuous function from a uniformly bounded function on a discrete space, taking values in a normed group

Equations

Taking the pointwise norm of a bounded continuous function with values in a seminormed_add_comm_group yields a bounded continuous function with values in ℝ.

Equations
@[protected, instance]

If ‖(1 : β)‖ = 1, then ‖(1 : α →ᵇ β)‖ = 1 if α is nonempty.

@[protected, instance]

The pointwise opposite of a bounded continuous function is again bounded continuous.

Equations
@[protected, instance]

The pointwise difference of two bounded continuous functions is again bounded continuous.

Equations
theorem bounded_continuous_function.sub_apply {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f g : bounded_continuous_function α β) {x : α} :
(f - g) x = f x - g x
@[simp]
theorem bounded_continuous_function.zsmul_apply {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (r : ) (f : bounded_continuous_function α β) (v : α) :
(r f) v = r f v
@[protected, instance]
Equations

The nnnorm of a function is controlled by the supremum of the pointwise nnnorms

has_bounded_smul (in particular, topological module) structure #

In this section, if β is a metric space and a 𝕜-module whose addition and scalar multiplication are compatible with the metric structure, then we show that the space of bounded continuous functions from α to β inherits a so-called has_bounded_smul structure (in particular, a has_continuous_mul structure, which is the mathlib formulation of being a topological module), by using pointwise operations and checking that they are compatible with the uniform distance.

@[simp]
theorem bounded_continuous_function.coe_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [has_zero 𝕜] [has_zero β] [has_smul 𝕜 β] [has_bounded_smul 𝕜 β] (c : 𝕜) (f : bounded_continuous_function α β) :
(c f) = λ (x : α), c f x
theorem bounded_continuous_function.smul_apply {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [has_zero 𝕜] [has_zero β] [has_smul 𝕜 β] [has_bounded_smul 𝕜 β] (c : 𝕜) (f : bounded_continuous_function α β) (x : α) :
(c f) x = c f x
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.module {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [semiring 𝕜] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] :
Equations

The evaluation at a point, as a continuous linear map from α →ᵇ β to β.

Equations

The linear map forgetting that a bounded continuous function is bounded.

Equations

Normed space structure #

In this section, if β is a normed space, then we show that the space of bounded continuous functions from α to β inherits a normed space structure, by using pointwise operations and checking that they are compatible with the uniform distance.

@[protected]

Postcomposition of bounded continuous functions into a normed module by a continuous linear map is a continuous linear map. Upgraded version of continuous_linear_map.comp_left_continuous, similar to linear_map.comp_left.

Equations

Normed ring structure #

In this section, if R is a normed ring, then we show that the space of bounded continuous functions from α to R inherits a normed ring structure, by using pointwise operations and checking that they are compatible with the uniform distance.

@[protected, instance]
Equations
@[simp]
theorem bounded_continuous_function.coe_pow {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] (n : ) (f : bounded_continuous_function α R) :
(f ^ n) = f ^ n
@[simp]
theorem bounded_continuous_function.pow_apply {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] (n : ) (f : bounded_continuous_function α R) (v : α) :
(f ^ n) v = f v ^ n
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations

Normed commutative ring structure #

In this section, if R is a normed commutative ring, then we show that the space of bounded continuous functions from α to R inherits a normed commutative ring structure, by using pointwise operations and checking that they are compatible with the uniform distance.

Normed algebra structure #

In this section, if γ is a normed algebra, then we show that the space of bounded continuous functions from α to γ inherits a normed algebra structure, by using pointwise operations and checking that they are compatible with the uniform distance.

@[simp]
theorem bounded_continuous_function.algebra_map_apply {α : Type u} {γ : Type w} {𝕜 : Type u_2} [normed_field 𝕜] [topological_space α] [normed_ring γ] [normed_algebra 𝕜 γ] (k : 𝕜) (a : α) :

Structure as normed module over scalar functions #

If β is a normed 𝕜-space, then we show that the space of bounded continuous functions from α to β is naturally a module over the algebra of bounded continuous functions from α to 𝕜.

Star structures #

In this section, if β is a normed ⋆-group, then so is the space of bounded continuous functions from α to β, by using the star operation pointwise.

If 𝕜 is normed field and a ⋆-ring over which β is a normed algebra and a star module, then the space of bounded continuous functions from α to β is a star module.

If β is a ⋆-ring in addition to being a normed ⋆-group, then α →ᵇ β inherits a ⋆-ring structure.

In summary, if β is a C⋆-algebra over 𝕜, then so is α →ᵇ β; note that completeness is guaranteed when β is complete (see bounded_continuous_function.complete).

@[simp]

The right-hand side of this equality can be parsed star ∘ ⇑f because of the instance pi.has_star. Upon inspecting the goal, one sees ⊢ ⇑(star f) = star ⇑f.

@[protected, instance]

The nonnegative part of a bounded continuous -valued function as a bounded continuous ℝ≥0-valued function.

Equations

The absolute value of a bounded continuous -valued function as a bounded continuous ℝ≥0-valued function.

Equations

Decompose a bounded continuous function to its positive and negative parts.

Express the absolute value of a bounded continuous function in terms of its positive and negative parts.