MeasureTheory.integral_eq_zero_of_add_right_eq_neg
theorem MeasureTheory.integral_eq_zero_of_add_right_eq_neg :
∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : AddGroup G]
[inst_4 : MeasurableAdd G] [inst_5 : μ.IsAddRightInvariant],
(∀ (x : G), f (x + g) = -f x) → ∫ (x : G), f x ∂μ = 0
This theorem states that if a function `f : G → E` for a measurable space `G` and a normed add commutative group `E`, satisfies a property such that for any `x` in `G`, translating `x` by some fixed value `g` (i.e., `x + g`) and then applying `f` negates the original result of `f(x)`, then the integral of the function `f` with respect to a right-invariant measure `μ` is equal to zero. Here right-invariant means that translating the entire space `G` by `g` does not change the measure `μ`.
More concisely: If `f : G → E` is a measurable function on a measurable space `(G, μ)` with a right-invariant measure `μ`, such that `f(x + g) = -f(x)` for all `x` in `G` and fixed `g` in `G`, then the integral of `f` with respect to `μ` is equal to zero.
|
MeasureTheory.integral_add_left_eq_self
theorem MeasureTheory.integral_add_left_eq_self :
∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure G} [inst_3 : AddGroup G] [inst_4 : MeasurableAdd G]
[inst_5 : μ.IsAddLeftInvariant] (f : G → E) (g : G), ∫ (x : G), f (g + x) ∂μ = ∫ (x : G), f x ∂μ
The theorem `MeasureTheory.integral_add_left_eq_self` states that for any type `G` with a measurable space structure, an addition group structure, and a measure `μ` that is left-invariant, and for any type `E` which is a normed addable commutative group and also a normed space over the real numbers, the integral of a function `f : G → E` does not change if we translate the function by left-addition with a fixed element `g` from `G`. In other words, the integral of `f` over `G` with respect to `μ` is the same as the integral of the function `(g + x)` over `G` with respect to `μ`. This is expressed with the integral notation as `∫ (x : G), f (g + x) ∂μ = ∫ (x : G), f x ∂μ`.
More concisely: For any left-invariant measure `μ` on a measurable space `(G, Σ)` with an abelian group structure, and for any integrable function `f : G → ℝ`, we have `∫(x : G) f(g + x) dμ = ∫(x : G) f x dμ` for any fixed `g` in `G`.
|
MeasureTheory.integral_add_right_eq_self
theorem MeasureTheory.integral_add_right_eq_self :
∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure G} [inst_3 : AddGroup G] [inst_4 : MeasurableAdd G]
[inst_5 : μ.IsAddRightInvariant] (f : G → E) (g : G), ∫ (x : G), f (x + g) ∂μ = ∫ (x : G), f x ∂μ
This theorem, `MeasureTheory.integral_add_right_eq_self`, states that for any type `G` with a measurable space structure, an add group structure, and a measurability under addition, and any type `E` that is a normed commutative add group as well as a normed space over the real numbers ℝ, given a measure `μ` on `G` that is right-invariant under addition, and a function `f` from `G` to `E`, the integral of `f` translated by any element `g` from `G` (i.e., the integral of `f(x + g)`) with respect to `μ` is the same as the integral of `f` with respect to `μ`. In mathematical terms, this theorem is saying that ∫ f(x + g) dμ = ∫ f(x) dμ for right-invariant measures.
More concisely: For any right-invariant measure μ on a measurable add group G with values in a normed commutative add group E over ℝ, the integral of a measurable function f from G to E with respect to μ is translation invariant, that is, ∫ f(x + g) dμ = ∫ f(x) dμ for all x in G and g in E.
|
MeasureTheory.integral_mul_right_eq_self
theorem MeasureTheory.integral_mul_right_eq_self :
∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure G} [inst_3 : Group G] [inst_4 : MeasurableMul G]
[inst_5 : μ.IsMulRightInvariant] (f : G → E) (g : G), ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
This theorem states that for any function `f` from a group `G` to a normed add commutative group `E`, and any element `g` in `G`, the integral of `f` with respect to a right-invariant measure `μ` remains unchanged when `f` is translated by right-multiplication with `g`. In other words, the integral of `f(x * g)` with respect to `μ` is identical to the integral of `f(x)` with respect to the same measure. This is true for all measurable spaces `G` and `E` where `G` has a group structure and `G` has an operation of multiplication that is measurable.
More concisely: For any measurable function `f` from a group `(G, *)` to a normed add commutative group `(E, +)`, and right-invariant measure `μ` on `G`, the integral of `f(x * g)` over `G` with respect to `μ` equals the integral of `f(x)` over `G` for all `g` in `G`.
|
MeasureTheory.integral_mul_left_eq_self
theorem MeasureTheory.integral_mul_left_eq_self :
∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure G} [inst_3 : Group G] [inst_4 : MeasurableMul G]
[inst_5 : μ.IsMulLeftInvariant] (f : G → E) (g : G), ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
This theorem states that if you have a function `f` from a type `G` to a type `E`, where `G` is a group with a left-invariant measure `μ` and `E` is a normed additively commutative group that is a normed space over the reals, then the integral of `f` over `G` with respect to `μ` remains the same even if the function `f` is translated by left-multiplication with an element `g` from `G`. Essentially, if you shift the function `f` left by `g`, the integral of the function with respect to the measure `μ` does not change.
More concisely: If `f` is a function from a group `G` to a normed additively commutative group `E` with a left-invariant measure `μ`, then for all `g` in `G`, the integral of `f` over `G` with respect to `μ` equals the integral of `f ∘ lmap g` over `G`. Here, `lmap g` denotes left multiplication by `g` in `G`.
|
MeasureTheory.integral_eq_zero_of_add_left_eq_neg
theorem MeasureTheory.integral_eq_zero_of_add_left_eq_neg :
∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : AddGroup G]
[inst_4 : MeasurableAdd G] [inst_5 : μ.IsAddLeftInvariant],
(∀ (x : G), f (g + x) = -f x) → ∫ (x : G), f x ∂μ = 0
This theorem states that for a given function `f` from a measurable space `G` to a normed add commutative group `E`, if the function `f` negates itself under some left-translation by an element `g` of `G` (i.e., for all `x` in `G`, `f(g + x) = -f(x)`), then the integral of the function `f` with respect to a left-invariant measure `μ` is zero. This theorem holds under the conditions that `G` is also an add group and the measure `μ` is add-left-invariant.
More concisely: If `f` is a measurable function from a left-invariant measure space `(G, μ)` (where `G` is an add group) to a normed add commutative group `E`, and `f` negates itself under left-translation by some `g` in `G`, then the integral of `f` with respect to `μ` is zero.
|
MeasureTheory.integral_eq_zero_of_mul_right_eq_neg
theorem MeasureTheory.integral_eq_zero_of_mul_right_eq_neg :
∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : Group G]
[inst_4 : MeasurableMul G] [inst_5 : μ.IsMulRightInvariant],
(∀ (x : G), f (x * g) = -f x) → ∫ (x : G), f x ∂μ = 0
This theorem states that for any measurable space `G`, normed additively commutative group `E`, and normed space over the reals `E`, if a function `f` from `G` to `E` satisfies the property that for all `x` in `G`, the right-translation of `f` by an element `g` of `G` negates `f`, and if the measure `μ` on `G` is right-invariant (meaning that the measure of a set is unchanged if every element of the set is multiplied on the right by `g`), then the integral of the function `f` with respect to the measure `μ` is zero. In mathematical notation, if for all `x` in `G`, `f(x * g) = -f(x)`, and `μ` is a right-invariant measure, then the integral of `f` over `G` with respect to `μ` is zero: `∫ f dμ = 0`.
More concisely: If `f` is a measurable function from a measurable space `(G, μ)` to a normed space `E` over the reals, such that for all `x` in `G` and `g` in `G`, `f(x * g) = -f(x)`, and `μ` is a right-invariant measure, then the integral of `f` with respect to `μ` is zero: `∫ f dμ = 0`.
|
MeasureTheory.integral_eq_zero_of_mul_left_eq_neg
theorem MeasureTheory.integral_eq_zero_of_mul_left_eq_neg :
∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : Group G]
[inst_4 : MeasurableMul G] [inst_5 : μ.IsMulLeftInvariant],
(∀ (x : G), f (g * x) = -f x) → ∫ (x : G), f x ∂μ = 0
This theorem states that if a function, when left-multiplied by a certain value, becomes the negation of the original function, then the integral of that function with respect to a left-invariant measure equals zero. Here, the left-invariant measure, represented by `μ`, is a mathematical concept found in the theory of measure spaces, and it remains unchanged when the points of the space are left-multiplied by some fixed element. This theorem applies to a function `f` from a type `G`, which forms a group under multiplication, to a normed additively commutative group `E` over the real numbers, and the elements of `G` are measurable with respect to multiplication.
More concisely: If a measurable function `f` from a left-invariant measure space `(G, μ)`, where `G` is a group under multiplication and `E` is a real normed additively commutative group, satisfies `f * x = -f` for all `x` in `G`, then `∫f dμ = 0`.
|