Documentation

BrownianMotion.Choquet.AnalyticSet

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 Set.iInter_prod {α : Type u_4} {β : Type u_5} {ι : Type u_6} {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :

(⋂ (i : ι), t i) ×ˢ s = ⋂ (i : ι), t i ×ˢ s

theorem isCompactSystem_singleton_empty {α : Type u_4} :

IsCompactSystem {∅}

theorem IsCompactSystem.sum {𝓚 : Type u_3} {q : Set (Set 𝓚)} {𝓚' : Type u_4} {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_4} {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 IsCompactSystem.sigma {𝓚 : ℕ → Type u_4} {q : (n : ℕ) → Set (Set (𝓚 n))} (hq : ∀ (n : ℕ), IsCompactSystem (q n)) :

IsCompactSystem {t : Set ((n : ℕ) × 𝓚 n) | ∃ (s : Finset ℕ), t ∈ (↑s).sigma '' Set.univ.pi fun (n : ℕ) => insert Set.univ (q n)}

def MeasureTheory.IsPavingAnalyticFor {𝓧 : Type u_1} (p : Set (Set 𝓧)) (𝓚 : Type u_4) (s : Set 𝓧) :

A set s is analytic for a paving (predicate) p and a type 𝓚 if there exists a compact system q of 𝓚 such that s is the projections of a set t that satisfies prodSigmaDelta p q.

Equations

MeasureTheory.IsPavingAnalyticFor p 𝓚 s = ∃ (q : Set (Set 𝓚)), ∅ ∈ q ∧ IsCompactSystem q ∧ ∃ t ∈ MeasureTheory.prodSigmaDelta p q, s = Prod.fst '' t

Instances For

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

A set s is analytic for a paving (predicate) p if there exists a type 𝓚 and a compact system q of 𝓚 such that s is the projections of a set t that satisfies prodSigmaDelta p q.

Equations

MeasureTheory.IsPavingAnalytic p s = ∃ (𝓚 : Type), Nonempty 𝓚 ∧ MeasureTheory.IsPavingAnalyticFor p 𝓚 s

Instances For

theorem MeasureTheory.IsPavingAnalyticFor.isPavingAnalytic {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓚 : Type} [Nonempty 𝓚] (hs : IsPavingAnalyticFor p 𝓚 s) :

IsPavingAnalytic p s

theorem MeasureTheory.isPavingAnalyticFor_of_mem {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (𝓚 : Type u_4) [Nonempty 𝓚] (hs : s ∈ p) :

IsPavingAnalyticFor p 𝓚 s

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

IsPavingAnalytic p s

theorem MeasureTheory.IsPavingAnalyticFor.mono {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hp : p ⊆ p') (hs : IsPavingAnalyticFor p 𝓚 s) :

IsPavingAnalyticFor p' 𝓚 s

theorem MeasureTheory.IsPavingAnalytic.mono {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hp : p ⊆ p') (hs : IsPavingAnalytic p s) :

IsPavingAnalytic p' s

theorem MeasureTheory.IsPavingAnalyticFor.exists_mem_countableSupClosure_superset {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) :

∃ t ∈ countableSupClosure p, s ⊆ t

theorem MeasureTheory.IsPavingAnalyticFor.empty {𝓧 : Type u_1} {p : Set (Set 𝓧)} (𝓚 : Type u_4) (hp_empty : ∅ ∈ p) :

IsPavingAnalyticFor p 𝓚 ∅

@[simp]

theorem MeasureTheory.IsPavingAnalytic.empty {𝓧 : Type u_1} {p : Set (Set 𝓧)} (hp_empty : ∅ ∈ p) :

IsPavingAnalytic p ∅

@[simp]

theorem MeasureTheory.isPavingAnalyticFor_iff_eq_empty {𝓧 : Type u_1} {p : Set (Set 𝓧)} (𝓚 : Type u_4) [IsEmpty 𝓚] (hp_empty : ∅ ∈ p) (s : Set 𝓧) :

IsPavingAnalyticFor p 𝓚 s ↔ s = ∅

theorem MeasureTheory.IsPavingAnalyticFor.iInter {𝓧 : Type u_1} {p : Set (Set 𝓧)} {𝓚 : ℕ → Type u_4} {s : ℕ → Set 𝓧} (hs : ∀ (n : ℕ), IsPavingAnalyticFor p (𝓚 n) (s n)) :

IsPavingAnalyticFor p ((n : ℕ) → 𝓚 n) (⋂ (n : ℕ), s n)

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

IsPavingAnalytic p (⋂ (n : ℕ), s n)

theorem MeasureTheory.IsPavingAnalyticFor.iUnion {𝓧 : Type u_1} {p : Set (Set 𝓧)} {𝓚 : ℕ → Type u_4} {s : ℕ → Set 𝓧} (hs : ∀ (n : ℕ), IsPavingAnalyticFor p (𝓚 n) (s n)) :

IsPavingAnalyticFor p ((n : ℕ) × 𝓚 n) (⋃ (n : ℕ), s n)

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

IsPavingAnalytic p (⋃ (n : ℕ), s n)

theorem MeasureTheory.IsPavingAnalyticFor.inter {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓚' : Type u_4} {t : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) (ht : IsPavingAnalyticFor p 𝓚' t) :

IsPavingAnalyticFor p (𝓚 × 𝓚') (s ∩ t)

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

IsPavingAnalytic p (s ∩ t)

theorem MeasureTheory.IsPavingAnalyticFor.union {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓚' : Type u_4} {t : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) (ht : IsPavingAnalyticFor p 𝓚' t) :

IsPavingAnalyticFor p (𝓚 ⊕ 𝓚') (s ∪ t)

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

IsPavingAnalytic p (s ∪ t)

theorem MeasureTheory.isPavingAnalyticFor_of_mem_countableInfClosure_of_imp {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hs : s ∈ countableInfClosure p') (hqp : ∀ x ∈ p', IsPavingAnalyticFor p 𝓚 x) :

IsPavingAnalyticFor p (ℕ → 𝓚) s

theorem MeasureTheory.isPavingAnalytic_of_mem_countableInfClosure_of_imp {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hs : s ∈ countableInfClosure p') (hqp : ∀ x ∈ p', IsPavingAnalytic p x) :

IsPavingAnalytic p s

theorem MeasureTheory.isPavingAnalyticFor_of_mem_countableSupClosure_of_imp {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hs : s ∈ countableSupClosure p') (hqp : ∀ x ∈ p', IsPavingAnalyticFor p 𝓚 x) :

IsPavingAnalyticFor p ((_ : ℕ) × 𝓚) s

theorem MeasureTheory.isPavingAnalytic_of_mem_countableSupClosure_of_imp {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hs : s ∈ countableSupClosure p') (hqp : ∀ x ∈ p', IsPavingAnalytic p x) :

IsPavingAnalytic p s

theorem MeasureTheory.IsPavingAnalyticFor.fst {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {𝓚' : Type u_4} (hq_empty : ∅ ∈ q) (hq : IsCompactSystem q) {s : Set (𝓧 × 𝓚)} (hs : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q) 𝓚' s) :

IsPavingAnalyticFor p (𝓚 × 𝓚') (Prod.fst '' s)

The projection of an analytic set is analytic.

theorem MeasureTheory.IsPavingAnalytic.fst {𝓧 : Type u_1} {p : Set (Set 𝓧)} {𝓚 : Type} [Nonempty 𝓚] {q : Set (Set 𝓚)} (hq_empty : ∅ ∈ q) (hq : IsCompactSystem q) {s : Set (𝓧 × 𝓚)} (hs : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q) s) :

IsPavingAnalytic p (Prod.fst '' s)

The projection of an analytic set is analytic.

theorem MeasureTheory.IsPavingAnalyticFor.prod_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set 𝓨} (ht : r t) (hs : IsPavingAnalyticFor p 𝓚 s) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) 𝓚 (t ×ˢ s)

theorem MeasureTheory.IsPavingAnalytic.prod_left {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set 𝓨} (ht : r t) (hs : IsPavingAnalytic p s) :

IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) (t ×ˢ s)

theorem MeasureTheory.IsPavingAnalyticFor.prod_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set 𝓨} (hs : IsPavingAnalyticFor p 𝓚 s) (ht : r t) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) 𝓚 (s ×ˢ t)

theorem MeasureTheory.IsPavingAnalytic.prod_right {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set 𝓨} (hs : IsPavingAnalytic p s) (ht : r t) :

IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) (s ×ˢ t)

theorem MeasureTheory.isPavingAnalyticFor_of_image2_prod_isPavingAnalyticFor_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓨 × 𝓧)} (ht : t ∈ Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r (IsPavingAnalyticFor p 𝓚)) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) 𝓚 t

