refactor(measure_theory/haar_measure): move general material to content.lean, make content a structure (#7615)

Several facts that are proved only for the Haar measure (including for instance regularity) are true for any measure constructed from a content. We move these facts to the `content.lean` file (and make `content` a structure for easier management). Also, move the notion of regular measure to its own file, and make it a class.

Author: sgouezel

src/measure_theory/borel_space.lean

@@ -21,7 +21,6 @@ import measure_theory.arithmetic
   structures such that all open sets are measurable; equivalently, `borel α ≤ ‹measurable_space α›`.
 * `borel_space` instances on `empty`, `unit`, `bool`, `nat`, `int`, `rat`;
 * `measurable` and `borel_space` instances on `ℝ`, `ℝ≥0`, `ℝ≥0∞`.
-* A measure is `regular` if it is finite on compact sets, inner regular and outer regular.
 
 ## Main statements
 
@@ -1341,88 +1340,6 @@ ae_measurable_comp_iff_of_closed_embedding (λ y : 𝕜, y • c) (closed_embedd
 
 end normed_space
 
-namespace measure_theory
-namespace measure
-
-variables [topological_space α] {μ : measure α}
-
-/-- A measure `μ` is regular if
-  - it is finite on all compact sets;
-  - it is outer regular: `μ(A) = inf { μ(U) | A ⊆ U open }` for `A` measurable;
-  - it is inner regular: `μ(U) = sup { μ(K) | K ⊆ U compact }` for `U` open. -/
-structure regular (μ : measure α) : Prop :=
-(lt_top_of_is_compact : ∀ {{K : set α}}, is_compact K → μ K < ∞)
-(outer_regular : ∀ {{A : set α}}, measurable_set A →
-  (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), μ U) ≤ μ A)
-(inner_regular : ∀ {{U : set α}}, is_open U →
-  μ U ≤ ⨆ (K : set α) (h : is_compact K) (h2 : K ⊆ U), μ K)
-
-namespace regular
-
-lemma outer_regular_eq (hμ : μ.regular) {{A : set α}}
-  (hA : measurable_set A) : (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), μ U) = μ A :=
-le_antisymm (hμ.outer_regular hA) $ le_infi $ λ s, le_infi $ λ hs, le_infi $ λ h2s, μ.mono h2s
-
-lemma inner_regular_eq (hμ : μ.regular) {{U : set α}}
-  (hU : is_open U) : (⨆ (K : set α) (h : is_compact K) (h2 : K ⊆ U), μ K) = μ U :=
-le_antisymm (supr_le $ λ s, supr_le $ λ hs, supr_le $ λ h2s, μ.mono h2s) (hμ.inner_regular hU)
-
-lemma exists_compact_not_null (hμ : regular μ) : (∃ K, is_compact K ∧ μ K ≠ 0) ↔ μ ≠ 0 :=
-by simp_rw [ne.def, ← measure_univ_eq_zero, ← hμ.inner_regular_eq is_open_univ,
-    ennreal.supr_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-
-protected lemma map [opens_measurable_space α] [measurable_space β] [topological_space β]
-  [t2_space β] [borel_space β] (hμ : μ.regular) (f : α ≃ₜ β) :
-  (measure.map f μ).regular :=
-begin
-  have hf := f.measurable,
-  have h2f := f.to_equiv.injective.preimage_surjective,
-  have h3f := f.to_equiv.surjective,
-  split,
-  { intros K hK, rw [map_apply hf hK.measurable_set],
-    apply hμ.lt_top_of_is_compact, rwa f.compact_preimage },
-  { intros A hA, rw [map_apply hf hA, ← hμ.outer_regular_eq (hf hA)],
-    refine le_of_eq _, apply infi_congr (preimage f) h2f,
-    intro U, apply infi_congr_Prop f.is_open_preimage, intro hU,
-    apply infi_congr_Prop h3f.preimage_subset_preimage_iff, intro h2U,
-    rw [map_apply hf hU.measurable_set], },
-  { intros U hU,
-    rw [map_apply hf hU.measurable_set, ← hμ.inner_regular_eq (hU.preimage f.continuous)],
-    refine ge_of_eq _, apply supr_congr (preimage f) h2f,
-    intro K, apply supr_congr_Prop f.compact_preimage, intro hK,
-    apply supr_congr_Prop h3f.preimage_subset_preimage_iff, intro h2U,
-    rw [map_apply hf hK.measurable_set] }
-end
-
-protected lemma smul (hμ : μ.regular) {x : ℝ≥0∞} (hx : x < ∞) :
-  (x • μ).regular :=
-begin
-  split,
-  { intros K hK, exact ennreal.mul_lt_top hx (hμ.lt_top_of_is_compact hK) },
-  { intros A hA, rw [coe_smul],
-    refine le_trans _ (ennreal.mul_left_mono $ hμ.outer_regular hA),
-    simp only [infi_and'], simp only [infi_subtype'],
-    haveI : nonempty {s : set α // is_open s ∧ A ⊆ s} := ⟨⟨set.univ, is_open_univ, subset_univ _⟩⟩,
-    rw [ennreal.mul_infi], refl', exact ne_of_lt hx },
-  { intros U hU, rw [coe_smul], refine le_trans (ennreal.mul_left_mono $ hμ.inner_regular hU) _,
-    simp only [supr_and'], simp only [supr_subtype'],
-    rw [ennreal.mul_supr], refl' }
-end
-
-/-- A regular measure in a σ-compact space is σ-finite. -/
-protected lemma sigma_finite [opens_measurable_space α] [t2_space α] [sigma_compact_space α]
-  (hμ : regular μ) : sigma_finite μ :=
-⟨⟨{ set := compact_covering α,
-  set_mem := λ n, (is_compact_compact_covering α n).measurable_set,
-  finite := λ n, hμ.lt_top_of_is_compact $ is_compact_compact_covering α n,
-  spanning := Union_compact_covering α }⟩⟩
-
-
-end regular
-
-end measure
-end measure_theory
-
 lemma is_compact.measure_lt_top_of_nhds_within [topological_space α]
   {s : set α} {μ : measure α} (h : is_compact s) (hμ : ∀ x ∈ s, μ.finite_at_filter (𝓝[s] x)) :
   μ s < ∞ :=