# Measurably generated filters #

We say that a filter `f` is measurably generated if every set `s ∈ f` includes a measurable set `t ∈ f`. This property is useful, e.g., to extract a measurable witness of `Filter.Eventually`.

source
@[simp]
theorem MeasurableSpace.generateFrom_singleton {α : Type u_1} (s : Set α) :
generateFrom {s} = MeasurableSpace.comap (fun (x : α) => x ∈ s) ⊤

The sigma-algebra generated by a single set `s` is `{∅, s, sᶜ, univ}`.

source
theorem MeasurableSpace.generateFrom_singleton_le {α : Type u_1} {m : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) :
generateFrom {s} ≤ m
source
theorem MeasureTheory.measurableSet_generateFrom_singleton_iff {α : Type u_1} {s t : Set α} :
MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = s ᶜ ∨ t = Set.univ
source
class Filter.IsMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] (f : Filter α) :
Prop

A filter `f` is measurably generates if each `s ∈ f` includes a measurable `t ∈ f`.

- exists_measurable_subset ⦃s : Set α⦄ : s ∈ f → ∃ t ∈ f, MeasurableSet t ∧ t ⊆ s

Instances

source
instance Filter.isMeasurablyGenerated_bot {α : Type u_1} [MeasurableSpace α] :
⊥.IsMeasurablyGenerated
source
instance Filter.isMeasurablyGenerated_top {α : Type u_1} [MeasurableSpace α] :
⊤.IsMeasurablyGenerated
source
theorem Filter.Eventually.exists_measurable_mem {α : Type u_1} [MeasurableSpace α] {f : Filter α} [f.IsMeasurablyGenerated] {p : α → Prop} (h : ∀ᶠ (x : α) in f, p x) :
∃ s ∈ f, MeasurableSet s ∧ ∀ x ∈ s, p x
source
theorem Filter.Eventually.exists_measurable_mem_of_smallSets {α : Type u_1} [MeasurableSpace α] {f : Filter α} [f.IsMeasurablyGenerated] {p : Set α → Prop} (h : ∀ᶠ (s : Set α) in f.smallSets, p s) :
∃ s ∈ f, MeasurableSet s ∧ p s
source
instance Filter.inf_isMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] (f g : Filter α) [f.IsMeasurablyGenerated] [g.IsMeasurablyGenerated] :
(f ⊓ g).IsMeasurablyGenerated
source
theorem Filter.principal_isMeasurablyGenerated_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} :
(principal s).IsMeasurablyGenerated ↔ MeasurableSet s
source
theorem MeasurableSet.principal_isMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] {s : Set α} :
MeasurableSet s → (Filter.principal s).IsMeasurablyGenerated

Alias of the reverse direction of `Filter.principal_isMeasurablyGenerated_iff`.

