feat(measure_theory/*): a few lemmas about (is_)measurable in `Π i,…

… π i` (#4948)

src/measure_theory/borel_space.lean

@@ -221,10 +221,29 @@ instance opens_measurable_space.to_measurable_singleton_class [t1_space α] :
   measurable_singleton_class α :=
 ⟨λ x, is_closed_singleton.is_measurable⟩
 
+instance pi.opens_measurable_space {ι : Type*} {π : ι → Type*} [fintype ι]
+  [t' : Π i, topological_space (π i)]
+  [Π i, measurable_space (π i)] [∀ i, second_countable_topology (π i)]
+  [∀ i, opens_measurable_space (π i)] :
+  opens_measurable_space (Π i, π i) :=
+begin
+  constructor,
+  choose g hc he ho hu hinst using λ i, is_open_generated_countable_inter (π i),
+  have : Pi.topological_space =
+    generate_from {t | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, s a ∈ g a) ∧ t = pi ↑i s},
+  { rw [funext hinst, pi_generate_from_eq] },
+  rw [borel_eq_generate_from_of_subbasis this],
+  apply generate_from_le,
+  rintros _ ⟨s, i, hi, rfl⟩,
+  refine is_measurable_pi i.countable_to_set (λ a ha, is_open.is_measurable _),
+  rw [hinst], 
+  exact generate_open.basic _ (hi a ha)
+end
+
 instance prod.opens_measurable_space [second_countable_topology α] [second_countable_topology β] :
   opens_measurable_space (α × β) :=
 begin
-  refine ⟨_⟩,
+  constructor,
   rcases is_open_generated_countable_inter α with ⟨a, ha₁, ha₂, ha₃, ha₄, ha₅⟩,
   rcases is_open_generated_countable_inter β with ⟨b, hb₁, hb₂, hb₃, hb₄, hb₅⟩,
   have : prod.topological_space = generate_from {g | ∃u∈a, ∃v∈b, g = set.prod u v},
@@ -392,6 +411,16 @@ variables [topological_space α] [measurable_space α] [borel_space α]
   [topological_space γ] [measurable_space γ] [borel_space γ]
   [measurable_space δ]
 
+lemma pi_le_borel_pi {ι : Type*} {π : ι → Type*} [Π i, topological_space (π i)]
+  [Π i, measurable_space (π i)] [∀ i, borel_space (π i)] :
+  measurable_space.pi ≤ borel (Π i, π i) :=
+begin
+  have : ‹Π i, measurable_space (π i)› = λ i, borel (π i) :=
+    funext (λ i, borel_space.measurable_eq),
+  rw [this],
+  exact supr_le (λ i, comap_le_iff_le_map.2 $ (continuous_apply i).borel_measurable)
+end
+
 lemma prod_le_borel_prod : prod.measurable_space ≤ borel (α × β) :=
 begin
   rw [‹borel_space α›.measurable_eq, ‹borel_space β›.measurable_eq],
@@ -400,6 +429,13 @@ begin
   { exact comap_le_iff_le_map.mpr continuous_snd.borel_measurable }
 end
 
+instance pi.borel_space {ι : Type*} {π : ι → Type*} [fintype ι]
+  [t' : Π i, topological_space (π i)]
+  [Π i, measurable_space (π i)] [∀ i, second_countable_topology (π i)]
+  [∀ i, borel_space (π i)] :
+  borel_space (Π i, π i) :=
+⟨le_antisymm pi_le_borel_pi opens_measurable_space.borel_le⟩
+
 instance prod.borel_space [second_countable_topology α] [second_countable_topology β] :
   borel_space (α × β) :=
 ⟨le_antisymm prod_le_borel_prod opens_measurable_space.borel_le⟩

src/measure_theory/measurable_space.lean

@@ -350,19 +350,14 @@ iff.refl _
 
 theorem is_measurable_Sup {ms : set (measurable_space α)} {s : set α} :
   @is_measurable _ (Sup ms) s ↔
-    generate_measurable (⋃₀ (measurable_space.is_measurable' '' ms)) s :=
+    generate_measurable {s : set α | ∃ m ∈ ms, @is_measurable _ m s} s :=
 begin
-  change @is_measurable' _ (generate_from _) _ ↔ _,
-  dsimp [generate_from],
-  rw (show (⨆ (b : measurable_space α) (H : b ∈ ms), set_of (@is_measurable _ b)) =
-    (⋃₀ (is_measurable' '' ms)),
-  { ext,
-    simp only [exists_prop, mem_Union, sUnion_image, mem_set_of_eq],
-    refl, })
+  change @is_measurable' _ (generate_from $ ⋃ m ∈ ms, _) _ ↔ _,
+  simp [generate_from, ← set_of_exists]
 end
 
 theorem is_measurable_supr {ι} {m : ι → measurable_space α} {s : set α} :
-  @is_measurable _ (supr m) s ↔ generate_measurable (⋃ i, (m i).is_measurable') s :=
+  @is_measurable _ (supr m) s ↔ generate_measurable {s : set α | ∃ i, @is_measurable _ (m i) s} s :=
 begin
   convert @is_measurable_Sup _ (range m) s,
   simp,
@@ -713,6 +708,14 @@ lemma measurable_pi_lambda (f : α → Π a, π a) (hf : ∀ a, measurable (λ c
   measurable f :=
 measurable.of_le_map $ supr_le $ assume a, measurable_space.comap_le_iff_le_map.2 (hf a)
 
+lemma is_measurable_pi {s : set δ} {t : Π i : δ, set (π i)} (hs : countable s)
+  (ht : ∀ i ∈ s, is_measurable (t i)) :
+  is_measurable (s.pi t) :=
+begin
+  rw [pi_def],
+  exact is_measurable.bInter hs (λ i hi, measurable_pi_apply _ (ht i hi))
+end
+
 end pi
 
 instance {α β} [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α ⊕ β) :=

src/measure_theory/measure_space.lean

@@ -1338,17 +1338,13 @@ lemma eventually_eq_dirac' [measurable_singleton_class α] {a : α} (f : α →
   f =ᵐ[dirac a] const α (f a) :=
 by { rw [dirac_ae_eq], show f a = f a, refl }
 
-lemma measure_diff_of_ae_le {s t : set α} (H : s ≤ᵐ[μ] t) :
-  μ (s \ t) = 0 :=
-flip measure_mono_null H $ λ x hx H, hx.2 (H hx.1)
-
 /-- If `s ⊆ t` modulo a set of measure `0`, then `μ s ≤ μ t`. -/
 lemma measure_mono_ae {s t : set α} (H : s ≤ᵐ[μ] t) :
   μ s ≤ μ t :=
 calc μ s ≤ μ (s ∪ t)       : measure_mono $ subset_union_left s t
      ... = μ (t ∪ s \ t)   : by rw [union_diff_self, set.union_comm]
      ... ≤ μ t + μ (s \ t) : measure_union_le _ _
-     ... = μ t             : by rw [measure_diff_of_ae_le H, add_zero]
+     ... = μ t             : by rw [ae_le_set.1 H, add_zero]
 
 alias measure_mono_ae ← filter.eventually_le.measure_le