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.

@[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}.

theorem MeasurableSpace.generateFrom_singleton_le {α : Type u_1} {m : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) : generateFrom {s} ≤ m

theorem MeasureTheory.measurableSet_generateFrom_singleton_iff {α : Type u_1} {s t : Set α} : MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = Set.univ

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

instance Filter.isMeasurablyGenerated_bot {α : Type u_1} [MeasurableSpace α] : ⊥.IsMeasurablyGenerated

instance Filter.isMeasurablyGenerated_top {α : Type u_1} [MeasurableSpace α] : ⊤.IsMeasurablyGenerated

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

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

instance Filter.inf_isMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] (f g : Filter α) [f.IsMeasurablyGenerated] [g.IsMeasurablyGenerated] : (f ⊓ g).IsMeasurablyGenerated

theorem Filter.principal_isMeasurablyGenerated_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} : (principal s).IsMeasurablyGenerated ↔ MeasurableSet s

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.

instance Filter.iInf_isMeasurablyGenerated {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] {f : ι → Filter α} [∀ (i : ι), (f i).IsMeasurablyGenerated] : (⨅ (i : ι), f i).IsMeasurablyGenerated

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.

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)

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)

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)

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

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

Equations

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

@[simp]

theorem MeasurableSet.mem_coe {α : Type u_1} [MeasurableSpace α] (a : α) (s : Subtype MeasurableSet) : a ∈ ↑s ↔ a ∈ s

instance MeasurableSet.Subtype.instEmptyCollection {α : Type u_1} [MeasurableSpace α] : EmptyCollection (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.coe_empty {α : Type u_1} [MeasurableSpace α] : ↑∅ = ∅

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, ⋯⟩ }

@[simp]

theorem MeasurableSet.coe_insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Subtype MeasurableSet) : ↑(insert a s) = insert a ↑s

instance MeasurableSet.Subtype.instSingleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] : Singleton α (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.coe_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) : ↑{a} = {a}

instance MeasurableSet.Subtype.instLawfulSingleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] : LawfulSingleton α (Subtype MeasurableSet)

instance MeasurableSet.Subtype.instHasCompl {α : Type u_1} [MeasurableSpace α] : HasCompl (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.coe_compl {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) : ↑sᶜ = (↑s)ᶜ

instance MeasurableSet.Subtype.instUnion {α : Type u_1} [MeasurableSpace α] : Union (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.coe_union {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) : ↑(s ∪ t) = ↑s ∪ ↑t

instance MeasurableSet.Subtype.instSup {α : Type u_1} [MeasurableSpace α] : Max (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.sup_eq_union {α : Type u_1} [MeasurableSpace α] (s t : { s : Set α // MeasurableSet s }) : s ⊔ t = s ∪ t

instance MeasurableSet.Subtype.instInter {α : Type u_1} [MeasurableSpace α] : Inter (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.coe_inter {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) : ↑(s ∩ t) = ↑s ∩ ↑t

instance MeasurableSet.Subtype.instInf {α : Type u_1} [MeasurableSpace α] : Min (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.inf_eq_inter {α : Type u_1} [MeasurableSpace α] (s t : { s : Set α // MeasurableSet s }) : s ⊓ t = s ∩ t

instance MeasurableSet.Subtype.instSDiff {α : Type u_1} [MeasurableSpace α] : SDiff (Subtype MeasurableSet)

Equations

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

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

Equations

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

@[simp]

theorem MeasurableSet.coe_sdiff {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) : ↑(s \ t) = ↑s \ ↑t

@[simp]

theorem MeasurableSet.coe_himp {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) : ↑(s ⇨ t) = ↑s ⇨ ↑t

instance MeasurableSet.Subtype.instBot {α : Type u_1} [MeasurableSpace α] : Bot (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.coe_bot {α : Type u_1} [MeasurableSpace α] : ↑⊥ = ⊥

instance MeasurableSet.Subtype.instTop {α : Type u_1} [MeasurableSpace α] : Top (Subtype MeasurableSet)

Equations

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

@[simp]

theorem MeasurableSet.coe_top {α : Type u_1} [MeasurableSpace α] : ↑⊤ = ⊤

noncomputable instance MeasurableSet.Subtype.instBooleanAlgebra {α : Type u_1} [MeasurableSpace α] : BooleanAlgebra (Subtype MeasurableSet)

Equations

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

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)

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)

theorem MeasurableSet.measurableSet_limsup {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) : MeasurableSet (Filter.limsup s Filter.atTop)

theorem MeasurableSet.measurableSet_liminf {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) : MeasurableSet (Filter.liminf s Filter.atTop)