feat(measure_theory/measure/haar_lebesgue): the Lebesgue measure is d…

…oubling (#16885)

Also split the file `measure_theory/covering/density_theorem` in two, to avoid importing all the differentiation theory into `haar_lebesgue.lean`.

src/analysis/special_functions/stirling.lean

@@ -60,7 +60,7 @@ We have the expression
 -/
 lemma log_stirling_seq_formula (n : ℕ) : log (stirling_seq n.succ) =
   log n.succ!- 1 / 2 * log (2 * n.succ) - n.succ * log (n.succ / exp 1) :=
-by rw [stirling_seq, log_div, log_mul, sqrt_eq_rpow, log_rpow, log_pow, tsub_tsub];
+by rw [stirling_seq, log_div, log_mul, sqrt_eq_rpow, log_rpow, real.log_pow, tsub_tsub];
   try { apply ne_of_gt }; positivity -- TODO: Make `positivity` handle `≠ 0` goals
 
 /--
@@ -90,7 +90,7 @@ begin
 end
 
 /-- The sequence `log ∘ stirling_seq ∘ succ` is monotone decreasing -/
-lemma log_stirling_seq'_antitone : antitone (log ∘ stirling_seq ∘ succ) :=
+lemma log_stirling_seq'_antitone : antitone (real.log ∘ stirling_seq ∘ succ) :=
 antitone_nat_of_succ_le $ λ n, sub_nonneg.mp $ (log_stirling_seq_diff_has_sum n).nonneg $ λ m,
   by positivity
 

src/data/real/nnreal.lean

@@ -485,6 +485,10 @@ end
   real.to_nnreal (bit1 r) = bit1 (real.to_nnreal r) :=
 (real.to_nnreal_add (by simp [hr]) zero_le_one).trans (by simp [bit1])
 
+lemma to_nnreal_pow {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : (x ^ n).to_nnreal = (x.to_nnreal) ^ n :=
+by rw [← nnreal.coe_eq, nnreal.coe_pow, real.coe_to_nnreal _ (pow_nonneg hx _),
+  real.coe_to_nnreal x hx]
+
 end to_nnreal
 
 end real

src/measure_theory/covering/density_theorem.lean

@@ -3,17 +3,13 @@ Copyright (c) 2022 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import measure_theory.measure.doubling
 import measure_theory.covering.vitali
 import measure_theory.covering.differentiation
-import analysis.special_functions.log.base
 
 /-!
 # Doubling measures and Lebesgue's density theorem
 
-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 `ε`.
-
 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 → ∞`.
@@ -23,12 +19,9 @@ with results about differentiation along a Vitali family to obtain an explicit f
 density theorem.
 
 ## Main results
-
-  * `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_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.
+
 -/
 
 noncomputable theory
@@ -38,97 +31,10 @@ open_locale nnreal topological_space
 
 local attribute [instance] emetric.second_countable_of_sigma_compact
 
-/-- 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 `ε`.
-
-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 α) :=
-(exists_measure_closed_ball_le_mul [] :
-  ∃ (C : ℝ≥0), ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closed_ball x (2 * ε)) ≤ C * μ (closed_ball x ε))
-
 namespace is_doubling_measure
 
 variables {α : Type*} [metric_space α] [measurable_space α] (μ : measure α) [is_doubling_measure μ]
 
