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.

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

Product of two sets of sets.

Equations

• MeasureTheory.memProd p q = {s : Set (𝓧 × 𝓚) | ∃ (A : Set 𝓧) (B : Set 𝓚), A ∈ p ∧ B ∈ q ∧ s = A ×ˢ B}

theorem MeasureTheory.memProd_prod {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {A : Set 𝓧} {B : Set 𝓚} (hp : A ∈ p) (hq : B ∈ q) : A ×ˢ B ∈ memProd p q

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

def MeasureTheory.memSigma {𝓧 : Type u_1} (p : Set (Set 𝓧)) : Set (Set 𝓧)

The set is a countable union of sets that satisfy the property.

Equations

• MeasureTheory.memSigma p = {s : Set 𝓧 | ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), A n ∈ p) ∧ s = ⋃ (n : ℕ), A n}

theorem MeasureTheory.memSigma_of_mem {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : s ∈ p) : s ∈ memSigma p

theorem MeasureTheory.memSigma.iUnion {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : ℕ → Set 𝓧} (hs : ∀ (n : ℕ), s n ∈ memSigma p) : ⋃ (n : ℕ), s n ∈ memSigma p

theorem MeasureTheory.memSigma.union {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s t : Set 𝓧} (hs : s ∈ memSigma p) (ht : t ∈ memSigma p) : s ∪ t ∈ memSigma p

def MeasureTheory.memDelta {𝓧 : Type u_1} (p : Set (Set 𝓧)) : Set (Set 𝓧)

The set is a countable intersection of sets that satisfy the property.

Equations

• MeasureTheory.memDelta p = {s : Set 𝓧 | ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), A n ∈ p) ∧ s = ⋂ (n : ℕ), A n}

theorem MeasureTheory.memDelta_of_mem {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : s ∈ p) : s ∈ memDelta p

theorem MeasureTheory.memDelta.iInter {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : ℕ → Set 𝓧} (hs : ∀ (n : ℕ), s n ∈ memDelta p) : ⋂ (n : ℕ), s n ∈ memDelta p

theorem MeasureTheory.memDelta.inter {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s t : Set 𝓧} (hs : s ∈ memDelta p) (ht : t ∈ memDelta p) : s ∩ t ∈ memDelta p

def MeasureTheory.memProdSigmaDelta {𝓧 : 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.memProdSigmaDelta p q = MeasureTheory.memDelta (MeasureTheory.memSigma (MeasureTheory.memProd p q))

def MeasureTheory.memFiniteInter {𝓧 : Type u_1} (p : Set (Set 𝓧)) : Set (Set 𝓧)

The set is a finite intersection of sets that satisfy the property.

Equations

• MeasureTheory.memFiniteInter p = {s : Set 𝓧 | ∃ (t : Finset ℕ) (A : ℕ → Set 𝓧), (∀ n ∈ t, A n ∈ p) ∧ s = ⋂ n ∈ t, A n}

theorem MeasureTheory.memFiniteInter_of_mem {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : s ∈ p) : s ∈ memFiniteInter p

theorem MeasureTheory.memFiniteInter.inter {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s t : Set 𝓧} (hs : s ∈ memFiniteInter p) (ht : t ∈ memFiniteInter p) : s ∩ t ∈ memFiniteInter p

def MeasureTheory.memFiniteUnion {𝓧 : Type u_1} (p : Set (Set 𝓧)) : Set (Set 𝓧)

The set is a finite union of sets that satisfy the property.

Equations

• MeasureTheory.memFiniteUnion p = {s : Set 𝓧 | ∃ (t : Finset ℕ) (A : ℕ → Set 𝓧), (∀ n ∈ t, A n ∈ p) ∧ s = ⋃ n ∈ t, A n}

theorem MeasureTheory.memFiniteUnion_of_mem {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : s ∈ p) : s ∈ memFiniteUnion p

theorem MeasureTheory.memFiniteUnion.union {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s t : Set 𝓧} (hs : s ∈ memFiniteUnion p) (ht : t ∈ memFiniteUnion p) : s ∪ t ∈ memFiniteUnion p

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

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

theorem MeasureTheory.memProdSigmaDelta_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 ∈ memProdSigmaDelta p q

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

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

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

theorem IsCompactSystem.memProd {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hp : IsCompactSystem p) (hq : IsCompactSystem q) : IsCompactSystem (MeasureTheory.memProd p q)

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

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

theorem MeasureTheory.fst_iInter_of_memFiniteUnion_memProd_of_antitone {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hq : IsCompactSystem q) {B : ℕ → Set (𝓧 × 𝓚)} (hB_anti : Antitone B) (hB : ∀ (n : ℕ), memFiniteUnion (memProd p q) (B n)) : Prod.fst '' ⋂ (n : ℕ), B n = ⋂ (n : ℕ), Prod.fst '' B n