MeasureTheory.lintegral_mul_left_eq_self
theorem MeasureTheory.lintegral_mul_left_eq_self :
∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Group G]
[inst_2 : MeasurableMul G] [inst_3 : μ.IsMulLeftInvariant] (f : G → ENNReal) (g : G),
∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
This theorem states that for any given measurable space 'G', measure 'μ', group 'G', measurable multiplication on 'G', and a left-invariant measure 'μ', the Lebesgue integral of a function 'f' from 'G' to the nonnegative extended real numbers (ENNReal), where 'f' is translated by left-multiplication with an element 'g' of 'G', is equal to the Lebesgue integral of 'f' itself. In other words, multiplying an element 'x' in 'G' by 'g' (from the left) and then applying 'f', doesn't change the overall Lebesgue integral when measured with respect to 'μ'.
More concisely: For any measurable space 'G' with left-invariant measure 'μ', and measurable function 'f' from 'G' to the nonnegative extended real numbers, the Lebesgue integrals of 'f' and 'g ∘ f' (left-multiplication of 'f' by 'g') are equal, where 'g' is any element in 'G'.
|
MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant
theorem MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant :
∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : TopologicalSpace G]
[inst_2 : Group G] [inst_3 : TopologicalGroup G] [inst_4 : BorelSpace G] [inst_5 : μ.IsMulLeftInvariant]
[inst_6 : μ.Regular] [inst_7 : NeZero μ] {f : G → ENNReal}, Continuous f → (∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0)
This theorem states that for a given type `G` which is a measurable space, a topological space, a group, a topological group, and a Borel space, and for a measure `μ` on `G` that is regular, non-zero and left multiplication invariant, if `f` is a continuous nonnegative function mapping from `G` to the extended nonnegative real numbers (usually denoted [0, ∞]), then the Lebesgue integral of `f` with respect to the measure `μ` is zero if and only if the function `f` is identically zero.
More concisely: For a measurable space (G, Σ), topological space, group, topological group, and Borel space, if μ is a regular, non-zero, left multiplication invariant measure on G and f is a continuous, non-negative function from G to [0, ∞], then ∫fdμ = 0 if and only if f is identically zero.
|
MeasureTheory.lintegral_add_left_eq_self
theorem MeasureTheory.lintegral_add_left_eq_self :
∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G]
[inst_2 : MeasurableAdd G] [inst_3 : μ.IsAddLeftInvariant] (f : G → ENNReal) (g : G),
∫⁻ (x : G), f (g + x) ∂μ = ∫⁻ (x : G), f x ∂μ
This theorem states that for any type `G` which is a measurable space and an additive group, and for any measure `μ` on `G` which is left-invariant under addition, the Lebesgue integral of any function `f` from `G` to the extended nonnegative real numbers (`ENNReal`) remains unchanged if we translate the function by left-addition with any element `g` from `G`. In mathematical notation, this is stating that for all `f` and `g`, ∫⁻ (x : G), f (g + x) ∂μ = ∫⁻ (x : G), f x ∂μ.
More concisely: For any measurable space and additive group `(G, +)` with left-invariant measure `μ`, and for any function `f : G → ENNReal`, the Lebesgue integral of `f` over `G` is equal to the integral of the translated function `x mapsto f (x + g)` for any `g ∈ G`, i.e., ∫⁻(x : G), f (g + x) dμ = ∫⁻(x : G), f x dμ.
|
MeasureTheory.lintegral_add_right_eq_self
theorem MeasureTheory.lintegral_add_right_eq_self :
∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G]
[inst_2 : MeasurableAdd G] [inst_3 : μ.IsAddRightInvariant] (f : G → ENNReal) (g : G),
∫⁻ (x : G), f (x + g) ∂μ = ∫⁻ (x : G), f x ∂μ
This theorem, `MeasureTheory.lintegral_add_right_eq_self`, states that for any given type `G` equipped with a measurable space structure, an additive group structure, and a measurable-add structure, with `μ` being a right-invariant measure on `G`, the Lebesgue integral of a function `f` from `G` to the extended nonnegative real numbers (`ENNReal`) remains unchanged even after translating the function by right-addition with some element `g` from `G`. This means the integral over all `x` in `G` of `f(x + g)` with respect to measure `μ` is equal to the integral over all `x` in `G` of `f(x)` with respect to the same measure `μ`.
More concisely: For any measurable space `(G, Σ, μ)` with a right-invariant measure `μ`, and any additive function `f : G → ENNReal`, the Lebesgue integrals of `f` and `x ↦ f(x + g)` are equal for all `g ∈ G`.
|
MeasureTheory.lintegral_mul_right_eq_self
theorem MeasureTheory.lintegral_mul_right_eq_self :
∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Group G]
[inst_2 : MeasurableMul G] [inst_3 : μ.IsMulRightInvariant] (f : G → ENNReal) (g : G),
∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ
This theorem states that for any type 'G' with a measurable space structure, a measure 'μ', a group structure, and a measurable multiplication structure, and provided that the measure 'μ' is right-invariant, the Lebesgue integral of a function 'f' from 'G' to the extended nonnegative real numbers (denoted as '[0, ∞]'), where each input 'x' is right-multiplied by an element 'g' of 'G', is equal to the Lebesgue integral of the function 'f' without this multiplication. In other words, the value of the Lebesgue integral of 'f' does not change if we multiply its input by a fixed group element on the right.
More concisely: For any right-invariant measure μ on a measurable group (G, *, μ) and measurable function f : G -> [0, ∞], the Lebesgue integrals of f and the function g -> f(gg^-1) are equal.
|
MeasureTheory.lintegral_eq_zero_of_isAddLeftInvariant
theorem MeasureTheory.lintegral_eq_zero_of_isAddLeftInvariant :
∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : TopologicalSpace G]
[inst_2 : AddGroup G] [inst_3 : TopologicalAddGroup G] [inst_4 : BorelSpace G] [inst_5 : μ.IsAddLeftInvariant]
[inst_6 : μ.Regular] [inst_7 : NeZero μ] {f : G → ENNReal}, Continuous f → (∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0)
The theorem `MeasureTheory.lintegral_eq_zero_of_isAddLeftInvariant` states that, for any topological add group `G` equipped with a Borel measurable space, a regular, nonzero, left-invariant measure `μ`, and a continuous nonnegative function `f` from `G` to the extended nonnegative real numbers, the Lebesgue integral of `f` with respect to `μ` is zero if and only if `f` is the zero function. Here, a left-invariant measure is one for which the measure of any subset is equal to the measure of that subset translated by any element of the group `G`, and a regular measure is one that can be approximated from both above and below by compact and open sets respectively. The function `f` is considered to be nonnegative because it maps to the extended nonnegative real numbers, a set which includes all nonnegative real numbers along with positive infinity.
More concisely: A left-invariant, regular, nonzero measure `μ` on a topological add group `G` assigns integral zero to a continuous, nonnegative function `f` if and only if `f` is the zero function.
|