feat(measure_theory/measure): new class is_finite_measure_on_compacts (…

…#10827)

We have currently four independent type classes guaranteeing that a measure of compact sets is finite: `is_locally_finite_measure`, `is_regular_measure`, `is_haar_measure` and `is_add_haar_measure`. Instead of repeting lemmas for all these classes, we introduce a new typeclass saying that a measure is finite on compact sets.

src/measure_theory/constructions/borel_space.lean

@@ -1177,6 +1177,18 @@ def homemorph.to_measurable_equiv (h : α ≃ₜ β) : α ≃ᵐ β :=
   measurable_to_fun := h.continuous_to_fun.measurable,
   measurable_inv_fun := h.continuous_inv_fun.measurable }
 
+protected lemma is_finite_measure_on_compacts.map
+  {α : Type*} {m0 : measurable_space α} [topological_space α] [opens_measurable_space α]
+  {β : Type*} [measurable_space β] [topological_space β] [borel_space β]
+  [t2_space β] (μ : measure α) [is_finite_measure_on_compacts μ] (f : α ≃ₜ β) :
+  is_finite_measure_on_compacts (measure.map f μ) :=
+⟨begin
+  assume K hK,
+  rw [measure.map_apply f.measurable hK.measurable_set],
+  apply is_compact.measure_lt_top,
+  rwa f.compact_preimage
+end⟩
+
 end borel_space
 
 instance empty.borel_space : borel_space empty := ⟨borel_eq_top_of_discrete.symm⟩

src/measure_theory/covering/besicovitch_vector_space.lean

@@ -172,7 +172,7 @@ begin
   have J : (s.card : ℝ≥0∞) * ennreal.of_real (δ ^ (finrank ℝ E))
     ≤ ennreal.of_real (ρ ^ (finrank ℝ E)) :=
       (ennreal.mul_le_mul_right (μ.add_haar_ball_pos _ zero_lt_one).ne'
-        (μ.add_haar_ball_lt_top _ _).ne).1 I,
+        measure_ball_lt_top.ne).1 I,
   have K : (s.card : ℝ) ≤ (5 : ℝ) ^ finrank ℝ E,
     by simpa [ennreal.to_real_mul, div_eq_mul_inv] using
       ennreal.to_real_le_of_le_of_real (pow_nonneg ρpos.le _) J,
@@ -339,7 +339,7 @@ close enough to `1`. The number of such configurations is bounded by `multiplici
 suitably small.
 
 To check that the points `c' i` are `1 - δ`-separated, one treats separately the cases where
