<commit_before>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import measure_theory.integral.lebesgue
import measure_theory.measure.regular

/-!
# 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 measure `μ.inv : A ↦ μ(A⁻¹)` and show that it is right invariant iff
  `μ` is left invariant.
* We define a class `is_haar_measure μ`, requiring that the measure `μ` is left-invariant, finite
  on compact sets, and positive on open sets.

We also give analogues of all these notions in the additive world.
-/

noncomputable theory

open_locale ennreal pointwise big_operators
open has_inv set function measure_theory.measure

namespace measure_theory

variables {G : Type*}

section

variables [measurable_space G] [has_mul G]

/-- A measure `μ` on a topological group is left invariant
  if the measure of left translations of a set are equal to the measure of the set itself.
  To left translate sets we use preimage under left multiplication,
  since preimages are nicer to work with than images. -/
@[to_additive "A measure on a topological group is left invariant
  if the measure of left translations of a set are equal to the measure of the set itself.
  To left translate sets we use preimage under left addition,
  since preimages are nicer to work with than images."]
def is_mul_left_invariant (μ : set G → ℝ≥0∞) : Prop :=
∀ (g : G) {A : set G} (h : measurable_set A), μ ((λ h, g * h) ⁻¹' A) = μ A

/-- A measure `μ` on a topological group is right invariant
  if the measure of right translations of a set are equal to the measure of the set itself.
  To right translate sets we use preimage under right multiplication,
  since preimages are nicer to work with than images. -/
@[to_additive "A measure on a topological group is right invariant
  if the measure of right translations of a set are equal to the measure of the set itself.
  To right translate sets we use preimage under right addition,
  since preimages are nicer to work with than images."]
def is_mul_right_invariant (μ : set G → ℝ≥0∞) : Prop :=
∀ (g : G) {A : set G} (h : measurable_set A), μ ((λ h, h * g) ⁻¹' A) = μ A

@[to_additive measure_theory.is_add_left_invariant.smul]
lemma is_mul_left_invariant.smul {μ : measure G} (h : is_mul_left_invariant μ) (c : ℝ≥0∞) :
  is_mul_left_invariant ((c • μ : measure G) : set G → ℝ≥0∞) :=
λ g A hA, by rw [smul_apply, smul_apply, h g hA]

@[to_additive measure_theory.is_add_right_invariant.smul]
lemma is_mul_right_invariant.smul {μ : measure G} (h : is_mul_right_invariant μ) (c : ℝ≥0∞) :
  is_mul_right_invariant ((c • μ : measure G) : set G → ℝ≥0∞) :=
λ g A hA, by rw [smul_apply, smul_apply, h g hA]

end

namespace measure

variables [measurable_space G]

@[to_additive]
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_mul_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_const_mul g) hA]
end

@[to_additive]
lemma _root_.measure_theory.is_mul_left_invariant.measure_preimage_mul
  [topological_space G] [group G] [topological_group G] [borel_space G]
  {μ : measure G} (h : is_mul_left_invariant μ) (g : G) (A : set G) :
  μ ((λ h, g * h) ⁻¹' A) = μ A :=
calc μ ((λ h, g * h) ⁻¹' A) = measure.map (λ h, g * h) μ A :
  ((homeomorph.mul_left g).to_measurable_equiv.map_apply A).symm
... = μ A : by rw map_mul_left_eq_self.2 h g

@[to_additive]
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_mul_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_const g) hA]
end

/-- The measure `A ↦ μ (A⁻¹)`, where `A⁻¹` is the pointwise inverse of `A`. -/
@[to_additive "The measure `A ↦ μ (- A)`, where `- A` is the pointwise negation of `A`."]
protected def inv [has_inv G] (μ : measure G) : measure G :=
measure.map inv μ

variables [group G] [topological_space G] [topological_group G] [borel_space G]

@[to_additive]
lemma inv_apply (μ : measure G) {s : set G} (hs : measurable_set s) :
  μ.inv s = μ s⁻¹ :=
measure.map_apply measurable_inv hs

@[simp, to_additive] protected lemma inv_inv (μ : measure G) : μ.inv.inv = μ :=
begin
  ext1 s hs, rw [μ.inv.inv_apply hs, μ.inv_apply, set.inv_inv],
  exact measurable_inv hs
end

variables {μ : measure G}

@[to_additive]
instance regular.inv [t2_space G] [regular μ] : regular μ.inv :=
regular.map (homeomorph.inv G)

end measure

section inv
variables [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G]
  {μ : measure G}

@[simp, to_additive] lemma regular_inv_iff [t2_space G] : μ.inv.regular ↔ μ.regular :=
begin
  split,
  { introI h,
    rw ←μ.inv_inv,
    exact measure.regular.inv },
  { introI h,
    exact measure.regular.inv }
end

@[to_additive]
lemma is_mul_left_invariant.inv (h : is_mul_left_invariant μ) :
  is_mul_right_invariant μ.inv :=
begin
  intros g A hA,
  rw [μ.inv_apply (measurable_mul_const g hA), μ.inv_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

@[to_additive]
lemma is_mul_right_invariant.inv (h : is_mul_right_invariant μ) : is_mul_left_invariant μ.inv :=
begin
  intros g A hA,
  rw [μ.inv_apply (measurable_const_mul g hA), μ.inv_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, to_additive]
lemma is_mul_right_invariant_inv : is_mul_right_invariant μ.inv ↔ is_mul_left_invariant μ :=
⟨λ h, by { rw ← μ.inv_inv, exact h.inv }, λ h, h.inv⟩

@[simp, to_additive]<commit_msg>chore(measure_theory/group/basic): drop measurability assumption (#10367)<commit_after>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import measure_theory.integral.lebesgue
import measure_theory.measure.regular
import measure_theory.group.measurable_equiv

/-!
# 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 measure `μ.inv : A ↦ μ(A⁻¹)` and show that it is right invariant iff
  `μ` is left invariant.
* We define a class `is_haar_measure μ`, requiring that the measure `μ` is left-invariant, finite
  on compact sets, and positive on open sets.

We also give analogues of all these notions in the additive world.
-/

noncomputable theory

open_locale ennreal pointwise big_operators
open has_inv set function measure_theory.measure

namespace measure_theory

variables {G : Type*}

section

variables [measurable_space G] [has_mul G]

/-- A measure `μ` on a topological group is left invariant
  if the measure of left translations of a set are equal to the measure of the set itself.
  To left translate sets we use preimage under left multiplication,
  since preimages are nicer to work with than images. -/
@[to_additive "A measure on a topological group is left invariant
  if the measure of left translations of a set are equal to the measure of the set itself.
  To left translate sets we use preimage under left addition,
  since preimages are nicer to work with than images."]
def is_mul_left_invariant (μ : set G → ℝ≥0∞) : Prop :=
∀ (g : G) {A : set G} (h : measurable_set A), μ ((λ h, g * h) ⁻¹' A) = μ A

/-- A measure `μ` on a topological group is right invariant
  if the measure of right translations of a set are equal to the measure of the set itself.
  To right translate sets we use preimage under right multiplication,
  since preimages are nicer to work with than images. -/
@[to_additive "A measure on a topological group is right invariant
  if the measure of right translations of a set are equal to the measure of the set itself.
  To right translate sets we use preimage under right addition,
  since preimages are nicer to work with than images."]
def is_mul_right_invariant (μ : set G → ℝ≥0∞) : Prop :=
∀ (g : G) {A : set G} (h : measurable_set A), μ ((λ h, h * g) ⁻¹' A) = μ A

@[to_additive measure_theory.is_add_left_invariant.smul]
lemma is_mul_left_invariant.smul {μ : measure G} (h : is_mul_left_invariant μ) (c : ℝ≥0∞) :
  is_mul_left_invariant ((c • μ : measure G) : set G → ℝ≥0∞) :=
λ g A hA, by rw [smul_apply, smul_apply, h g hA]

@[to_additive measure_theory.is_add_right_invariant.smul]
lemma is_mul_right_invariant.smul {μ : measure G} (h : is_mul_right_invariant μ) (c : ℝ≥0∞) :
  is_mul_right_invariant ((c • μ : measure G) : set G → ℝ≥0∞) :=
λ g A hA, by rw [smul_apply, smul_apply, h g hA]

end

namespace measure

variables [measurable_space G]

@[to_additive]
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_mul_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_const_mul g) hA]
end

@[to_additive]
lemma _root_.measure_theory.is_mul_left_invariant.measure_preimage_mul
  [topological_space G] [group G] [topological_group G] [borel_space G]
  {μ : measure G} (h : is_mul_left_invariant μ) (g : G) (A : set G) :
  μ ((λ h, g * h) ⁻¹' A) = μ A :=
calc μ ((λ h, g * h) ⁻¹' A) = measure.map (λ h, g * h) μ A :
  ((homeomorph.mul_left g).to_measurable_equiv.map_apply A).symm
... = μ A : by rw map_mul_left_eq_self.2 h g

@[to_additive]
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_mul_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_const g) hA]
end

/-- The measure `A ↦ μ (A⁻¹)`, where `A⁻¹` is the pointwise inverse of `A`. -/
@[to_additive "The measure `A ↦ μ (- A)`, where `- A` is the pointwise negation of `A`."]
protected def inv [has_inv G] (μ : measure G) : measure G :=
measure.map inv μ

variables [group G] [topological_space G] [topological_group G] [borel_space G]

@[to_additive]
lemma inv_apply (μ : measure G) (s : set G) :
  μ.inv s = μ s⁻¹ :=
(measurable_equiv.inv G).map_apply s

@[simp, to_additive] protected lemma inv_inv (μ : measure G) : μ.inv.inv = μ :=
(measurable_equiv.inv G).map_symm_map

variables {μ : measure G}

@[to_additive]
instance regular.inv [t2_space G] [regular μ] : regular μ.inv :=
regular.map (homeomorph.inv G)

end measure

section inv
variables [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G]
  {μ : measure G}

@[simp, to_additive] lemma regular_inv_iff [t2_space G] : μ.inv.regular ↔ μ.regular :=
begin
  split,
  { introI h,
    rw ←μ.inv_inv,
    exact measure.regular.inv },
  { introI h,
    exact measure.regular.inv }
end

@[to_additive]
lemma is_mul_left_invariant.inv (h : is_mul_left_invariant μ) :
  is_mul_right_invariant μ.inv :=
begin
  intros g A hA,
  rw [μ.inv_apply, μ.inv_apply],
  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

@[to_additive]
lemma is_mul_right_invariant.inv (h : is_mul_right_invariant μ) : is_mul_left_invariant μ.inv :=
begin
  intros g A hA,
  rw [μ.inv_apply, μ.inv_apply],
  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, to_additive]
lemma is_mul_right_invariant_inv : is_mul_right_invariant μ.inv ↔ is_mul_left_invariant μ :=
⟨λ h, by { rw ← μ.inv_inv, exact h.inv }, λ h, h.inv⟩

@[simp, to_additive]
{'fraction_non_alphanumeric': 0.10316815597075549, 'fraction_numerical': 0.003249390739236393, 'mean_word_length': 4.21431596781025, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3500911', 'n_tokens_mistral': 4822, 'n_tokens_neox': 4525, 'n_words': 1657}