MeasureTheory.measurePreserving_prod_mul_swap_right
theorem MeasureTheory.measurePreserving_prod_mul_swap_right :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : μ.IsMulRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 * z.2)) (μ.prod ν) (ν.prod μ)
This theorem states that for any type `G` equipped with a measurable space structure, a group structure, and a measurable multiplication operation, and for any two `sigma-finite` measures `μ` and `ν` on `G`, where `μ` is right invariant under multiplication, the map that takes a pair of elements `(x, y)` and maps them to `(y, xy)` preserves the measure `μ × ν`, transforming it into `ν × μ`.
More concisely: For any measurable groups `(G, μ, ν)` with right invariant `μ` under multiplication, the measure product `μ × ν` is transformed into `ν × μ` under the map sending `(x, y)` to `(y, xy)`.
|
MeasureTheory.measure_eq_sub_vadd
theorem MeasureTheory.measure_eq_sub_vadd :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
{s : Set G} [inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddLeftInvariant] [inst_7 : ν.IsAddLeftInvariant],
MeasurableSet s → ↑↑ν s ≠ 0 → ↑↑ν s ≠ ⊤ → μ = (↑↑μ s / ↑↑ν s) • ν
This theorem states that, given a measurable space `G` that also forms an additive group and supports measurable addition and negation, any two left-invariant Borel measures `μ` and `ν` over this space, which are both sigma-finite, are unique up to a scalar, as long as a given set `s` in `G` is measurable and its measure under `ν` is neither zero nor infinite. Specifically, the measure `μ` is equal to the measure of `s` under `μ` divided by the measure of `s` under `ν`, all multiplied by `ν`.
More concisely: Given a sigma-finite, measurable additive group `G` with a measurable set `s` of finite, non-zero measure under a sigma-finite left-invariant Borel measure `ν`, any two such measures `μ` and `ν` are proportional: `μ = (μ(s) / ν(s)) * ν`.
|
MeasureTheory.measure_add_right_null
theorem MeasureTheory.measure_add_right_null :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] {s : Set G} [inst_4 : MeasurableNeg G]
[inst_5 : μ.IsAddLeftInvariant] (y : G), ↑↑μ ((fun x => x + y) ⁻¹' s) = 0 ↔ ↑↑μ s = 0
This theorem, named `MeasureTheory.measure_add_right_null`, states that for any type `G` equipped with a `MeasurableSpace` structure, an `AddGroup` structure, and a `MeasurableAdd₂` structure, for any measure `μ` on `G` that is `SigmaFinite` and `IsAddLeftInvariant`, for any set `s` in `G`, and for any element `y` in `G`, the measure of the preimage of `s` under the function that adds `y` to an element is zero if and only if the measure of `s` is zero. This is essentially saying that shifting a set by an element in an additive group does not change its measure, if its measure is zero.
More concisely: For any `SigmaFinite` and `IsAddLeftInvariant` measure `μ` on an additive group `G` with `MeasurableSpace` and `AddGroup` structures, the preimage of a measurable set under the function that adds a fixed element of `G` has measure zero if and only if the original set has measure zero.
|
MeasureTheory.measurePreserving_prod_mul_swap
theorem MeasureTheory.measurePreserving_prod_mul_swap :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : μ.IsMulLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2, z.2 * z.1)) (μ.prod ν) (ν.prod μ)
This theorem states that for any type `G` equipped with a measurable space structure, a group structure, and a measurable multiplication, and given two measures `μ` and `ν` on `G` (which are both sigma-finite and `μ` is mul-left-invariant), the map `(x, y) ↦ (y, yx)` preserves the measure `μ × ν`, turning it into `ν × μ`. This map is known as `SR` in Halmos' book, being composed of two maps `S` and `R` where `S` is the map `(x, y) ↦ (x, xy)` and `R` is the function that swaps the pair elements.
More concisely: Given two sigma-finite measures `μ` and `ν` on a measurable group `(G, Σ)` with multiplication, if `μ` is left-invariant and `(x, y) �mapsto (y, yx)` preserves `μ × ν`, then `ν × μ` is the measure preserved.
|
MeasureTheory.measurePreserving_sub_prod
theorem MeasureTheory.measurePreserving_sub_prod :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1 - z.2, z.2)) (μ.prod ν) (μ.prod ν)
This theorem states that for any type `G` with a measurable space structure, an additive group structure, and a `MeasurableAdd₂` instance, and for any measures `μ` and `ν` on `G` that are sigma-finite, if `G` also has a `MeasurableNeg` instance and `μ` is add-right-invariant, then the map `(x, y) ↦ (x - y, y)` preserves the measure `μ × ν`. That is, the measure of any set under the product measure `μ × ν` is the same before and after applying this map.
More concisely: For any measurable additive groups `G` equipped with sigma-finite, add-right-invariant measures `μ` and `ν`, the map `(x, y) ↦ (x - y, y)` preserves the product measure `μ × ν`.
|
MeasureTheory.absolutelyContinuous_of_isMulLeftInvariant
theorem MeasureTheory.absolutelyContinuous_of_isMulLeftInvariant :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableInv G] [inst_6 : μ.IsMulLeftInvariant] [inst_7 : ν.IsMulLeftInvariant],
ν ≠ 0 → μ.AbsolutelyContinuous ν
This theorem states that for any type `G` which has a structure of measurable space, group, and also supports measurable multiplication and inversion, if `μ` and `ν` are two measures on `G` which are both sigma finite and left multiplication invariant, then if `ν` is not zero, `μ` is absolutely continuous with respect to `ν`. This is a significant property in measure theory, implying that almost everywhere results for `ν` will also hold for `μ`.
More concisely: If `G` is a measurable group with two sigma-finite, left multiplication invariant measures `μ` and `ν`, where `ν` is non-zero, then `μ` is absolutely continuous with respect to `ν`.
|
MeasureTheory.measurePreserving_prod_add_swap
theorem MeasureTheory.measurePreserving_prod_add_swap :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : μ.IsAddLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2, z.2 + z.1)) (μ.prod ν) (ν.prod μ)
The theorem `MeasureTheory.measurePreserving_prod_add_swap` states that for any type `G` that is a measurable space and an additive group, and for any two measures `μ` and `ν` on `G` (with `ν` and `μ` being sigma finite, and `μ` being left invariant under addition), the map that takes a pair `(x, y)` to `(y, y + x)` preserves the measure when going from `μ × ν` to `ν × μ`. In other words, this transformation doesn't change the "total weight" of the measure, despite changing the order of the elements and adding them together in a specific way.
More concisely: For any sigma-finite, left-invariant measures μ and ν on the measurable additive group G, the measure of the product space G x G under μ × ν is equal to the measure under ν × μ, when applying the transformation that swaps the first and second elements and adds the second to the first.
|
MeasureTheory.quasiMeasurePreserving_inv
theorem MeasureTheory.quasiMeasurePreserving_inv :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableInv G]
[inst_5 : μ.IsMulLeftInvariant], MeasureTheory.Measure.QuasiMeasurePreserving Inv.inv μ μ
The theorem `MeasureTheory.quasiMeasurePreserving_inv` states that for any type `G` which has a measurable space structure, a group structure, a structure that allows for the measurement of multiplied elements, and an inverted element that can be measured, and for any measure `μ` on `G` which is sigma-finite and left-multiplication-invariant, the function `Inv.inv` which inverts an element of a group, is quasi-measure-preserving. In other words, the process of inverting elements in the group `G` doesn't significantly affect the measure `μ`.
More concisely: Given a sigma-finite, left-multiplication-invariant measure `μ` on a measurable group `G` with a measurable inverted element, the measure-preserving involution function `Inv.inv` is quasi-measure-preserving.
|
MeasureTheory.measurePreserving_prod_div
theorem MeasureTheory.measurePreserving_prod_div :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableInv G] [inst_6 : ν.IsMulRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 / z.1)) (μ.prod ν) (μ.prod ν)
The theorem `MeasureTheory.measurePreserving_prod_div` states that for any two measures `μ` and `ν` over a measurable space `G` with a group structure, the map that takes a pair `(x, y)` to `(x, y / x)` preserves the measure. This is true provided `ν` is right multiplication invariant and both `μ` and `ν` are sigma-finite measures. The group `G` also requires the structure of a measurable inverse and measurable multiplication.
More concisely: For sigma-finite measures μ and ν on a measurable group G with right multiplication invariant ν and measurable inverse and multiplication structures, the map (x, y) ↔ (x, y / x) preserves the measure.
|
MeasureTheory.measure_mul_right_null
theorem MeasureTheory.measure_mul_right_null :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] {s : Set G} [inst_4 : MeasurableInv G]
[inst_5 : μ.IsMulLeftInvariant] (y : G), ↑↑μ ((fun x => x * y) ⁻¹' s) = 0 ↔ ↑↑μ s = 0
This theorem, titled `MeasureTheory.measure_mul_right_null`, states that for any type `G` that has a measurable space structure, a group structure, a measurable multiplication, and a measurable inversion, given a sigma-finite measure `μ` on `G` that is left-invariant, for any element `y` in `G`, the measure of the preimage of a set `s` under the function that multiplies each element by `y` is zero if and only if the measure of the set `s` is zero. In essence, it says that under these conditions, multiplying each element of a set by a fixed element and measuring the resulting set yields zero if and only if the original set had measure zero.
More concisely: For any sigma-finite, left-invariant measure `μ` on a measurable group `G` with measurable multiplication and inversion, the preimage of a null set under multiplication by any fixed element `y` in `G` is also a null set.
|
MeasureTheory.measurePreserving_prod_mul
theorem MeasureTheory.measurePreserving_prod_mul :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : ν.IsMulLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1, z.1 * z.2)) (μ.prod ν) (μ.prod ν)
This theorem states that in the context of a measurable space `G`, which also forms a group and has a two-argument measurable multiplication function, the multiplicative shear mapping `(x, y) ↦ (x, xy)` preserves the product measure `μ × ν`. This property is fundamental to the definition of a measurable group as given in Halmos's work (Section 59), where this mapping is referred to as `S`. The theorem further requires that the measures `μ` and `ν` are sigma-finite and that `ν` is left-invariant under multiplication.
More concisely: In a sigma-finite measurable group `(G, μ, ν)` with a two-argument measurable multiplication function, the multiplicative shear mapping `(x, y) ↦ (x, xy)` preserves the product measure `μ × ν`, assuming `ν` is left-invariant under multiplication.
|
MeasureTheory.absolutelyContinuous_neg
theorem MeasureTheory.absolutelyContinuous_neg :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableNeg G]
[inst_5 : μ.IsAddLeftInvariant], μ.AbsolutelyContinuous μ.neg
This theorem states that for any type `G` with a measurable space structure, an additive group structure and a condition that addition of two elements of `G` is measurable, given a sigma-finite measure `μ` on `G` that is additively left-invariant and assuming the negation operation on `G` is measurable, the measure `μ` is absolutely continuous with respect to the measure `A ↦ μ (- A)`, where `- A` is the pointwise negation of `A`. In other words, for any subset of `G` such that the measure of its pointwise negation under `μ` is zero, the measure of the subset itself under `μ` is also zero.
More concisely: Given a sigma-finite, additively left-invariant measure `μ` on a measurable additive group `G` with measurable negation, `μ` is absolutely continuous with respect to `μ` (-), i.e., for any measurable set `A` with `μ`(-`A`) = 0, `μ`(`A`) = 0.
|
MeasureTheory.quasiMeasurePreserving_neg
theorem MeasureTheory.quasiMeasurePreserving_neg :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableNeg G]
[inst_5 : μ.IsAddLeftInvariant], MeasureTheory.Measure.QuasiMeasurePreserving Neg.neg μ μ
This theorem, named `MeasureTheory.quasiMeasurePreserving_neg`, states that for any type `G` that is a measurable space, an add group, and for which the addition of two elements is measurable, the negation operation (i.e., producing the additive inverse of a number) is a quasi-measure preserving transformation with respect to any sigma-finite measure `μ` on `G`. In other words, if `μ` is a measure on `G` that is add-left-invariant (the measure of a set is unchanged if we add the same element to every point in the set), and if the negation operation is also measurable in `G`, then applying the negation operation doesn't significantly change the measure as defined by `μ`.
More concisely: Given a measurable space `(G, Σ, μ)` where `G` is an add group with measurable addition, the negation operation on `G` is a quasi-measure preserving transformation with respect to `μ`.
|
MeasureTheory.measurePreserving_add_prod_neg
theorem MeasureTheory.measurePreserving_add_prod_neg :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddLeftInvariant] [inst_7 : ν.IsAddLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2 + z.1, -z.1)) (μ.prod ν) (μ.prod ν)
This theorem states that the map `(x, y) ↦ (y + x, - x)` preserves the measure in the context of an additive group `G`, where `G` is a measurable space with a second measurable addition operation. The measure is defined by two measures `μ` and `ν`, both of which are sigma-finite and left invariant under addition. The measure-preserving property holds for the product measure of `μ` and `ν`.
More concisely: The theorem asserts that the map `(x, y) ↦ (y + x, -x)` preserves the product measure `μ ⊤ ν` in the additive group `G`, where `μ` and `ν` are sigma-finite, left invariant measures.
|
MeasureTheory.measurePreserving_prod_inv_mul
theorem MeasureTheory.measurePreserving_prod_inv_mul :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableInv G] [inst_6 : ν.IsMulLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1, z.1⁻¹ * z.2)) (μ.prod ν) (μ.prod ν)
This theorem states that for any type `G` that has a measurable space structure, a group structure, a `MeasurableMul₂ G` instance (which ensures that the multiplication operation is measurable), a `MeasurableInv G` instance (which ensures that the inversion operation is measurable), and a measure `ν` that is left-invariant under multiplication, the map `(x, y) ↦ (x, x⁻¹y)` is measure-preserving with respect to the product measure of `μ` and `ν`. This means that for any measurable set in the co-domain, its preimage under this map has the same measure. This is the inverse map `S⁻¹` referred to in Halmos's book, where `S` is the map `(x, y) ↦ (x, xy)`.
More concisely: For any measurable group `(G, μ)` with a left-invariant measure `ν` and measurable multiplication and inversion operations, the map `(x, y) ↦ (x, x⁻¹y)` is measure-preserving with respect to the product measure of `μ` and `ν`.
|
MeasureTheory.measurePreserving_mul_prod
theorem MeasureTheory.measurePreserving_mul_prod :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : μ.IsMulRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1 * z.2, z.2)) (μ.prod ν) (μ.prod ν)
This theorem states that for any type `G` with a measurable space structure, a group structure, and a measurable multiplication operation, and given two sigma-finite measures `μ` and `ν` on `G` where `μ` is right invariant under multiplication, the map that takes a pair `(x, y)` to `(xy, y)` preserves the measure `μ × ν`.
More concisely: Given measurable spaces `(G, Σ)`, a group structure on `G` with measurable multiplication, two sigma-finite measures `μ` and `ν` on `G` with `μ` right invariant under multiplication, the product measure `μ × ν` is invariant under the map `(x, y) ↦ (xy, y)`.
|
MeasureTheory.quasiMeasurePreserving_mul_right
theorem MeasureTheory.quasiMeasurePreserving_mul_right :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableInv G]
[inst_5 : μ.IsMulLeftInvariant] (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun h => h * g) μ μ
This theorem states that for any type `G` with a measurable space structure, a group structure, and a structure of measurable multiplication, given a measure `μ` that is sigma-finite and left-invariant, and any element `g` of `G`, the function which multiplies each element `h` of `G` by `g` on the right is quasi-measure preserving with respect to `μ`. In other words, a left-invariant measure is almost preserved when we multiply elements of the group by a fixed element on the right side. Note that this should not be mistaken with the fact that the measure is preserved by right multiplication.
More concisely: For any sigma-finite, left-invariant measure `μ` on a measurable group `(G, σ)` with measurable multiplication, the right multiplication-by-`g` function on `G` is quasi-measure preserving with respect to `μ`, for any `g` in `G`.
|
MeasureTheory.measure_mul_lintegral_eq
theorem MeasureTheory.measure_mul_lintegral_eq :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
{s : Set G} [inst_5 : MeasurableInv G] [inst_6 : μ.IsMulLeftInvariant] [inst_7 : ν.IsMulLeftInvariant],
MeasurableSet s →
∀ (f : G → ENNReal),
Measurable f → ↑↑μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
The theorem `MeasureTheory.measure_mul_lintegral_eq` states that for any type `G` equipped with a `MeasurableSpace` structure, a group structure, and a `MeasurableMul₂` structure, given two measures `μ` and `ν` on `G` that are both sigma-finite, a set `s` of `G` that is measurable, a function `f` from `G` to the extended nonnegative real numbers that is measurable, and provided that `G` has a `MeasurableInv` structure and both `μ` and `ν` are left-invariant under multiplication, then the product of measure `μ` with respect to set `s` and the integral of `f` with respect to measure `ν` equals the integral over `G` of the product of the measure `ν` of the preimage under multiplication by `x` of the set `s` and the value of `f` at the inverse of `x`, with respect to the measure `μ`.
More concisely: For any measurable set s in a sigma-finite, left-invariant, measurable group G with measures μ and ν, and measurable function f, the integral of f(x)ν(dx) over s equals the integral of (x → ν(s.map x).μ(dx)) * f(x) over G.
|
MeasureTheory.measurePreserving_mul_prod_inv_right
theorem MeasureTheory.measurePreserving_mul_prod_inv_right :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableInv G] [inst_6 : μ.IsMulRightInvariant] [inst_7 : ν.IsMulRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
The theorem `MeasureTheory.measurePreserving_mul_prod_inv_right` states that for any type `G` that has a measurable space structure, a group structure, a measurable multiplication, and a measurable inverse, and for any measures `μ` and `ν` on `G` that are sigma-finite and right-invariant, the function which maps a pair `(x, y)` to `(xy, x⁻¹)` preserves the measure of the product of `μ` and `ν`. In other words, the measure of a set under the product of `μ` and `ν` before applying the function is the same as the measure of the set under the product of `μ` and `ν` after applying the function.
More concisely: For measurable spaces (G, σG) with a group structure, measurable multiplication and inverse, and sigma-finite, right-invariant measures μ and ν, the measure of sets is preserved under the function mapping (x, y) to (xy, x⁻¹) in the product measure μ ⊤ ν.
|
MeasureTheory.measurePreserving_prod_sub_swap
theorem MeasureTheory.measurePreserving_prod_sub_swap :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 - z.2)) (μ.prod ν) (ν.prod μ)
The theorem `MeasureTheory.measurePreserving_prod_sub_swap` states that for any type `G` that is a measurable space and an add group, and for any two measures `μ` and `ν` on `G` that are sigma finite, the map `(x, y) ↦ (y, x - y)` preserves the measure when going from the product measure `μ × ν` to `ν × μ`. This also requires `G` to be measurable under addition and for the measure `μ` to be right invariant under addition.
More concisely: For measurable spaces and add groups G, and sigma-finite measures μ and ν on G that are right invariant with respect to μ and measurable under addition, the measure preserving map (x, y) ↦ (y, x - y) transforms μ × ν into ν × μ.
|
MeasureTheory.measurePreserving_add_prod_neg_right
theorem MeasureTheory.measurePreserving_add_prod_neg_right :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddRightInvariant] [inst_7 : ν.IsAddRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1 + z.2, -z.1)) (μ.prod ν) (μ.prod ν)
The theorem `MeasureTheory.measurePreserving_add_prod_neg_right` states that for any type `G` that has a measurable space structure, is an additive group, and supports the operation of measurable addition and measurable negation, the map that takes a pair `(x, y)` to `(x + y, -x)` preserves the measure. This is true when the measures `μ` and `ν` are sigma-finite and are right-invariant with respect to addition. The measure-preserving property is with respect to the product measure of `μ` and `ν`.
More concisely: For measurable spaces `(X, Σμ)` and `(Y, Σν)` with sigma-finite, right-invariant measures `μ` and `ν`, the map `((x, y) ↦ (x + y, -x)) : X × Y → X × Y` is measure-preserving with respect to the product measure `μ ⨯ ν` on `X × Y`.
|
MeasureTheory.measure_eq_div_smul
theorem MeasureTheory.measure_eq_div_smul :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
{s : Set G} [inst_5 : MeasurableInv G] [inst_6 : μ.IsMulLeftInvariant] [inst_7 : ν.IsMulLeftInvariant],
MeasurableSet s → ↑↑ν s ≠ 0 → ↑↑ν s ≠ ⊤ → μ = (↑↑μ s / ↑↑ν s) • ν
This theorem states that in the context of a measurable group `G` (that is, a group with a structure of measurable space where the group operation and the inverse operation are measurable), any two left-invariant Borel measures `μ` and `ν` (measures that remain unchanged under left-multiplication by an element of the group) are identical up to a scaling factor. Specifically, if a set `s` in `G` is measurable, and the measure `ν` of `s` is neither zero nor infinite, then the measure `μ` can be expressed as the measure `μ` of `s` divided by the measure `ν` of `s`, all scaled by `ν`. Both measures `μ` and `ν` are assumed to be sigma-finite, meaning that `G` can be decomposed into a countable union of measurable sets with finite measure.
More concisely: In a measurable group endowed with two left-invariant, sigma-finite Borel measures, they are proportional.
|
MeasureTheory.measurePreserving_prod_inv_mul_swap
theorem MeasureTheory.measurePreserving_prod_inv_mul_swap :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableInv G] [inst_6 : μ.IsMulLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2, z.2⁻¹ * z.1)) (μ.prod ν) (ν.prod μ)
The theorem `MeasureTheory.measurePreserving_prod_inv_mul_swap` states that for any type `G` that has a measurable space structure, a group structure, a measurable multiplicative operation, and an involution operation, and for any two sigma-finite measures `μ` and `ν` on this type, where `μ` is left-invariant under multiplication, the function that takes a pair `(x, y)` and maps it to `(y, y⁻¹x)` preserves the measure of the product measure `μ × ν`, i.e., the measure of the image of a set under this function with respect to `ν × μ` is the same as the measure of the original set with respect to `μ × ν`. This function corresponds to the function `S⁻¹R` in Halmos's notation, where `S` is the map `(x, y) ↦ (x, xy)` and `R` is the function that swaps the elements of a pair.
More concisely: Given a measurable space `(G, Σ)` with a group structure, measurable multiplicative operation, involution operation, and two sigma-finite measures `μ` and `ν` where `μ` is left-invariant, the function `(x, y) ↦ (y, y⁻¹x)` preserves the measure of the product `μ × ν`, i.e., `μ×ν(A) = μ×ν((y, y⁻¹x)⁻¹(A))` for all `A ∈ Σ`.
|
MeasureTheory.measurePreserving_prod_add
theorem MeasureTheory.measurePreserving_prod_add :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : ν.IsAddLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1, z.1 + z.2)) (μ.prod ν) (μ.prod ν)
The theorem `MeasureTheory.measurePreserving_prod_add` states that for any type `G` that is a measurable space and also an additive group, with the property that the operation of addition is measurable (the type `G` has the structure `MeasurableAdd₂`), given two measures `μ` and `ν` on `G` that are sigma finite, and if the measure `ν` is left-invariant under addition, then the shear mapping `(x, y) ↦ (x, x + y)` preserves the product measure `μ × ν`. In other words, the measure of any set under `μ × ν` is the same before and after applying the shear mapping.
More concisely: Given two sigma-finite measures `μ` and `ν` on a measurable additive group `G`, if `ν` is left-invariant under addition, then the product measure `μ × ν` is preserved by the shear mapping `(x, y) ↦ (x, x + y)`.
|
MeasureTheory.measurePreserving_add_prod
theorem MeasureTheory.measurePreserving_add_prod :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : μ.IsAddRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1 + z.2, z.2)) (μ.prod ν) (μ.prod ν)
This theorem states that for any type `G` that has a measurable space, an add group, and measurable addition, and any two measures `μ` and `ν` on this type, if `ν` and `μ` are sigma finite and `μ` is add right invariant, then the map that takes a pair `(x, y)` to `(x + y, y)` preserves the measure `μ × ν`. In other words, the measure of any set under the product measure `μ × ν` is the same before and after applying this map.
More concisely: Given measurable spaces `(G, Σ)` with an add group structure and measurable addition, sigma-finite measures `μ` and `ν` on `G`, if `μ` is add right invariant, then the measure `μ × ν` is preserved under the function `(x, y) ↦ (x + y, y)`.
|
MeasureTheory.measurePreserving_prod_div_swap
theorem MeasureTheory.measurePreserving_prod_div_swap :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableInv G] [inst_6 : μ.IsMulRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 / z.2)) (μ.prod ν) (ν.prod μ)
The theorem `MeasureTheory.measurePreserving_prod_div_swap` states that for any type `G` equipped with a measurable space structure, a group structure, and a measurable multiplication, given two measures `μ` and `ν` on `G` where both measures are sigma-finite and `μ` is right multiplication invariant, the map `(x, y) ↦ (y, x / y)` preserves the measure when going from the product measure `μ × ν` to the product measure `ν × μ`.
More concisely: For measurable spaces `(G, Σ)` with a group structure and measurable multiplication, if `μ` and `ν` are sigma-finite measures on `G` with `μ` being right multiplication invariant, then the measure preserving map is `(x, y) ↦ (y, x / y)` for the product measures `μ × ν` and `ν × μ`.
|
MeasureTheory.measure_lintegral_div_measure
theorem MeasureTheory.measure_lintegral_div_measure :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
{s : Set G} [inst_5 : MeasurableInv G] [inst_6 : μ.IsMulLeftInvariant] [inst_7 : ν.IsMulLeftInvariant],
MeasurableSet s →
↑↑ν s ≠ 0 →
↑↑ν s ≠ ⊤ →
∀ (f : G → ENNReal),
Measurable f → ↑↑μ s * ∫⁻ (y : G), f y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν = ∫⁻ (x : G), f x ∂μ
This theorem, named `MeasureTheory.measure_lintegral_div_measure`, is a technical lemma that relates two different measures, similar to a theorem from Halmos' Measure Theory (§60 Th. A). The theorem operates in the context of a measurable space `G` equipped with the structure of a group and measurable multiplication and inversion, and two sigma-finite measures `μ` and `ν` on this space. The measures are both assumed to be left-invariant under the group operation.
Given a measurable set `s` in `G`, such that the measure `ν(s)` is neither zero nor infinity, and a measurable function `f : G → ENNReal` (the extended non-negative reals), the theorem states the equality of two expressions. On the left-hand side, we have the product of `μ(s)` and an integral over `G` (with respect to measure `ν`) of `f(y⁻¹) / ν(s * y⁻¹)`. On the right-hand side, we simply have the integral of `f` over `G` with respect to measure `μ`. This theorem is particularly useful when `f` is the characteristic function of a measurable set `t`, as it then essentially asserts that `μ(t) = c * μ(s)` for a constant `c` that does not depend on `μ`.
The theorem comes with a note that there is a gap in the last step of the proof in Halmos' book, which this theorem fills by proving an inequality for almost all `x` in a certain context.
More concisely: Given a measurable space `G` equipped with a group structure, two left-invariant sigma-finite measures `μ` and `ν`, and a measurable function `f : G → ℝ+`, for a measurable set `s` with finite `ν(s)`, the integral of `f(y⁻¹) / ν(s * y⁻¹) dν over `G` equals the integral of `f` over `s` with respect to `μ`.
|
MeasureTheory.measurePreserving_mul_prod_inv
theorem MeasureTheory.measurePreserving_mul_prod_inv :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableInv G] [inst_6 : μ.IsMulLeftInvariant] [inst_7 : ν.IsMulLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
This theorem states that for any type `G` equipped with a measurable space structure, a group structure, and a binary operation that is measure-preserving (denoted by `MeasurableMul₂ G`), and given two measures `μ` and `ν` on `G` that are both sigma-finite and left-invariant under multiplication, the map `(x, y) ↦ (yx, x⁻¹)` is measure-preserving. This relates to the function `S⁻¹RSR` in [Halmos, §59], where `S` is the map `(x, y) ↦ (x, xy)` and `R` is `Prod.swap`. The theorem implies that performing the transformation won't change the measures of sets under the measures `μ.prod ν`.
More concisely: Given a measure-preserving binary operation on a sigma-finite, left-inverse measure space `(G, μ, ν)` with group structure, the map `(x, y) ↦ (yx, x⁻¹)` is measure-preserving with respect to the product measure `μ.prod ν`.
|
MeasureTheory.inv_absolutelyContinuous
theorem MeasureTheory.inv_absolutelyContinuous :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableInv G]
[inst_5 : μ.IsMulLeftInvariant], μ.inv.AbsolutelyContinuous μ
The theorem `MeasureTheory.inv_absolutelyContinuous` states that for any group `G` with a measurable space structure, a measurable multiplication operation, an inversion operation, and any `sigma-finite` measure `μ` on `G` that is left invariant under multiplication, the measure `A ↦ μ (A⁻¹)` (the pointwise inverse of `A`) is absolutely continuous with respect to `μ`. In other words, if a set `A` has measure `0` under `μ`, then its inverse also has measure `0` under `μ`.
More concisely: If `μ` is a `σ-finite`, left-invariant, measurable measure on the measurable group `(G, Σ, μ)` with measurable multiplication and inversion operations, then the measure of the inverse of a set of measure 0 is also 0: `A ↦ μ(A⁻¹)` is absolutely continuous with respect to `μ`.
|
MeasureTheory.measurePreserving_prod_neg_add
theorem MeasureTheory.measurePreserving_prod_neg_add :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableNeg G] [inst_6 : ν.IsAddLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1, -z.1 + z.2)) (μ.prod ν) (μ.prod ν)
This theorem states that for any type `G` that is a measurable space and an add group, and for which the addition of two elements is measurable, given two measures `μ` and `ν` such that `ν` is add-left-invariant and both `μ` and `ν` are sigma finite, and also given that the negation operation on `G` is measurable, the map that takes a pair `(x, y)` to `(x, -x+y)` is measure preserving with respect to the product measure of `μ` and `ν`.
More concisely: Given measurable spaces and add groups `(G, Σ)` with measurable addition and negation, sigma-finite measures `μ` and `ν` that are add-left-invariant for `ν`, the map `(x, y) ↦ (x, -x + y)` is measure-preserving with respect to the product measure `μ ⊤ ν`.
|
MeasureTheory.absolutelyContinuous_inv
theorem MeasureTheory.absolutelyContinuous_inv :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableInv G]
[inst_5 : μ.IsMulLeftInvariant], μ.AbsolutelyContinuous μ.inv
The theorem `MeasureTheory.absolutelyContinuous_inv` states that for any measurable space `G` with a group structure, which additionally has a measurable two-sided multiplication and measurable inversion, and for any σ-finite measure `μ` on this space that is left multiplication invariant, `μ` is absolutely continuous with respect to its inversion, `μ.inv`. In other words, if for any set `A`, the measure of the inverse set `A⁻¹` with respect to `μ` is zero, then the measure of `A` with respect to `μ` is also zero.
More concisely: If `μ` is a left multiplication-invariant, σ-finite measure on a measurable group `G` with measurable two-sided multiplication and measurable inversion, then `μ` is absolutely continuous with respect to its inversion `μ.inv`, i.e., `μ(A) = 0` if and only if `μ.inv(A⁻¹) = 0`.
|
MeasureTheory.measurePreserving_prod_neg_add_swap
theorem MeasureTheory.measurePreserving_prod_neg_add_swap :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddLeftInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2, -z.2 + z.1)) (μ.prod ν) (ν.prod μ)
This theorem states that for any type `G` that has a measurable space structure, an additive group structure, and a structure that allows for measurable addition, and for any two sigma-finite measures `μ` and `ν` on `G` where `μ` is add-left invariant and `G` supports measurable negation, the map `(x, y) ↦ (y, -y + x)` preserves measure when moving from the product measure `μ × ν` to `ν × μ`. In mathematical terms, if we have two measures on a set which has these properties, swapping the measures and applying the map won't change the total measure.
More concisely: For measurable additive groups `G` with sigma-finite add-left invariant measure `μ` and measures `μ` and `ν` that support measurable negation, the map `(x, y) ↦ (y, -y + x)` preserves measure between the product measures `μ × ν` and `ν × μ`.
|
MeasureTheory.measurePreserving_prod_add_swap_right
theorem MeasureTheory.measurePreserving_prod_add_swap_right :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : μ.IsAddRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 + z.2)) (μ.prod ν) (ν.prod μ)
For any type `G` that is a measurable space and an additive group, and for any measures `μ` and `ν` on `G` such that `ν` and `μ` are sigma-finite and `μ` is add-right-invariant, the theorem `MeasureTheory.measurePreserving_prod_add_swap_right` states that the map `(x, y) ↦ (y, x + y)` preserves the measure from `μ × ν` to `ν × μ`. In other words, the joint measure under the mapping `(x, y) ↦ (y, x + y)` remains the same.
More concisely: For measurable spaces and additive groups `G` with sigma-finite, add-right-invariant measure `μ` and another measure `ν`, the map `(x, y) ↦ (y, x + y)` preserves the measure on `G × G`, i.e., `μ × ν = ν × μ`.
|
MeasureTheory.measure_lintegral_sub_measure
theorem MeasureTheory.measure_lintegral_sub_measure :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
{s : Set G} [inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddLeftInvariant] [inst_7 : ν.IsAddLeftInvariant],
MeasurableSet s →
↑↑ν s ≠ 0 →
↑↑ν s ≠ ⊤ →
∀ (f : G → ENNReal),
Measurable f → ↑↑μ s * ∫⁻ (y : G), f (-y) / ↑↑ν ((fun x => x + -y) ⁻¹' s) ∂ν = ∫⁻ (x : G), f x ∂μ
The theorem `MeasureTheory.measure_lintegral_sub_measure` asserts that for any two measures `μ` and `ν` on a measurable space `G` that has an addition operation (making it an `AddGroup`) and is also `MeasurableAdd₂`, where both `μ` and `ν` are sigma finite, and the measures are left invariant under the addition operation. Given a measurable set `s` such that the measure of `s` under `ν` is non-zero and finite and a measurable function `f : G → ENNReal`, the measure of `s` under `μ` times the integral over `G` of the function `f(-y)` divided by the measure of `s` shifted by `-y` under `ν` (computed with respect to `ν`) equals the integral over `G` of `f` with respect to `μ`. This theorem is a technical result relating two different measures and is found in Halmos' Measure Theory (Section 60, Theorem A).
More concisely: For sigma-finite measures μ and ν on a measurable additive group G that are left invariant under addition and have non-zero, finite measures on a measurable set s, the integral of a measurable function f with respect to μ is equal to the product of the measure of s under μ and the integral of the function f(-y) with respect to ν, evaluated at shifted sets.
|
MeasureTheory.quasiMeasurePreserving_add_left
theorem MeasureTheory.quasiMeasurePreserving_add_left :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableNeg G]
[inst_5 : μ.IsAddRightInvariant] (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g + h) μ μ
This theorem states that for any type `G` equipped with a measurable space structure, an addition group structure, the ability to measure the result of adding two elements of the type `G`, and a right-invariant measure `μ` (one that doesn't change if you add an element to the right), if `G` also has a negation operation that is measurable, then left addition by any element `g` of `G` is quasi-measure preserving with respect to `μ`. In other words, adding an element on the left side 'almost' preserves the measure.
More concisely: For any measurable additive group `(G, +)` equipped with a right-invariant measure `μ`, if `-` is a measurable negation operation on `G`, then left multiplication by any element of `G` is a quasi-measure preserving transformation with respect to `μ`.
|
MeasureTheory.measurePreserving_prod_sub
theorem MeasureTheory.measurePreserving_prod_sub :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableNeg G] [inst_6 : ν.IsAddRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 - z.1)) (μ.prod ν) (μ.prod ν)
This theorem states that for any type `G`, which is equipped with a measurable space structure, an addition group structure, and a measure-additive structure, the map that sends a pair `(x, y)` to `(x, y - x)` preserves measure. This holds for any measures `μ` and `ν` on `G`, provided that `ν` is right-invariant under addition, and both `μ` and `ν` are sigma-finite. In other words, the measure of any set under the original measures `μ` and `ν` is the same as its measure under the transformed measures, after applying the function `(x, y) ↦ (x, y - x)`.
More concisely: For any sigma-finite measure `μ` and right-invariant, measure-additive measure `ν` on a measurable group `G`, the measure of a set under `μ` is equal to the measure of the set under the transformed measures `(μ, ν)` that sends `(x, y)` to `(x, y - x)`.
|
MeasureTheory.absolutelyContinuous_of_isAddLeftInvariant
theorem MeasureTheory.absolutelyContinuous_of_isAddLeftInvariant :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddLeftInvariant] [inst_7 : ν.IsAddLeftInvariant],
ν ≠ 0 → μ.AbsolutelyContinuous ν
The theorem `MeasureTheory.absolutelyContinuous_of_isAddLeftInvariant` states that for any two nonzero measures ν and μ on a measurable space G, which is also an add group with a measurable addition operation, if both ν and μ are left-invariant measures and both are sigma-finite, and if the negation operation on G is measurable, then μ is absolutely continuous with respect to ν. This means that if a set of points in G has measure zero according to ν, it also has measure zero according to μ.
More concisely: If ν and μ are two left-invariant, sigma-finite measures on the measurable add group G with a measurable negation operation, then μ is absolutely continuous with respect to ν.
|
MeasureTheory.measurePreserving_div_prod
theorem MeasureTheory.measurePreserving_div_prod :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
[inst_5 : MeasurableInv G] [inst_6 : μ.IsMulRightInvariant],
MeasureTheory.MeasurePreserving (fun z => (z.1 / z.2, z.2)) (μ.prod ν) (μ.prod ν)
This theorem is about measure theory in the context of a certain type `G`, which is equipped with a measurable space structure, a group structure, a measurable multiplication, a measurable inverse, a right invariant measure `μ`, and sigma-finite measures `μ` and `ν`. The theorem asserts that for all such settings, the map `(x, y) ↦ (x / y, y)` preserves the measure `μ × ν`. In other words, the measure of the set in the range of this function is the same as the measure of the original set in the domain of the function.
More concisely: Given measurable spaces `(X, Σ_X)` and `(Y, Σ_Y)` with group structures `G` and `H` respectively, equipped with sigma-finite measures `μ` and `ν`, the map `(x, y) ↦ (x / y, y)` from `(X × Y, Σ_X ⊤ Σ_Y)` to `(G × Y, Σ_G ⊤ Σ_Y)` is measurable and preserves the product measure `μ × ν`, i.e., `(μ × ν) ((x, y) ↦ (g, y)) = μ(x) * ν(y)`.
|
MeasureTheory.quasiMeasurePreserving_mul_left
theorem MeasureTheory.quasiMeasurePreserving_mul_left :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableInv G]
[inst_5 : μ.IsMulRightInvariant] (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g * h) μ μ
This theorem states that for any group `G` with a defined measurable space and a measurable binary multiplication operation, along with a sigma-finite measure `μ` that is right-invariant (meaning the measure of any set is unchanged if everything in the set is multiplied on the right by a group element), then left-multiplication by any element `g` of the group is quasi-measure-preserving. In other words, the measure of a set and the measure of the image of the set under left-multiplication by `g` only differ by a null set. This theorem should not be confused with the property that left-multiplication by `g` is measure-preserving, which is a stronger condition.
More concisely: For any sigma-finite, right-invariant measure `μ` on a group `G` with measurable binary multiplication, left-multiplication by any `g` in `G` is quasi-measure-preserving: the measure difference is a null set.
|
MeasureTheory.measure_add_lintegral_eq
theorem MeasureTheory.measure_add_lintegral_eq :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ ν : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ]
{s : Set G} [inst_5 : MeasurableNeg G] [inst_6 : μ.IsAddLeftInvariant] [inst_7 : ν.IsAddLeftInvariant],
MeasurableSet s →
∀ (f : G → ENNReal),
Measurable f → ↑↑μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ↑↑ν ((fun z => z + x) ⁻¹' s) * f (-x) ∂μ
This theorem, referred to as the computation performed in the proof of [Halmos, §60 Th. A], asserts that for any type `G` which is a measurable space and an add group, with the property that two-operator addition is measurable, and two measures `μ` and `ν` on this space (which are assumed to be sigma finite), any measurable set `s`, and any measurable function `f` from `G` to the extended nonnegative real numbers (ENNReal), the measure of `s` times the integral of `f` with respect to `ν` is equal to the integral over `G` of the measure of the preimage of `s` under the function `z -> z + x` times `f` of the negation of `x`, with respect to `μ`, given that both measures `μ` and `ν` are additive left invariants and the type `G` supports negation which is measurable. In mathematical notation, this would be expressed as:
\[ \mu(s) \int f(y) d\nu = \int \nu(\{z \in G : z + x \in s\}) f(-x) d\mu \]
for all measurable set `s` and all measurable functions `f : G → [0, ∞]`, where `μ` and `ν` are additive left invariant sigma finite measures on the measurable space `G`.
More concisely: For any measurable add group G with two-operator addition measurable, and two sigma-finite, additive left invariant measures μ and ν, the integral of f(y) dν over a measurable set s equals the integral of ν(z + x ∈ s) f(-x) dμ over G for all measurable functions f : G → [0, ∞].
|
MeasureTheory.quasiMeasurePreserving_add_right
theorem MeasureTheory.quasiMeasurePreserving_add_right :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableNeg G]
[inst_5 : μ.IsAddLeftInvariant] (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun h => h + g) μ μ
This theorem states that for any type `G` that is a measurable space, an addition group, and has measurable two-argument addition, given a measure `μ` on `G` that is σ-finite and left-invariant under addition, and any element `g` from `G`, the function that adds `g` to the right of its argument is quasi-measure-preserving with respect to the measure `μ`. This means that if a set of elements of `G` has a certain measure under `μ`, then the set of their sums with `g` has the same outer measure. This property is specific to *left*-invariant measures and should not be confused with the property of quasi-measure-preservation under *right*-addition.
More concisely: For any left-invariant, σ-finite measure `μ` on the measurable additive group `G`, the right translation by any fixed element `g` in `G` is a quasi-measure-preserving function with respect to `μ`.
|
MeasureTheory.neg_absolutelyContinuous
theorem MeasureTheory.neg_absolutelyContinuous :
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
(μ : MeasureTheory.Measure G) [inst_3 : MeasureTheory.SigmaFinite μ] [inst_4 : MeasurableNeg G]
[inst_5 : μ.IsAddLeftInvariant], μ.neg.AbsolutelyContinuous μ
This theorem states that for any type `G` which is a `MeasurableSpace`, an `AddGroup`, and has a `MeasurableNeg`, and any measure `μ` on `G` that is `SigmaFinite` and `IsAddLeftInvariant`, the measure `A ↦ μ (- A)`, where `- A` is the pointwise negation of `A`, is absolutely continuous with respect to the measure `μ`. In mathematical terms, this means that if `μ(A) = 0`, then `μ(-A) = 0` as well.
More concisely: For any measurable space and add group `G` with measurable negation, and Sigma-finite, additively invariant measure `μ`, the measure `μ` of the negation of any measurable set `A` is zero whenever `μ(A)` is zero.
|