-/-- A doubling constant for a doubling measure.
-
-See also `is_doubling_measure.scaling_constant_of`. -/
-def doubling_constant : ℝ≥0 := classical.some $ exists_measure_closed_ball_le_mul μ
-
-lemma exists_measure_closed_ball_le_mul' :
-  ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closed_ball x (2 * ε)) ≤ doubling_constant μ * μ (closed_ball x ε) :=
-classical.some_spec $ exists_measure_closed_ball_le_mul μ
-
-lemma exists_eventually_forall_measure_closed_ball_le_mul (K : ℝ) :
-  ∃ (C : ℝ≥0), ∀ᶠ ε in 𝓝[>] 0, ∀ x t (ht : t ≤ K),
-    μ (closed_ball x (t * ε)) ≤ C * μ (closed_ball x ε) :=
-begin
-  let C := doubling_constant μ,
-  have hμ : ∀ (n : ℕ), ∀ᶠ ε in 𝓝[>] 0, ∀ x,
-    μ (closed_ball x (2^n * ε)) ≤ ↑(C^n) * μ (closed_ball x ε),
-  { intros n,
-    induction n with n ih, { simp, },
-    replace ih := eventually_nhds_within_pos_mul_left (two_pos : 0 < (2 : ℝ)) ih,
-    refine (ih.and (exists_measure_closed_ball_le_mul' μ)).mono (λ ε hε x, _),
-    calc μ (closed_ball x (2^(n + 1) * ε))
-          = μ (closed_ball x (2^n * (2 * ε))) : by rw [pow_succ', mul_assoc]
-      ... ≤ ↑(C^n) * μ (closed_ball x (2 * ε)) : hε.1 x
-      ... ≤ ↑(C^n) * (C * μ (closed_ball x ε)) : ennreal.mul_left_mono (hε.2 x)
-      ... = ↑(C^(n + 1)) * μ (closed_ball x ε) : by rw [← mul_assoc, pow_succ', ennreal.coe_mul], },
-  rcases lt_or_le K 1 with hK | hK,
-  { refine ⟨1, _⟩,
-    simp only [ennreal.coe_one, one_mul],
-    exact eventually_mem_nhds_within.mono (λ ε hε x t ht,
-      measure_mono $ closed_ball_subset_closed_ball (by nlinarith [mem_Ioi.mp hε])), },
-  { refine ⟨C^⌈real.logb 2 K⌉₊, ((hμ ⌈real.logb 2 K⌉₊).and eventually_mem_nhds_within).mono
-      (λ ε hε x t ht, le_trans (measure_mono $ closed_ball_subset_closed_ball _) (hε.1 x))⟩,
-    refine mul_le_mul_of_nonneg_right (ht.trans _) (mem_Ioi.mp hε.2).le,
-    conv_lhs { rw ← real.rpow_logb two_pos (by norm_num) (by linarith : 0 < K), },
-    rw ← real.rpow_nat_cast,
-    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`. -/
-def scaling_constant_of (K : ℝ) : ℝ≥0 :=
-max (classical.some $ exists_eventually_forall_measure_closed_ball_le_mul μ K) 1
-
-lemma eventually_measure_mul_le_scaling_constant_of_mul (K : ℝ) :
-  ∃ (R : ℝ), 0 < R ∧ ∀ x t r (ht : t ∈ Ioc 0 K) (hr : r ≤ R),
-    μ (closed_ball x (t * r)) ≤ scaling_constant_of μ K * μ (closed_ball x r) :=
-begin
-  have h := classical.some_spec (exists_eventually_forall_measure_closed_ball_le_mul μ K),
-  rcases mem_nhds_within_Ioi_iff_exists_Ioc_subset.1 h with ⟨R, Rpos, hR⟩,
-  refine ⟨R, Rpos, λ x t r ht hr, _⟩,
-  rcases lt_trichotomy r 0 with rneg|rfl|rpos,
-  { have : t * r < 0, from mul_neg_of_pos_of_neg ht.1 rneg,
-    simp only [closed_ball_eq_empty.2 this, measure_empty, zero_le'] },
-  { simp only [mul_zero, closed_ball_zero],
-    refine le_mul_of_one_le_of_le _ le_rfl,
-    apply ennreal.one_le_coe_iff.2 (le_max_right _ _) },
-  { apply (hR ⟨rpos, hr⟩ x t ht.2).trans _,
-    exact ennreal.mul_le_mul (ennreal.coe_le_coe.2 (le_max_left _ _)) le_rfl }
-end
-
-/-- A scale below which the doubling measure `μ` satisfies good rescaling properties when one
-multiplies the radius of balls by at most `K`, as stated
-in `measure_mul_le_scaling_constant_of_mul`. -/
-def scaling_scale_of (K : ℝ) : ℝ :=
-(eventually_measure_mul_le_scaling_constant_of_mul μ K).some
-
-lemma scaling_scale_of_pos (K : ℝ) : 0 < scaling_scale_of μ K :=
-(eventually_measure_mul_le_scaling_constant_of_mul μ K).some_spec.1
-
-lemma measure_mul_le_scaling_constant_of_mul {K : ℝ} {x : α} {t r : ℝ}
-  (ht : t ∈ Ioc 0 K) (hr : r ≤ scaling_scale_of μ K) :
-  μ (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
-
 section
 variables [second_countable_topology α] [borel_space α] [is_locally_finite_measure μ]
 

src/measure_theory/measure/doubling.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2022 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import measure_theory.measure.measure_space
+import analysis.special_functions.log.base
+
+/-!
+# 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 `ε`.
+
+This file records basic files on 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.
+-/
+
+noncomputable theory
+
+open set filter metric measure_theory topological_space
+open_locale nnreal topological_space
+
+/-- 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 `ε`.
+
+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 α) :=
+(exists_measure_closed_ball_le_mul [] :
+  ∃ (C : ℝ≥0), ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closed_ball x (2 * ε)) ≤ C * μ (closed_ball x ε))
+
+namespace is_doubling_measure
+
+variables {α : Type*} [metric_space α] [measurable_space α] (μ : measure α) [is_doubling_measure μ]
+
+/-- A doubling constant for a doubling measure.
+
+See also `is_doubling_measure.scaling_constant_of`. -/
+def doubling_constant : ℝ≥0 := classical.some $ exists_measure_closed_ball_le_mul μ
+
+lemma exists_measure_closed_ball_le_mul' :
+  ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closed_ball x (2 * ε)) ≤ doubling_constant μ * μ (closed_ball x ε) :=
+classical.some_spec $ exists_measure_closed_ball_le_mul μ
+
+lemma exists_eventually_forall_measure_closed_ball_le_mul (K : ℝ) :
+  ∃ (C : ℝ≥0), ∀ᶠ ε in 𝓝[>] 0, ∀ x t (ht : t ≤ K),
+    μ (closed_ball x (t * ε)) ≤ C * μ (closed_ball x ε) :=
+begin
+  let C := doubling_constant μ,
+  have hμ : ∀ (n : ℕ), ∀ᶠ ε in 𝓝[>] 0, ∀ x,
+    μ (closed_ball x (2^n * ε)) ≤ ↑(C^n) * μ (closed_ball x ε),
+  { intros n,
+    induction n with n ih, { simp, },
+    replace ih := eventually_nhds_within_pos_mul_left (two_pos : 0 < (2 : ℝ)) ih,
+    refine (ih.and (exists_measure_closed_ball_le_mul' μ)).mono (λ ε hε x, _),
+    calc μ (closed_ball x (2^(n + 1) * ε))
+          = μ (closed_ball x (2^n * (2 * ε))) : by rw [pow_succ', mul_assoc]
+      ... ≤ ↑(C^n) * μ (closed_ball x (2 * ε)) : hε.1 x
+      ... ≤ ↑(C^n) * (C * μ (closed_ball x ε)) : ennreal.mul_left_mono (hε.2 x)
+      ... = ↑(C^(n + 1)) * μ (closed_ball x ε) : by rw [← mul_assoc, pow_succ', ennreal.coe_mul], },
+  rcases lt_or_le K 1 with hK | hK,
+  { refine ⟨1, _⟩,
+    simp only [ennreal.coe_one, one_mul],
+    exact eventually_mem_nhds_within.mono (λ ε hε x t ht,
+      measure_mono $ closed_ball_subset_closed_ball (by nlinarith [mem_Ioi.mp hε])), },
+  { refine ⟨C^⌈real.logb 2 K⌉₊, ((hμ ⌈real.logb 2 K⌉₊).and eventually_mem_nhds_within).mono
+      (λ ε hε x t ht, le_trans (measure_mono $ closed_ball_subset_closed_ball _) (hε.1 x))⟩,
+    refine mul_le_mul_of_nonneg_right (ht.trans _) (mem_Ioi.mp hε.2).le,
+    conv_lhs { rw ← real.rpow_logb two_pos (by norm_num) (by linarith : 0 < K), },
+    rw ← real.rpow_nat_cast,
+    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`. -/
+def scaling_constant_of (K : ℝ) : ℝ≥0 :=
+max (classical.some $ exists_eventually_forall_measure_closed_ball_le_mul μ K) 1
+
+lemma eventually_measure_mul_le_scaling_constant_of_mul (K : ℝ) :
+  ∃ (R : ℝ), 0 < R ∧ ∀ x t r (ht : t ∈ Ioc 0 K) (hr : r ≤ R),
+    μ (closed_ball x (t * r)) ≤ scaling_constant_of μ K * μ (closed_ball x r) :=
+begin
+  have h := classical.some_spec (exists_eventually_forall_measure_closed_ball_le_mul μ K),
+  rcases mem_nhds_within_Ioi_iff_exists_Ioc_subset.1 h with ⟨R, Rpos, hR⟩,
+  refine ⟨R, Rpos, λ x t r ht hr, _⟩,
+  rcases lt_trichotomy r 0 with rneg|rfl|rpos,
+  { have : t * r < 0, from mul_neg_of_pos_of_neg ht.1 rneg,
+    simp only [closed_ball_eq_empty.2 this, measure_empty, zero_le'] },
+  { simp only [mul_zero, closed_ball_zero],
+    refine le_mul_of_one_le_of_le _ le_rfl,
+    apply ennreal.one_le_coe_iff.2 (le_max_right _ _) },
+  { apply (hR ⟨rpos, hr⟩ x t ht.2).trans _,
+    exact ennreal.mul_le_mul (ennreal.coe_le_coe.2 (le_max_left _ _)) le_rfl }
+end
+
+/-- A scale below which the doubling measure `μ` satisfies good rescaling properties when one
+multiplies the radius of balls by at most `K`, as stated
+in `measure_mul_le_scaling_constant_of_mul`. -/
+def scaling_scale_of (K : ℝ) : ℝ :=
+(eventually_measure_mul_le_scaling_constant_of_mul μ K).some
+
+lemma scaling_scale_of_pos (K : ℝ) : 0 < scaling_scale_of μ K :=
+(eventually_measure_mul_le_scaling_constant_of_mul μ K).some_spec.1
+
+lemma measure_mul_le_scaling_constant_of_mul {K : ℝ} {x : α} {t r : ℝ}
+  (ht : t ∈ Ioc 0 K) (hr : r ≤ scaling_scale_of μ K) :
+  μ (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

src/measure_theory/measure/haar_lebesgue.lean

@@ -8,6 +8,7 @@ import measure_theory.measure.haar
 import linear_algebra.finite_dimensional
 import analysis.normed_space.pointwise
 import measure_theory.group.pointwise
+import measure_theory.measure.doubling
 
 /-!
 # Relationship between the Haar and Lebesgue measures
@@ -21,7 +22,7 @@ We deduce basic properties of any Haar measure on a finite dimensional real vect
 * `add_haar_preimage_linear_map` : when `f` is a linear map with nonzero determinant, the measure
   of `f ⁻¹' s` is the measure of `s` multiplied by the absolute value of the inverse of the
   determinant of `f`.
-* `add_haar_image_linear_map` :  when `f` is a linear map, the measure of `f '' s` is the
+* `add_haar_image_linear_map` : when `f` is a linear map, the measure of `f '' s` is the
   measure of `s` multiplied by the absolute value of the determinant of `f`.
 * `add_haar_submodule` : a strict submodule has measure `0`.
 * `add_haar_smul` : the measure of `r • s` is `|r| ^ dim * μ s`.
@@ -36,7 +37,7 @@ small `r`, see `eventually_nonempty_inter_smul_of_density_one`.
 -/
 
 open topological_space set filter metric
-open_locale ennreal pointwise topological_space
+open_locale ennreal pointwise topological_space nnreal
 
 /-- The interval `[0,1]` as a compact set with non-empty interior. -/
 def topological_space.positive_compacts.Icc01 : positive_compacts ℝ :=
@@ -501,6 +502,15 @@ 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 μ :=
+begin
+  refine ⟨⟨(2 : ℝ≥0) ^ (finrank ℝ E), _⟩⟩,
+  filter_upwards [self_mem_nhds_within] with r hr x,
+  rw [add_haar_closed_ball_mul μ x zero_le_two (le_of_lt hr), add_haar_closed_ball_center μ x,
+    ennreal.of_real, real.to_nnreal_pow zero_le_two],
+  simp only [real.to_nnreal_bit0, real.to_nnreal_one, le_refl],
+end
+
 /-!
 ### Density points