chore(measure_theory/measure/doubling): rename is_doubling_measure …

…to `is_unif_loc_doubling_measure` (#18709)

With thanks to Jireh for highlighting our non-standard terminology.

See also [Zulip conversation](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/definition.20of.20doubling.20measures).

src/analysis/calculus/monotone.lean

@@ -30,7 +30,7 @@ limit of `(f y - f x) / (y - x)` by a lower and upper approximation argument fro
 behavior of `μ [x, y]`.
 -/
 
-open set filter function metric measure_theory measure_theory.measure is_doubling_measure
+open set filter function metric measure_theory measure_theory.measure is_unif_loc_doubling_measure
 open_locale topology
 
 /-- If `(f y - f x) / (y - x)` converges to a limit as `y` tends to `x`, then the same goes if

src/dynamics/ergodic/add_circle.lean

@@ -61,7 +61,8 @@ begin
   obtain ⟨d, -, hd⟩ : ∃ d, d ∈ s ∧ ∀ {ι'} {l : filter ι'} (w : ι' → add_circle T) (δ : ι' → ℝ),
     tendsto δ l (𝓝[>] 0) → (∀ᶠ j in l, d ∈ closed_ball (w j) (1 * δ j)) →
       tendsto (λ j, μ (s ∩ closed_ball (w j) (δ j)) / μ (closed_ball (w j) (δ j))) l (𝓝 1) :=
-    exists_mem_of_measure_ne_zero_of_ae h (is_doubling_measure.ae_tendsto_measure_inter_div μ s 1),
+    exists_mem_of_measure_ne_zero_of_ae h
+      (is_unif_loc_doubling_measure.ae_tendsto_measure_inter_div μ s 1),
   let I : ι → set (add_circle T) := λ j, closed_ball d (T / (2 * ↑(n j))),
   replace hd : tendsto (λ j, μ (s ∩ I j) / μ (I j)) l (𝓝 1),
   { let δ : ι → ℝ := λ j, T / (2 * ↑(n j)),

src/measure_theory/covering/besicovitch.lean

@@ -1140,7 +1140,7 @@ to `1` when `r` tends to `0`, for almost every `x` in `s`.
 This shows that almost every point of `s` is a Lebesgue density point for `s`.
 A stronger version holds for measurable sets, see `ae_tendsto_measure_inter_div_of_measurable_set`.
 
-See also `is_doubling_measure.ae_tendsto_measure_inter_div`. -/
+See also `is_unif_loc_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) :=

src/measure_theory/covering/density_theorem.lean

@@ -8,19 +8,21 @@ import measure_theory.covering.vitali
 import measure_theory.covering.differentiation
 
 /-!
-# Doubling measures and Lebesgue's density theorem
+# Uniformly locally doubling measures and Lebesgue's density theorem
 
 Lebesgue's density theorem states that given a set `S` in a sigma compact metric space with
-locally-finite doubling measure `μ` then for almost all points `x` in `S`, for any sequence of
-closed balls `B₀, B₁, B₂, ...` containing `x`, the limit `μ (S ∩ Bⱼ) / μ (Bⱼ) → 1` as `j → ∞`.
+locally-finite uniformly locally doubling measure `μ` then for almost all points `x` in `S`, for any
+sequence of closed balls `B₀, B₁, B₂, ...` containing `x`, the limit `μ (S ∩ Bⱼ) / μ (Bⱼ) → 1` as
+`j → ∞`.
 
-In this file we combine general results about existence of Vitali families for doubling measures
-with results about differentiation along a Vitali family to obtain an explicit form of Lebesgue's
-density theorem.
+In this file we combine general results about existence of Vitali families for uniformly locally
+doubling measures with results about differentiation along a Vitali family to obtain an explicit
+form of Lebesgue's density theorem.
 
 ## Main results
-  * `is_doubling_measure.ae_tendsto_measure_inter_div`: a version of Lebesgue's density theorem for
-  sequences of balls converging on a point but whose centres are not required to be fixed.
+  * `is_unif_loc_doubling_measure.ae_tendsto_measure_inter_div`: a version of Lebesgue's density
+  theorem for sequences of balls converging on a point but whose centres are not required to be
+  fixed.
 
 -/
 
@@ -29,17 +31,18 @@ noncomputable theory
 open set filter metric measure_theory topological_space
 open_locale nnreal topology
 
-namespace is_doubling_measure
+namespace is_unif_loc_doubling_measure
 
-variables {α : Type*} [metric_space α] [measurable_space α] (μ : measure α) [is_doubling_measure μ]
+variables {α : Type*} [metric_space α] [measurable_space α]
+          (μ : measure α) [is_unif_loc_doubling_measure μ]
 
 section
 variables [second_countable_topology α] [borel_space α] [is_locally_finite_measure μ]
 
 open_locale topology
 
-/-- A Vitali family in a space with a doubling measure, designed so that the sets at `x` contain
-all `closed_ball y r` when `dist x y ≤ K * r`. -/
+/-- A Vitali family in a space with a uniformly locally doubling measure, designed so that the sets
+at `x` contain all `closed_ball y r` when `dist x y ≤ K * r`. -/
 @[irreducible] def vitali_family (K : ℝ) : vitali_family μ :=
 begin
   /- the Vitali covering theorem gives a family that works well at small scales, thanks to the
@@ -59,8 +62,8 @@ begin
     (R / 4) (by linarith),
 end
 
-/-- In the Vitali family `is_doubling_measure.vitali_family K`, the sets based at `x` contain all
-balls `closed_ball y r` when `dist x y ≤ K * r`. -/
+/-- In the Vitali family `is_unif_loc_doubling_measure.vitali_family K`, the sets based at `x`
+contain all balls `closed_ball y r` when `dist x y ≤ K * r`. -/
 lemma closed_ball_mem_vitali_family_of_dist_le_mul
   {K : ℝ} {x y : α} {r : ℝ} (h : dist x y ≤ K * r) (rpos : 0 < r) :
   closed_ball y r ∈ (vitali_family μ K).sets_at x :=
@@ -171,4 +174,4 @@ using hx.comp (tendsto_closed_ball_filter_at μ _ _ δlim xmem)
 
 end applications
 
-end is_doubling_measure
+end is_unif_loc_doubling_measure

src/measure_theory/covering/liminf_limsup.lean

@@ -6,17 +6,17 @@ Authors: Oliver Nash
 import measure_theory.covering.density_theorem
 
 /-!
-# Liminf, limsup, and doubling measures.
+# Liminf, limsup, and uniformly locally doubling measures.
 
 This file is a place to collect lemmas about liminf and limsup for subsets of a metric space
-carrying a doubling measure.
+carrying a uniformly locally doubling measure.
 
 ## Main results:
 
  * `blimsup_cthickening_mul_ae_eq`: the limsup of the closed thickening of a sequence of subsets
-   of a metric space is unchanged almost everywhere for a doubling measure if the sequence of
-   distances is multiplied by a positive scale factor. This is a generalisation of a result of
-   Cassels, appearing as Lemma 9 on page 217 of
+   of a metric space is unchanged almost everywhere for a uniformly locally doubling measure if the
+   sequence of distances is multiplied by a positive scale factor. This is a generalisation of a
+   result of Cassels, appearing as Lemma 9 on page 217 of
    [J.W.S. Cassels, *Some metrical theorems in Diophantine approximation. I*](cassels1950).
  * `blimsup_thickening_mul_ae_eq`: a variant of `blimsup_cthickening_mul_ae_eq` for thickenings
    rather than closed thickenings.
@@ -28,7 +28,7 @@ open_locale nnreal ennreal topology
 
 variables {α : Type*} [metric_space α] [second_countable_topology α] [measurable_space α]
   [borel_space α]
-variables (μ : measure α) [is_locally_finite_measure μ] [is_doubling_measure μ]
+variables (μ : measure α) [is_locally_finite_measure μ] [is_unif_loc_doubling_measure μ]
 
 /-- This is really an auxiliary result en route to `blimsup_cthickening_ae_le_of_eventually_mul_le`
 (which is itself an auxiliary result en route to `blimsup_cthickening_mul_ae_eq`).
@@ -56,7 +56,8 @@ begin
 
   We obtain our contradiction by showing that there exists `η < 1` such that
   `μ (W ∩ (B j)) / μ (B j) ≤ η` for sufficiently large `j`. In fact we claim that `η = 1 - C⁻¹`
-  is such a value where `C` is the scaling constant of `M⁻¹` for the doubling measure `μ`.
+  is such a value where `C` is the scaling constant of `M⁻¹` for the uniformly locally doubling
+  measure `μ`.
 
   To prove the claim, let `b j = closed_ball (w j) (M * r₁ (f j))` and for given `j` consider the
   sets `b j` and `W ∩ (B j)`. These are both subsets of `B j` and are disjoint for large enough `j`
@@ -76,7 +77,7 @@ begin
     tendsto δ l (𝓝[>] 0) → (∀ᶠ j in l, d ∈ closed_ball (w j) (2 * δ j)) →
     tendsto (λ j, μ (W ∩ closed_ball (w j) (δ j)) / μ (closed_ball (w j) (δ j))) l (𝓝 1) :=
     measure.exists_mem_of_measure_ne_zero_of_ae contra
-      (is_doubling_measure.ae_tendsto_measure_inter_div μ W 2),
+      (is_unif_loc_doubling_measure.ae_tendsto_measure_inter_div μ W 2),
   replace hd : d ∈ blimsup Y₁ at_top p := ((mem_diff _).mp hd).1,
   obtain ⟨f : ℕ → ℕ, hf⟩ := exists_forall_mem_of_has_basis_mem_blimsup' at_top_basis hd,
   simp only [forall_and_distrib] at hf,
@@ -96,9 +97,9 @@ begin
     { exact mem_Union₂.mp (cthickening_subset_Union_closed_ball_of_lt (s (f j)) (by positivity)
         (lt_two_mul_self hrp') (hf₀ j)), }, },
   choose w hw hw' using hf₀,
-  let C := is_doubling_measure.scaling_constant_of μ M⁻¹,
+  let C := is_unif_loc_doubling_measure.scaling_constant_of μ M⁻¹,
   have hC : 0 < C :=
-    lt_of_lt_of_le zero_lt_one (is_doubling_measure.one_le_scaling_constant_of μ M⁻¹),
+    lt_of_lt_of_le zero_lt_one (is_unif_loc_doubling_measure.one_le_scaling_constant_of μ M⁻¹),
   suffices : ∃ (η < (1 : ℝ≥0)), ∀ᶠ j in at_top,
     μ (W ∩ closed_ball (w j) (r₁ (f j))) / μ (closed_ball (w j) (r₁ (f j))) ≤ η,
   { obtain ⟨η, hη, hη'⟩ := this,
@@ -123,7 +124,7 @@ begin
     simp only [mem_Union, exists_prop],
     exact ⟨f j, ⟨hf₁ j, hj.le.trans (hf₂ j)⟩, ha⟩, },
   have h₄ : ∀ᶠ j in at_top, μ (B j) ≤ C * μ (b j) :=
-    (hr.eventually (is_doubling_measure.eventually_measure_le_scaling_constant_mul'
+    (hr.eventually (is_unif_loc_doubling_measure.eventually_measure_le_scaling_constant_mul'
       μ M hM)).mono (λ j hj, hj (w j)),
   refine (h₃.and h₄).mono (λ j hj₀, _),
   change μ (W ∩ B j) / μ (B j) ≤ ↑(1 - C⁻¹),
@@ -175,8 +176,8 @@ end
 
 /-- Given a sequence of subsets `sᵢ` of a metric space, together with a sequence of radii `rᵢ`
 such that `rᵢ → 0`, the set of points which belong to infinitely many of the closed
-`rᵢ`-thickenings of `sᵢ` is unchanged almost everywhere for a doubling measure if the `rᵢ` are all
-scaled by a positive constant.
+`rᵢ`-thickenings of `sᵢ` is unchanged almost everywhere for a uniformly locally doubling measure if
+the `rᵢ` are all scaled by a positive constant.
 
 This lemma is a generalisation of Lemma 9 appearing on page 217 of
 [J.W.S. Cassels, *Some metrical theorems in Diophantine approximation. I*](cassels1950).
@@ -256,8 +257,8 @@ end
 
 /-- Given a sequence of subsets `sᵢ` of a metric space, together with a sequence of radii `rᵢ`
 such that `rᵢ → 0`, the set of points which belong to infinitely many of the
-`rᵢ`-thickenings of `sᵢ` is unchanged almost everywhere for a doubling measure if the `rᵢ` are all
-scaled by a positive constant.
+`rᵢ`-thickenings of `sᵢ` is unchanged almost everywhere for a uniformly locally doubling measure if
+the `rᵢ` are all scaled by a positive constant.
 
 This lemma is a generalisation of Lemma 9 appearing on page 217 of
 [J.W.S. Cassels, *Some metrical theorems in Diophantine approximation. I*](cassels1950).

src/measure_theory/covering/one_dim.lean

@@ -14,7 +14,7 @@ in `density_theorems.lean`. In this file, we expand the API for this theory in o
 by showing that intervals belong to the relevant Vitali family.
 -/
 
-open set measure_theory is_doubling_measure filter
+open set measure_theory is_unif_loc_doubling_measure filter
 open_locale topology
 
 namespace real

src/measure_theory/integral/periodic.lean

@@ -107,7 +107,7 @@ begin
   { simp [hε, min_eq_left (by linarith : T ≤ 2 * ε)], },
 end
 
-instance : is_doubling_measure (volume : measure (add_circle T)) :=
+instance : is_unif_loc_doubling_measure (volume : measure (add_circle T)) :=
 begin
   refine ⟨⟨real.to_nnreal 2, filter.eventually_of_forall $ λ ε x, _⟩⟩,
   simp only [volume_closed_ball],

src/measure_theory/measure/doubling.lean

@@ -7,46 +7,49 @@ import analysis.special_functions.log.base
 import measure_theory.measure.measure_space_def
 
 /-!
-# Doubling measures
+# Uniformly locally doubling measures
 
-A doubling measure `μ` on a metric space is a measure for which there exists a constant `C` such
-that for all sufficiently small radii `ε`, and for any centre, the measure of a ball of radius
-`2 * ε` is bounded by `C` times the measure of the concentric ball of radius `ε`.
+A uniformly locally doubling measure `μ` on a metric space is a measure for which there exists a
+constant `C` such that for all sufficiently small radii `ε`, and for any centre, the measure of a
+ball of radius `2 * ε` is bounded by `C` times the measure of the concentric ball of radius `ε`.
 
-This file records basic files on doubling measures.
+This file records basic facts about uniformly locally doubling measures.
 
 ## Main definitions
 
-  * `is_doubling_measure`: the definition of a doubling measure (as a typeclass).
-  * `is_doubling_measure.doubling_constant`: a function yielding the doubling constant `C` appearing
-  in the definition of a doubling measure.
+  * `is_unif_loc_doubling_measure`: the definition of a uniformly locally doubling measure (as a
+  typeclass).
+  * `is_unif_loc_doubling_measure.doubling_constant`: a function yielding the doubling constant `C`
+  appearing in the definition of a uniformly locally doubling measure.
 -/
 
 noncomputable theory
 
 open set filter metric measure_theory topological_space
 open_locale ennreal nnreal topology
 
-/-- A measure `μ` is said to be a doubling measure if there exists a constant `C` such that for
-all sufficiently small radii `ε`, and for any centre, the measure of a ball of radius `2 * ε` is
-bounded by `C` times the measure of the concentric ball of radius `ε`.
+/-- A measure `μ` is said to be a uniformly locally doubling measure if there exists a constant `C`
+such that for all sufficiently small radii `ε`, and for any centre, the measure of a ball of radius
+`2 * ε` is bounded by `C` times the measure of the concentric ball of radius `ε`.
 
 Note: it is important that this definition makes a demand only for sufficiently small `ε`. For
-example we want hyperbolic space to carry the instance `is_doubling_measure volume` but volumes grow
-exponentially in hyperbolic space. To be really explicit, consider the hyperbolic plane of
-curvature -1, the area of a disc of radius `ε` is `A(ε) = 2π(cosh(ε) - 1)` so `A(2ε)/A(ε) ~ exp(ε)`.
--/
-class is_doubling_measure {α : Type*} [metric_space α] [measurable_space α] (μ : measure α) :=
+example we want hyperbolic space to carry the instance `is_unif_loc_doubling_measure volume` but
+volumes grow exponentially in hyperbolic space. To be really explicit, consider the hyperbolic plane
+of curvature -1, the area of a disc of radius `ε` is `A(ε) = 2π(cosh(ε) - 1)` so
+`A(2ε)/A(ε) ~ exp(ε)`. -/
+class is_unif_loc_doubling_measure
+  {α : Type*} [metric_space α] [measurable_space α] (μ : measure α) :=
 (exists_measure_closed_ball_le_mul [] :
   ∃ (C : ℝ≥0), ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closed_ball x (2 * ε)) ≤ C * μ (closed_ball x ε))
 
-namespace is_doubling_measure
+namespace is_unif_loc_doubling_measure
 
-variables {α : Type*} [metric_space α] [measurable_space α] (μ : measure α) [is_doubling_measure μ]
+variables {α : Type*} [metric_space α] [measurable_space α]
+          (μ : measure α) [is_unif_loc_doubling_measure μ]
 
-/-- A doubling constant for a doubling measure.
+/-- A doubling constant for a uniformly locally doubling measure.
 
-See also `is_doubling_measure.scaling_constant_of`. -/
+See also `is_unif_loc_doubling_measure.scaling_constant_of`. -/
 def doubling_constant : ℝ≥0 := classical.some $ exists_measure_closed_ball_le_mul μ
 
 lemma exists_measure_closed_ball_le_mul' :
@@ -82,8 +85,8 @@ begin
     exact real.rpow_le_rpow_of_exponent_le one_le_two (nat.le_ceil (real.logb 2 K)), },
 end
 
-/-- A variant of `is_doubling_measure.doubling_constant` which allows for scaling the radius by
-values other than `2`. -/
+/-- A variant of `is_unif_loc_doubling_measure.doubling_constant` which allows for scaling the
+radius by values other than `2`. -/
 def scaling_constant_of (K : ℝ) : ℝ≥0 :=
 max (classical.some $ exists_eventually_forall_measure_closed_ball_le_mul μ K) 1
 
@@ -139,4 +142,4 @@ lemma measure_mul_le_scaling_constant_of_mul {K : ℝ} {x : α} {t r : ℝ}
   μ (closed_ball x (t * r)) ≤ scaling_constant_of μ K * μ (closed_ball x r) :=
 (eventually_measure_mul_le_scaling_constant_of_mul μ K).some_spec.2 x t r ht hr
 
-end is_doubling_measure
+end is_unif_loc_doubling_measure

src/measure_theory/measure/haar_lebesgue.lean

@@ -566,7 +566,8 @@ calc
     { simp only [ennreal.of_real_ne_top, ne.def, not_false_iff] }
   end
 
-@[priority 100] instance is_doubling_measure_of_is_add_haar_measure : is_doubling_measure μ :=
+@[priority 100] instance is_unif_loc_doubling_measure_of_is_add_haar_measure :
+  is_unif_loc_doubling_measure μ :=
 begin
   refine ⟨⟨(2 : ℝ≥0) ^ (finrank ℝ E), _⟩⟩,
   filter_upwards [self_mem_nhds_within] with r hr x,