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.

def MeasureTheory.IsPavingAnalyticFor {𝓧 : Type u_1} (p : Set 𝓧 → Prop) (𝓚 : 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 memProdSigmaDelta p q.

Equations

MeasureTheory.IsPavingAnalyticFor p 𝓚 s = ∃ (q : Set 𝓚 → Prop), q ∅ ∧ IsCompactSystem q ∧ ∃ (t : Set (𝓧 × 𝓚)), MeasureTheory.memProdSigmaDelta p q t ∧ s = Prod.fst '' t

Instances For

def MeasureTheory.IsPavingAnalytic {𝓧 : Type u_1} (p : Set 𝓧 → Prop) (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 memProdSigmaDelta p q.

Equations

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

Instances For

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

IsPavingAnalytic p s

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

IsPavingAnalyticFor p 𝓚 s

theorem MeasureTheory.isPavingAnalytic_of_prop {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} (hs : p s) :

IsPavingAnalytic p s

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

IsPavingAnalyticFor p' 𝓚 s

theorem MeasureTheory.IsPavingAnalytic.mono {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} {p' : Set 𝓧 → Prop} (hp : ∀ (s : Set 𝓧), p s → p' s) (hs : IsPavingAnalytic p s) :

IsPavingAnalytic p' s

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

∃ (t : Set 𝓧), memSigma p t ∧ s ⊆ t

theorem MeasureTheory.IsPavingAnalyticFor.iInter {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {𝓚 : ℕ → 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 𝓧 → Prop} {s : ℕ → Set 𝓧} (hs : ∀ (n : ℕ), IsPavingAnalytic p (s n)) :

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

theorem MeasureTheory.IsPavingAnalyticFor.iUnion {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {𝓚 : ℕ → 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 𝓧 → Prop} {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 𝓧 → Prop} {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 𝓧 → Prop} {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 𝓧 → Prop} {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 𝓧 → Prop} {s t : Set 𝓧} (hs : IsPavingAnalytic p s) (ht : IsPavingAnalytic p t) :

IsPavingAnalytic p (s ∪ t)

theorem MeasureTheory.isPavingAnalyticFor_of_memDelta_of_imp {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {s : Set 𝓧} {p' : Set 𝓧 → Prop} (hs : memDelta p' s) (hqp : ∀ (x : Set 𝓧), p' x → IsPavingAnalyticFor p 𝓚 x) :

IsPavingAnalyticFor p (ℕ → 𝓚) s

theorem MeasureTheory.isPavingAnalytic_of_memDelta_of_imp {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} {p' : Set 𝓧 → Prop} (hs : memDelta p' s) (hqp : ∀ (x : Set 𝓧), p' x → IsPavingAnalytic p x) :

IsPavingAnalytic p s

theorem MeasureTheory.isPavingAnalyticFor_of_memSigma_of_imp {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {s : Set 𝓧} {p' : Set 𝓧 → Prop} (hs : memSigma p' s) (hqp : ∀ (x : Set 𝓧), p' x → IsPavingAnalyticFor p 𝓚 x) :

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

theorem MeasureTheory.isPavingAnalytic_of_memSigma_of_imp {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} {p' : Set 𝓧 → Prop} (hs : memSigma p' s) (hqp : ∀ (x : Set 𝓧), p' x → IsPavingAnalytic p x) :

IsPavingAnalytic p s

theorem MeasureTheory.IsPavingAnalyticFor.fst {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} {𝓚' : Type u_4} (hq_empty : q ∅) (hq : IsCompactSystem q) {s : Set (𝓧 × 𝓚)} (hs : IsPavingAnalyticFor (memProd 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 𝓧 → Prop} {𝓚 : Type} [Nonempty 𝓚] {q : Set 𝓚 → Prop} (hq_empty : q ∅) (hq : IsCompactSystem q) {s : Set (𝓧 × 𝓚)} (hs : IsPavingAnalytic (memProd 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 𝓧 → Prop} {s : Set 𝓧} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set 𝓨} (ht : r t) (hs : IsPavingAnalyticFor p 𝓚 s) :

IsPavingAnalyticFor (memProd r p) 𝓚 (t ×ˢ s)

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

IsPavingAnalytic (memProd r p) (t ×ˢ s)

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

IsPavingAnalyticFor (memProd p r) 𝓚 (s ×ˢ t)

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

IsPavingAnalytic (memProd p r) (s ×ˢ t)

theorem MeasureTheory.isPavingAnalyticFor_of_memProd_isPavingAnalyticFor_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓨 × 𝓧)} (ht : memProd r (IsPavingAnalyticFor p 𝓚) t) :

IsPavingAnalyticFor (memProd r p) 𝓚 t

theorem MeasureTheory.isPavingAnalytic_of_memProd_isPavingAnalytic_left {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓨 × 𝓧)} (ht : memProd r (IsPavingAnalytic p) t) :

IsPavingAnalytic (memProd r p) t

theorem MeasureTheory.isPavingAnalyticFor_of_memProd_isPavingAnalyticFor_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓧 × 𝓨)} (ht : memProd (IsPavingAnalyticFor p 𝓚) r t) :

IsPavingAnalyticFor (memProd p r) 𝓚 t

theorem MeasureTheory.isPavingAnalytic_of_memProd_isPavingAnalytic_right {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓧 × 𝓨)} (ht : memProd (IsPavingAnalytic p) r t) :

IsPavingAnalytic (memProd p r) t

theorem MeasureTheory.isPavingAnalyticFor_of_memSigma_memProd_isPavingAnalyticFor_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓨 × 𝓧)} (ht : memSigma (memProd r (IsPavingAnalyticFor p 𝓚)) t) :

IsPavingAnalyticFor (memProd r p) ((_ : ℕ) × 𝓚) t

theorem MeasureTheory.isPavingAnalyticFor_of_memSigma_memProd_isPavingAnalyticFor_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {𝓨 : Type u_4} {r : Set 𝓨 → Prop} {t : Set (𝓧 × 𝓨)} (ht : memSigma (memProd (IsPavingAnalyticFor p 𝓚) r) t) :

IsPavingAnalyticFor (memProd p r) ((_ : ℕ) × 𝓚) t

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

IsPavingAnalyticFor (memProd r p) ((_ : ℕ) × 𝓚) (t ×ˢ s)

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

IsPavingAnalyticFor (memProd p r) ((_ : ℕ) × 𝓚) (s ×ˢ t)

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

IsPavingAnalyticFor (memProd r p) (((_ : ℕ) × 𝓚') × (_ : ℕ) × 𝓚) (t ×ˢ s)

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

IsPavingAnalytic (memProd r p) (t ×ˢ s)

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

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

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

IsPavingAnalytic p s

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

IsPavingAnalyticFor (fun (u : Set 𝓧) => ∃ (v : Set 𝓧), p v ∧ u = v ∩ t) 𝓚 (s ∩ t)

theorem MeasureTheory.exists_isPavingAnalyticFor_of_inter_set {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {s : Set 𝓧} (t : Set 𝓧) (hs : IsPavingAnalyticFor (fun (u : Set 𝓧) => ∃ (v : Set 𝓧), p v ∧ u = v ∩ t) 𝓚 s) :

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

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

IsPavingAnalytic p s

theorem MeasureTheory.aux (K : Set ℝ) (hK : IsCompact K) :

memSigma IsCompact Kᶜ

theorem MeasureTheory.aux' {𝓧 : Type u_1} [MeasurableSpace 𝓧] (s : Set (𝓧 × ℝ)) (hs : memProd MeasurableSet IsCompact s) :

memSigma (memProd MeasurableSet IsCompact) sᶜ

theorem MeasureTheory.borel_eq_generateFrom_isCompact :

borel ℝ = MeasurableSpace.generateFrom IsCompact

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

MeasureTheory.IsPavingAnalytic IsCompact s

theorem MeasureTheory.IsPavingAnalytic_measurableSet_iff_isPavingAnalytic_compact (s : Set ℝ) :

IsPavingAnalytic IsCompact s ↔ IsPavingAnalytic MeasurableSet s

theorem MeasureTheory.isCountablySpanning_isCompact :

IsCountablySpanning IsCompact

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

MeasureTheory.IsPavingAnalytic (MeasureTheory.memProd MeasurableSet IsCompact) s

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

IsPavingAnalytic (memProd MeasurableSet IsCompact) s ↔ IsPavingAnalytic MeasurableSet s

theorem MeasureTheory.isPavingAnalytic_fst_of_memProd_measurableSet_isCompact {𝓧 : Type u_1} [MeasurableSpace 𝓧] {s : Set (𝓧 × ℝ)} (hs : IsPavingAnalytic (memProd MeasurableSet IsCompact) 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 𝓧} [MeasurableSpace 𝓧] [MeasurableSpace 𝓚] [StandardBorelSpace 𝓚] (hs : IsMeasurableAnalyticFor 𝓚 s) :

IsMeasurableAnalytic s

If a set is analytic in the measurable sense for any space 𝓚, then it is analytic for ℝ.

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

IsPavingAnalytic MeasurableSet s