-both `∥c i∥` and `∥c j∥` are `≤ 2`, where one of them is `≤ 2` and the other one is `` > 2`, and
+both `∥c i∥` and `∥c j∥` are `≤ 2`, where one of them is `≤ 2` and the other one is `> 2`, and
 where both of them are `> 2`.
 -/
 

src/measure_theory/group/basic.lean

@@ -318,17 +318,15 @@ namespace measure
 /-- A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to compact
 sets and positive mass to open sets. -/
 class is_haar_measure {G : Type*} [group G] [topological_space G] [measurable_space G]
-  (μ : measure G) : Prop :=
+  (μ : measure G) extends is_finite_measure_on_compacts μ : Prop :=
 (left_invariant : is_mul_left_invariant μ)
-(compact_lt_top : ∀ (K : set G), is_compact K → μ K < ∞)
 (open_pos : ∀ (U : set G), is_open U → U.nonempty → 0 < μ U)
 
 /-- A measure on an additive group is an additive Haar measure if it is left-invariant, and gives
 finite mass to compact sets and positive mass to open sets. -/
 class is_add_haar_measure {G : Type*} [add_group G] [topological_space G] [measurable_space G]
-  (μ : measure G) : Prop :=
+  (μ : measure G) extends is_finite_measure_on_compacts μ : Prop :=
 (add_left_invariant : is_add_left_invariant μ)
-(compact_lt_top : ∀ (K : set G), is_compact K → μ K < ∞)
 (open_pos : ∀ (U : set G), is_open U → U.nonempty → 0 < μ U)
 
 attribute [to_additive] is_haar_measure
@@ -337,11 +335,6 @@ section
 
 variables [group G] [measurable_space G] [topological_space G] (μ : measure G) [is_haar_measure μ]
 
-@[to_additive]
-lemma _root_.is_compact.haar_lt_top {K : set G} (hK : is_compact K) :
-  μ K < ∞ :=
-is_haar_measure.compact_lt_top K hK
-
 @[to_additive]
 lemma _root_.is_open.haar_pos {U : set G} (hU : is_open U) (h'U : U.nonempty) :
   0 < μ U :=
@@ -379,9 +372,9 @@ by simp_rw [mul_comm, haar_preimage_mul μ g A]
 lemma is_haar_measure.smul {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) :
   is_haar_measure (c • μ) :=
 { left_invariant := (is_mul_left_invariant_haar μ).smul _,
-  compact_lt_top := λ K hK, begin
+  lt_top_of_is_compact := λ K hK, begin
     change c * μ K < ∞,
-    simp [lt_top_iff_ne_top, (hK.haar_lt_top μ).ne, cpos, ctop],
+    simp [lt_top_iff_ne_top, hK.measure_lt_top.ne, cpos, ctop],
   end,
   open_pos := λ U U_open U_ne, bot_lt_iff_ne_bot.2 $ begin
     change c * μ U ≠ 0,
@@ -396,7 +389,7 @@ lemma is_haar_measure_of_is_compact_nonempty_interior [topological_group G] [bor
   (K : set G) (hK : is_compact K) (h'K : (interior K).nonempty) (h : μ K ≠ 0) (h' : μ K ≠ ∞) :
   is_haar_measure μ :=
 { left_invariant := hμ,
-  compact_lt_top := λ L hL, hμ.measure_lt_top_of_is_compact' _ h'K h' hL,
+  lt_top_of_is_compact := λ L hL, hμ.measure_lt_top_of_is_compact' _ h'K h' hL,
   open_pos := λ U hU, hμ.measure_pos_of_is_open K hK h hU }
 
 /-- The image of a Haar measure under a group homomorphism which is also a homeomorphism is again
@@ -416,12 +409,12 @@ lemma is_haar_measure_map [borel_space G] [topological_group G] {H : Type*} [gro
     ext y,
     simp only [mul_equiv.apply_symm_apply, comp_app, mul_equiv.map_mul],
   end,
-  compact_lt_top := begin
+  lt_top_of_is_compact := begin
     assume K hK,
     rw map_apply hf.measurable hK.measurable_set,
     have : f.symm '' K = f ⁻¹' K := equiv.image_eq_preimage _ _,
     rw ← this,
-    exact is_compact.haar_lt_top _ (hK.image hfsymm)
+    exact is_compact.measure_lt_top (hK.image hfsymm)
   end,
   open_pos := begin
     assume U hU h'U,
@@ -440,7 +433,7 @@ instance is_haar_measure.sigma_finite
   sigma_finite μ :=
 ⟨⟨{ set := compact_covering G,
   set_mem := λ n, mem_univ _,
-  finite := λ n, is_compact.haar_lt_top μ $ is_compact_compact_covering G n,
+  finite := λ n, is_compact.measure_lt_top $ is_compact_compact_covering G n,
   spanning := Union_compact_covering G }⟩⟩
 
 open_locale topological_space
@@ -463,7 +456,7 @@ begin
   { rcases exists_compact_subset is_open_univ (mem_univ (1 : G)) with ⟨K, hK⟩,
     exact ⟨K, hK.1, hK.2.1⟩ },
   have K_inf : set.infinite K := infinite_of_mem_nhds (1 : G) (mem_interior_iff_mem_nhds.1 K_int),
-  have μKlt : μ K ≠ ∞ := (K_compact.haar_lt_top μ).ne,
+  have μKlt : μ K ≠ ∞ := K_compact.measure_lt_top.ne,
   have I : ∀ (n : ℕ), μ {(1 : G)} ≤ μ K / n,
   { assume n,
     obtain ⟨t, tK, tn⟩ : ∃ (t : finset G), ↑t ⊆ K ∧ t.card = n := K_inf.exists_subset_card_eq n,

src/measure_theory/group/prod.lean

@@ -197,7 +197,7 @@ begin
     ((λ z, z * x) ⁻¹' E).indicator (λ (b : G), 1) y,
   { intros x y, symmetry, convert indicator_comp_right (λ y, y * x), ext1 z, refl },
   have h3E : ∀ y, ν ((λ x, x * y) ⁻¹' E) ≠ ∞ :=
-    λ y, (regular.lt_top_of_is_compact $ (homeomorph.mul_right _).compact_preimage.mpr hE).ne,
+    λ y, (is_compact.measure_lt_top $ (homeomorph.mul_right _).compact_preimage.mpr hE).ne,
   simp_rw [this, lintegral_mul_const _ (mE _), lintegral_indicator _ (measurable_mul_const _ Em),
     set_lintegral_one, g, inv_inv,
     ennreal.mul_div_cancel' (measure_mul_right_ne_zero hν h2E _) (h3E _)]

src/measure_theory/measure/content.lean

@@ -354,16 +354,16 @@ begin
     rcases hr with ⟨U, hUo, hAU, hr⟩,
     rw [← μ.outer_measure_of_is_open U hUo, ← μ.measure_apply hUo.measurable_set] at hr,
     exact ⟨U, hAU, hUo, hr⟩ },
-  split,
-  { intros K hK,
+  haveI : is_finite_measure_on_compacts μ.measure,
+  { refine ⟨λ K hK, _⟩,
     rw [measure_apply _ hK.measurable_set],
     exact μ.outer_measure_lt_top_of_is_compact hK },
-  { intros U hU r hr,
-    rw [measure_apply _ hU.measurable_set, μ.outer_measure_of_is_open U hU] at hr,
-    simp only [inner_content, lt_supr_iff] at hr,
-    rcases hr with ⟨K, hKU, hr⟩,
-    refine ⟨K.1, hKU, K.2, hr.trans_le _⟩,
-    exact (μ.le_outer_measure_compacts K).trans (le_to_measure_apply _ _ _) },
+  refine ⟨λ U hU r hr, _⟩,
+  rw [measure_apply _ hU.measurable_set, μ.outer_measure_of_is_open U hU] at hr,
+  simp only [inner_content, lt_supr_iff] at hr,
+  rcases hr with ⟨K, hKU, hr⟩,
+  refine ⟨K.1, hKU, K.2, hr.trans_le _⟩,
+  exact (μ.le_outer_measure_compacts K).trans (le_to_measure_apply _ _ _)
 end
 
 end content

src/measure_theory/measure/haar.lean

@@ -609,11 +609,11 @@ theorem is_haar_measure_eq_smul_is_haar_measure
 begin
   have K : positive_compacts G := classical.choice (topological_space.nonempty_positive_compacts G),
   have νpos : 0 < ν K.1 := haar_pos_of_nonempty_interior _ K.2.2,
-  have νlt : ν K.1 < ∞ := is_compact.haar_lt_top _ K.2.1,
+  have νlt : ν K.1 < ∞ := is_compact.measure_lt_top K.2.1,
   refine ⟨μ K.1 / ν K.1, _, _, _⟩,
   { simp only [νlt.ne, (μ.haar_pos_of_nonempty_interior K.property.right).ne', ne.def,
       ennreal.div_zero_iff, not_false_iff, or_self] },
-  { simp only [div_eq_mul_inv, νpos.ne', (is_compact.haar_lt_top μ K.property.left).ne, or_self,
+  { simp only [div_eq_mul_inv, νpos.ne', (is_compact.measure_lt_top K.property.left).ne, or_self,
       ennreal.inv_eq_top, with_top.mul_eq_top_iff, ne.def, not_false_iff, and_false, false_and] },
   { calc
     μ = μ K.1 • haar_measure K : haar_measure_unique (is_mul_left_invariant_haar μ) K
@@ -651,7 +651,7 @@ begin
          rw [one_pow, one_mul] },
   have : c^2 = 1^2 :=
     (ennreal.mul_eq_mul_right (haar_pos_of_nonempty_interior _ K.2.2).ne'
-      (is_compact.haar_lt_top _ K.2.1).ne).1 this,
+      (is_compact.measure_lt_top K.2.1).ne).1 this,
   have : c = 1 := (ennreal.pow_strict_mono two_ne_zero).injective this,
   rw [hc, this, one_smul]
 end

src/measure_theory/measure/haar_lebesgue.lean

@@ -216,16 +216,6 @@ begin
   rw [this, add_haar_preimage_add]
 end
 
-lemma add_haar_closed_ball_lt_top {E : Type*} [normed_group E] [proper_space E] [measurable_space E]
-  (μ : measure E) [is_add_haar_measure μ] (x : E) (r : ℝ) :
-  μ (closed_ball x r) < ∞ :=
-(proper_space.is_compact_closed_ball x r).add_haar_lt_top μ
-
-lemma add_haar_ball_lt_top {E : Type*} [normed_group E] [proper_space E] [measurable_space E]
-  (μ : measure E) [is_add_haar_measure μ] (x : E) (r : ℝ) :
-  μ (ball x r) < ∞ :=
-lt_of_le_of_lt (measure_mono ball_subset_closed_ball) (add_haar_closed_ball_lt_top μ x r)
-
 lemma add_haar_ball_pos {E : Type*} [normed_group E] [measurable_space E]
   (μ : measure E) [is_add_haar_measure μ] (x : E) {r : ℝ} (hr : 0 < r) :
   0 < μ (ball x r) :=
@@ -291,8 +281,9 @@ begin
   { exact (hr rfl).elim },
   { rw [← closed_ball_diff_ball,
         measure_diff ball_subset_closed_ball measurable_set_closed_ball measurable_set_ball
-          ((add_haar_ball_lt_top μ x r).ne),
-        add_haar_ball_of_pos μ _ h, add_haar_closed_ball μ _ h.le, tsub_self] }
+          measure_ball_lt_top.ne,
+        add_haar_ball_of_pos μ _ h, add_haar_closed_ball μ _ h.le, tsub_self];
+    apply_instance }
 end
 
 lemma add_haar_sphere [nontrivial E] (x : E) (r : ℝ) :

src/measure_theory/measure/measure_space.lean

@@ -2185,6 +2185,39 @@ begin
   simp only [ennreal.coe_ne_top, ennreal.coe_of_nnreal_hom, ne.def, not_false_iff],
 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 < ∞)
+
+/-- A compact subset has finite measure for a measure which is finite on compacts. -/
+lemma _root_.is_compact.measure_lt_top
+  [topological_space α] {μ : measure α} [is_finite_measure_on_compacts μ]
+  ⦃K : set α⦄ (hK : is_compact K) : μ K < ∞ :=
+is_finite_measure_on_compacts.lt_top_of_is_compact hK
+
+/-- A bounded subset has finite measure for a measure which is finite on compact sets, in a
+proper space. -/
+lemma _root_.metric.bounded.measure_lt_top [pseudo_metric_space α] [proper_space α]
+  {μ : measure α} [is_finite_measure_on_compacts μ] ⦃s : set α⦄ (hs : metric.bounded s) :
+  μ s < ∞ :=
+calc μ s ≤ μ (closure s) : measure_mono subset_closure
+... < ∞ : (metric.is_compact_of_is_closed_bounded is_closed_closure hs.closure).measure_lt_top
+
+lemma measure_closed_ball_lt_top [pseudo_metric_space α] [proper_space α]
+  {μ : measure α} [is_finite_measure_on_compacts μ] {x : α} {r : ℝ} :
+  μ (metric.closed_ball x r) < ∞ :=
+metric.bounded_closed_ball.measure_lt_top
+
+lemma measure_ball_lt_top [pseudo_metric_space α] [proper_space α]
+  {μ : measure α} [is_finite_measure_on_compacts μ] {x : α} {r : ℝ} :
+  μ (metric.ball x r) < ∞ :=
+metric.bounded_ball.measure_lt_top
+
+protected lemma is_finite_measure_on_compacts.smul [topological_space α] (μ : measure α)
+  [is_finite_measure_on_compacts μ] {c : ℝ≥0∞} (hc : c ≠ ∞) :
+  is_finite_measure_on_compacts (c • μ) :=
+⟨λ K hK, ennreal.mul_lt_top hc (hK.measure_lt_top).ne⟩
+
 omit m0
 
 @[priority 100] -- see Note [lower instance priority]
@@ -2881,9 +2914,9 @@ lemma measure_lt_top_of_nhds_within (h : is_compact s) (hμ : ∀ x ∈ s, μ.fi
 is_compact.induction_on h (by simp) (λ s t hst ht, (measure_mono hst).trans_lt ht)
   (λ s t hs ht, (measure_union_le s t).trans_lt (ennreal.add_lt_top.2 ⟨hs, ht⟩)) hμ
 
-lemma measure_lt_top (h : is_compact s) {μ : measure α} [is_locally_finite_measure μ] :
-  μ s < ∞ :=
-h.measure_lt_top_of_nhds_within $ λ x hx, μ.finite_at_nhds_within _ _
+@[priority 100] -- see Note [lower instance priority]
+instance {μ : measure α} [is_locally_finite_measure μ] : is_finite_measure_on_compacts μ :=
+⟨λ s hs, hs.measure_lt_top_of_nhds_within $ λ x hx, μ.finite_at_nhds_within _ _⟩
 
 lemma measure_zero_of_nhds_within (hs : is_compact s) :
   (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0 :=
@@ -2933,13 +2966,6 @@ lemma measure_Ioo_lt_top : μ (Ioo a b) < ∞ :=
 
 end measure_Ixx
 
-lemma metric.bounded.measure_lt_top [metric_space α] [proper_space α]
-  [measurable_space α] {μ : measure α} [is_locally_finite_measure μ] {s : set α}
-  (hs : metric.bounded s) :
-  μ s < ∞ :=
-(measure_mono subset_closure).trans_lt (metric.compact_iff_closed_bounded.2
-  ⟨is_closed_closure, metric.bounded_closure_of_bounded hs⟩).measure_lt_top
-
 section piecewise
 
 variables [measurable_space α] {μ : measure α} {s t : set α} {f g : α → β}

src/measure_theory/measure/regular.lean

@@ -210,12 +210,12 @@ This definition implies the same equality for any (not necessarily measurable) s
   - it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
   - it is inner regular for open sets, using compact sets:
     `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open. -/
