feat(measure_theory/measurable_space): introduce filter.is_measurably_generated (#3594)

Sometimes I want to extract an `is_measurable` witness of a `filter.eventually` statement.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: urkud

src/measure_theory/borel_space.lean

@@ -34,7 +34,7 @@ import analysis.normed_space.basic
 noncomputable theory
 
 open classical set
-open_locale classical big_operators
+open_locale classical big_operators topological_space
 
 universes u v w x y
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort y} {s t u : set α}
@@ -205,6 +205,20 @@ h.is_closed.is_measurable
 lemma is_measurable_closure : is_measurable (closure s) :=
 is_closed_closure.is_measurable
 
+instance nhds_is_measurably_generated (a : α) : (𝓝 a).is_measurably_generated :=
+begin
+  rw [nhds, infi_subtype'],
+  refine @filter.infi_is_measurably_generated _ _ _ _ (λ i, _),
+  exact i.2.2.is_measurable.principal_is_measurably_generated
+end
+
+/-- If `s` is a measurable set, then `nhds_within a s` is a measurably generated filter for
+each `a`. This cannot be an `instance` because it depends on a non-instance `hs : is_measurable s`.
+-/
+lemma is_measurable.nhds_within_is_measurably_generated {s : set α} (hs : is_measurable s) (a : α) :
+  (nhds_within a s).is_measurably_generated :=
+by haveI := hs.principal_is_measurably_generated; exact filter.inf_is_measurably_generated _ _
+
 @[priority 100] -- see Note [lower instance priority]
 instance opens_measurable_space.to_measurable_singleton_class [t1_space α] :
   measurable_singleton_class α :=
@@ -217,6 +231,14 @@ lemma is_measurable_Ici : is_measurable (Ici a) := is_closed_Ici.is_measurable
 lemma is_measurable_Iic : is_measurable (Iic a) := is_closed_Iic.is_measurable
 lemma is_measurable_Icc : is_measurable (Icc a b) := is_closed_Icc.is_measurable
 
+instance at_top_is_measurably_generated : (filter.at_top : filter α).is_measurably_generated :=
+@filter.infi_is_measurably_generated _ _ _ _ $
+  λ a, (is_measurable_Ici : is_measurable (Ici a)).principal_is_measurably_generated
+
+instance at_bot_is_measurably_generated : (filter.at_bot : filter α).is_measurably_generated :=
+@filter.infi_is_measurably_generated _ _ _ _ $
+  λ a, (is_measurable_Iic : is_measurable (Iic a)).principal_is_measurably_generated
+
 end order_closed_topology
 
 section order_closed_topology

src/measure_theory/measurable_space.lean

@@ -7,6 +7,7 @@ import data.set.disjointed
 import data.set.countable
 import data.indicator_function
 import data.equiv.encodable.lattice
+import order.filter.basic
 
 /-!
 # Measurable spaces and measurable functions
@@ -30,6 +31,9 @@ A measurable equivalence between measurable spaces is an equivalence
 which respects the σ-algebras, that is, for which both directions of
 the equivalence are measurable functions.
 
+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`.
+
 ## Main statements
 
 The main theorem of this file is Dynkin's π-λ theorem, which appears
@@ -59,7 +63,7 @@ measurable space, measurable function, dynkin system
 
 local attribute [instance] classical.prop_decidable
 open set encodable
-open_locale classical
+open_locale classical filter
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort x}
@@ -1075,3 +1079,58 @@ this.rec_on h_basic h_empty
   (assume f hf ht, h_union f hf $ assume i, by rw [eq]; exact ht _)
 
 end measurable_space
+
+namespace filter
+
+variables [measurable_space α]
+
+/-- A filter `f` is measurably generates if each `s ∈ f` includes a measurable `t ∈ f`. -/
+class is_measurably_generated (f : filter α) : Prop :=
+(exists_measurable_subset : ∀ ⦃s⦄, s ∈ f → ∃ t ∈ f, is_measurable t ∧ t ⊆ s)
+
+lemma eventually.exists_measurable_mem {f : filter α} [is_measurably_generated f]
+  {p : α → Prop} (h : ∀ᶠ x in f, p x) :
+  ∃ s ∈ f, is_measurable s ∧ ∀ x ∈ s, p x :=
+is_measurably_generated.exists_measurable_subset h
+
+instance inf_is_measurably_generated (f g : filter α) [is_measurably_generated f]
+  [is_measurably_generated g] :
+  is_measurably_generated (f ⊓ g) :=
+begin
+  refine ⟨_⟩,
+  rintros t ⟨sf, hsf, sg, hsg, ht⟩,
+  rcases is_measurably_generated.exists_measurable_subset hsf with ⟨s'f, hs'f, hmf, hs'sf⟩,
+  rcases is_measurably_generated.exists_measurable_subset hsg with ⟨s'g, hs'g, hmg, hs'sg⟩,
+  refine ⟨s'f ∩ s'g, inter_mem_inf_sets hs'f hs'g, hmf.inter hmg, _⟩,
+  exact subset.trans (inter_subset_inter hs'sf hs'sg) ht
+end
+
+lemma principal_is_measurably_generated_iff {s : set α} :
+  is_measurably_generated (𝓟 s) ↔ is_measurable s :=
+begin
+  refine ⟨_, λ hs, ⟨λ t ht, ⟨s, mem_principal_self s, hs, ht⟩⟩⟩,
+  rintros ⟨hs⟩,
+  rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩,
+  have : t = s := subset.antisymm hts ht,
+  rwa ← this
+end
+
+alias principal_is_measurably_generated_iff ↔
+  _ is_measurable.principal_is_measurably_generated
+
+instance infi_is_measurably_generated {f : ι → filter α} [∀ i, is_measurably_generated (f i)] :
+  is_measurably_generated (⨅ i, f i) :=
+begin
+  refine ⟨λ s hs, _⟩,
+  rw [← equiv.plift.surjective.infi_comp, mem_infi_iff] at hs,
+  rcases hs with ⟨t, ht, ⟨V, hVf, hVs⟩⟩,
+  choose U hUf hU using λ i, is_measurably_generated.exists_measurable_subset (hVf i),
+  refine ⟨⋂ i : t, U i, _, _, _⟩,
+  { rw [← equiv.plift.surjective.infi_comp, mem_infi_iff],
+    refine ⟨t, ht, U, hUf, subset.refl _⟩ },
+  { haveI := ht.countable.to_encodable,
+    refine is_measurable.Inter (λ i, (hU i).1) },
+  { exact subset.trans (Inter_subset_Inter $ λ i, (hU i).2) hVs }
+end
+
+end filter

src/measure_theory/measure_space.lean

@@ -1109,6 +1109,10 @@ instance : countable_Inter_filter μ.ae :=
   exact measure_Union_null (subtype.forall.2 hS)
 end⟩
 
+instance ae_is_measurably_generated : is_measurably_generated μ.ae :=
+⟨λ s hs, let ⟨t, hst, htm, htμ⟩ := exists_is_measurable_superset_of_measure_eq_zero hs in
+  ⟨tᶜ, compl_mem_ae_iff.2 htμ, htm.compl, compl_subset_comm.1 hst⟩⟩
+
 lemma ae_all_iff {ι : Type*} [encodable ι] {p : α → ι → Prop} :
   (∀ᵐ a ∂ μ, ∀i, p a i) ↔ (∀i, ∀ᵐ a ∂ μ, p a i) :=
 eventually_countable_forall