def boundedFunctionSpace (X : Type u_1) (Y : Type u_2) [MetricSpace Y] : Set (X → Y)

Definition 3.5 (Space of bounded functions): for metric spaces X and Y, define B(X → Y) as the set of functions f : X → Y for which there exist y0 : Y and M < ∞ such that dist (f x) y0 ≤ M for all x : X.

Equations

• boundedFunctionSpace X Y = {f : X → Y | ∃ (y0 : Y) (M : ℝ), ∀ (x : X), dist (f x) y0 ≤ M}

noncomputable def uniformSupMetric (X : Type u_1) (Y : Type u_2) [MetricSpace Y] (f g : { f : X → Y // f ∈ boundedFunctionSpace X Y }) : ℝ

Definition 3.6: [Uniform (supremum) metric] If X is nonempty, define d_∞(f,g) = sup_{x ∈ X} dist (f x) (g x) for f,g ∈ B(X → Y); if X is empty, set d_∞(f,g) = 0 for all f,g ∈ B(X → Y).

Equations

• uniformSupMetric X Y f g = if x : IsEmpty X then 0 else sSup (Set.range fun (x : X) => dist (↑f x) (↑g x))

def boundedContinuousFunctionSpace (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] : Set (X → Y)

Definition 3.7 [Bounded continuous functions]: for metric spaces X and Y, define C(X → Y) as the set of bounded functions f : X → Y that are continuous.

Equations

• boundedContinuousFunctionSpace X Y = {f : X → Y | f ∈ boundedFunctionSpace X Y ∧ Continuous f}

@[reducible, inline]

abbrev unitIntervalSubtype : Type

The unit interval as a subtype of ℝ.

Equations

• unitIntervalSubtype = { x : ℝ // x ∈ Set.Icc 0 1 }

theorem doubleOnUnitInterval_bounded : (fun (x : unitIntervalSubtype) => 2 * ↑x) ∈ boundedFunctionSpace unitIntervalSubtype ℝ

The function x ↦ 2x on the unit interval is bounded.

theorem tripleOnUnitInterval_bounded : (fun (x : unitIntervalSubtype) => 3 * ↑x) ∈ boundedFunctionSpace unitIntervalSubtype ℝ

The function x ↦ 3x on the unit interval is bounded.

def doubleOnUnitInterval : { f : unitIntervalSubtype → ℝ // f ∈ boundedFunctionSpace unitIntervalSubtype ℝ }

The function x ↦ 2x on the unit interval, as an element of the bounded function space.

Equations

• doubleOnUnitInterval = ⟨fun (x : unitIntervalSubtype) => 2 * ↑x, doubleOnUnitInterval_bounded⟩

def tripleOnUnitInterval : { f : unitIntervalSubtype → ℝ // f ∈ boundedFunctionSpace unitIntervalSubtype ℝ }

The function x ↦ 3x on the unit interval, as an element of the bounded function space.

Equations

• tripleOnUnitInterval = ⟨fun (x : unitIntervalSubtype) => 3 * ↑x, tripleOnUnitInterval_bounded⟩

theorem helperForExample_3_4_3_not_isEmpty_unitIntervalSubtype : ¬IsEmpty unitIntervalSubtype

Helper for Example 3.4.3: the unit interval subtype is nonempty.

theorem helperForExample_3_4_3_dist_double_triple (x : unitIntervalSubtype) : dist (2 * ↑x) (3 * ↑x) = ↑x

Helper for Example 3.4.3: the distance between 2x and 3x is x on [0,1].

theorem helperForExample_3_4_3_range_coe_unitIntervalSubtype : (Set.range fun (x : unitIntervalSubtype) => ↑x) = Set.Icc 0 1

Helper for Example 3.4.3: the range of the coercion from [0,1] is Set.Icc 0 1.

theorem uniformSupMetric_double_triple_unitInterval : uniformSupMetric unitIntervalSubtype ℝ doubleOnUnitInterval tripleOnUnitInterval = 1

Example 3.4.3: for X = [0,1] and Y = ℝ with the usual metrics, if f(x)=2x and g(x)=3x, then d_∞(f,g)=1.

theorem helperForProposition_3_4_4_bddAbove_dist_range {X : Type u_1} {Y : Type u_2} [MetricSpace Y] (f g : { f : X → Y // f ∈ boundedFunctionSpace X Y }) : BddAbove (Set.range fun (x : X) => dist (↑f x) (↑g x))

Helper for Proposition 3.4.4: the range of pointwise distances is bounded above.

theorem helperForProposition_3_4_4_dist_le_uniformSupMetric {X : Type u_1} {Y : Type u_2} [MetricSpace Y] (hX : ¬IsEmpty X) (f g : { f : X → Y // f ∈ boundedFunctionSpace X Y }) (x : X) : dist (↑f x) (↑g x) ≤ uniformSupMetric X Y f g

Helper for Proposition 3.4.4: each pointwise distance is bounded by the uniform metric.

theorem helperForProposition_3_4_4_uniformSupMetric_le_of_forall_dist_le {X : Type u_1} {Y : Type u_2} [MetricSpace Y] (hX : ¬IsEmpty X) (f g : { f : X → Y // f ∈ boundedFunctionSpace X Y }) (R : ℝ) (hR : ∀ (x : X), dist (↑f x) (↑g x) ≤ R) : uniformSupMetric X Y f g ≤ R

Helper for Proposition 3.4.4: a uniform pointwise bound controls the uniform metric.

theorem helperForProposition_3_4_4_uniformSupMetric_nonneg {X : Type u_1} {Y : Type u_2} [MetricSpace Y] (f g : { f : X → Y // f ∈ boundedFunctionSpace X Y }) : 0 ≤ uniformSupMetric X Y f g

Helper for Proposition 3.4.4: the uniform metric is nonnegative.

theorem tendsto_uniformSupMetric_iff_uniformlyConvergent {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (fseq : ℕ → { f : X → Y // f ∈ boundedFunctionSpace X Y }) (f : { f : X → Y // f ∈ boundedFunctionSpace X Y }) : Filter.Tendsto (fun (n : ℕ) => uniformSupMetric X Y (fseq n) f) Filter.atTop (nhds 0) ↔ TendstoUniformly (fun (n : ℕ) => ↑(fseq n)) (↑f) Filter.atTop

Proposition 3.4.4: Let X and Y be metric spaces and let f^{(n)} be a sequence in B(X → Y) with f ∈ B(X → Y). Then the following are equivalent: (1) d_∞(f^{(n)}, f) → 0 as n → ∞; (2) f^{(n)} → f uniformly on X (i.e. the usual ε–N condition).

theorem boundedContinuousFunctionSpace_subset_boundedFunctionSpace (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] : boundedContinuousFunctionSpace X Y ⊆ boundedFunctionSpace X Y

Proposition 3.4.5 (Inclusion into bounded functions): for metric spaces X and Y, C(X → Y) is a subset of B(X → Y).

theorem completeSpace_boundedContinuousFunction (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] [CompleteSpace Y] : CompleteSpace (BoundedContinuousFunction X Y)

Theorem 3.4.5 (Completeness of bounded continuous functions): for metric spaces X and Y with Y complete, the space of bounded continuous functions C(X → Y) is complete with respect to the uniform metric (equivalently, every Cauchy sequence converges uniformly to a bounded continuous function).

theorem continuous_of_tendstoUniformly {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (fseq : ℕ → X → Y) (f : X → Y) (hcont : ∀ (n : ℕ), Continuous (fseq n)) (hconv : TendstoUniformly fseq f Filter.atTop) : Continuous f

Proposition 3.4.6 (Uniform limits preserve continuity): let X and Y be metric spaces. If (fseq n) is a sequence of functions X → Y converging uniformly to f (with respect to the uniform metric), and each fseq n is continuous, then f is continuous.