|
| 1 | +/- |
| 2 | +Copyright (c) 2018 Sébastien Gouëzel. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Sébastien Gouëzel, Mario Carneiro, Yury Kudryashov, Heather Macbeth |
| 5 | +-/ |
| 6 | +import Mathlib.Topology.ContinuousMap.Bounded.Basic |
| 7 | +import Mathlib.Topology.MetricSpace.Equicontinuity |
| 8 | + |
| 9 | +/-! |
| 10 | +# The Arzelà–Ascoli theorem for bounded continuous functions |
| 11 | +
|
| 12 | +Arzelà–Ascoli asserts that, on a compact space, a set of functions sharing a common modulus of |
| 13 | +continuity and taking values in a compact set forms a compact subset for the topology of |
| 14 | +uniform convergence. This file proves the theorem and several useful variations around it. |
| 15 | +-/ |
| 16 | + |
| 17 | +open Set Metric |
| 18 | + |
| 19 | +universe u v |
| 20 | + |
| 21 | +namespace BoundedContinuousFunction |
| 22 | + |
| 23 | +variable {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] |
| 24 | + |
| 25 | +/-- First version, with pointwise equicontinuity and range in a compact space. -/ |
| 26 | +theorem arzela_ascoli₁ [CompactSpace β] (A : Set (α →ᵇ β)) (closed : IsClosed A) |
| 27 | + (H : Equicontinuous ((↑) : A → α → β)) : IsCompact A := by |
| 28 | + simp_rw [Equicontinuous, Metric.equicontinuousAt_iff_pair] at H |
| 29 | + refine isCompact_of_totallyBounded_isClosed ?_ closed |
| 30 | + refine totallyBounded_of_finite_discretization fun ε ε0 => ?_ |
| 31 | + rcases exists_between ε0 with ⟨ε₁, ε₁0, εε₁⟩ |
| 32 | + let ε₂ := ε₁ / 2 / 2 |
| 33 | + /- We have to find a finite discretization of `u`, i.e., finite information |
| 34 | + that is sufficient to reconstruct `u` up to `ε`. This information will be |
| 35 | + provided by the values of `u` on a sufficiently dense set `tα`, |
| 36 | + slightly translated to fit in a finite `ε₂`-dense set `tβ` in the image. Such |
| 37 | + sets exist by compactness of the source and range. Then, to check that these |
| 38 | + data determine the function up to `ε`, one uses the control on the modulus of |
| 39 | + continuity to extend the closeness on tα to closeness everywhere. -/ |
| 40 | + have ε₂0 : ε₂ > 0 := half_pos (half_pos ε₁0) |
| 41 | + have : ∀ x : α, ∃ U, x ∈ U ∧ IsOpen U ∧ |
| 42 | + ∀ y ∈ U, ∀ z ∈ U, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂ := fun x => |
| 43 | + let ⟨U, nhdsU, hU⟩ := H x _ ε₂0 |
| 44 | + let ⟨V, VU, openV, xV⟩ := _root_.mem_nhds_iff.1 nhdsU |
| 45 | + ⟨V, xV, openV, fun y hy z hz f hf => hU y (VU hy) z (VU hz) ⟨f, hf⟩⟩ |
| 46 | + choose U hU using this |
| 47 | + /- For all `x`, the set `hU x` is an open set containing `x` on which the elements of `A` |
| 48 | + fluctuate by at most `ε₂`. |
| 49 | + We extract finitely many of these sets that cover the whole space, by compactness. -/ |
| 50 | + obtain ⟨tα : Set α, _, hfin, htα : univ ⊆ ⋃ x ∈ tα, U x⟩ := |
| 51 | + isCompact_univ.elim_finite_subcover_image (fun x _ => (hU x).2.1) fun x _ => |
| 52 | + mem_biUnion (mem_univ _) (hU x).1 |
| 53 | + rcases hfin.nonempty_fintype with ⟨_⟩ |
| 54 | + obtain ⟨tβ : Set β, _, hfin, htβ : univ ⊆ ⋃y ∈ tβ, ball y ε₂⟩ := |
| 55 | + @finite_cover_balls_of_compact β _ _ isCompact_univ _ ε₂0 |
| 56 | + rcases hfin.nonempty_fintype with ⟨_⟩ |
| 57 | + -- Associate to every point `y` in the space a nearby point `F y` in `tβ` |
| 58 | + choose F hF using fun y => show ∃ z ∈ tβ, dist y z < ε₂ by simpa using htβ (mem_univ y) |
| 59 | + -- `F : β → β`, `hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂` |
| 60 | + /- Associate to every function a discrete approximation, mapping each point in `tα` |
| 61 | + to a point in `tβ` close to its true image by the function. -/ |
| 62 | + classical |
| 63 | + refine ⟨tα → tβ, by infer_instance, fun f a => ⟨F (f.1 a), (hF (f.1 a)).1⟩, ?_⟩ |
| 64 | + rintro ⟨f, hf⟩ ⟨g, hg⟩ f_eq_g |
| 65 | + -- If two functions have the same approximation, then they are within distance `ε` |
| 66 | + refine lt_of_le_of_lt ((dist_le <| le_of_lt ε₁0).2 fun x => ?_) εε₁ |
| 67 | + obtain ⟨x', x'tα, hx'⟩ := mem_iUnion₂.1 (htα (mem_univ x)) |
| 68 | + calc |
| 69 | + dist (f x) (g x) ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') := |
| 70 | + dist_triangle4_right _ _ _ _ |
| 71 | + _ ≤ ε₂ + ε₂ + ε₁ / 2 := by |
| 72 | + refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_) |
| 73 | + · exact (hU x').2.2 _ hx' _ (hU x').1 hf |
| 74 | + · exact (hU x').2.2 _ hx' _ (hU x').1 hg |
| 75 | + · have F_f_g : F (f x') = F (g x') := |
| 76 | + (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g :) |
| 77 | + calc |
| 78 | + dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) := |
| 79 | + dist_triangle_right _ _ _ |
| 80 | + _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g] |
| 81 | + _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2) |
| 82 | + _ = ε₁ / 2 := add_halves _ |
| 83 | + _ = ε₁ := by rw [add_halves, add_halves] |
| 84 | + |
| 85 | +/-- Second version, with pointwise equicontinuity and range in a compact subset. -/ |
| 86 | +theorem arzela_ascoli₂ (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β)) (closed : IsClosed A) |
| 87 | + (in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous ((↑) : A → α → β)) : |
| 88 | + IsCompact A := by |
| 89 | + /- This version is deduced from the previous one by restricting to the compact type in the target, |
| 90 | + using compactness there and then lifting everything to the original space. -/ |
| 91 | + have M : LipschitzWith 1 Subtype.val := LipschitzWith.subtype_val s |
| 92 | + let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M |
| 93 | + refine IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed |
| 94 | + fun f hf => ?_ |
| 95 | + · haveI : CompactSpace s := isCompact_iff_compactSpace.1 hs |
| 96 | + refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_ |
| 97 | + rw [isUniformEmbedding_subtype_val.isUniformInducing.equicontinuous_iff] |
| 98 | + exact H.comp (A.restrictPreimage F) |
| 99 | + · let g := codRestrict s f fun x => in_s f x hf |
| 100 | + rw [show f = F g by ext; rfl] at hf ⊢ |
| 101 | + exact ⟨g, hf, rfl⟩ |
| 102 | + |
| 103 | +/-- Third (main) version, with pointwise equicontinuity and range in a compact subset, but |
| 104 | +without closedness. The closure is then compact. -/ |
| 105 | +theorem arzela_ascoli [T2Space β] (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β)) |
| 106 | + (in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous ((↑) : A → α → β)) : |
| 107 | + IsCompact (closure A) := |
| 108 | + /- This version is deduced from the previous one by checking that the closure of `A`, in |
| 109 | + addition to being closed, still satisfies the properties of compact range and equicontinuity. -/ |
| 110 | + arzela_ascoli₂ s hs (closure A) isClosed_closure |
| 111 | + (fun _ x hf => |
| 112 | + (mem_of_closed' hs.isClosed).2 fun ε ε0 => |
| 113 | + let ⟨g, gA, dist_fg⟩ := Metric.mem_closure_iff.1 hf ε ε0 |
| 114 | + ⟨g x, in_s g x gA, lt_of_le_of_lt (dist_coe_le_dist _) dist_fg⟩) |
| 115 | + (H.closure' continuous_coe) |
| 116 | + |
| 117 | +end BoundedContinuousFunction |
0 commit comments