[Merged by Bors] - feat(measure_theory/covering) weaken sigma_compact_space to second_countable_topology

src/measure_theory/covering/besicovitch.lean

@@ -1109,7 +1109,7 @@ begin
   { exact closed_ball_subset_closed_ball hr.2 }
 end
 
-variables [metric_space β] [measurable_space β] [borel_space β] [sigma_compact_space β]
+variables [metric_space β] [measurable_space β] [borel_space β] [second_countable_topology β]
   [has_besicovitch_covering β]
 
 /-- In a space with the Besicovitch covering property, the ratio of the measure of balls converges
@@ -1119,7 +1119,6 @@ lemma ae_tendsto_rn_deriv
   ∀ᵐ x ∂μ, tendsto (λ r, ρ (closed_ball x r) / μ (closed_ball x r))
     (𝓝[>] 0) (𝓝 (ρ.rn_deriv μ x)) :=
 begin
-  haveI : second_countable_topology β := emetric.second_countable_of_sigma_compact β,
   filter_upwards [vitali_family.ae_tendsto_rn_deriv (besicovitch.vitali_family μ) ρ] with x hx,
   exact hx.comp (tendsto_filter_at μ x)
 end
@@ -1134,7 +1133,6 @@ lemma ae_tendsto_measure_inter_div_of_measurable_set
   ∀ᵐ x ∂μ, tendsto (λ r, μ (s ∩ closed_ball x r) / μ (closed_ball x r))
     (𝓝[>] 0) (𝓝 (s.indicator 1 x)) :=
 begin
-  haveI : second_countable_topology β := emetric.second_countable_of_sigma_compact β,
   filter_upwards [vitali_family.ae_tendsto_measure_inter_div_of_measurable_set
     (besicovitch.vitali_family μ) hs],
   assume x hx,
@@ -1150,10 +1148,7 @@ See also `is_doubling_measure.ae_tendsto_measure_inter_div`. -/
 lemma ae_tendsto_measure_inter_div (μ : measure β) [is_locally_finite_measure μ] (s : set β) :
   ∀ᵐ x ∂(μ.restrict s), tendsto (λ r, μ (s ∩ (closed_ball x r)) / μ (closed_ball x r))
     (𝓝[>] 0) (𝓝 1) :=
-begin
-  haveI : second_countable_topology β := emetric.second_countable_of_sigma_compact β,
-  filter_upwards [vitali_family.ae_tendsto_measure_inter_div (besicovitch.vitali_family μ)]
-    with x hx using hx.comp (tendsto_filter_at μ x),
-end
+by filter_upwards [vitali_family.ae_tendsto_measure_inter_div (besicovitch.vitali_family μ)]
+    with x hx using hx.comp (tendsto_filter_at μ x)
 
 end besicovitch

src/measure_theory/covering/density_theorem.lean

@@ -29,8 +29,6 @@ noncomputable theory
 open set filter metric measure_theory topological_space
 open_locale nnreal topological_space
 
-local attribute [instance] emetric.second_countable_of_sigma_compact
-
 namespace is_doubling_measure
 
 variables {α : Type*} [metric_space α] [measurable_space α] (μ : measure α) [is_doubling_measure μ]
@@ -135,7 +133,7 @@ end
 end
 
 section applications
-variables [sigma_compact_space α] [borel_space α] [is_locally_finite_measure μ]
+variables [second_countable_topology α] [borel_space α] [is_locally_finite_measure μ]
   {E : Type*} [normed_add_comm_group E]
 
 /-- A version of *Lebesgue's density theorem* for a sequence of closed balls whose centers are

src/measure_theory/covering/differentiation.lean

@@ -13,8 +13,8 @@ import measure_theory.decomposition.lebesgue
 /-!
 # Differentiation of measures
 
