# Lebesgue Integration on Groups #

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

theorem MeasureTheory.lintegral_add_left_eq_self {G : Type u_1} [] {μ : } [] [] (f : GENNReal) (g : G) :
∫⁻ (x : G), f (g + x)μ = ∫⁻ (x : G), f xμ

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

theorem MeasureTheory.lintegral_mul_left_eq_self {G : Type u_1} [] {μ : } [] [] (f : GENNReal) (g : G) :
∫⁻ (x : G), f (g * x)μ = ∫⁻ (x : G), f xμ

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

theorem MeasureTheory.lintegral_add_right_eq_self {G : Type u_1} [] {μ : } [] [] (f : GENNReal) (g : G) :
∫⁻ (x : G), f (x + g)μ = ∫⁻ (x : G), f xμ

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

theorem MeasureTheory.lintegral_mul_right_eq_self {G : Type u_1} [] {μ : } [] [] (f : GENNReal) (g : G) :
∫⁻ (x : G), f (x * g)μ = ∫⁻ (x : G), f xμ

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

theorem MeasureTheory.lintegral_sub_right_eq_self {G : Type u_1} [] {μ : } [] [] (f : GENNReal) (g : G) :
∫⁻ (x : G), f (x - g)μ = ∫⁻ (x : G), f xμ
theorem MeasureTheory.lintegral_div_right_eq_self {G : Type u_1} [] {μ : } [] [] (f : GENNReal) (g : G) :
∫⁻ (x : G), f (x / g)μ = ∫⁻ (x : G), f xμ
theorem MeasureTheory.lintegral_eq_zero_of_isAddLeftInvariant {G : Type u_1} [] {μ : } [] [] [] [] {f : GENNReal} (hf : ) :
∫⁻ (x : G), f xμ = 0 f = 0

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

theorem MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant {G : Type u_1} [] {μ : } [] [] [] [] [] {f : GENNReal} (hf : ) :
∫⁻ (x : G), f xμ = 0 f = 0

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