mathlib documentation

measure_theory.group.integration

Integration on Groups #

We develop properties of integrals with a group as domain. This file contains properties about integrability, Lebesgue integration and Bochner integration.

theorem measure_theory.integrable.comp_neg {G : Type u_4} {F : Type u_6} [measurable_space G] [normed_add_comm_group F] {μ : measure_theory.measure G} [add_group G] [has_measurable_neg G] [μ.is_neg_invariant] {f : G → F} (hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (t : G), f (-t)) μ
theorem measure_theory.integrable.comp_inv {G : Type u_4} {F : Type u_6} [measurable_space G] [normed_add_comm_group F] {μ : measure_theory.measure G} [group G] [has_measurable_inv G] [μ.is_inv_invariant] {f : G → F} (hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (t : G), f t⁻¹) μ
theorem measure_theory.integral_inv_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] [group G] [has_measurable_inv G] (f : G → E) (μ : measure_theory.measure G) [μ.is_inv_invariant] :
(x : G), f x⁻¹ μ = (x : G), f x μ
theorem measure_theory.integral_neg_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] [add_group G] [has_measurable_neg G] (f : G → E) (μ : measure_theory.measure G) [μ.is_neg_invariant] :
(x : G), f (-x) μ = (x : G), f x μ
theorem measure_theory.lintegral_mul_left_eq_self {G : Type u_4} [measurable_space G] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] [μ.is_mul_left_invariant] (f : G → ennreal) (g : G) :
∫⁻ (x : G), f (g * x) μ = ∫⁻ (x : G), f x μ

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

theorem measure_theory.lintegral_add_left_eq_self {G : Type u_4} [measurable_space G] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] [μ.is_add_left_invariant] (f : G → ennreal) (g : G) :
∫⁻ (x : G), f (g + x) μ = ∫⁻ (x : G), f x μ

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

theorem measure_theory.lintegral_add_right_eq_self {G : Type u_4} [measurable_space G] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] [μ.is_add_right_invariant] (f : G → ennreal) (g : G) :
∫⁻ (x : G), f (x + g) μ = ∫⁻ (x : G), f x μ

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

theorem measure_theory.lintegral_mul_right_eq_self {G : Type u_4} [measurable_space G] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] [μ.is_mul_right_invariant] (f : G → ennreal) (g : G) :
∫⁻ (x : G), f (x * g) μ = ∫⁻ (x : G), f x μ

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

@[simp]
theorem measure_theory.lintegral_sub_right_eq_self {G : Type u_4} [measurable_space G] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] [μ.is_add_right_invariant] (f : G → ennreal) (g : G) :
∫⁻ (x : G), f (x - g) μ = ∫⁻ (x : G), f x μ
@[simp]
theorem measure_theory.lintegral_div_right_eq_self {G : Type u_4} [measurable_space G] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] [μ.is_mul_right_invariant] (f : G → ennreal) (g : G) :
∫⁻ (x : G), f (x / g) μ = ∫⁻ (x : G), f x μ
@[simp]
theorem measure_theory.integral_add_left_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] [μ.is_add_left_invariant] (f : G → E) (g : G) :
(x : G), f (g + x) μ = (x : G), f x μ

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

@[simp]
theorem measure_theory.integral_mul_left_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] [μ.is_mul_left_invariant] (f : G → E) (g : G) :
(x : G), f (g * x) μ = (x : G), f x μ

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

@[simp]
theorem measure_theory.integral_add_right_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] [μ.is_add_right_invariant] (f : G → E) (g : G) :
(x : G), f (x + g) μ = (x : G), f x μ

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

@[simp]
theorem measure_theory.integral_mul_right_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] [μ.is_mul_right_invariant] (f : G → E) (g : G) :
(x : G), f (x * g) μ = (x : G), f x μ

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

