# mathlibdocumentation

measure_theory.group

# 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.
def measure_theory.is_mul_left_invariant {G : Type u_1} [has_mul G] (μ : set Gℝ≥0∞) :
Prop

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.

Equations
• = ∀ (g : G) {A : set G}, μ ((λ (h : G), g * h) ⁻¹' A) = μ A
def measure_theory.is_add_left_invariant {G : Type u_1} [has_add G] (μ : set Gℝ≥0∞) :
Prop

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 measure_theory.is_add_right_invariant {G : Type u_1} [has_add G] (μ : set Gℝ≥0∞) :
Prop

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 measure_theory.is_mul_right_invariant {G : Type u_1} [has_mul G] (μ : set Gℝ≥0∞) :
Prop

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.

Equations
• = ∀ (g : G) {A : set G}, μ ((λ (h : G), h * g) ⁻¹' A) = μ A
theorem measure_theory.measure.map_add_left_eq_self {G : Type u_1} [has_add G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), = μ)
theorem measure_theory.measure.map_mul_left_eq_self {G : Type u_1} [has_mul G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), = μ)
theorem measure_theory.measure.map_add_right_eq_self {G : Type u_1} [has_add G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), (measure_theory.measure.map (λ (h : G), h + g)) μ = μ)
theorem measure_theory.measure.map_mul_right_eq_self {G : Type u_1} [has_mul G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), (measure_theory.measure.map (λ (h : G), h * g)) μ = μ)
def measure_theory.measure.inv {G : Type u_1} [has_inv G] (μ : measure_theory.measure G) :

The measure A ↦ μ (A⁻¹), where A⁻¹ is the pointwise inverse of A.

Equations
def measure_theory.measure.neg {G : Type u_1} [has_neg G] (μ : measure_theory.measure G) :

The measure A ↦ μ (- A), where - A is the pointwise negation of A.

theorem measure_theory.measure.neg_apply {G : Type u_1} [add_group G] [borel_space G] (μ : measure_theory.measure G) {s : set G} (hs : measurable_set s) :
(μ.neg) s = μ (-s)
theorem measure_theory.measure.inv_apply {G : Type u_1} [group G] [borel_space G] (μ : measure_theory.measure G) {s : set G} (hs : measurable_set s) :
(μ.inv) s = μ s⁻¹
@[simp]
theorem measure_theory.measure.inv_inv {G : Type u_1} [group G] [borel_space G] (μ : measure_theory.measure G) :
μ.inv.inv = μ
@[simp]
theorem measure_theory.measure.neg_neg {G : Type u_1} [add_group G] [borel_space G] (μ : measure_theory.measure G) :
μ.neg.neg = μ
theorem measure_theory.measure.regular.inv {G : Type u_1} [group G] [borel_space G] {μ : measure_theory.measure G} [t2_space G] (hμ : μ.regular) :
@[simp]
@[simp]
@[simp]
@[simp]

Properties of regular left invariant measures

theorem measure_theory.is_mul_left_invariant.null_iff_empty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (hμ : μ.regular) (h3μ : μ 0) {s : set G} (hs : is_open s) :
μ s = 0 s =
theorem measure_theory.measure.is_add_left_invariant.null_iff_empty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (hμ : μ.regular) (h3μ : μ 0) {s : set G} (hs : is_open s) :
μ s = 0 s =
theorem measure_theory.is_mul_left_invariant.null_iff {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (hμ : μ.regular) {s : set G} (hs : is_open s) :
μ s = 0 s = μ = 0
theorem measure_theory.measure.is_add_left_invariant.null_iff {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (hμ : μ.regular) {s : set G} (hs : is_open s) :
μ s = 0 s = μ = 0
theorem measure_theory.measure.is_add_left_invariant.measure_ne_zero_iff_nonempty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (hμ : μ.regular) (h3μ : μ 0) {s : set G} (hs : is_open s) :
theorem measure_theory.is_mul_left_invariant.measure_ne_zero_iff_nonempty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (hμ : μ.regular) (h3μ : μ 0) {s : set G} (hs : is_open s) :
theorem measure_theory.lintegral_eq_zero_of_is_mul_left_invariant {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (hμ : μ.regular) (h3μ : μ 0) {f : G → ℝ≥0∞} (hf : continuous f) :
∫⁻ (x : G), f x μ = 0 f = 0

For nonzero regular left invariant measures, the integral of a continuous nonnegative function f is 0 iff f is 0.

theorem measure_theory.lintegral_mul_left_eq_self {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (g * x) μ = ∫⁻ (x : G), f x μ

Translating a function by left-multiplication does not change its lintegral with respect to a left-invariant measure.

theorem measure_theory.lintegral_add_left_eq_self {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (g + x) μ = ∫⁻ (x : G), f x μ
theorem measure_theory.lintegral_add_right_eq_self {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (x + g) μ = ∫⁻ (x : G), f x μ
theorem measure_theory.lintegral_mul_right_eq_self {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (x * g) μ = ∫⁻ (x : G), f x μ

Translating a function by right-multiplication does not change its lintegral with respect to a right-invariant measure.