English
A version of Arzelà–Ascoli for a set A of bounded continuous functions with equicontinuity and compact range; A is compact.
Русский
Версия закона Арзеля–Азколи для множества A ограниченных непрерывных функций с экконтинуированием и компактным образом; A компактно.
LaTeX
$$$\\text{arzela_ascoli₁} \\ [\\text{CompactSpace } β] \\ (A \\subseteq α \\to β) \\text{ is compact under assumptions}$$$
Lean4
/-- First version, with pointwise equicontinuity and range in a compact space. -/
theorem arzela_ascoli₁ [CompactSpace β] (A : Set (α →ᵇ β)) (closed : IsClosed A)
(H : Equicontinuous ((↑) : A → α → β)) : IsCompact A :=
by
simp_rw [Equicontinuous, Metric.equicontinuousAt_iff_pair] at H
refine TotallyBounded.isCompact_of_isClosed ?_ closed
refine totallyBounded_of_finite_discretization fun ε ε0 => ?_
rcases exists_between ε0 with ⟨ε₁, ε₁0, εε₁⟩
let ε₂ :=
ε₁ / 2 /
2
/- We have to find a finite discretization of `u`, i.e., finite information
that is sufficient to reconstruct `u` up to `ε`. This information will be
provided by the values of `u` on a sufficiently dense set `tα`,
slightly translated to fit in a finite `ε₂`-dense set `tβ` in the image. Such
sets exist by compactness of the source and range. Then, to check that these
data determine the function up to `ε`, one uses the control on the modulus of
continuity to extend the closeness on tα to closeness everywhere. -/
have ε₂0 : ε₂ > 0 := half_pos (half_pos ε₁0)
have : ∀ x : α, ∃ U, x ∈ U ∧ IsOpen U ∧ ∀ y ∈ U, ∀ z ∈ U, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂ := fun x =>
let ⟨U, nhdsU, hU⟩ := H x _ ε₂0
let ⟨V, VU, openV, xV⟩ := _root_.mem_nhds_iff.1 nhdsU
⟨V, xV, openV, fun y hy z hz f hf => hU y (VU hy) z (VU hz) ⟨f, hf⟩⟩
choose U hU using this
obtain ⟨tα : Set α, _, hfin, htα : univ ⊆ ⋃ x ∈ tα, U x⟩ :=
isCompact_univ.elim_finite_subcover_image (fun x _ => (hU x).2.1) fun x _ => mem_biUnion (mem_univ _) (hU x).1
rcases hfin.nonempty_fintype with ⟨_⟩
obtain ⟨tβ : Set β, _, hfin, htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂⟩ :=
@finite_cover_balls_of_compact β _ _ isCompact_univ _ ε₂0
rcases hfin.nonempty_fintype with
⟨_⟩
-- Associate to every point `y` in the space a nearby point `F y` in `tβ`
choose F hF using fun y =>
show ∃ z ∈ tβ, dist y z < ε₂ by
simpa using
htβ
(mem_univ y)
-- `F : β → β`, `hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂`
/- Associate to every function a discrete approximation, mapping each point in `tα`
to a point in `tβ` close to its true image by the function. -/
classical
refine ⟨tα → tβ, by infer_instance, fun f a => ⟨F (f.1 a), (hF (f.1 a)).1⟩, ?_⟩
rintro ⟨f, hf⟩ ⟨g, hg⟩ f_eq_g
refine lt_of_le_of_lt ((dist_le <| le_of_lt ε₁0).2 fun x => ?_) εε₁
obtain ⟨x', x'tα, hx'⟩ := mem_iUnion₂.1 (htα (mem_univ x))
calc
dist (f x) (g x) ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') := dist_triangle4_right _ _ _ _
_ ≤ ε₂ + ε₂ + ε₁ / 2 := by
refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
· exact (hU x').2.2 _ hx' _ (hU x').1 hf
· exact (hU x').2.2 _ hx' _ (hU x').1 hg
· have F_f_g : F (f x') = F (g x') := (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g :)
calc
dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) := dist_triangle_right _ _ _
_ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
_ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
_ = ε₁ / 2 := add_halves _
_ = ε₁ := by rw [add_halves, add_halves]
