feat(measure_theory/function/strongly_measurable): more basic propert…

…ies of `strongly_measurable` (#12164)

src/algebra/support.lean

@@ -204,6 +204,11 @@ lemma support_smul [semiring R] [add_comm_monoid M] [module R M]
   support (f • g) = support f ∩ support g :=
 ext $ λ x, smul_ne_zero
 
+lemma support_const_smul_of_ne_zero [semiring R] [add_comm_monoid M] [module R M]
+  [no_zero_smul_divisors R M] (c : R) (g : α → M) (hc : c ≠ 0) :
+  support (c • g) = support g :=
+ext $ λ x, by simp only [hc, mem_support, pi.smul_apply, ne.def, smul_eq_zero, false_or]
+
 @[simp] lemma support_inv [group_with_zero G₀] (f : α → G₀) :
   support (λ x, (f x)⁻¹) = support f :=
 set.ext $ λ x, not_congr inv_eq_zero

src/measure_theory/constructions/borel_space.lean

@@ -1764,18 +1764,34 @@ variables [measurable_space β] [metric_space β] [borel_space β]
 
 open metric
 
-/-- A limit (over a general filter) of measurable `ℝ≥0` valued functions is measurable. -/
-lemma measurable_of_tendsto_nnreal' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : filter ι)
+/-- A limit (over a general filter) of measurable `ℝ≥0∞` valued functions is measurable. -/
+lemma measurable_of_tendsto_ennreal' {ι} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} (u : filter ι)
   [ne_bot u] [is_countably_generated u] (hf : ∀ i, measurable (f i)) (lim : tendsto f u (𝓝 g)) :
   measurable g :=
 begin
   rcases u.exists_seq_tendsto with ⟨x, hx⟩,
-  rw [tendsto_pi_nhds] at lim, rw [← measurable_coe_nnreal_ennreal_iff],
-  have : ∀ y, liminf at_top (λ n, (f (x n) y : ℝ≥0∞)) = (g y : ℝ≥0∞) :=
-    λ y, ((ennreal.continuous_coe.tendsto (g y)).comp $ (lim y).comp hx).liminf_eq,
-  simp only [← this],
+  rw [tendsto_pi_nhds] at lim,
+  have : (λ y, liminf at_top (λ n, (f (x n) y : ℝ≥0∞))) = g :=
+    by { ext1 y, exact ((lim y).comp hx).liminf_eq, },
+  rw ← this,
   show measurable (λ y, liminf at_top (λ n, (f (x n) y : ℝ≥0∞))),
-  exact measurable_liminf (λ n, (hf (x n)).coe_nnreal_ennreal),
+  exact measurable_liminf (λ n, hf (x n)),
+end
+
+/-- A sequential limit of measurable `ℝ≥0∞` valued functions is measurable. -/
+lemma measurable_of_tendsto_ennreal {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞}
+  (hf : ∀ i, measurable (f i)) (lim : tendsto f at_top (𝓝 g)) : measurable g :=
+measurable_of_tendsto_ennreal' at_top hf lim
+
+/-- A limit (over a general filter) of measurable `ℝ≥0` valued functions is measurable. -/
+lemma measurable_of_tendsto_nnreal' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : filter ι)
+  [ne_bot u] [is_countably_generated u] (hf : ∀ i, measurable (f i)) (lim : tendsto f u (𝓝 g)) :
+  measurable g :=
+begin
+  simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢,
+  refine measurable_of_tendsto_ennreal' u hf _,
+  rw tendsto_pi_nhds at lim ⊢,
+  exact λ x, (ennreal.continuous_coe.tendsto (g x)).comp (lim x),
 end
 
 /-- A sequential limit of measurable `ℝ≥0` valued functions is measurable. -/