@[simp]
theorem measure_theory.integral_div_right_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] [μ.is_mul_right_invariant] (f : G → E) (g : G) :
(x : G), f (x / g) μ = (x : G), f x μ
@[simp]
theorem measure_theory.integral_sub_right_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] [μ.is_add_right_invariant] (f : G → E) (g : G) :
(x : G), f (x - g) μ = (x : G), f x μ
theorem measure_theory.integral_eq_zero_of_add_left_eq_neg {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} {f : G → E} {g : G} [add_group G] [has_measurable_add G] [μ.is_add_left_invariant] (hf' : ∀ (x : G), f (g + x) = -f x) :
(x : G), f x μ = 0

If some left-translate of a function negates it, then the integral of the function with respect to a left-invariant measure is 0.

theorem measure_theory.integral_eq_zero_of_mul_left_eq_neg {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} {f : G → E} {g : G} [group G] [has_measurable_mul G] [μ.is_mul_left_invariant] (hf' : ∀ (x : G), f (g * x) = -f x) :
(x : G), f x μ = 0

If some left-translate of a function negates it, then the integral of the function with respect to a left-invariant measure is 0.

theorem measure_theory.integral_eq_zero_of_add_right_eq_neg {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} {f : G → E} {g : G} [add_group G] [has_measurable_add G] [μ.is_add_right_invariant] (hf' : ∀ (x : G), f (x + g) = -f x) :
(x : G), f x μ = 0

If some right-translate of a function negates it, then the integral of the function with respect to a right-invariant measure is 0.

theorem measure_theory.integral_eq_zero_of_mul_right_eq_neg {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure G} {f : G → E} {g : G} [group G] [has_measurable_mul G] [μ.is_mul_right_invariant] (hf' : ∀ (x : G), f (x * g) = -f x) :
(x : G), f x μ = 0

If some right-translate of a function negates it, then the integral of the function with respect to a right-invariant measure is 0.

theorem measure_theory.integrable.comp_mul_left {G : Type u_4} {F : Type u_6} [measurable_space G] [normed_add_comm_group F] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] {f : G → F} [μ.is_mul_left_invariant] (hf : measure_theory.integrable f μ) (g : G) :
measure_theory.integrable (λ (t : G), f (g * t)) μ
theorem measure_theory.integrable.comp_add_left {G : Type u_4} {F : Type u_6} [measurable_space G] [normed_add_comm_group F] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] {f : G → F} [μ.is_add_left_invariant] (hf : measure_theory.integrable f μ) (g : G) :
measure_theory.integrable (λ (t : G), f (g + t)) μ
theorem measure_theory.integrable.comp_mul_right {G : Type u_4} {F : Type u_6} [measurable_space G] [normed_add_comm_group F] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] {f : G → F} [μ.is_mul_right_invariant] (hf : measure_theory.integrable f μ) (g : G) :
measure_theory.integrable (λ (t : G), f (t * g)) μ
theorem measure_theory.integrable.comp_add_right {G : Type u_4} {F : Type u_6} [measurable_space G] [normed_add_comm_group F] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] {f : G → F} [μ.is_add_right_invariant] (hf : measure_theory.integrable f μ) (g : G) :
measure_theory.integrable (λ (t : G), f (t + g)) μ
theorem measure_theory.integrable.comp_sub_right {G : Type u_4} {F : Type u_6} [measurable_space G] [normed_add_comm_group F] {μ : measure_theory.measure G} [add_group G] [has_measurable_add G] {f : G → F} [μ.is_add_right_invariant] (hf : measure_theory.integrable f μ) (g : G) :
measure_theory.integrable (λ (t : G), f (t - g)) μ
theorem measure_theory.integrable.comp_div_right {G : Type u_4} {F : Type u_6} [measurable_space G] [normed_add_comm_group F] {μ : measure_theory.measure G} [group G] [has_measurable_mul G] {f : G → F} [μ.is_mul_right_invariant] (hf : measure_theory.integrable f μ) (g : G) :
measure_theory.integrable (λ (t : G), f (t / g)) μ
@[simp]
theorem measure_theory.integral_sub_left_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] [add_group G] [has_measurable_add G] [has_measurable_neg G] (f : G → E) (μ : measure_theory.measure G) [μ.is_neg_invariant] [μ.is_add_left_invariant] (x' : G) :
(x : G), f (x' - x) μ = (x : G), f x μ
@[simp]
theorem measure_theory.integral_div_left_eq_self {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] [group G] [has_measurable_mul G] [has_measurable_inv G] (f : G → E) (μ : measure_theory.measure G) [μ.is_inv_invariant] [μ.is_mul_left_invariant] (x' : G) :
(x : G), f (x' / x) μ = (x : G), f x μ
@[simp]
theorem measure_theory.integral_smul_eq_self {α : Type u_3} {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] [group G] [measurable_space α] [mul_action G α] [has_measurable_smul G α] {μ : measure_theory.measure α} [measure_theory.smul_invariant_measure G α μ] (f : α → E) {g : G} :
(x : α), f (g x) μ = (x : α), f x μ
@[simp]
theorem measure_theory.integral_vadd_eq_self {α : Type u_3} {G : Type u_4} {E : Type u_5} [measurable_space G] [normed_add_comm_group E] [normed_space E] [complete_space E] [add_group G] [measurable_space α] [add_action G α] [has_measurable_vadd G α] {μ : measure_theory.measure α} [measure_theory.vadd_invariant_measure G α μ] (f : α → E) {g : G} :
(x : α), f (g +ᵥ x) μ = (x : α), f x μ

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

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