-@[protect_proj] class regular (μ : measure α) extends outer_regular μ : Prop :=
-(lt_top_of_is_compact : ∀ ⦃K : set α⦄, is_compact K → μ K < ∞)
+@[protect_proj] class regular (μ : measure α)
+  extends is_finite_measure_on_compacts μ, outer_regular μ : Prop :=
 (inner_regular : inner_regular μ is_compact is_open)
 
 /-- A measure `μ` is weakly regular if
-  - it is outer regular: `μ(A) = inf { μ(U) | A ⊆ U open }` for `A` measurable;
+  - it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
   - it is inner regular for open sets, using closed sets:
     `μ(U) = sup {μ(F) | F ⊆ U compact}` for `U` open. -/
 @[protect_proj] class weakly_regular (μ : measure α) extends outer_regular μ : Prop :=
@@ -456,7 +456,7 @@ end inner_regular
 namespace regular
 
 instance zero : regular (0 : measure α) :=
-⟨λ K hK, ennreal.coe_lt_top, λ U hU r hr, ⟨∅, empty_subset _, is_compact_empty, hr⟩⟩
+⟨λ U hU r hr, ⟨∅, empty_subset _, is_compact_empty, hr⟩⟩
 
 /-- If `μ` is a regular measure, then any open set can be approximated by a compact subset. -/
 lemma _root_.is_open.exists_lt_is_compact [regular μ] ⦃U : set α⦄ (hU : is_open U)