theorem MeasureTheory.isPavingAnalytic_of_image2_prod_isPavingAnalytic_left {𝓧 : Type u_1} {p : Set (Set 𝓧)} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓨 × 𝓧)} (ht : t ∈ Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r (IsPavingAnalytic p)) :

IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) t

theorem MeasureTheory.isPavingAnalyticFor_of_image2_prod_isPavingAnalyticFor_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓧 × 𝓨)} (ht : t ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) (IsPavingAnalyticFor p 𝓚) r) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) 𝓚 t

theorem MeasureTheory.isPavingAnalytic_of_image2_prod_isPavingAnalytic_right {𝓧 : Type u_1} {p : Set (Set 𝓧)} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓧 × 𝓨)} (ht : t ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) (IsPavingAnalytic p) r) :

IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) t

theorem MeasureTheory.isPavingAnalyticFor_of_mem_countableSupClosure_image2_prod_isPavingAnalyticFor_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓨 × 𝓧)} (ht : t ∈ countableSupClosure (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r (IsPavingAnalyticFor p 𝓚))) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) ((_ : ℕ) × 𝓚) t

theorem MeasureTheory.isPavingAnalyticFor_of_mem_countableSupClosure_image2_prod_isPavingAnalyticFor_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓧 × 𝓨)} (ht : t ∈ countableSupClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) (IsPavingAnalyticFor p 𝓚) r)) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) ((_ : ℕ) × 𝓚) t

