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} [MeasurableSpace G] {μ : MeasureTheory.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_left_eq_self {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.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_right_eq_self {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.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_mul_right_eq_self {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.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_sub_right_eq_self {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.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_right_eq_self {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Group G] [MeasurableMul G] [μ.IsMulRightInvariant] (f : G → ENNReal) (g : G) : ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ

theorem MeasureTheory.lintegral_eq_zero_of_isAddLeftInvariant {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup 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.

theorem MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [TopologicalSpace G] [Group G] [TopologicalGroup 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.