feat(measure_theory): generalize null_of_locally_null to `outer_mea…

…sure`, add versions (#11535)

* generalize `null_of_locally_null`;
* don't intersect with `s` twice;
* add a contraposed version;
* golf.

src/measure_theory/covering/differentiation.lean

@@ -200,7 +200,7 @@ begin
   apply null_of_locally_null s (λ x hx, _),
   obtain ⟨o, xo, o_open, μo⟩ : ∃ o : set α, x ∈ o ∧ is_open o ∧ μ o < ∞ :=
     measure.exists_is_open_measure_lt_top μ x,
-  refine ⟨o, mem_nhds_within_of_mem_nhds (o_open.mem_nhds xo), _⟩,
+  refine ⟨s ∩ o, inter_mem_nhds_within _ (o_open.mem_nhds xo), _⟩,
   let s' := s ∩ o,
   by_contra,
   apply lt_irrefl (ρ s'),
@@ -474,8 +474,8 @@ begin
   refine null_of_locally_null _ (λ x hx, _),
   obtain ⟨o, xo, o_open, μo⟩ : ∃ o : set α, x ∈ o ∧ is_open o ∧ ρ o < ∞ :=
     measure.exists_is_open_measure_lt_top ρ x,
-  refine ⟨o, mem_nhds_within_of_mem_nhds (o_open.mem_nhds xo), le_antisymm _ bot_le⟩,
   let s := {x : α | v.lim_ratio_meas hρ x = ∞} ∩ o,
+  refine ⟨s, inter_mem_nhds_within _ (o_open.mem_nhds xo), le_antisymm _ bot_le⟩,
   have ρs : ρ s ≠ ∞ := ((measure_mono (inter_subset_right _ _)).trans_lt μo).ne,
   have A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ q⁻¹ * ρ s,
   { assume q hq,
@@ -500,8 +500,8 @@ begin
   refine null_of_locally_null _ (λ x hx, _),
   obtain ⟨o, xo, o_open, μo⟩ : ∃ o : set α, x ∈ o ∧ is_open o ∧ μ o < ∞ :=
     measure.exists_is_open_measure_lt_top μ x,
-  refine ⟨o, mem_nhds_within_of_mem_nhds (o_open.mem_nhds xo), le_antisymm _ bot_le⟩,
   let s := {x : α | v.lim_ratio_meas hρ x = 0} ∩ o,
+  refine ⟨s, inter_mem_nhds_within _ (o_open.mem_nhds xo), le_antisymm _ bot_le⟩,
   have μs : μ s ≠ ∞ := ((measure_mono (inter_subset_right _ _)).trans_lt μo).ne,
   have A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ q * μ s,
   { assume q hq,

src/measure_theory/covering/vitali.lean

@@ -274,7 +274,7 @@ begin
       calc 20 * min 1 (R / 20) ≤ 20 * (R/20) :
         mul_le_mul_of_nonneg_left (min_le_right _ _) (by norm_num)
       ... = R : by ring } },
-  choose r hr using this,
+  choose r hr0 hr1 hrμ,
   -- we restrict to a subfamily `t'` of `t`, made of elements small enough to ensure that
   -- they only see a finite part of the measure.
   let t' := {a ∈ t | ∃ x, a ⊆ closed_ball x (r x)},
@@ -283,10 +283,9 @@ begin
     ∀ a ∈ t', ∃ b ∈ u, set.nonempty (a ∩ b) ∧ diam a ≤ 2 * diam b,
   { have A : ∀ (a : set α), a ∈ t' → diam a ≤ 2,
     { rintros a ⟨hat, ⟨x, hax⟩⟩,
-      calc diam a ≤ diam (closed_ball x (r x)) : diam_mono hax bounded_closed_ball
-      ... ≤ 2 * r x : diam_closed_ball (hr x).1.le
-      ... ≤ 2 * 1 : mul_le_mul_of_nonneg_left (hr x).2.1 zero_le_two
-      ... = 2 : by norm_num },
+      calc diam a ≤ 2 * 1 : diam_le_of_subset_closed_ball zero_le_one
+        (hax.trans $ closed_ball_subset_closed_ball $ hr1 x)
+      ... = 2 : mul_one _ },
     have B : ∀ (a : set α), a ∈ t' → a.nonempty :=
       λ a hat', set.nonempty.mono interior_subset (ht a hat'.1),
     exact exists_disjoint_subfamily_covering_enlargment t' diam 2 one_lt_two
@@ -316,14 +315,14 @@ begin
     have R0_bdd : bdd_above ((λ a, r (y a)) '' v),
     { refine ⟨1, λ r' hr', _⟩,
       rcases (mem_image _ _ _).1 hr' with ⟨b, hb, rfl⟩,
-      exact (hr _).2.1 },
+      exact hr1 _ },
     rcases le_total R0 (r x) with H|H,