-On a metric space with a measure `μ`, consider a Vitali family (i.e., for each `x` one has a family
-of sets shrinking to `x`, with a good behavior with respect to covering theorems).
+On a second countable metric space with a measure `μ`, consider a Vitali family (i.e., for each `x`
+one has a family of sets shrinking to `x`, with a good behavior with respect to covering theorems).
 Consider also another measure `ρ`. Then, for almost every `x`, the ratio `ρ a / μ a` converges when
 `a` shrinks to `x` along the Vitali family, towards the Radon-Nikodym derivative of `ρ` with
 respect to `μ`. This is the main theorem on differentiation of measures.
@@ -56,6 +56,19 @@ almost everywhere measurable, again based on the disjoint subcovering argument
 (see `vitali_family.exists_measurable_supersets_lim_ratio`), and then proceed as sketched above
 but replacing `v.lim_ratio ρ` by a measurable version called `v.lim_ratio_meas ρ`.
 
+## Counterexample
+
+The standing assumption in this file is that spaces are second countable. Without this assumption,
+measures may be zero locally but nonzero globally, which is not compatible with differentiation
+theory (which deduces global information from local one). Here is an example displaying this
+behavior.
+
+Define a measure `μ` by `μ s = 0` if `s` is covered by countably many balls of radius `1`,
+and `μ s = ∞` otherwise. This is indeed a countably additive measure, which is moreover
+locally finite and doubling at small scales. It vanishes on every ball of radius `1`, so all the
+quantities in differentiation theory (defined as ratios of measures as the radius tends to zero)
+make no sense. However, the measure is not globally zero if the space is big enough.
+
 ## References
 
 * [Herbert Federer, Geometric Measure Theory, Chapter 2.9][Federer1996]
