Bounded continuous functions
The type of bounded continuous functions taking values in a metric space, with the uniform distance.
def
bounded_continuous_function
(α : Type u)
(β : Type v)
[topological_space α]
[metric_space β] :
Type (max u v)
The type of bounded continuous functions from a topological space to a metric space
Equations
- bounded_continuous_function α β = {f // continuous f ∧ ∃ (C : ℝ), ∀ (x y : α), has_dist.dist (f x) (f y) ≤ C}
@[instance]
def
bounded_continuous_function.has_coe_to_fun
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β] :
Equations
- bounded_continuous_function.has_coe_to_fun = {F := λ (x : bounded_continuous_function α β), α → β, coe := subtype.val (λ (f : α → β), continuous f ∧ ∃ (C : ℝ), ∀ (x y : α), has_dist.dist (f x) (f y) ≤ C)}
theorem
bounded_continuous_function.bounded_range
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f : bounded_continuous_function α β} :
def
bounded_continuous_function.mk_of_compact
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[compact_space α]
(f : α → β) :
If a function is continuous on a compact space, it is automatically bounded, and therefore gives rise to an element of the type of bounded continuous functions
Equations
- bounded_continuous_function.mk_of_compact f hf = ⟨f, _⟩
def
bounded_continuous_function.mk_of_discrete
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[discrete_topology α]
(f : α → β) :
(∃ (C : ℝ), ∀ (x y : α), has_dist.dist (f x) (f y) ≤ C) → bounded_continuous_function α β
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
- bounded_continuous_function.mk_of_discrete f hf = ⟨f, _⟩
@[instance]
def
bounded_continuous_function.has_dist
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β] :
The uniform distance between two bounded continuous functions
Equations
- bounded_continuous_function.has_dist = {dist := λ (f g : bounded_continuous_function α β), has_Inf.Inf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C}}
theorem
bounded_continuous_function.dist_eq
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f g : bounded_continuous_function α β} :
has_dist.dist f g = has_Inf.Inf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C}
theorem
bounded_continuous_function.dist_set_exists
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f g : bounded_continuous_function α β} :
theorem
bounded_continuous_function.dist_coe_le_dist
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f g : bounded_continuous_function α β}
(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
@[ext]
theorem
bounded_continuous_function.ext
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f g : bounded_continuous_function α β} :
theorem
bounded_continuous_function.ext_iff
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f g : bounded_continuous_function α β} :
theorem
bounded_continuous_function.dist_le
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f g : bounded_continuous_function α β}
{C : ℝ} :
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
bounded_continuous_function.dist_zero_of_empty
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f g : bounded_continuous_function α β} :
¬nonempty α → has_dist.dist f g = 0
On an empty space, bounded continuous functions are at distance 0
@[instance]
def
bounded_continuous_function.metric_space
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β] :
The type of bounded continuous functions, with the uniform distance, is a metric space.
Equations
- bounded_continuous_function.metric_space = {to_has_dist := bounded_continuous_function.has_dist _inst_2, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : bounded_continuous_function α β), ennreal.of_real ((λ (f g : bounded_continuous_function α β), has_Inf.Inf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C}) x y), edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (f g : bounded_continuous_function α β), has_Inf.Inf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C}) bounded_continuous_function.metric_space._proof_6 bounded_continuous_function.metric_space._proof_7 bounded_continuous_function.metric_space._proof_8, uniformity_dist := _}
def
bounded_continuous_function.const
(α : Type u)
{β : Type v}
[topological_space α]
[metric_space β] :
β → bounded_continuous_function α β
Constant as a continuous bounded function.
Equations
- bounded_continuous_function.const α b = ⟨λ (x : α), b, _⟩
@[simp]
theorem
bounded_continuous_function.coe_const
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
(b : β) :
theorem
bounded_continuous_function.const_apply
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
(a : α)
(b : β) :
⇑(bounded_continuous_function.const α b) a = b
@[instance]
def
bounded_continuous_function.inhabited
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[inhabited β] :
If the target space is inhabited, so is the space of bounded continuous functions
Equations
theorem
bounded_continuous_function.continuous_eval
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β] :
continuous (λ (p : bounded_continuous_function α β × α), ⇑(p.fst) p.snd)
The evaluation map is continuous, as a joint function of u and x
theorem
bounded_continuous_function.continuous_evalx
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{x : α} :
continuous (λ (f : bounded_continuous_function α β), ⇑f x)
In particular, when x is fixed, f → f x is continuous
theorem
bounded_continuous_function.continuous_evalf
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
{f : bounded_continuous_function α β} :
When f is fixed, x → f x is also continuous, by definition
@[instance]
def
bounded_continuous_function.complete_space
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[complete_space β] :
Bounded continuous functions taking values in a complete space form a complete space.
Equations
def
bounded_continuous_function.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[metric_space β]
[metric_space γ]
(G : β → γ)
{C : nnreal} :
lipschitz_with C G → bounded_continuous_function α β → bounded_continuous_function α γ
Composition (in the target) of a bounded continuous function with a Lipschitz map again gives a bounded continuous function
Equations
- bounded_continuous_function.comp G H f = ⟨λ (x : α), G (⇑f x), _⟩
theorem
bounded_continuous_function.lipschitz_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[metric_space β]
[metric_space γ]
{G : β → γ}
{C : nnreal}
(H : lipschitz_with C G) :
The composition operator (in the target) with a Lipschitz map is Lipschitz
theorem
bounded_continuous_function.uniform_continuous_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[metric_space β]
[metric_space γ]
{G : β → γ}
{C : nnreal}
(H : lipschitz_with C G) :
The composition operator (in the target) with a Lipschitz map is uniformly continuous
theorem
bounded_continuous_function.continuous_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[metric_space β]
[metric_space γ]
{G : β → γ}
{C : nnreal}
(H : lipschitz_with C G) :
The composition operator (in the target) with a Lipschitz map is continuous
def
bounded_continuous_function.cod_restrict
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
(s : set β)
(f : bounded_continuous_function α β) :
(∀ (x : α), ⇑f x ∈ s) → bounded_continuous_function α ↥s
Restriction (in the target) of a bounded continuous function taking values in a subset
Equations
- bounded_continuous_function.cod_restrict s f H = ⟨set.cod_restrict ⇑f s H, _⟩
theorem
bounded_continuous_function.arzela_ascoli₁
{α : Type u}
{β : Type v}
[topological_space α]
[compact_space α]
[metric_space β]
[compact_space β]
(A : set (bounded_continuous_function α β)) :
is_closed A → (∀ (x : α) (ε : ℝ), ε > 0 → (∃ (U : set α) (H : U ∈ nhds x), ∀ (y z : α), y ∈ U → z ∈ U → ∀ (f : bounded_continuous_function α β), f ∈ A → has_dist.dist (⇑f y) (⇑f z) < ε)) → is_compact A
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 α]
[metric_space β]
(s : set β)
(hs : is_compact s)
(A : set (bounded_continuous_function α β)) :
is_closed A → (∀ (f : bounded_continuous_function α β) (x : α), f ∈ A → ⇑f x ∈ s) → (∀ (x : α) (ε : ℝ), ε > 0 → (∃ (U : set α) (H : U ∈ nhds x), ∀ (y z : α), y ∈ U → z ∈ U → ∀ (f : bounded_continuous_function α β), f ∈ A → has_dist.dist (⇑f y) (⇑f z) < ε)) → is_compact A
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 α]
[metric_space β]
(s : set β)
(hs : is_compact s)
(A : set (bounded_continuous_function α β)) :
(∀ (f : bounded_continuous_function α β) (x : α), f ∈ A → ⇑f x ∈ s) → (∀ (x : α) (ε : ℝ), ε > 0 → (∃ (U : set α) (H : U ∈ nhds x), ∀ (y z : α), y ∈ U → z ∈ U → ∀ (f : bounded_continuous_function α β), f ∈ A → has_dist.dist (⇑f y) (⇑f z) < ε)) → is_compact (closure A)
Third (main) version, with pointwise equicontinuity and range in a compact subset, but without closedness. The closure is then compact
theorem
bounded_continuous_function.equicontinuous_of_continuity_modulus
{β : Type v}
[metric_space β]
{α : Type u}
[metric_space α]
(b : ℝ → ℝ)
(b_lim : filter.tendsto b (nhds 0) (nhds 0))
(A : set (bounded_continuous_function α β))
(H : ∀ (x y : α) (f : bounded_continuous_function α β), f ∈ A → has_dist.dist (⇑f x) (⇑f y) ≤ b (has_dist.dist x y))
(x : α)
(ε : ℝ) :
@[instance]
def
bounded_continuous_function.has_zero
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β] :
Equations
@[simp]
theorem
bounded_continuous_function.coe_zero
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
{x : α} :
@[instance]
def
bounded_continuous_function.has_norm
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β] :
Equations
- bounded_continuous_function.has_norm = {norm := λ (u : bounded_continuous_function α β), has_dist.dist u 0}
theorem
bounded_continuous_function.norm_def
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f : bounded_continuous_function α β) :
∥f∥ = has_dist.dist f 0
theorem
bounded_continuous_function.norm_eq
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f : bounded_continuous_function α β) :
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.
theorem
bounded_continuous_function.norm_coe_le_norm
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f : bounded_continuous_function α β)
(x : α) :
theorem
bounded_continuous_function.dist_le_two_norm'
{β : Type v}
{γ : Type w}
[normed_group β]
{f : γ → β}
{C : ℝ}
(hC : ∀ (x : γ), ∥f x∥ ≤ C)
(x y : γ) :
has_dist.dist (f x) (f y) ≤ 2 * C
theorem
bounded_continuous_function.dist_le_two_norm
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f : bounded_continuous_function α β)
(x y : α) :
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 α]
[normed_group β]
{f : bounded_continuous_function α β}
{C : ℝ} :
The norm of a function is controlled by the supremum of the pointwise norms
theorem
bounded_continuous_function.norm_const_le
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(b : β) :
Norm of const α b is less than or equal to ∥b∥. If α is nonempty,
then it is equal to ∥b∥.
@[simp]
theorem
bounded_continuous_function.norm_const_eq
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
[h : nonempty α]
(b : β) :
def
bounded_continuous_function.of_normed_group
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f : α → β)
(Hf : continuous f)
(C : ℝ) :
(∀ (x : α), ∥f x∥ ≤ C) → bounded_continuous_function α β
Constructing a bounded continuous function from a uniformly bounded continuous function taking values in a normed group.
Equations
- bounded_continuous_function.of_normed_group f Hf C H = ⟨λ (n : α), f n, _⟩
theorem
bounded_continuous_function.norm_of_normed_group_le
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
{f : α → β}
(hfc : continuous f)
{C : ℝ}
(hC : 0 ≤ C)
(hfC : ∀ (x : α), ∥f x∥ ≤ C) :
∥bounded_continuous_function.of_normed_group f hfc C hfC∥ ≤ C
def
bounded_continuous_function.of_normed_group_discrete
{α : Type u}
{β : Type v}
[topological_space α]
[discrete_topology α]
[normed_group β]
(f : α → β)
(C : ℝ) :
(∀ (x : α), ∥f x∥ ≤ C) → bounded_continuous_function α β
Constructing a bounded continuous function from a uniformly bounded function on a discrete space, taking values in a normed group
Equations
@[instance]
def
bounded_continuous_function.has_add
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β] :
The pointwise sum of two bounded continuous functions is again bounded continuous.
Equations
- bounded_continuous_function.has_add = {add := λ (f g : bounded_continuous_function α β), bounded_continuous_function.of_normed_group (⇑f + ⇑g) _ (∥f∥ + ∥g∥) _}
@[instance]
def
bounded_continuous_function.has_neg
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β] :
The pointwise opposite of a bounded continuous function is again bounded continuous.
Equations
- bounded_continuous_function.has_neg = {neg := λ (f : bounded_continuous_function α β), bounded_continuous_function.of_normed_group (-⇑f) _ ∥f∥ _}
@[simp]
theorem
bounded_continuous_function.coe_add
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f g : bounded_continuous_function α β) :
theorem
bounded_continuous_function.add_apply
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f g : bounded_continuous_function α β)
{x : α} :
@[simp]
theorem
bounded_continuous_function.coe_neg
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f : bounded_continuous_function α β) :
theorem
bounded_continuous_function.neg_apply
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f : bounded_continuous_function α β)
{x : α} :
theorem
bounded_continuous_function.forall_coe_zero_iff_zero
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f : bounded_continuous_function α β) :
@[instance]
def
bounded_continuous_function.add_comm_group
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β] :
Equations
- bounded_continuous_function.add_comm_group = {add := has_add.add bounded_continuous_function.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg bounded_continuous_function.has_neg, add_left_neg := _, add_comm := _}
@[simp]
theorem
bounded_continuous_function.coe_sub
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f g : bounded_continuous_function α β) :
theorem
bounded_continuous_function.sub_apply
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f g : bounded_continuous_function α β)
{x : α} :
@[instance]
def
bounded_continuous_function.normed_group
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β] :
theorem
bounded_continuous_function.abs_diff_coe_le_dist
{α : Type u}
{β : Type v}
[topological_space α]
[normed_group β]
(f g : bounded_continuous_function α β)
{x : α} :
theorem
bounded_continuous_function.coe_le_coe_add_dist
{α : Type u}
[topological_space α]
{x : α}
{f g : bounded_continuous_function α ℝ} :
⇑f x ≤ ⇑g x + has_dist.dist f g
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.
@[instance]
def
bounded_continuous_function.has_scalar
{α : Type u}
{β : Type v}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_group β]
[normed_space 𝕜 β] :
Equations
- bounded_continuous_function.has_scalar = {smul := λ (c : 𝕜) (f : bounded_continuous_function α β), bounded_continuous_function.of_normed_group (c • ⇑f) _ (∥c∥ * ∥f∥) _}
@[simp]
theorem
bounded_continuous_function.coe_smul
{α : Type u}
{β : Type v}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_group β]
[normed_space 𝕜 β]
(c : 𝕜)
(f : bounded_continuous_function α β) :
theorem
bounded_continuous_function.smul_apply
{α : Type u}
{β : Type v}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_group β]
[normed_space 𝕜 β]
(c : 𝕜)
(f : bounded_continuous_function α β)
(x : α) :
@[instance]
def
bounded_continuous_function.semimodule
{α : Type u}
{β : Type v}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_group β]
[normed_space 𝕜 β] :
Equations
- bounded_continuous_function.semimodule = semimodule.of_core {to_has_scalar := {smul := has_scalar.smul bounded_continuous_function.has_scalar}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}
@[instance]
def
bounded_continuous_function.normed_space
{α : Type u}
{β : Type v}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_group β]
[normed_space 𝕜 β] :
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.
@[instance]
def
bounded_continuous_function.ring
{α : Type u}
[topological_space α]
{R : Type u_1}
[normed_ring R] :
Equations
- bounded_continuous_function.ring = {add := add_comm_group.add bounded_continuous_function.add_comm_group, add_assoc := _, zero := add_comm_group.zero bounded_continuous_function.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg bounded_continuous_function.add_comm_group, add_left_neg := _, add_comm := _, mul := λ (f g : bounded_continuous_function α R), bounded_continuous_function.of_normed_group (⇑f * ⇑g) _ (∥f∥ * ∥g∥) _, mul_assoc := _, one := bounded_continuous_function.const α 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[instance]
def
bounded_continuous_function.normed_ring
{α : Type u}
[topological_space α]
{R : Type u_1}
[normed_ring R] :
Equations
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.
def
bounded_continuous_function.C
{α : Type u}
{γ : Type w}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_ring γ]
[normed_algebra 𝕜 γ] :
bounded_continuous_function.const as a ring_hom.
Equations
- bounded_continuous_function.C = {to_fun := λ (c : 𝕜), bounded_continuous_function.const α (⇑(algebra_map 𝕜 γ) c), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[instance]
def
bounded_continuous_function.algebra
{α : Type u}
{γ : Type w}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_ring γ]
[normed_algebra 𝕜 γ] :
algebra 𝕜 (bounded_continuous_function α γ)
Equations
@[instance]
def
bounded_continuous_function.normed_algebra
{α : Type u}
{γ : Type w}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_ring γ]
[normed_algebra 𝕜 γ]
[nonempty α] :
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 𝕜.
@[instance]
def
bounded_continuous_function.has_scalar'
{α : Type u}
{β : Type v}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_group β]
[normed_space 𝕜 β] :
Equations
- bounded_continuous_function.has_scalar' = {smul := λ (f : bounded_continuous_function α 𝕜) (g : bounded_continuous_function α β), bounded_continuous_function.of_normed_group (λ (x : α), ⇑f x • ⇑g x) _ (∥f∥ * ∥g∥) _}
@[instance]
def
bounded_continuous_function.module'
{α : Type u}
{β : Type v}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_group β]
[normed_space 𝕜 β] :
Equations
- bounded_continuous_function.module' = semimodule.of_core {to_has_scalar := {smul := has_scalar.smul bounded_continuous_function.has_scalar'}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}
theorem
bounded_continuous_function.norm_smul_le
{α : Type u}
{β : Type v}
{𝕜 : Type u_1}
[normed_field 𝕜]
[topological_space α]
[normed_group β]
[normed_space 𝕜 β]
(f : bounded_continuous_function α 𝕜)
(g : bounded_continuous_function α β) :