theorem MeasureTheory.IsPavingAnalyticFor.prod_mem_countableSupClosure_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set 𝓨} (ht : t ∈ countableSupClosure r) (hs : IsPavingAnalyticFor p 𝓚 s) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) ((_ : ℕ) × 𝓚) (t ×ˢ s)

theorem MeasureTheory.IsPavingAnalyticFor.prod_mem_countableSupClosure_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set 𝓨} (hs : IsPavingAnalyticFor p 𝓚 s) (ht : t ∈ countableSupClosure r) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) ((_ : ℕ) × 𝓚) (s ×ˢ t)

theorem MeasureTheory.IsPavingAnalyticFor.prod {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_4} {𝓚' : Type u_5} {r : Set 𝓨 → Prop} {t : Set 𝓨} (ht : IsPavingAnalyticFor r 𝓚' t) (hs : IsPavingAnalyticFor p 𝓚 s) :

IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) (((_ : ℕ) × 𝓚') × (_ : ℕ) × 𝓚) (t ×ˢ s)

theorem MeasureTheory.IsPavingAnalytic.prod {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set 𝓨} (ht : IsPavingAnalytic r t) (hs : IsPavingAnalytic p s) :

IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) (t ×ˢ s)

theorem MeasureTheory.isPavingAnalyticFor_isPavingAnalyticFor {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalyticFor (IsPavingAnalyticFor p 𝓚) 𝓚 s) :

IsPavingAnalyticFor p (𝓚 × (ℕ → (_ : ℕ) × 𝓚)) s

theorem MeasureTheory.isPavingAnalytic_isPavingAnalytic {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalytic (IsPavingAnalytic p) s) :

IsPavingAnalytic p s

@[simp]

theorem MeasureTheory.isPavingAnalytic_isPavingAnalytic_iff {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} :

IsPavingAnalytic (IsPavingAnalytic p) s ↔ IsPavingAnalytic p s

theorem MeasureTheory.IsPavingAnalyticFor.inter_set {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) (t : Set 𝓧) :

IsPavingAnalyticFor {u : Set 𝓧 | ∃ v ∈ p, u = v ∩ t} 𝓚 (s ∩ t)

theorem MeasureTheory.exists_isPavingAnalyticFor_of_inter_set {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (t : Set 𝓧) (hs : IsPavingAnalyticFor {u : Set 𝓧 | ∃ v ∈ p, u = v ∩ t} 𝓚 s) :

∃ (s' : Set 𝓧), IsPavingAnalyticFor p 𝓚 s' ∧ s = s' ∩ t

theorem MeasureTheory.isPavingAnalytic_of_measurableSet_generateFrom {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hp_empty : ∅ ∈ p) (hp : ∀ s ∈ p, IsPavingAnalytic p sᶜ) (hs : MeasurableSet s) :

IsPavingAnalytic p s

theorem MeasureTheory.Iic_mem_countableSupClosure_Icc (u : ℝ) :

Set.Iic u ∈ countableSupClosure {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}

theorem MeasureTheory.Ici_mem_countableSupClosure_Icc (u : ℝ) :

Set.Ici u ∈ countableSupClosure {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}

theorem MeasureTheory.Iio_mem_countableSupClosure_Icc (u : ℝ) :

Set.Iio u ∈ countableSupClosure {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}

theorem MeasureTheory.Ioi_mem_countableSupClosure_Icc (u : ℝ) :

Set.Ioi u ∈ countableSupClosure {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}

theorem MeasureTheory.univ_mem_countableSupClosure_Icc :

Set.univ ∈ countableSupClosure {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}

theorem MeasureTheory.aux_Icc (l u : ℝ) :

(Set.Icc l u)ᶜ ∈ countableSupClosure {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}

theorem MeasureTheory.aux'_Icc {𝓧 : Type u_1} [MeasurableSpace 𝓧] (s : Set (𝓧 × ℝ)) (hs : s ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ℝ) => x1 ×ˢ x2) MeasurableSet {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}) :

sᶜ ∈ countableSupClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ℝ) => x1 ×ˢ x2) MeasurableSet {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t})