@@ -64,8 +77,6 @@ but replacing `v.lim_ratio ρ` by a measurable version called `v.lim_ratio_meas
 open measure_theory metric set filter topological_space measure_theory.measure
 open_locale filter ennreal measure_theory nnreal topological_space
 
-local attribute [instance] emetric.second_countable_of_sigma_compact
-
 variables {α : Type*} [metric_space α] {m0 : measurable_space α}
 {μ : measure α} (v : vitali_family μ)
 {E : Type*} [normed_add_comm_group E]
@@ -113,7 +124,7 @@ end
 
 /-- If two measures `ρ` and `ν` have, at every point of a set `s`, arbitrarily small sets in a
 Vitali family satisfying `ρ a ≤ ν a`, then `ρ s ≤ ν s` if `ρ ≪ μ`.-/
-theorem measure_le_of_frequently_le [sigma_compact_space α] [borel_space α]
+theorem measure_le_of_frequently_le [second_countable_topology α] [borel_space α]
   {ρ : measure α} (ν : measure α) [is_locally_finite_measure ν]
   (hρ : ρ ≪ μ) (s : set α) (hs : ∀ x ∈ s, ∃ᶠ a in v.filter_at x, ρ a ≤ ν a) :
   ρ s ≤ ν s :=
@@ -141,7 +152,7 @@ end
 
 section
 
-variables [sigma_compact_space α] [borel_space α] [is_locally_finite_measure μ]
+variables [second_countable_topology α] [borel_space α] [is_locally_finite_measure μ]
   {ρ : measure α} [is_locally_finite_measure ρ]
 
 /-- If a measure `ρ` is singular with respect to `μ`, then for `μ` almost every `x`, the ratio
@@ -797,7 +808,7 @@ begin
   A minor technical inconvenience is that constants are not integrable, so to apply previous lemmas
   we need to replace `c` with the restriction of `c` to a finite measure set `A n` in the
   above sketch. -/
-  let A := measure_theory.measure.finite_spanning_sets_in_open μ,
+  let A := measure_theory.measure.finite_spanning_sets_in_open' μ,
   rcases h'f.is_separable_range with ⟨t, t_count, ht⟩,
   have main : ∀ᵐ x ∂μ, ∀ (n : ℕ) (c : E) (hc : c ∈ t),
     tendsto (λ a, (∫⁻ y in a, ‖f y - (A.set n).indicator (λ y, c) y‖₊ ∂μ) / μ a)

src/measure_theory/covering/liminf_limsup.lean

@@ -21,10 +21,11 @@ carrying a doubling measure.
 
 -/
 
-open set filter metric measure_theory
+open set filter metric measure_theory topological_space
 open_locale nnreal ennreal topological_space
 
-variables {α : Type*} [metric_space α] [sigma_compact_space α] [measurable_space α] [borel_space α]
+variables {α : Type*} [metric_space α] [second_countable_topology α] [measurable_space α]
+  [borel_space α]
 variables (μ : measure α) [is_locally_finite_measure μ] [is_doubling_measure μ]
 
 /-- This is really an auxiliary result en route to `blimsup_cthickening_ae_le_of_eventually_mul_le`

src/measure_theory/measure/measure_space.lean

@@ -3368,6 +3368,17 @@ begin
     ennreal.coe_of_nnreal_hom, ne.def, not_false_iff],
 end
 
+protected lemma measure.is_topological_basis_is_open_lt_top [topological_space α] (μ : measure α)
+  [is_locally_finite_measure μ] :
+  topological_space.is_topological_basis {s | is_open s ∧ μ s < ∞} :=
+begin
+  refine topological_space.is_topological_basis_of_open_of_nhds (λ s hs, hs.1) _,
+  assume x s xs hs,
+  rcases μ.exists_is_open_measure_lt_top x with ⟨v, xv, hv, μv⟩,
+  refine ⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt _ μv⟩, ⟨xv, xs⟩, inter_subset_right _ _⟩,
+  exact measure_mono (inter_subset_left _ _),
+end
+
 /-- A measure `μ` is finite on compacts if any compact set `K` satisfies `μ K < ∞`. -/
 @[protect_proj] class is_finite_measure_on_compacts [topological_space α] (μ : measure α) : Prop :=
 (lt_top_of_is_compact : ∀ ⦃K : set α⦄, is_compact K → μ K < ∞)
@@ -3920,6 +3931,43 @@ def measure_theory.measure.finite_spanning_sets_in_open [topological_space α]
     ((is_compact_compact_covering α n).exists_open_superset_measure_lt_top μ).some_spec.fst)
     (Union_compact_covering α) }
 
+open topological_space
+
+/-- A locally finite measure on a second countable topological space admits a finite spanning
+sequence of open sets. -/
+@[irreducible] def measure_theory.measure.finite_spanning_sets_in_open' [topological_space α]
+  [second_countable_topology α] {m : measurable_space α} (μ : measure α)
+  [is_locally_finite_measure μ] :
+  μ.finite_spanning_sets_in {K | is_open K} :=
+begin
+  suffices H : nonempty (μ.finite_spanning_sets_in {K | is_open K}), from H.some,
+  casesI is_empty_or_nonempty α,
+  { exact
+      ⟨{ set := λ n, ∅, set_mem := λ n, by simp, finite := λ n, by simp, spanning := by simp }⟩ },
+  inhabit α,
+  let S : set (set α) := {s | is_open s ∧ μ s < ∞},
+  obtain ⟨T, T_count, TS, hT⟩ : ∃ T : set (set α), T.countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S :=
+    is_open_sUnion_countable S (λ s hs, hs.1),
+  rw μ.is_topological_basis_is_open_lt_top.sUnion_eq at hT,
+  have T_ne : T.nonempty,
+  { by_contra h'T,
+    simp only [not_nonempty_iff_eq_empty.1 h'T, sUnion_empty] at hT,
+    simpa only [← hT] using mem_univ (default : α) },
+  obtain ⟨f, hf⟩ : ∃ f : ℕ → set α, T = range f, from T_count.exists_eq_range T_ne,
+  have fS : ∀ n, f n ∈ S,
+  { assume n,
+    apply TS,
+    rw hf,
+    exact mem_range_self n },
+  refine ⟨{ set := f, set_mem := λ n, (fS n).1, finite := λ n, (fS n).2, spanning := _ }⟩,
+  apply eq_univ_of_forall (λ x, _),
+  obtain ⟨t, tT, xt⟩ : ∃ (t : set α), t ∈ range f ∧ x ∈ t,
+  { have : x ∈ ⋃₀ T, by simp only [hT],
+    simpa only [mem_sUnion, exists_prop, ← hf] },
+  obtain ⟨n, rfl⟩ : ∃ (n : ℕ), f n = t, by simpa only using tT,
+  exact mem_Union_of_mem _ xt,
+end
+
 section measure_Ixx
 
 variables [preorder α] [topological_space α] [compact_Icc_space α]

src/measure_theory/measure/regular.lean

@@ -66,12 +66,10 @@ is automatically satisfied by any finite measure on a metric space.
 
 * `set.measure_eq_infi_is_open` asserts that, when `μ` is outer regular, the measure of a
   set is the infimum of the measure of open sets containing it.
-* `set.exists_is_open_lt_of_lt'` asserts that, when `μ` is outer regular, for every set `s`
+* `set.exists_is_open_lt_of_lt` asserts that, when `μ` is outer regular, for every set `s`
   and `r > μ s` there exists an open superset `U ⊇ s` of measure less than `r`.
 * push forward of an outer regular measure is outer regular, and scalar multiplication of a regular
   measure by a finite number is outer regular.
