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_4} {S : Set (Set α)} (s : Set α) : s ∈ supClosure S ↔ ∃ (L : Finset (Set α)), L.Nonempty ∧ s = ⋃₀ ↑L ∧ ↑L ⊆ S

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

theorem mem_supClosure_set_iff' {α : Type u_4} {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_4} {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_4} {S : Set (Set α)} (s : Set α) : s ∈ infClosure (insert Set.univ S) ↔ ∃ (L : Finset (Set α)), s = ⋂₀ ↑L ∧ ↑L ⊆ insert Set.univ S

theorem isCompactSystem_Icc : IsCompactSystem {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}

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