@@ -521,28 +521,25 @@ protected lemma map [opens_measurable_space α] [measurable_space β] [topologic
   (measure.map f μ).regular :=
 begin
   haveI := outer_regular.map f μ,
-  split,
-  { intros K hK, rw [map_apply f.measurable hK.measurable_set],
-    apply regular.lt_top_of_is_compact,
-    rwa f.compact_preimage },
-  { exact regular.inner_regular.map f.to_equiv f.measurable (λ U hU, hU.preimage f.continuous)
-      (λ K hK, hK.image f.continuous) (λ K hK, hK.measurable_set) (λ U hU, hU.measurable_set) }
+  haveI := is_finite_measure_on_compacts.map μ f,
+  exact ⟨regular.inner_regular.map f.to_equiv f.measurable (λ U hU, hU.preimage f.continuous)
+      (λ K hK, hK.image f.continuous) (λ K hK, hK.measurable_set) (λ U hU, hU.measurable_set)⟩
 end
 
 protected lemma smul [regular μ] {x : ℝ≥0∞} (hx : x ≠ ∞) :
   (x • μ).regular :=
 begin
   haveI := outer_regular.smul μ hx,
-  exact ⟨λ K hK, ennreal.mul_lt_top hx (regular.lt_top_of_is_compact hK).ne,
-    regular.inner_regular.smul x⟩
+  haveI := is_finite_measure_on_compacts.smul μ hx,
+  exact ⟨regular.inner_regular.smul x⟩
 end
 
 /-- A regular measure in a σ-compact space is σ-finite. -/
 @[priority 100] -- see Note [lower instance priority]
 instance sigma_finite [sigma_compact_space α] [regular μ] : sigma_finite μ :=
 ⟨⟨{ set := compact_covering α,
   set_mem := λ n, trivial,
-  finite := λ n, regular.lt_top_of_is_compact $ is_compact_compact_covering α n,
+  finite := λ n, (is_compact_compact_covering α n).measure_lt_top,
   spanning := Union_compact_covering α }⟩⟩
 
 end regular