Analytic sets in the sense of a paved space

TODO: we use IsCompactSystem, which corresponds to semi-compact pavings for D-M. We use this and not compact pavings (which would be the same, but for arbitrary intersections instead of countable ones), because it's sufficient for our applications, and because it's easier to work with.

theorem mem_supClosure_set_iff {α : Type u_6} {S : Set (Set α)} (s : Set α) : s ∈ supClosure S ↔ ∃ (L : Finset (Set α)), L.Nonempty ∧ s = ⋃₀ ↑L ∧ ↑L ⊆ S

theorem mem_infClosure_set_iff {α : Type u_6} {S : Set (Set α)} (s : Set α) : s ∈ infClosure S ↔ ∃ (L : Finset (Set α)), L.Nonempty ∧ s = ⋂₀ ↑L ∧ ↑L ⊆ S

theorem mem_supClosure_set_iff' {α : Type u_6} {S : Set (Set α)} (s : Set α) : s ∈ supClosure S ↔ ∃ (t : Finset ℕ) (_ : t.Nonempty) (A : ℕ → Set α), (∀ n ∈ t, A n ∈ S) ∧ s = ⋃ n ∈ t, A n

theorem mem_supClosure_insert_empty_iff {α : Type u_6} {S : Set (Set α)} (s : Set α) : s ∈ supClosure (insert ∅ S) ↔ ∃ (L : Finset (Set α)), s = ⋃₀ ↑L ∧ ↑L ⊆ insert ∅ S

theorem mem_infClosure_insert_univ_iff {α : Type u_6} {S : Set (Set α)} (s : Set α) : s ∈ infClosure (insert Set.univ S) ↔ ∃ (L : Finset (Set α)), s = ⋂₀ ↑L ∧ ↑L ⊆ insert Set.univ S

theorem isCompactSystem_singleton_empty {α : Type u_6} : IsCompactSystem {∅}

theorem isCompactSystem_Icc (α : Type u_6) [TopologicalSpace α] [T2Space α] [Preorder α] [CompactIccSpace α] : IsCompactSystem {t : Set α | ∃ (a : α) (b : α), Set.Icc a b = t}

theorem isCompactSystem_insert_empty_Icc (α : Type u_6) [TopologicalSpace α] [T2Space α] [Preorder α] [CompactIccSpace α] : IsCompactSystem (insert ∅ {t : Set α | ∃ (a : α) (b : α), Set.Icc a b = t})

theorem IsCompactSystem.finsetCoe {𝓚 : Type u_3} : IsCompactSystem {t : Set 𝓚 | ∃ (s : Finset 𝓚), ↑s = t}

The set of Finset coercions forms a compact system.

theorem IsCompactSystem.equiv {𝓚 : Type u_3} {𝓚' : Type u_4} (e : 𝓚 ≃ 𝓚') {S : Set (Set 𝓚)} (hS : IsCompactSystem S) : IsCompactSystem {t : Set 𝓚' | ⇑e ⁻¹' t ∈ S}

Transport a compact system along an equivalence of types.

theorem iInter_sigma_eq_empty_iff {ι : Type u_5} {𝓚 : ι → Type u_6} {β : Type u_7} (s : β → Set ι) (f : β → (i : ι) → Set (𝓚 i)) : ⋂ (b : β), (s b).sigma (f b) = ∅ ↔ ∀ i ∈ ⋂ (b : β), s b, ⋂ (b : β), f b i = ∅

theorem iInter₂_sigma_eq_empty_iff {ι : Type u_5} {𝓚 : ι → Type u_6} {β : Type u_7} {p : β → Prop} (s : β → Set ι) (f : β → (i : ι) → Set (𝓚 i)) : ⋂ (b : β), ⋂ (_ : p b), (s b).sigma (f b) = ∅ ↔ ∀ i ∈ ⋂ (b : β), ⋂ (_ : p b), s b, ⋂ (b : β), ⋂ (_ : p b), f b i = ∅

Variant with an additional condition p b (e.g. b ≤ n for dissipate).

theorem IsCompactSystem.sigma {ι : Type u_5} {𝓚 : ι → Type u_6} {q : (i : ι) → Set (Set (𝓚 i))} (hq : ∀ (i : ι), IsCompactSystem (q i)) : IsCompactSystem {t : Set ((i : ι) × 𝓚 i) | ∃ (s : Finset ι), t ∈ (↑s).sigma '' Set.univ.pi q}

theorem IsCompactSystem.sigma_ofFintype {ι : Type u_5} [Finite ι] {𝓚 : ι → Type u_6} {q : (i : ι) → Set (Set (𝓚 i))} (hq : ∀ (i : ι), IsCompactSystem (q i)) : IsCompactSystem (Set.univ.sigma '' Set.univ.pi q)

Sigma variant with fixed s = Finset.univ: subsystem of IsCompactSystem.sigma.

