# 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} [] {μ : } [] [] [μ.IsNegInvariant] {f : GF} (hf : ) :
MeasureTheory.Integrable (fun (t : G) => f (-t)) μ
theorem MeasureTheory.Integrable.comp_inv {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [μ.IsInvInvariant] {f : GF} (hf : ) :
MeasureTheory.Integrable (fun (t : G) => f t⁻¹) μ
theorem MeasureTheory.integral_neg_eq_self {G : Type u_4} {E : Type u_5} [] [] [] [] (f : GE) (μ : ) [μ.IsNegInvariant] :
∫ (x : G), f (-x)μ = ∫ (x : G), f xμ
theorem MeasureTheory.integral_inv_eq_self {G : Type u_4} {E : Type u_5} [] [] [] [] (f : GE) (μ : ) [μ.IsInvInvariant] :
∫ (x : G), f x⁻¹μ = ∫ (x : G), f xμ
theorem MeasureTheory.integral_add_left_eq_self {G : Type u_4} {E : Type u_5} [] [] {μ : } [] [] [μ.IsAddLeftInvariant] (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} [] [] {μ : } [] [] [μ.IsMulLeftInvariant] (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} [] [] {μ : } [] [] [μ.IsAddRightInvariant] (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} [] [] {μ : } [] [] [μ.IsMulRightInvariant] (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} [] [] {μ : } [] [] [μ.IsAddRightInvariant] (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} [] [] {μ : } [] [] [μ.IsMulRightInvariant] (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} [] [] [μ.IsAddLeftInvariant] (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} [] [] [μ.IsMulLeftInvariant] (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} [] [] [μ.IsAddRightInvariant] (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} [] [] [μ.IsMulRightInvariant] (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} [μ.IsAddLeftInvariant] (hf : ) (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (g + t)) μ
theorem MeasureTheory.Integrable.comp_mul_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} [μ.IsMulLeftInvariant] (hf : ) (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (g * t)) μ
theorem MeasureTheory.Integrable.comp_add_right {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} [μ.IsAddRightInvariant] (hf : ) (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (t + g)) μ
theorem MeasureTheory.Integrable.comp_mul_right {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} [μ.IsMulRightInvariant] (hf : ) (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (t * g)) μ
theorem MeasureTheory.Integrable.comp_sub_right {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} [μ.IsAddRightInvariant] (hf : ) (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (t - g)) μ
theorem MeasureTheory.Integrable.comp_div_right {G : Type u_4} {F : Type u_6} [] {μ : } [] [] {f : GF} [μ.IsMulRightInvariant] (hf : ) (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (t / g)) μ
theorem MeasureTheory.Integrable.comp_sub_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [] {f : GF} [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (hf : ) (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (g - t)) μ
theorem MeasureTheory.Integrable.comp_div_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [] {f : GF} [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (hf : ) (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (g / t)) μ
theorem MeasureTheory.integrable_comp_sub_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [] (f : GF) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (g - t)) μ
theorem MeasureTheory.integrable_comp_div_left {G : Type u_4} {F : Type u_6} [] {μ : } [] [] [] (f : GF) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
MeasureTheory.Integrable (fun (t : G) => f (g / t)) μ
theorem MeasureTheory.integral_sub_left_eq_self {G : Type u_4} {E : Type u_5} [] [] [] [] [] (f : GE) (μ : ) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (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) (μ : ) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (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μ