English
The natural map to the uniformly continuous function space is an inducing map; the topology on α →ᵇ β is the initial topology induced by this map.
Русский
Естественное отображение в пространство равномерно непрерывных функций является индуцирующим отображением; топология на α →ᵇ β — начальная топология, индуцированная этим отображением.
LaTeX
$$IsInducing (UniformFun.ofFun ∘ (λ f, f))$$
Lean4
/-- Bounded continuous functions taking values in a complete space form a complete space. -/
instance instCompleteSpace [CompleteSpace β] : CompleteSpace (α →ᵇ β) :=
complete_of_cauchySeq_tendsto fun (f : ℕ → α →ᵇ β) (hf : CauchySeq f) => by
/- We have to show that `f n` converges to a bounded continuous function.
For this, we prove pointwise convergence to define the limit, then check
it is a continuous bounded function, and then check the norm convergence. -/
rcases cauchySeq_iff_le_tendsto_0.1 hf with ⟨b, b0, b_bound, b_lim⟩
have f_bdd := fun x n m N hn hm => le_trans (dist_coe_le_dist x) (b_bound n m N hn hm)
have fx_cau : ∀ x, CauchySeq fun n => f n x := fun x => cauchySeq_iff_le_tendsto_0.2 ⟨b, b0, f_bdd x, b_lim⟩
choose F hF using fun x =>
cauchySeq_tendsto_of_complete
(fx_cau x)
/- `F : α → β`, `hF : ∀ (x : α), Tendsto (fun n ↦ ↑(f n) x) atTop (𝓝 (F x))`
`F` is the desired limit function. Check that it is uniformly approximated by `f N`. -/
have fF_bdd : ∀ x N, dist (f N x) (F x) ≤ b N := fun x N =>
le_of_tendsto (tendsto_const_nhds.dist (hF x))
(Filter.eventually_atTop.2 ⟨N, fun n hn => f_bdd x N n N (le_refl N) hn⟩)
refine ⟨⟨⟨F, ?_⟩, ?_⟩, ?_⟩
· -- Check that `F` is continuous, as a uniform limit of continuous functions
have : TendstoUniformly (fun n x => f n x) F atTop :=
by
refine Metric.tendstoUniformly_iff.2 fun ε ε0 => ?_
refine ((tendsto_order.1 b_lim).2 ε ε0).mono fun n hn x => ?_
rw [dist_comm]
exact lt_of_le_of_lt (fF_bdd x n) hn
exact this.continuous (Eventually.of_forall fun N => (f N).continuous)
· -- Check that `F` is bounded
rcases (f 0).bounded with ⟨C, hC⟩
refine ⟨C + (b 0 + b 0), fun x y => ?_⟩
calc
dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) :=
dist_triangle4_left _ _ _ _
_ ≤ C + (b 0 + b 0) := add_le_add (hC x y) (add_le_add (fF_bdd x 0) (fF_bdd y 0))
· -- Check that `F` is close to `f N` in distance terms
refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (fun _ => dist_nonneg) ?_ b_lim)
exact fun N => (dist_le (b0 _)).2 fun x => fF_bdd x N