-* `measure_theory.measure.outer_regular.of_sigma_compact_space_of_is_locally_finite_measure`:
-  a locally finite measure on a `σ`-compact metric (or even pseudo emetric) space is outer regular.
 
 ### Weakly regular measures
 
@@ -87,9 +85,9 @@ is automatically satisfied by any finite measure on a metric space.
 * `measure_theory.measure.weakly_regular.of_pseudo_emetric_space_of_is_finite_measure` is an
   instance registering that a finite measure on a metric space is weakly regular (in fact, a pseudo
   emetric space is enough);
-* `measure_theory.measure.weakly_regular.of_pseudo_emetric_sigma_compact_space_of_locally_finite`
-  is an instance registering that a locally finite measure on a `σ`-compact metric space (or even
-  a pseudo emetric space) is weakly regular.
+* `measure_theory.measure.weakly_regular.of_pseudo_emetric_second_countable_of_locally_finite`
+  is an instance registering that a locally finite measure on a second countable metric space (or
+  even a pseudo emetric space) is weakly regular.
 
 ### Regular measures
 
@@ -613,23 +611,25 @@ instance of_pseudo_emetric_space_of_is_finite_measure {X : Type*} [pseudo_emetri
   weakly_regular μ :=
 (inner_regular.of_pseudo_emetric_space μ).weakly_regular_of_finite μ
 
-/-- Any locally finite measure on a `σ`-compact metric space (or even a pseudo emetric space) is
-weakly regular. -/
+/-- Any locally finite measure on a second countable metric space (or even a pseudo emetric space)
+is weakly regular. -/
 @[priority 100] -- see Note [lower instance priority]
-instance of_pseudo_emetric_sigma_compact_space_of_locally_finite {X : Type*}
-  [pseudo_emetric_space X] [sigma_compact_space X] [measurable_space X] [borel_space X]
+instance of_pseudo_emetric_second_countable_of_locally_finite {X : Type*} [pseudo_emetric_space X]
+  [topological_space.second_countable_topology X] [measurable_space X] [borel_space X]
   (μ : measure X) [is_locally_finite_measure μ] :
   weakly_regular μ :=
 begin
   haveI : outer_regular μ,
-  { refine (μ.finite_spanning_sets_in_open.mono' $ λ U hU, _).outer_regular,
+  { refine (μ.finite_spanning_sets_in_open'.mono' $ λ U hU, _).outer_regular,
     haveI : fact (μ U < ∞), from ⟨hU.2⟩,
     exact ⟨hU.1, infer_instance⟩ },
   exact ⟨inner_regular.of_pseudo_emetric_space μ⟩
 end
 
 end weakly_regular
 
+local attribute [instance] emetric.second_countable_of_sigma_compact
+
 /-- Any locally finite measure on a `σ`-compact (e)metric space is regular. -/
 @[priority 100] -- see Note [lower instance priority]
 instance regular.of_sigma_compact_space_of_is_locally_finite_measure {X : Type*}