mathlib3 documentation

measure_theory.group.integration

Integration on Groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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.

@[simp]
@[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.