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
MeasurableSet.of_mem_countableInfClosure
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{s : Set 𝓧}
(hs : s ∈ countableInfClosure MeasurableSet)
:
theorem
MeasurableSet.of_mem_countableInfClosure'
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{s : Set 𝓧}
{p : Set (Set 𝓧)}
(hs : s ∈ countableInfClosure p)
(hp : ∀ t ∈ p, MeasurableSet t)
:
theorem
MeasurableSet.of_mem_countableSupClosure'
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{s : Set 𝓧}
{p : Set (Set 𝓧)}
(hs : s ∈ countableSupClosure p)
(hp : ∀ t ∈ p, MeasurableSet t)
:
theorem
MeasurableSet.of_mem_supClosure
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{s : Set 𝓧}
{p : Set (Set 𝓧)}
(hs : s ∈ supClosure p)
(hp : ∀ t ∈ p, MeasurableSet t)
:
theorem
MeasurableSet.of_mem_image2_prod
{Ω : Type u_6}
{𝓧 : Type u_7}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{s : Set (𝓧 × Ω)}
{p : Set (Set 𝓧)}
{q : Set (Set Ω)}
(hs : s ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set Ω) => x1 ×ˢ x2) p q)
(hp : ∀ t ∈ p, MeasurableSet t)
(hq : ∀ t ∈ q, MeasurableSet t)
:
theorem
MeasurableSet.of_mem_prodSigmaDelta
{Ω : Type u_6}
{𝓧 : Type u_7}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{s : Set (𝓧 × Ω)}
{p : Set (Set 𝓧)}
{q : Set (Set Ω)}
(hs : s ∈ MeasureTheory.prodSigmaDelta p q)
(hp : ∀ t ∈ p, MeasurableSet t)
(hq : ∀ t ∈ q, MeasurableSet t)
:
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
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_6)
[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_6)
(hp_empty : ∅ ∈ p)
:
IsPavingAnalyticFor p 𝓚 ∅
theorem
MeasureTheory.IsPavingAnalyticFor.iInter
{𝓧 : Type u_1}
{p : Set (Set 𝓧)}
{𝓚 : ℕ → Type u_6}
{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_6}
{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_6}
{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}
{p : Set (Set 𝓧)}
{s : Set 𝓧}
{𝓚 𝓚' : Type u}
{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_6}
(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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{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_6}
{𝓚' : Type u_7}
{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_6}
{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 𝓧}
:
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
{ι : Type u_6}
[Nonempty ι]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
(u : ι)
:
theorem
MeasureTheory.Ici_mem_countableSupClosure_Icc
{ι : Type u_6}
[Nonempty ι]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
(u : ι)
:
theorem
MeasureTheory.Iio_mem_countableSupClosure_Icc
{ι : Type u_6}
[Nonempty ι]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[DenselyOrdered ι]
(u : ι)
:
theorem
MeasureTheory.Ioi_mem_countableSupClosure_Icc
{ι : Type u_6}
[Nonempty ι]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[DenselyOrdered ι]
(u : ι)
:
theorem
MeasureTheory.univ_mem_countableSupClosure_Icc
{ι : Type u_6}
[hι : Nonempty ι]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
:
theorem
MeasureTheory.aux_Icc
{ι : Type u_6}
[Nonempty ι]
[LinearOrder ι]
[DenselyOrdered ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
(l u : ι)
:
theorem
MeasureTheory.aux'_Icc
{𝓧 : Type u_1}
{ι : Type u_6}
[Nonempty ι]
[LinearOrder ι]
[DenselyOrdered ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace 𝓧]
(s : Set (𝓧 × ι))
(hs :
s ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) MeasurableSet
(insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}))
:
theorem
MeasureTheory.borel_eq_generateFrom_Icc'
(α : Type u_6)
[TopologicalSpace α]
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
:
theorem
MeasureTheory.borel_eq_generateFrom_Icc''
(α : Type u_6)
[TopologicalSpace α]
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
:
theorem
MeasurableSet.isPavingAnalytic_Icc_real
{ι : Type u_6}
{mι : MeasurableSpace ι}
[LinearOrder ι]
[DenselyOrdered ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[BorelSpace ι]
{s : Set ι}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.IsPavingAnalytic_measurableSet_iff_isPavingAnalytic_Icc
{ι : Type u_6}
{mι : MeasurableSpace ι}
[LinearOrder ι]
[DenselyOrdered ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[BorelSpace ι]
(s : Set ι)
:
theorem
MeasureTheory.isCountablySpanning_insert_empty_Icc
{ι : Type u_6}
[Nonempty ι]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
:
theorem
MeasurableSet.isPavingAnalytic_image2_prod
{𝓧 : Type u_1}
{ι : Type u_6}
{mι : MeasurableSpace ι}
[LinearOrder ι]
[DenselyOrdered ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[BorelSpace ι]
[Nonempty ι]
{s : Set (𝓧 × ι)}
{m𝓧 : MeasurableSpace 𝓧}
(hs : MeasurableSet s)
:
MeasureTheory.IsPavingAnalytic
(Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) MeasurableSet
(insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}))
s
theorem
MeasureTheory.isPavingAnalytic_image2_prod_measurableSet_Icc_iff
{𝓧 : Type u_1}
{ι : Type u_6}
{mι : MeasurableSpace ι}
[LinearOrder ι]
[DenselyOrdered ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[BorelSpace ι]
[Nonempty ι]
{s : Set (𝓧 × ι)}
[MeasurableSpace 𝓧]
:
IsPavingAnalytic
(Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) MeasurableSet
(insert ∅ {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}
{ι : Type}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[CompactIccSpace ι]
[Nonempty ι]
[MeasurableSpace 𝓧]
{s : Set (𝓧 × ι)}
(hs :
IsPavingAnalytic
(Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) MeasurableSet
(insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}))
s)
:
theorem
MeasurableSet.isPavingAnalytic_fst
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{s : Set (𝓧 × ℝ)}
(hs : MeasurableSet s)
:
def
MeasureTheory.IsMeasurableAnalyticFor
{𝓧 : Type u_1}
(𝓚 : Type u_6)
[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
theorem
MeasureTheory.isMeasurableAnalyticFor_of_snd
{𝓧 : Type u_1}
{𝓚 : Type u_3}
{x✝ : MeasurableSpace 𝓚}
[MeasurableSpace 𝓧]
{s : Set 𝓧}
(t : Set (𝓚 × 𝓧))
(ht : MeasurableSet t)
(hst : s = Prod.snd '' t)
:
A set s of a measurable space 𝓧 is measurably analytic if it is the projection of
a measurable set of 𝓧 × ℝ.
Instances For
theorem
MeasureTheory.isMeasurableAnalytic_of_snd
{𝓧 : Type u_1}
[MeasurableSpace 𝓧]
{s : Set 𝓧}
(t : Set (ℝ × 𝓧))
(ht : MeasurableSet t)
(hst : s = Prod.snd '' t)
:
theorem
MeasureTheory.IsMeasurableAnalyticFor.isMeasurableAnalytic
{𝓧 : Type u_1}
{𝓚 : Type u_3}
{s : Set 𝓧}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓚 : MeasurableSpace 𝓚}
[StandardBorelSpace 𝓚]
(hs : IsMeasurableAnalyticFor 𝓚 s)
:
If a set is measurably analytic for any standard Borel space 𝓚,
then it is measurably analytic for ℝ.
theorem
MeasurableSet.isMeasurableAnalytic
{𝓧 : Type u_1}
{s : Set 𝓧}
{m𝓧 : MeasurableSpace 𝓧}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.IsMeasurableAnalytic.isPavingAnalytic
{𝓧 : Type u_1}
{s : Set 𝓧}
{m𝓧 : MeasurableSpace 𝓧}
(hs : IsMeasurableAnalytic s)
: