Lebesgue Integration on Groups

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

theorem MeasureTheory.lintegral_inv_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [InvolutiveInv G] [MeasurableInv G] [μ.IsInvInvariant] (f : G → ENNReal) : ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ

The Lebesgue integral of a function with respect to an inverse invariant measure is invariant under the change of variables x ↦ x⁻¹.

theorem MeasureTheory.lintegral_neg_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [InvolutiveNeg G] [MeasurableNeg G] [μ.IsNegInvariant] (f : G → ENNReal) : ∫⁻ (x : G), f (-x) ∂μ = ∫⁻ (x : G), f x ∂μ

The Lebesgue integral of a function with respect to an inverse invariant measure is invariant under the change of variables x ↦ -x.

theorem MeasureTheory.lintegral_mul_left_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [Group G] [MeasurableMul G] [μ.IsMulLeftInvariant] (f : G → ENNReal) (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_left_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [AddGroup G] [MeasurableAdd G] [μ.IsAddLeftInvariant] (f : G → ENNReal) (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_right_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [Group G] [MeasurableMul G] [μ.IsMulRightInvariant] (f : G → ENNReal) (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_add_right_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [AddGroup G] [MeasurableAdd G] [μ.IsAddRightInvariant] (f : G → ENNReal) (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_div_right_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [Group G] [MeasurableMul G] [μ.IsMulRightInvariant] (f : G → ENNReal) (g : G) : ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ

theorem MeasureTheory.lintegral_sub_right_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [AddGroup G] [MeasurableAdd G] [μ.IsAddRightInvariant] (f : G → ENNReal) (g : G) : ∫⁻ (x : G), f (x - g) ∂μ = ∫⁻ (x : G), f x ∂μ

theorem MeasureTheory.lintegral_div_left_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [Group G] [MeasurableMul G] [μ.IsMulLeftInvariant] [MeasurableInv G] [μ.IsInvInvariant] (f : G → ENNReal) (g : G) : ∫⁻ (x : G), f (g / x) ∂μ = ∫⁻ (x : G), f x ∂μ

theorem MeasureTheory.lintegral_sub_left_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [AddGroup G] [MeasurableAdd G] [μ.IsAddLeftInvariant] [MeasurableNeg G] [μ.IsNegInvariant] (f : G → ENNReal) (g : G) : ∫⁻ (x : G), f (g - x) ∂μ = ∫⁻ (x : G), f x ∂μ

theorem MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [BorelSpace G] [μ.IsMulLeftInvariant] [μ.Regular] [NeZero μ] {f : G → ENNReal} (hf : Continuous f) : ∫⁻ (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_isAddLeftInvariant {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [BorelSpace G] [μ.IsAddLeftInvariant] [μ.Regular] [NeZero μ] {f : G → ENNReal} (hf : Continuous f) : ∫⁻ (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.