source
instance Filter.iInf_isMeasurablyGenerated {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] {f : ι → Filter α} [∀ (i : ι), (f i).IsMeasurablyGenerated] :
(⨅ (i : ι), f i).IsMeasurablyGenerated
source
theorem measurableSet_tendsto {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace β} [MeasurableSpace γ] [Countable δ] {l : Filter δ} [l.IsCountablyGenerated] (l' : Filter γ) [l'.IsCountablyGenerated] [hl' : l'.IsMeasurablyGenerated] {f : δ → β → γ} (hf : ∀ (i : δ), Measurable (f i)) :
MeasurableSet {x : β | Filter.Tendsto (fun (n : δ) => f n x) l l'}

The set of points for which a sequence of measurable functions converges to a given value is measurable.

source
theorem MeasurableSet.iUnion_of_monotone_of_frequently {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α} (hsm : Monotone s) (hs : ∃ᶠ (i : ι) in Filter.atTop, MeasurableSet (s i)) :
MeasurableSet (⋃ (i : ι), s i)
source
theorem MeasurableSet.iInter_of_antitone_of_frequently {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α} (hsm : Antitone s) (hs : ∃ᶠ (i : ι) in Filter.atTop, MeasurableSet (s i)) :
MeasurableSet (⋂ (i : ι), s i)
source
theorem MeasurableSet.iUnion_of_monotone {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α} (hsm : Monotone s) (hs : ∀ (i : ι), MeasurableSet (s i)) :
MeasurableSet (⋃ (i : ι), s i)
source
theorem MeasurableSet.iInter_of_antitone {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α} (hsm : Antitone s) (hs : ∀ (i : ι), MeasurableSet (s i)) :
MeasurableSet (⋂ (i : ι), s i)

### Typeclasses on `Subtype MeasurableSet` #

source
instance MeasurableSet.Subtype.instMembership {α : Type u_1} [MeasurableSpace α] :
Membership α (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instMembership = { mem := fun (s : Subtype MeasurableSet) (a : α) => a ∈ ↑s }

source
@[simp]
theorem MeasurableSet.mem_coe {α : Type u_1} [MeasurableSpace α] (a : α) (s : Subtype MeasurableSet) :
a ∈ ↑s ↔ a ∈ s
source
instance MeasurableSet.Subtype.instEmptyCollection {α : Type u_1} [MeasurableSpace α] :
EmptyCollection (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instEmptyCollection = { emptyCollection := ⟨∅, ⋯⟩ }

source
@[simp]
theorem MeasurableSet.coe_empty {α : Type u_1} [MeasurableSpace α] :
↑∅ = ∅
source
instance MeasurableSet.Subtype.instInsert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :
Insert α (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instInsert = { insert := fun (a : α) (s : Subtype MeasurableSet) => ⟨insert a ↑s, ⋯⟩ }

source
@[simp]
theorem MeasurableSet.coe_insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Subtype MeasurableSet) :
↑(insert a s) = insert a ↑s
source
instance MeasurableSet.Subtype.instSingleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :
Singleton α (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instSingleton = { singleton := fun (a : α) => ⟨{a}, ⋯⟩ }

source
@[simp]
theorem MeasurableSet.coe_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) :
↑{a} = {a}
source
instance MeasurableSet.Subtype.instLawfulSingleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :
LawfulSingleton α (Subtype MeasurableSet)
source
instance MeasurableSet.Subtype.instHasCompl {α : Type u_1} [MeasurableSpace α] :
HasCompl (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instHasCompl = { compl := fun (x : Subtype MeasurableSet) => ⟨(↑x)ᶜ, ⋯⟩ }

source
@[simp]
theorem MeasurableSet.coe_compl {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) :
↑s ᶜ = (↑s)ᶜ
source
instance MeasurableSet.Subtype.instUnion {α : Type u_1} [MeasurableSpace α] :
Union (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instUnion = { union := fun (x y : Subtype MeasurableSet) => ⟨↑x ∪ ↑y, ⋯⟩ }

source
@[simp]
theorem MeasurableSet.coe_union {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) :
↑(s ∪ t) = ↑s ∪ ↑t
source
instance MeasurableSet.Subtype.instSup {α : Type u_1} [MeasurableSpace α] :
Max (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instSup = { max := fun (x y : Subtype MeasurableSet) => x ∪ y }

source
@[simp]
theorem MeasurableSet.sup_eq_union {α : Type u_1} [MeasurableSpace α] (s t : { s : Set α // MeasurableSet s }) :
s ⊔ t = s ∪ t
source
instance MeasurableSet.Subtype.instInter {α : Type u_1} [MeasurableSpace α] :
Inter (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instInter = { inter := fun (x y : Subtype MeasurableSet) => ⟨↑x ∩ ↑y, ⋯⟩ }

source
@[simp]
theorem MeasurableSet.coe_inter {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) :
↑(s ∩ t) = ↑s ∩ ↑t
source
instance MeasurableSet.Subtype.instInf {α : Type u_1} [MeasurableSpace α] :
Min (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instInf = { min := fun (x y : Subtype MeasurableSet) => x ∩ y }

source
@[simp]
theorem MeasurableSet.inf_eq_inter {α : Type u_1} [MeasurableSpace α] (s t : { s : Set α // MeasurableSet s }) :
s ⊓ t = s ∩ t
source
instance MeasurableSet.Subtype.instSDiff {α : Type u_1} [MeasurableSpace α] :
SDiff (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instSDiff = { sdiff := fun (x y : Subtype MeasurableSet) => ⟨↑x \ ↑y, ⋯⟩ }

source
noncomputable instance MeasurableSet.Subtype.instHImp {α : Type u_1} [MeasurableSpace α] :
HImp (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instHImp = { himp := fun (x y : Subtype MeasurableSet) => ⟨↑x ⇨ ↑y, ⋯⟩ }

source
@[simp]
theorem MeasurableSet.coe_sdiff {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) :
↑(s \ t) = ↑s \ ↑t
source
@[simp]
theorem MeasurableSet.coe_himp {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) :
↑(s ⇨ t) = ↑s ⇨ ↑t
source
instance MeasurableSet.Subtype.instBot {α : Type u_1} [MeasurableSpace α] :
Bot (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instBot = { bot := ∅ }

source
@[simp]
theorem MeasurableSet.coe_bot {α : Type u_1} [MeasurableSpace α] :
↑⊥ = ⊥
source
instance MeasurableSet.Subtype.instTop {α : Type u_1} [MeasurableSpace α] :
Top (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instTop = { top := ⟨Set.univ, ⋯⟩ }

source
@[simp]
theorem MeasurableSet.coe_top {α : Type u_1} [MeasurableSpace α] :
↑⊤ = ⊤
source
noncomputable instance MeasurableSet.Subtype.instBooleanAlgebra {α : Type u_1} [MeasurableSpace α] :
BooleanAlgebra (Subtype MeasurableSet)
Equations

- MeasurableSet.Subtype.instBooleanAlgebra = Function.Injective.booleanAlgebra (fun (a : Subtype MeasurableSet) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source
theorem MeasurableSet.measurableSet_blimsup {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} {p : ℕ → Prop} (h : ∀ (n : ℕ), p n → MeasurableSet (s n)) :
MeasurableSet (Filter.blimsup s Filter.atTop p)
source
theorem MeasurableSet.measurableSet_bliminf {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} {p : ℕ → Prop} (h : ∀ (n : ℕ), p n → MeasurableSet (s n)) :
MeasurableSet (Filter.bliminf s Filter.atTop p)
source
theorem MeasurableSet.measurableSet_limsup {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) :
MeasurableSet (Filter.limsup s Filter.atTop)
source
theorem MeasurableSet.measurableSet_liminf {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) :
MeasurableSet (Filter.liminf s Filter.atTop)