Analytic sets of a Polish space as analytic sets for a paving

We prove that in a Polish space, the analytic sets (MeasureTheory.AnalyticSet, the continuous images of ℕ → ℕ) are the sets that are analytic for the paving of closed sets (MeasureTheory.IsPavingAnalytic).

Main statements

• PiNat.isCompactSystem_cylinder_inter: the intersections of the cylinders of Π n, E n with a closed set form a compact system.
• MeasureTheory.AnalyticSet.isPavingAnalytic_isClosed: in a Hausdorff space, an analytic set is analytic for the paving of closed sets.
• MeasureTheory.AnalyticSet.prod: the product of two analytic sets is analytic.
• MeasureTheory.IsPavingAnalytic.analyticSet: in a Hausdorff space, a set that is analytic for a paving of analytic sets is analytic.
• MeasureTheory.analyticSet_iff_isPavingAnalytic_isClosed: in a Polish space, a set is analytic if and only if it is analytic for the paving of closed sets.

Implementation notes

For the first direction, we write an analytic set s as the range of a continuous map f : (ℕ → ℕ) → X. The graph of f is the intersection over n of the unions of the products closure (f '' C) ×ˢ C, where C ranges over the cylinders of length n. The cylinders form a compact system, and s is the projection of the graph.

For the converse, we write s as the projection of ⋂ n, ⋃ m, A n m ×ˢ K n m. A point x is in s if and only if there is σ : ℕ → ℕ such that x ∈ A n (σ n) for all n and the sets K n (σ n) have a common point. Since the sets K n m belong to a compact system, the second condition defines a closed set S of sequences. Hence s is the projection of the set ⋂ n, ⋃ m, A n m ×ˢ {σ ∈ S | σ n = m}, which is analytic.

theorem CountableSupClosed.iSup_mem_of_countable_range {α : Type u_1} {ι : Type u_2} [CompleteLattice α] [Nonempty ι] {S : Set α} (hS : CountableSupClosed S) {f : ι → α} (hf : (Set.range f).Countable) (hfS : ∀ (i : ι), f i ∈ S) : ⨆ (i : ι), f i ∈ S

If a set is closed under countable suprema, it contains the supremum of every family of its elements that takes countably many values.

Cylinders in spaces of sequences

theorem PiNat.exists_cylinder_subset_of_mem_nhds {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {x : (n : ℕ) → E n} {t : Set ((n : ℕ) → E n)} (ht : t ∈ nhds x) : ∃ (n : ℕ), cylinder x n ⊆ t

Every neighborhood of x contains a cylinder around x.

theorem PiNat.isClopen_of_forall_mem_cylinder {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {T : Set ((n : ℕ) → E n)} {N : ℕ} (h : ∀ (x y : (n : ℕ) → E n), y ∈ cylinder x N → (x ∈ T ↔ y ∈ T)) : IsClopen T

A set of sequences whose membership only depends on the first N terms is clopen.

theorem PiNat.countable_range_of_forall_mem_cylinder {E : ℕ → Type u_1} [∀ (n : ℕ), Countable (E n)] {α : Type u_2} {F : ((n : ℕ) → E n) → α} {N : ℕ} (hF : ∀ (x y : (n : ℕ) → E n), y ∈ cylinder x N → F x = F y) : (Set.range F).Countable

A function of sequences that only depends on the first N terms has countable range.

theorem PiNat.isCompactSystem_cylinder_inter {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {S : Set ((n : ℕ) → E n)} (hS : IsClosed S) : IsCompactSystem {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder x n ∩ S}

The intersections of the cylinders of Π n, E n with a closed set form a compact system.

theorem PiNat.isCompactSystem_cylinders {E : ℕ → Type u_1} : IsCompactSystem {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder x n}

The cylinders of Π n, E n form a compact system.

theorem MeasureTheory.mem_fst_image_iInter_iUnion_prod_iff {𝓧 : Type u_1} {𝓚 : Type u_2} {q : Set (Set 𝓚)} (hq : IsCompactSystem q) {A : ℕ → ℕ → Set 𝓧} {K : ℕ → ℕ → Set 𝓚} (hK : ∀ (n m : ℕ), K n m ∈ q) {x : 𝓧} : x ∈ Prod.fst '' ⋂ (n : ℕ), ⋃ (m : ℕ), A n m ×ˢ K n m ↔ ∃ (σ : ℕ → ℕ), (∀ (N : ℕ), (Set.dissipate (fun (n : ℕ) => K n (σ n)) N).Nonempty) ∧ ∀ (n : ℕ), x ∈ A n (σ n)

A point x is in the projection of ⋂ n, ⋃ m, A n m ×ˢ K n m, where the sets K n m belong to a compact system, if and only if there is σ : ℕ → ℕ such that x ∈ A n (σ n) for all n and the finite intersections of the sets K n (σ n) are nonempty.

theorem MeasureTheory.isClosed_setOf_forall_dissipate_nonempty {𝓚 : Type u_2} (K : ℕ → ℕ → Set 𝓚) : IsClosed {σ : ℕ → ℕ | ∀ (N : ℕ), (Set.dissipate (fun (n : ℕ) => K n (σ n)) N).Nonempty}

The set of sequences σ : ℕ → ℕ such that the finite intersections of the sets K n (σ n) are nonempty is closed.

theorem MeasureTheory.analyticSet_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} : AnalyticSet s ↔ s = ∅ ∨ ∃ (f : (ℕ → ℕ) → X), Continuous f ∧ Set.range f = s

A set is analytic if and only if it is empty or the continuous image of ℕ → ℕ. This is the definition of AnalyticSet, which is not exposed by Mathlib.

theorem MeasureTheory.AnalyticSet.isPavingAnalytic_isClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} [T2Space X] (hs : AnalyticSet s) : IsPavingAnalytic {t : Set X | IsClosed t} s

In a Hausdorff space, an analytic set is analytic for the paving of closed sets.

theorem MeasureTheory.AnalyticSet.prod {X : Type u_1} [TopologicalSpace X] {s : Set X} {Y : Type u_2} [TopologicalSpace Y] {t : Set Y} (hs : AnalyticSet s) (ht : AnalyticSet t) : AnalyticSet (s ×ˢ t)

The product of two analytic sets is analytic.

theorem MeasureTheory.IsPavingAnalytic.analyticSet {X : Type u_1} [TopologicalSpace X] {p : Set (Set X)} {s : Set X} [T2Space X] (hp : ∀ t ∈ p, AnalyticSet t) (hs : IsPavingAnalytic p s) : AnalyticSet s

In a Hausdorff space, a set that is analytic for a paving of analytic sets is analytic.

theorem MeasureTheory.analyticSet_iff_isPavingAnalytic_isClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} [PolishSpace X] : AnalyticSet s ↔ IsPavingAnalytic {t : Set X | IsClosed t} s

In a Polish space, a set is analytic if and only if it is analytic for the paving of closed sets.