theorem MeasureTheory.borel_eq_generateFrom_isCompact :

borel ℝ = MeasurableSpace.generateFrom IsCompact

theorem MeasureTheory.borel_eq_generateFrom_Icc' (α : Type u_4) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] :

borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), Set.Icc l u = S}

theorem MeasurableSet.isPavingAnalytic_Icc_real {s : Set ℝ} (hs : MeasurableSet s) :

MeasureTheory.IsPavingAnalytic {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t} s

theorem MeasureTheory.IsPavingAnalytic_measurableSet_iff_isPavingAnalytic_Icc (s : Set ℝ) :

IsPavingAnalytic {t : Set ℝ | MeasurableSet t} s ↔ IsPavingAnalytic {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t} s

theorem MeasureTheory.isCountablySpanning_isCompact :

IsCountablySpanning IsCompact

theorem MeasureTheory.isCountablySpanning_Icc :

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

theorem MeasurableSet.isPavingAnalytic_image2_prod {𝓧 : Type u_1} {s : Set (𝓧 × ℝ)} {m𝓧 : MeasurableSpace 𝓧} (hs : MeasurableSet s) :

MeasureTheory.IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ℝ) => x1 ×ˢ x2) MeasurableSet {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}) s

theorem MeasureTheory.isPavingAnalytic_image2_prod_measurableSet_Icc_iff {𝓧 : Type u_1} {s : Set (𝓧 × ℝ)} [MeasurableSpace 𝓧] :

IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ℝ) => x1 ×ˢ x2) MeasurableSet {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}) s ↔ IsPavingAnalytic MeasurableSet s

theorem MeasureTheory.isPavingAnalytic_fst_of_image2_prod_measurableSet_Icc {𝓧 : Type u_1} [MeasurableSpace 𝓧] {s : Set (𝓧 × ℝ)} (hs : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ℝ) => x1 ×ˢ x2) MeasurableSet {t : Set ℝ | ∃ (a : ℝ) (b : ℝ), Set.Icc a b = t}) s) :

IsPavingAnalytic MeasurableSet (Prod.fst '' s)

theorem MeasurableSet.isPavingAnalytic_fst {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {s : Set (𝓧 × ℝ)} (hs : MeasurableSet s) :

MeasureTheory.IsPavingAnalytic MeasurableSet (Prod.fst '' s)

def MeasureTheory.IsMeasurableAnalyticFor {𝓧 : Type u_1} (𝓚 : Type u_4) [MeasurableSpace 𝓚] [MeasurableSpace 𝓧] (s : Set 𝓧) :

A set s of a measurable space 𝓧 is measurably analytic for a measurable space 𝓚 if it is the projection of a measurable set of 𝓧 × 𝓚.

Equations

MeasureTheory.IsMeasurableAnalyticFor 𝓚 s = ∃ (t : Set (𝓧 × 𝓚)), MeasurableSet t ∧ s = Prod.fst '' t

Instances For

def MeasureTheory.IsMeasurableAnalytic {𝓧 : Type u_1} [MeasurableSpace 𝓧] (s : Set 𝓧) :

A set s of a measurable space 𝓧 is measurably analytic if it is the projection of a measurable set of 𝓧 × ℝ.

Equations

MeasureTheory.IsMeasurableAnalytic s = MeasureTheory.IsMeasurableAnalyticFor ℝ s

Instances For

theorem MeasureTheory.IsMeasurableAnalyticFor.isMeasurableAnalytic {𝓧 : Type u_1} {𝓚 : Type u_3} {s : Set 𝓧} {m𝓧 : MeasurableSpace 𝓧} {m𝓚 : MeasurableSpace 𝓚} [StandardBorelSpace 𝓚] (hs : IsMeasurableAnalyticFor 𝓚 s) :

IsMeasurableAnalytic s

If a set is measurably analytic for any standard Borel space 𝓚, then it is measurably analytic for ℝ.

theorem MeasureTheory.IsMeasurableAnalytic.isPavingAnalytic {𝓧 : Type u_1} {s : Set 𝓧} {m𝓧 : MeasurableSpace 𝓧} (hs : IsMeasurableAnalytic s) :

IsPavingAnalytic MeasurableSet s