-    { refine ⟨20 * r x, (hr x).2.2, λ a au hax, _⟩,
+    { refine ⟨20 * r x, hrμ x, λ a au hax, _⟩,
       refine (hy a au).trans _,
       apply closed_ball_subset_closed_ball',
       have : r (y a) ≤ R0 := le_cSup R0_bdd (mem_image_of_mem _ ⟨au, hax⟩),
-      linarith [(hr (y a)).1.le, (hr x).1.le, Idist_v a ⟨au, hax⟩] },
-    { have R0pos : 0 < R0 := (hr x).1.trans_le H,
+      linarith [(hr0 (y a)).le, (hr0 x).le, Idist_v a ⟨au, hax⟩] },
+    { have R0pos : 0 < R0 := (hr0 x).trans_le H,
       have vnonempty : v.nonempty,
       { by_contra,
         rw [← ne_empty_iff_nonempty, not_not] at h,
@@ -335,7 +334,7 @@ begin
         rcases (mem_image _ _ _).1 r'mem with ⟨a, hav, rfl⟩,
         exact ⟨a, hav, hr'⟩ },
       refine ⟨8 * R0, _, _⟩,
-      { apply lt_of_le_of_lt (measure_mono _) (hr (y a)).2.2,
+      { apply lt_of_le_of_lt (measure_mono _) (hrμ (y a)),
         apply closed_ball_subset_closed_ball',
         rw dist_comm,
         linarith [Idist_v a hav] },
@@ -345,9 +344,8 @@ begin
         have : r (y b) ≤ R0 := le_cSup R0_bdd (mem_image_of_mem _ ⟨bu, hbx⟩),
         linarith [Idist_v b ⟨bu, hbx⟩] } } },
   -- we will show that, in `ball x (r x)`, almost all `s` is covered by the family `u`.
-  refine ⟨ball x (r x), _, le_antisymm (le_of_forall_le_of_dense (λ ε εpos, _)) bot_le⟩,
-  { apply mem_nhds_within_of_mem_nhds (is_open_ball.mem_nhds _),
-    simp only [(hr x).left, mem_ball, dist_self] },
+  refine ⟨_ ∩ ball x (r x), inter_mem_nhds_within _ (ball_mem_nhds _ (hr0 _)),
+    nonpos_iff_eq_zero.mp (le_of_forall_le_of_dense (λ ε εpos, _))⟩,
   -- the elements of `v` are disjoint and all contained in a finite volume ball, hence the sum
   -- of their measures is finite.
   have I : ∑' (a : v), μ a < ∞,

src/measure_theory/measure/measure_space.lean

@@ -89,6 +89,7 @@ measure, almost everywhere, measure space, completion, null set, null measurable
 noncomputable theory
 
 open classical set filter (hiding map) function measurable_space
+  topological_space (second_countable_topology)
 open_locale classical topological_space big_operators filter ennreal nnreal
 
 variables {α β γ δ ι : Type*}
@@ -2294,7 +2295,7 @@ omit m0
 
 @[priority 100] -- see Note [lower instance priority]
 instance sigma_finite_of_locally_finite [topological_space α]
-  [topological_space.second_countable_topology α] [is_locally_finite_measure μ] :
+  [second_countable_topology α] [is_locally_finite_measure μ] :
   sigma_finite μ :=
 begin
   choose s hsx hsμ using μ.finite_at_nhds,
@@ -2305,17 +2306,30 @@ end
 
 /-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
 in a second-countable space. -/
-lemma null_of_locally_null [topological_space α] [topological_space.second_countable_topology α]
-  (s : set α) (hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ (s ∩ u) = 0) :
+lemma null_of_locally_null [topological_space α] [second_countable_topology α]
+  (s : set α) (hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0) :
   μ s = 0 :=
-begin
-  choose! u hu using hs,
-  obtain ⟨t, ts, t_count, ht⟩ : ∃ t ⊆ s, t.countable ∧ s ⊆ ⋃ x ∈ t, u x :=
-    topological_space.countable_cover_nhds_within (λ x hx, (hu x hx).1),
-  replace ht : s ⊆ ⋃ x ∈ t, s ∩ u x,
-    by { rw ← inter_bUnion, exact subset_inter (subset.refl _) ht },
-  apply measure_mono_null ht,
-  exact (measure_bUnion_null_iff t_count).2 (λ x hx, (hu x (ts hx)).2),
+μ.to_outer_measure.null_of_locally_null s hs
+
+lemma exists_mem_forall_mem_nhds_within_pos_measure [topological_space α]
+  [second_countable_topology α] {s : set α} (hs : μ s ≠ 0) :
+  ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < μ t :=
+μ.to_outer_measure.exists_mem_forall_mem_nhds_within_pos hs
+
+lemma exists_ne_forall_mem_nhds_pos_measure_preimage {β} [topological_space β] [t1_space β]
+  [second_countable_topology β] [nonempty β] {f : α → β} (h : ∀ b, ∃ᵐ x ∂μ, f x ≠ b) :
+  ∃ a b : β, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ (∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)) :=
+begin
+  -- We use an `outer_measure` so that the proof works without `measurable f`
+  set m : outer_measure β := outer_measure.map f μ.to_outer_measure,
+  replace h : ∀ b : β, m {b}ᶜ ≠ 0 := λ b, not_eventually.mpr (h b),
+  inhabit β,
+  have : m univ ≠ 0, from ne_bot_of_le_ne_bot (h default) (m.mono' $ subset_univ _),
+  rcases m.exists_mem_forall_mem_nhds_within_pos this with ⟨b, -, hb⟩,
+  simp only [nhds_within_univ] at hb,
+  rcases m.exists_mem_forall_mem_nhds_within_pos (h b) with ⟨a, hab : a ≠ b, ha⟩,
+  simp only [is_open_compl_singleton.nhds_within_eq hab] at ha,
+  exact ⟨a, b, hab, ha, hb⟩
 end
 
 /-- If two finite measures give the same mass to the whole space and coincide on a π-system made

src/measure_theory/measure/outer_measure.lean

@@ -52,7 +52,7 @@ outer measure, Carathéodory-measurable, Carathéodory's criterion
 
 noncomputable theory
 
-open set finset function filter encodable
+open set finset function filter encodable topological_space (second_countable_topology)
 open_locale classical big_operators nnreal topological_space ennreal
 
 namespace measure_theory
@@ -111,6 +111,29 @@ protected lemma union (m : outer_measure α) (s₁ s₂ : set α) :
   m (s₁ ∪ s₂) ≤ m s₁ + m s₂ :=
 rel_sup_add m m.empty (≤) m.Union_nat s₁ s₂
 
+/-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
+in a second-countable space. -/
+lemma null_of_locally_null [topological_space α] [second_countable_topology α] (m : outer_measure α)
+  (s : set α) (hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, m u = 0) :
+  m s = 0 :=
+begin
+  choose! u hxu hu₀ using hs,
+  obtain ⟨t, ts, t_count, ht⟩ : ∃ t ⊆ s, t.countable ∧ s ⊆ ⋃ x ∈ t, u x :=
+    topological_space.countable_cover_nhds_within hxu,
+  apply m.mono_null ht,
+  exact (m.bUnion_null_iff t_count).2 (λ x hx, hu₀ x (ts hx))
+end
+
+/-- If `m s ≠ 0`, then for some point `x ∈ s` and any `t ∈ 𝓝[s] x` we have `0 < m t`. -/
+lemma exists_mem_forall_mem_nhds_within_pos [topological_space α] [second_countable_topology α]
+  (m : outer_measure α) {s : set α} (hs : m s ≠ 0) :
+  ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < m t :=
+begin
+  contrapose! hs,
+  simp only [nonpos_iff_eq_zero, ← exists_prop] at hs,
+  exact m.null_of_locally_null s hs
+end
+
 /-- If `s : ι → set α` is a sequence of sets, `S = ⋃ n, s n`, and `m (S \ s n)` tends to zero along
 some nontrivial filter (usually `at_top` on `ι = ℕ`), then `m S = ⨆ n, m (s n)`. -/
 lemma Union_of_tendsto_zero {ι} (m : outer_measure α) {s : ι → set α}

src/topology/metric_space/basic.lean

@@ -2031,16 +2031,20 @@ begin
   simpa using diam_union xs xt
 end
 
-/-- The diameter of a closed ball of radius `r` is at most `2 r`. -/
-lemma diam_closed_ball {r : ℝ} (h : 0 ≤ r) : diam (closed_ball x r) ≤ 2 * r :=
-diam_le_of_forall_dist_le (mul_nonneg (le_of_lt zero_lt_two) h) $ λa ha b hb, calc
+lemma diam_le_of_subset_closed_ball {r : ℝ} (hr : 0 ≤ r) (h : s ⊆ closed_ball x r) :
+  diam s ≤ 2 * r :=
+diam_le_of_forall_dist_le (mul_nonneg zero_le_two hr) $ λa ha b hb, calc
   dist a b ≤ dist a x + dist b x : dist_triangle_right _ _ _
-  ... ≤ r + r : add_le_add ha hb
+  ... ≤ r + r : add_le_add (h ha) (h hb)
   ... = 2 * r : by simp [mul_two, mul_comm]
 
+/-- The diameter of a closed ball of radius `r` is at most `2 r`. -/
+lemma diam_closed_ball {r : ℝ} (h : 0 ≤ r) : diam (closed_ball x r) ≤ 2 * r :=
+diam_le_of_subset_closed_ball h subset.rfl
+
 /-- The diameter of a ball of radius `r` is at most `2 r`. -/
 lemma diam_ball {r : ℝ} (h : 0 ≤ r) : diam (ball x r) ≤ 2 * r :=
-le_trans (diam_mono ball_subset_closed_ball bounded_closed_ball) (diam_closed_ball h)
+diam_le_of_subset_closed_ball h ball_subset_closed_ball
 
 end diam