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.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] :
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] :
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) :
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) :
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) :
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) :
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) :
@[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) :
@[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) :
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) :
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) :
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) :
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) :
@[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) :
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) :
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) :
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) :
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) :
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)) μ
theorem
measure_theory.integrable.comp_div_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]
[has_measurable_inv G]
{f : G → F}
[μ.is_inv_invariant]
[μ.is_mul_left_invariant]
(hf : measure_theory.integrable f μ)
(g : G) :
measure_theory.integrable (λ (t : G), f (g / t)) μ
theorem
measure_theory.integrable.comp_sub_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]
[has_measurable_neg G]
{f : G → F}
[μ.is_neg_invariant]
[μ.is_add_left_invariant]
(hf : measure_theory.integrable f μ)
(g : G) :
measure_theory.integrable (λ (t : G), f (g - t)) μ
@[simp]
theorem
measure_theory.integrable_comp_div_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]
[has_measurable_inv G]
(f : G → F)
[μ.is_inv_invariant]
[μ.is_mul_left_invariant]
(g : G) :
measure_theory.integrable (λ (t : G), f (g / t)) μ ↔ measure_theory.integrable f μ
@[simp]
theorem
measure_theory.integrable_comp_sub_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]
[has_measurable_neg G]
(f : G → F)
[μ.is_neg_invariant]
[μ.is_add_left_invariant]
(g : G) :
measure_theory.integrable (λ (t : G), f (g - t)) μ ↔ measure_theory.integrable f μ
@[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) :
@[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) :
@[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} :
@[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} :
theorem
measure_theory.lintegral_eq_zero_of_is_add_left_invariant
{G : Type u_4}
[measurable_space G]
{μ : measure_theory.measure G}
[topological_space G]
[add_group G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.regular]
(hμ : μ ≠ 0)
{f : G → ennreal}
(hf : continuous f) :
For nonzero regular left invariant measures, the integral of a continuous nonnegative
function f is 0 iff f is 0.
theorem
measure_theory.lintegral_eq_zero_of_is_mul_left_invariant
{G : Type u_4}
[measurable_space G]
{μ : measure_theory.measure G}
[topological_space G]
[group G]
[topological_group G]
[borel_space G]
[μ.is_mul_left_invariant]
[μ.regular]
(hμ : μ ≠ 0)
{f : G → ennreal}
(hf : continuous f) :
For nonzero regular left invariant measures, the integral of a continuous nonnegative function
f is 0 iff f is 0.