From d9a6e478571a4f12a18960cc10f72412a4dcdd0c Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Tue, 4 Aug 2020 02:05:22 +0000
Subject: [PATCH] feat(measure_theory/group): regular, invariant, and conjugate
 measures (#3650)

Define the notion of a regular measure. I did this in Borel space, which required me to add an import measure_space -> borel_space.
Define left invariant and right invariant measures for groups
Define the conjugate measure, and show it is left invariant iff the original is right invariant
---
 src/measure_theory/borel_space.lean   |  71 +++++++++++++++-
 src/measure_theory/group.lean         | 115 ++++++++++++++++++++++++++
 src/measure_theory/measure_space.lean |   4 +
 3 files changed, 189 insertions(+), 1 deletion(-)
 create mode 100644 src/measure_theory/group.lean

diff --git a/src/measure_theory/borel_space.lean b/src/measure_theory/borel_space.lean
index 31aca6a8563dc..a80e045f8a71e 100644
--- a/src/measure_theory/borel_space.lean
+++ b/src/measure_theory/borel_space.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury Kudryashov
 -/
-import measure_theory.measurable_space
+import measure_theory.measure_space
 import topology.instances.ennreal
 import analysis.normed_space.basic
 
@@ -19,6 +19,7 @@ import analysis.normed_space.basic
   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`, `ennreal`.
+* A measure is `regular` if it is finite on compact sets, inner regular and outer regular.
 
 ## Main statements
 
@@ -712,3 +713,71 @@ lemma measurable.ennnorm {f : β → α} (hf : measurable f) :
 hf.nnnorm.ennreal_coe
 
 end normed_group
+
+namespace measure_theory
+namespace measure
+
+variables [measurable_space α] [topological_space α]
+
+/-- 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 α}}, is_measurable 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 {μ : measure α} (hμ : μ.regular) {{A : set α}}
+  (hA : is_measurable 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 {μ : measure α} (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)
+
+protected lemma map [opens_measurable_space α] [measurable_space β] [topological_space β]
+  [t2_space β] [borel_space β] {μ : measure α} (hμ : μ.regular) (f : α ≃ₜ β) :
+  (measure.map f μ).regular :=
+begin
+  have hf := f.continuous.measurable,
+  have h2f := f.to_equiv.injective.preimage_surjective,
+  have h3f := f.to_equiv.surjective,
+  split,
+  { intros K hK, rw [map_apply hf hK.is_measurable],
+    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.is_measurable], },
+  { intros U hU, rw [map_apply hf hU.is_measurable, ← hμ.inner_regular_eq (f.continuous U hU)],
+    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.is_measurable] }
+end
+
+protected lemma smul {μ : measure α} (hμ : μ.regular) {x : ennreal} (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
+
+end regular
+
+end measure
+end measure_theory
diff --git a/src/measure_theory/group.lean b/src/measure_theory/group.lean
new file mode 100644
index 0000000000000..febdb5faa917b
--- /dev/null
+++ b/src/measure_theory/group.lean
@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import measure_theory.borel_space
+/-!
+# Measures on Groups
+
+We develop some properties of measures on (topological) groups
+
+* We define properties on measures: left and right invariant measures
+* We define the conjugate `A ↦ μ (A⁻¹)` of a measure `μ`, and show that it is right invariant iff
+  `μ` is left invariant
+-/
+noncomputable theory
+
+open has_inv set function
+
+namespace measure_theory
+
+variables {G : Type*}
+
+section
+
+variables [measurable_space G] [has_mul G]
+
+/-- A measure `μ` on a topological group is left invariant if
+  for all measurable sets `s` and all `g`, we have `μ (gs) = μ s`,
+  where `gs` denotes the translate of `s` by left multiplication with `g`. -/
+def is_left_invariant (μ : set G → ennreal) : Prop :=
+∀ (g : G) {A : set G} (h : is_measurable A), μ ((λ h, g * h) ⁻¹' A) = μ A
+
+/-- A measure `μ` on a topological group is right invariant if
+  for all measurable sets `s` and all `g`, we have `μ (sg) = μ s`,
+  where `sg` denotes the translate of `s` by right multiplication with `g`. -/
+def is_right_invariant (μ : set G → ennreal) : Prop :=
+∀ (g : G) {A : set G} (h : is_measurable A), μ ((λ h, h * g) ⁻¹' A) = μ A
+
+end
+
+namespace measure
+
+variables [measurable_space G]
+
+lemma map_mul_left_eq_self [topological_space G] [has_mul G] [has_continuous_mul G] [borel_space G]
+  {μ : measure G} : (∀ g, measure.map ((*) g) μ = μ) ↔ is_left_invariant μ :=
+begin
+  apply forall_congr, intro g, rw [measure.ext_iff], apply forall_congr, intro A,
+  apply forall_congr, intro hA, rw [map_apply (measurable_mul_left g) hA]
+end
+
+lemma map_mul_right_eq_self [topological_space G] [has_mul G] [has_continuous_mul G] [borel_space G]
+  {μ : measure G} : (∀ g, measure.map (λ h, h * g) μ = μ) ↔ is_right_invariant μ :=
+begin
+  apply forall_congr, intro g, rw [measure.ext_iff], apply forall_congr, intro A,
+  apply forall_congr, intro hA, rw [map_apply (measurable_mul_right g) hA]
+end
+
+/-- The conjugate of a measure on a topological group.
+  Defined to be `A ↦ μ (A⁻¹)`, where `A⁻¹` is the pointwise inverse of `A`. -/
+protected def conj [group G] (μ : measure G) : measure G :=
+measure.map inv μ
+
+variables [group G] [topological_space G] [topological_group G] [borel_space G]
+
+lemma conj_apply (μ : measure G) {s : set G} (hs : is_measurable s) :
+  μ.conj s = μ s⁻¹ :=
+by { unfold measure.conj, rw [measure.map_apply measurable_inv hs, inv_preimage] }
+
+@[simp] lemma conj_conj (μ : measure G) : μ.conj.conj = μ :=
+begin
+  ext1 s hs, rw [μ.conj.conj_apply hs, μ.conj_apply, set.inv_inv], exact measurable_inv hs
+end
+
+variables {μ : measure G}
+
+lemma regular.conj [t2_space G] (hμ : μ.regular) : μ.conj.regular :=
+hμ.map (homeomorph.inv G)
+
+end measure
+
+section conj
+variables [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G]
+  {μ : measure G}
+
+@[simp] lemma regular_conj_iff [t2_space G] : μ.conj.regular ↔ μ.regular :=
+by { refine ⟨λ h, _, measure.regular.conj⟩, rw ←μ.conj_conj, exact measure.regular.conj h }
+
+lemma is_right_invariant_conj' (h : is_left_invariant μ) :
+  is_right_invariant μ.conj :=
+begin
+  intros g A hA, rw [μ.conj_apply (measurable_mul_right g hA), μ.conj_apply hA],
+  convert h g⁻¹ (measurable_inv hA) using 2,
+  simp only [←preimage_comp, ← inv_preimage],
+  apply preimage_congr, intro h, simp only [mul_inv_rev, comp_app, inv_inv]
+end
+
+lemma is_left_invariant_conj' (h : is_right_invariant μ) : is_left_invariant μ.conj :=
+begin
+  intros g A hA, rw [μ.conj_apply (measurable_mul_left g hA), μ.conj_apply hA],
+  convert h g⁻¹ (measurable_inv hA) using 2,
+  simp only [←preimage_comp, ← inv_preimage],
+  apply preimage_congr, intro h, simp only [mul_inv_rev, comp_app, inv_inv]
+end
+
+@[simp] lemma is_right_invariant_conj : is_right_invariant μ.conj ↔ is_left_invariant μ :=
+by { refine ⟨λ h, _, is_right_invariant_conj'⟩, rw ←μ.conj_conj, exact is_left_invariant_conj' h }
+
+@[simp] lemma is_left_invariant_conj : is_left_invariant μ.conj ↔ is_right_invariant μ :=
+by { refine ⟨λ h, _, is_left_invariant_conj'⟩, rw ←μ.conj_conj, exact is_right_invariant_conj' h }
+
+end conj
+
+end measure_theory
diff --git a/src/measure_theory/measure_space.lean b/src/measure_theory/measure_space.lean
index 12a1474d4e919..51594b3e25665 100644
--- a/src/measure_theory/measure_space.lean
+++ b/src/measure_theory/measure_space.lean
@@ -137,6 +137,10 @@ lemma to_outer_measure_injective {α} [measurable_space α] :
   μ₁ = μ₂ :=
 to_outer_measure_injective $ by rw [← trimmed, outer_measure.trim_congr h, trimmed]
 
+lemma ext_iff {α} [measurable_space α] {μ₁ μ₂ : measure α} :
+  μ₁ = μ₂ ↔ ∀s, is_measurable s → μ₁ s = μ₂ s :=
+⟨by { rintro rfl s hs, refl }, measure.ext⟩
+
 end measure
 
 section