theorem IsCompactSystem.sum {𝓚 𝓚' : Type u} {q : Set (Set 𝓚)} {q' : Set (Set 𝓚')} (hq : IsCompactSystem q) (hq' : IsCompactSystem q') : IsCompactSystem {t : Set (𝓚 ⊕ 𝓚') | Sum.inl ⁻¹' t ∈ q ∧ Sum.inr ⁻¹' t ∈ q'}

theorem IsCompactSystem.pi {𝓚 : ℕ → Type u_6} {q : (n : ℕ) → Set (Set (𝓚 n))} (hq : ∀ (n : ℕ), IsCompactSystem (q n)) : IsCompactSystem (Set.univ.pi '' Set.univ.pi fun (n : ℕ) => insert Set.univ (q n))

theorem MeasureTheory.mem_image2_prod_mono {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {p' : Set (Set 𝓧)} (hp : p ⊆ p') {q' : Set (Set 𝓚)} (hq : q ⊆ q') {s : Set (𝓧 × 𝓚)} (hs : s ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q) : s ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p' q'

theorem InfClosed.image2_prod {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hp_inter : InfClosed p) (hq_inter : InfClosed q) : InfClosed (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q)

def MeasureTheory.prodSigmaDelta {𝓧 : Type u_1} {𝓚 : Type u_3} (p : Set (Set 𝓧)) (q : Set (Set 𝓚)) : Set (Set (𝓧 × 𝓚))

The set is a countable intersection of countable unions of sets that can be written as a product of two sets, each satisfying a property.

Equations

• MeasureTheory.prodSigmaDelta p q = countableInfClosure (countableSupClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q))

theorem MeasureTheory.biUnion_finset_mem_supClosure' {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Finset ℕ} (hs_nonempty : s.Nonempty) {A : ℕ → Set 𝓧} (hs : ∀ n ∈ s, A n ∈ p) : ⋃ n ∈ s, A n ∈ supClosure p

theorem MeasureTheory.biUnion_finset_mem_supClosure {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Finset ℕ} (hs_nonempty : s.Nonempty) {A : ℕ → Set 𝓧} (hs : ∀ n ∈ s, A n ∈ supClosure p) : ⋃ n ∈ s, A n ∈ supClosure p

theorem MeasureTheory.mem_prodSigmaDelta_iff {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {s : Set (𝓧 × 𝓚)} : s ∈ prodSigmaDelta p q ↔ ∃ (A : ℕ → ℕ → Set 𝓧) (_ : ∀ (n m : ℕ), A n m ∈ p) (K : ℕ → ℕ → Set 𝓚) (_ : ∀ (n m : ℕ), K n m ∈ q), s = ⋂ (n : ℕ), ⋃ (m : ℕ), A n m ×ˢ K n m

theorem MeasureTheory.mem_countableSupClosure_image2_prod_iff {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {s : Set (𝓧 × 𝓚)} : s ∈ countableSupClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q) ↔ ∃ (A : ℕ → Set 𝓧) (_ : ∀ (n : ℕ), A n ∈ p) (K : ℕ → Set 𝓚) (_ : ∀ (n : ℕ), K n ∈ q), s = ⋃ (n : ℕ), A n ×ˢ K n

theorem MeasureTheory.mem_prodSigmaDelta_of_mem {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {s : Set 𝓧} {t : Set 𝓚} (hs : s ∈ p) (hq : t ∈ q) : s ×ˢ t ∈ prodSigmaDelta p q

theorem MeasureTheory.prodSigmaDelta.mono {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {p' : Set (Set 𝓧)} {q' : Set (Set 𝓚)} (hp : p ⊆ p') (hq : q ⊆ q') {s : Set (𝓧 × 𝓚)} (hs : s ∈ prodSigmaDelta p q) : s ∈ prodSigmaDelta p' q'

theorem InfClosed.mem_countableInfClosure_iff {𝓧 : Type u_1} {p : Set (Set 𝓧)} (hp : InfClosed p) {s : Set 𝓧} : s ∈ countableInfClosure p ↔ ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), A n ∈ p) ∧ Antitone A ∧ s = ⋂ (n : ℕ), A n

If the set is inf-closed, elements of countablInfClosure can be written as countable intersections of antitone sequences of sets.

theorem SupClosed.mem_countableSupClosure_iff {𝓧 : Type u_1} {p : Set (Set 𝓧)} (hp : SupClosed p) {s : Set 𝓧} : s ∈ countableSupClosure p ↔ ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), A n ∈ p) ∧ Monotone A ∧ s = ⋃ (n : ℕ), A n

If the set is sup-closed, elements of countableSupClosure can be written as countable unions of monotone sequences of sets.

theorem IsCompactSystem.image2_prod {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hp : IsCompactSystem p) (hq : IsCompactSystem q) : IsCompactSystem (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q)

theorem IsCompactSystem.countableInfClosure {𝓧 : Type u_1} {p : Set (Set 𝓧)} (hp : IsCompactSystem p) : IsCompactSystem (countableInfClosure p)

theorem IsCompactSystem.infClosure {𝓧 : Type u_1} {p : Set (Set 𝓧)} (hp : IsCompactSystem p) : IsCompactSystem (infClosure p)

theorem IsCompactSystem.supClosure {𝓧 : Type u_1} {p : Set (Set 𝓧)} (hp : IsCompactSystem p) : IsCompactSystem (supClosure p)

theorem MeasureTheory.fst_iInter_of_supClosure_image2_prod_of_antitone {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hq_empty : ∅ ∈ q) (hq : IsCompactSystem q) {B : ℕ → Set (𝓧 × 𝓚)} (hB_anti : Antitone B) (hB : ∀ (n : ℕ), B n ∈ supClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q)) : Prod.fst '' ⋂ (n : ℕ), B n = ⋂ (n : ℕ), Prod.fst '' B n