# Documentation

Mathlib.MeasureTheory.Group.Integral

# Bochner Integration on Groups #

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

theorem MeasureTheory.Integrable.comp_neg {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} (hf : ) :
theorem MeasureTheory.Integrable.comp_inv {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} (hf : ) :
theorem MeasureTheory.integral_neg_eq_self {G : Type u_4} {E : Type u_5} [] [] [] [] (f : GE) (μ : ) :
∫ (x : G), f (-x)μ = ∫ (x : G), f xμ
theorem MeasureTheory.integral_inv_eq_self {G : Type u_4} {E : Type u_5} [] [] [] [] (f : GE) (μ : ) :
∫ (x : G), f x⁻¹μ = ∫ (x : G), f xμ
theorem MeasureTheory.integral_add_left_eq_self {G : Type u_4} {E : Type u_5} [] [] {μ : } [] [] (f : GE) (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.

theorem MeasureTheory.integral_mul_left_eq_self {G : Type u_4} {E : Type u_5} [] [] {μ : } [] [] (f : GE) (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.

theorem MeasureTheory.integral_add_right_eq_self {G : Type u_4} {E : Type u_5} [] [] {μ : } [] [] (f : GE) (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.

theorem MeasureTheory.integral_mul_right_eq_self {G : Type u_4} {E : Type u_5} [] [] {μ : } [] [] (f : GE) (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.

theorem MeasureTheory.integral_sub_right_eq_self {G : Type u_4} {E : Type u_5} [] [] {μ : } [] [] (f : GE) (g : G) :
∫ (x : G), f (x - g)μ = ∫ (x : G), f xμ
theorem MeasureTheory.integral_div_right_eq_self {G : Type u_4} {E : Type u_5} [] [] {μ : } [] [] (f : GE) (g : G) :
∫ (x : G), f (x / g)μ = ∫ (x : G), f xμ
theorem MeasureTheory.integral_eq_zero_of_add_left_eq_neg {G : Type u_4} {E : Type u_5} [] [] {μ : } {f : GE} {g : G} [] [] (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 MeasureTheory.integral_eq_zero_of_mul_left_eq_neg {G : Type u_4} {E : Type u_5} [] [] {μ : } {f : GE} {g : G} [] [] (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 MeasureTheory.integral_eq_zero_of_add_right_eq_neg {G : Type u_4} {E : Type u_5} [] [] {μ : } {f : GE} {g : G} [] [] (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 MeasureTheory.integral_eq_zero_of_mul_right_eq_neg {G : Type u_4} {E : Type u_5} [] [] {μ : } {f : GE} {g : G} [] [] (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 MeasureTheory.Integrable.comp_add_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} (hf : ) (g : G) :
MeasureTheory.Integrable fun t => f (g + t)
theorem MeasureTheory.Integrable.comp_mul_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} (hf : ) (g : G) :
MeasureTheory.Integrable fun t => f (g * t)
theorem MeasureTheory.Integrable.comp_add_right {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} (hf : ) (g : G) :
MeasureTheory.Integrable fun t => f (t + g)
theorem MeasureTheory.Integrable.comp_mul_right {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} (hf : ) (g : G) :
MeasureTheory.Integrable fun t => f (t * g)
theorem MeasureTheory.Integrable.comp_sub_right {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} (hf : ) (g : G) :
MeasureTheory.Integrable fun t => f (t - g)
theorem MeasureTheory.Integrable.comp_div_right {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} (hf : ) (g : G) :
MeasureTheory.Integrable fun t => f (t / g)
theorem MeasureTheory.Integrable.comp_sub_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [] {f : GF} (hf : ) (g : G) :
MeasureTheory.Integrable fun t => f (g - t)
theorem MeasureTheory.Integrable.comp_div_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [] {f : GF} (hf : ) (g : G) :
MeasureTheory.Integrable fun t => f (g / t)
theorem MeasureTheory.integrable_comp_sub_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [] (f : GF) (g : G) :
(MeasureTheory.Integrable fun t => f (g - t))
theorem MeasureTheory.integrable_comp_div_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [] (f : GF) (g : G) :
(MeasureTheory.Integrable fun t => f (g / t))
theorem MeasureTheory.integral_sub_left_eq_self {G : Type u_4} {E : Type u_5} [] [] [] [] [] (f : GE) (μ : ) (x' : G) :
∫ (x : G), f (x' - x)μ = ∫ (x : G), f xμ
theorem MeasureTheory.integral_div_left_eq_self {G : Type u_4} {E : Type u_5} [] [] [] [] [] (f : GE) (μ : ) (x' : G) :
∫ (x : G), f (x' / x)μ = ∫ (x : G), f xμ
theorem MeasureTheory.integral_vadd_eq_self {α : Type u_3} {G : Type u_4} {E : Type u_5} [] [] [] [] [] [] {μ : } (f : αE) {g : G} :
∫ (x : α), f (g +ᵥ x)μ = ∫ (x : α), f xμ
theorem MeasureTheory.integral_smul_eq_self {α : Type u_3} {G : Type u_4} {E : Type u_5} [] [] [] [] [] [] {μ : } (f : αE) {g : G} :
∫ (x : α), f (g x)μ = ∫ (x : α), f xμ