MeasureTheory.eventually_nhds_one_measure_smul_diff_lt
theorem MeasureTheory.eventually_nhds_one_measure_smul_diff_lt :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
{μ : MeasureTheory.Measure G} [inst_3 : Group G] [inst_4 : TopologicalGroup G] [inst_5 : LocallyCompactSpace G]
[inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_7 : μ.InnerRegularCompactLTTop] {k : Set G},
IsCompact k → IsClosed k → ∀ {ε : ENNReal}, ε ≠ 0 → ∀ᶠ (g : G) in nhds 1, ↑↑μ (g • k \ k) < ε
This theorem states that in a topological group with a Borel measure that is finite on compact sets, given a compact and closed set `k`, the measure of the symmetric difference between `k` and its translates (i.e., the set of points `g • k \ k` where `g` is close enough to the identity element) can be made arbitrarily small. More formally, for any non-zero extended non-negative real number `ε`, there exists a neighborhood of the identity element such that for all `g` in this neighborhood, the measure of `g • k \ k` is less than `ε`. This is known as the continuity of the measure of translates of a compact set.
More concisely: In a topological group with a finite Borel measure on compact sets, the measure of the symmetric difference between a compact and closed set and its translates can be made arbitrarily small by choosing a sufficiently close translation.
|
MeasureTheory.Measure.measurePreserving_neg
theorem MeasureTheory.Measure.measurePreserving_neg :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Neg G] [inst_2 : MeasurableNeg G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsNegInvariant], MeasureTheory.MeasurePreserving Neg.neg μ μ
The theorem `MeasureTheory.Measure.measurePreserving_neg` states that for any type `G` which has a `MeasurableSpace` and `Neg` structure, any `MeasurableNeg` function `Neg.neg` and a measure `μ` in the `MeasureTheory.Measure` class that is invariant under negation (`MeasureTheory.Measure.IsNegInvariant μ`), the `Neg.neg` function is measure-preserving (denoted by `MeasureTheory.MeasurePreserving Neg.neg μ μ`). This means that the measure of a set and the measure of its image under negation are the same. The `Neg.neg` function computes the negative or opposite of a given number in `G`, and "measure-preserving" means that the measure of a set remains the same after the transformation.
More concisely: For any measure-preserving negation function and invariant-under-negation measure on a measurable space, the negation function is measure-preserving.
|
MeasureTheory.forall_measure_preimage_mul_iff
theorem MeasureTheory.forall_measure_preimage_mul_iff :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Mul G] [inst_2 : MeasurableMul G]
(μ : MeasureTheory.Measure G),
(∀ (g : G) (A : Set G), MeasurableSet A → ↑↑μ ((fun h => g * h) ⁻¹' A) = ↑↑μ A) ↔ μ.IsMulLeftInvariant
The theorem `MeasureTheory.forall_measure_preimage_mul_iff` states that for any type `G` that has a `MeasurableSpace` structure, a multiplication operation, and a `MeasurableMul` structure, and for any measure `μ` on `G`, the measure `μ` is left invariant under multiplication if and only if, for every element `g` of `G` and every measurable set `A` of `G`, the measure of the preimage of `A` under the function that multiplies `g` with every element, equals the measure of `A`. This theorem provides an alternative way to prove that a measure is left invariant under multiplication.
More concisely: For any measurable space `(G, Σ)` with a multiplication operation and a measurable multiplication structure, and any measure `μ` on `G`, `μ` is left invariant under multiplication if and only if for all `g ∈ G` and `A ∈ Σ`, `μ(g⁇⁻¹(A)) = μ(A)`, where `g⁇⁻¹(A)` denotes the preimage of `A` under the function that multiplies `g` with every element.
|
MeasureTheory.Measure.map_neg_eq_self
theorem MeasureTheory.Measure.map_neg_eq_self :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Neg G] (μ : MeasureTheory.Measure G)
[inst_2 : μ.IsNegInvariant], MeasureTheory.Measure.map Neg.neg μ = μ
The theorem `MeasureTheory.Measure.map_neg_eq_self` states that for any type `G` which is a measurable space and has a negation operation, and any measure `μ` on `G` that is invariant under negation (i.e., the measure of a set and its negation are the same), the measure obtained by pushing forward `μ` along the negation map is the same as the original measure `μ`. This means, intuitively, that if you transform all the points in your space by negation, the measure of the sets remains unchanged.
More concisely: For any measurable space (G, Σ) with negation operation and invariant-under-negation measure μ, the pushforward measure of μ under the negation map is equal to μ itself.
|
MeasureTheory.Measure.isAddHaarMeasure_map_of_isFiniteMeasure
theorem MeasureTheory.Measure.isAddHaarMeasure_map_of_isFiniteMeasure :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsAddHaarMeasure] [inst_4 : BorelSpace G]
[inst_5 : TopologicalAddGroup G] {H : Type u_4} [inst_6 : AddGroup H] [inst_7 : TopologicalSpace H]
[inst_8 : MeasurableSpace H] [inst_9 : BorelSpace H] [inst_10 : TopologicalAddGroup H]
[inst_11 : MeasureTheory.IsFiniteMeasure μ] (f : G →+ H),
Continuous ⇑f → Function.Surjective ⇑f → (MeasureTheory.Measure.map (⇑f) μ).IsAddHaarMeasure
The theorem `MeasureTheory.Measure.isAddHaarMeasure_map_of_isFiniteMeasure` states that for any finite additive Haar measure `μ` on a measurable space `G`, which also forms an additive group, a topological space, and a Borel space with a topological additive group structure, and for any continuous and surjective additive group homomorphism `f` from `G` to another similar group `H`, the image of `μ` under `f` is also an additive Haar measure. In other words, if `μ` is a finite additive Haar measure on `G`, and `f` is a continuous and surjective homomorphism mapping `G` to `H`, then the pushforward of `μ` through `f` is an additive Haar measure on `H`.
More concisely: Given a finite additive Haar measure μ on a topological Borel group G, and a continuous and surjective group homomorphism f : G -> H, the pushforward of μ through f is a finite additive Haar measure on H.
|
MeasureTheory.forall_measure_preimage_mul_right_iff
theorem MeasureTheory.forall_measure_preimage_mul_right_iff :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Mul G] [inst_2 : MeasurableMul G]
(μ : MeasureTheory.Measure G),
(∀ (g : G) (A : Set G), MeasurableSet A → ↑↑μ ((fun h => h * g) ⁻¹' A) = ↑↑μ A) ↔ μ.IsMulRightInvariant
This theorem states that for any measurable space `G` with a multiplication operation and a compatible measurability structure, a measure `μ` on `G` is right invariant under multiplication if and only if, for every element `g` of `G` and every measurable set `A`, the measure of the preimage of `A` under the function which multiplies every element by `g` is equal to the measure of `A`. Here, the preimage of `A` under a function `f` is the set of all inputs to `f` that produce an output in `A`.
More concisely: A measure μ on a measurable space (G, Σ) with multiplication operation is right invariant if and only if for all measurable sets A and g ∈ G, μ(A) = μ(g⁻¹(A)), where g⁻¹(A) denotes the preimage of A under the function g that multiplies every element by g.
|
MeasureTheory.forall_measure_preimage_add_iff
theorem MeasureTheory.forall_measure_preimage_add_iff :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Add G] [inst_2 : MeasurableAdd G]
(μ : MeasureTheory.Measure G),
(∀ (g : G) (A : Set G), MeasurableSet A → ↑↑μ ((fun h => g + h) ⁻¹' A) = ↑↑μ A) ↔ μ.IsAddLeftInvariant
This theorem, `MeasureTheory.forall_measure_preimage_add_iff`, provides an alternative method for proving that a measure `μ` is left invariant under addition. Specifically, for any type `G` that has a measurable space structure, an addition operation, and a measure `μ`, the measure `μ` is left invariant under addition if and only if for every `g` in `G` and for every measurable set `A` in `G`, the measure of the preimage of `A` under the function `(fun h => g + h)` is equal to the measure of `A`. In other words, adding a fixed element to all elements of a set doesn't change the measure of the set.
More concisely: For a measurable space (G, Σ) with addition operation +, and measure μ, μ is left invariant under addition if and only if for all g in G and measurable A in Σ, μ(A) = μ((fun h => g + h) ``^`` A).
|
MeasureTheory.Measure.inv_inv
theorem MeasureTheory.Measure.inv_inv :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [inst_2 : MeasurableInv G]
(μ : MeasureTheory.Measure G), μ.inv.inv = μ
The theorem `MeasureTheory.Measure.inv_inv` states that for any type `G` with a measurable space structure, an involution operation, and a measurable involution (expressed by the typeclasses `MeasurableSpace G`, `InvolutiveInv G`, and `MeasurableInv G` respectively), and for any measure `μ` over this type `G`, the measure obtained by applying the `inv` operation twice on `μ` is equal to `μ` itself. In other words, the `inv` operation on measures is its own inverse. This is similar to saying that the double application of the mathematical function of taking the inverse (`A ↦ 1/A`) to any measure gives back the original measure.
More concisely: For any measurable space `(G, Σ, μ)` with an involutive measurable involution, the measure `μ` is invariant under the involution operation, i.e., `μ = μ ∘ inv`.
|
MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant'
theorem MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant' :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
{μ : MeasureTheory.Measure G} [inst_3 : AddGroup G] [inst_4 : TopologicalAddGroup G]
[inst_5 : μ.IsAddLeftInvariant] {U : Set G},
(interior U).Nonempty → ↑↑μ U ≠ ⊤ → ∀ {K : Set G}, IsCompact K → ↑↑μ K < ⊤
The theorem `MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant'` states that for any measurable, topological group `G` with Borel space and a left-invariant measure `μ`, and a set `U` within that group, if the interior of `U` is not empty and the measure of `U` is finite, then for any compact set `K` within the group, the measure of `K` will also be finite. In other words, if a left-invariant measure gives a finite value to a set with a non-empty interior, it will also give a finite value to any compact set within the same group.
More concisely: Given a measurable, topological group with a Borel space and a finite, left-invariant measure, any compact subset has finite measure if the measure of a set with non-empty interior is finite.
|
MeasureTheory.measure_univ_of_isAddLeftInvariant
theorem MeasureTheory.measure_univ_of_isAddLeftInvariant :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
[inst_3 : AddGroup G] [inst_4 : TopologicalAddGroup G] [inst_5 : WeaklyLocallyCompactSpace G]
[inst_6 : NoncompactSpace G] (μ : MeasureTheory.Measure G) [inst_7 : μ.IsOpenPosMeasure]
[inst_8 : μ.IsAddLeftInvariant], ↑↑μ Set.univ = ⊤
The theorem `MeasureTheory.measure_univ_of_isAddLeftInvariant` states that, in a noncompact locally compact additive group G, if we have a left-invariant measure μ that assigns a positive value to open sets, then the measure of the entire set (i.e., the "mass") is infinite. Here, G is equipped with a measurable space structure, a topological space structure, a Borel space structure, and it is a topological additive group. Furthermore, G is a weakly locally compact space and a noncompact space. The measure μ is both an open positive measure (meaning it assigns positive value to nonempty open sets) and left invariant (meaning that translation by a group element doesn't change the measure). In this context, `Set.univ` refers to the universal set containing all elements of G, and `⊤` means infinity. This theorem is essentially capturing the intuition that in a "big enough" space, a "sufficiently positive" measure will have infinite total mass.
More concisely: In a noncompact, locally compact, topological additive group equipped with a left-invariant open positive measure, the measure of the universal set is infinite.
|
MeasureTheory.measurePreserving_mul_left
theorem MeasureTheory.measurePreserving_mul_left :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Mul G] [inst_2 : MeasurableMul G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsMulLeftInvariant] (g : G),
MeasureTheory.MeasurePreserving (fun x => g * x) μ μ
This theorem states that for any given type `G` that has a multiplicative structure and a measure theory defined on it, if the measure `μ` on the `G` type is left-multiplication invariant, then for any element `g` of type `G`, the function that multiplies `g` to the left of its input is a measure-preserving function with respect to measure `μ`. In mathematical terms, this means that for any `g` in `G`, the mapping `x ↦ g * x` is measure-preserving.
More concisely: If `μ` is a left-multiplication invariant measure on the multiplicative type `G`, then the left multiplication by any `g` in `G` is a measure-preserving function with respect to `μ`.
|
MeasureTheory.measurePreserving_mul_right
theorem MeasureTheory.measurePreserving_mul_right :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Mul G] [inst_2 : MeasurableMul G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsMulRightInvariant] (g : G),
MeasureTheory.MeasurePreserving (fun x => x * g) μ μ
This theorem states that for any type `G` that has a measurable space, a multiplication operation, and a measurable multiplication operation, along with a measure `μ` that is right invariant under multiplication, the function that multiplies each element by a fixed element `g` from `G` preserves the measure `μ`. In other words, the measure of any set under this multiplication operation is the same as the measure of the original set.
More concisely: For any measurable space `(G, Σ, μ)` with right-invariant measure `μ` under multiplication and measurable multiplication operation, the function `x ↦ g * x` preserves the measure `μ`, i.e., `μ(g * E) = μ(E)` for every set `E ∈ Σ`.
|
IsCompact.closure_subset_of_measurableSet_of_group
theorem IsCompact.closure_subset_of_measurableSet_of_group :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G] [inst_3 : Group G]
[inst_4 : TopologicalGroup G] {k s : Set G}, IsCompact k → MeasurableSet s → k ⊆ s → closure k ⊆ s
The theorem states that for any type `G` that has a measurable space, topological space, borel space structures and is a group with a topology, if a compact set `k` is a subset of a measurable set `s`, then the closure of `k` is also a subset of `s`. In other words, if a compact set is included in a measurable set, then its closure, which is the smallest closed set containing the compact set, is also included in that measurable set.
More concisely: If `k` is a compact subset of the measurable set `s` in a topological group `G` with borel structure, then the closure of `k` is included in `s`.
|
MeasureTheory.map_mul_left_eq_self
theorem MeasureTheory.map_mul_left_eq_self :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Mul G] (μ : MeasureTheory.Measure G)
[inst_2 : μ.IsMulLeftInvariant] (g : G), MeasureTheory.Measure.map (fun x => g * x) μ = μ
The theorem `MeasureTheory.map_mul_left_eq_self` states that for any type `G` with a measurable space structure and a multiplication operation, any measure `μ` on `G` that is left invariant under multiplication, and any element `g` of `G`, the measure obtained by pushing forward `μ` along the function that multiplies by `g` on the left is equal to `μ` itself. In other words, left multiplication by `g` does not change the measure `μ` if `μ` is left invariant under multiplication.
More concisely: For any measurable space `(G, Σ, μ)` with a left multiplication-invariant measure `μ`, the pushforward measure of `μ` under left multiplication by any element `g` in `G` is equal to `μ` itself.
|
MeasureTheory.Measure.isHaarMeasure_map_of_isFiniteMeasure
theorem MeasureTheory.Measure.isHaarMeasure_map_of_isFiniteMeasure :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsHaarMeasure] [inst_4 : BorelSpace G] [inst_5 : TopologicalGroup G]
{H : Type u_4} [inst_6 : Group H] [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H]
[inst_9 : BorelSpace H] [inst_10 : TopologicalGroup H] [inst_11 : MeasureTheory.IsFiniteMeasure μ] (f : G →* H),
Continuous ⇑f → Function.Surjective ⇑f → (MeasureTheory.Measure.map (⇑f) μ).IsHaarMeasure
This theorem states that if we have a finite Haar measure on a topological group, and we apply a continuous surjective group homomorphism, the measure of the image is again a Haar measure. Specifically, given a group `G` with a measurable space structure, a topological space structure, and a BorelSpace structure, and a Haar measure `μ` on `G` which is also finite, and another group `H` similarly equipped, if we have a continuous surjective group homomorphism from `G` to `H`, the image of `μ` under this homomorphism, defined by the map operation, is again a Haar measure.
Here, a Haar measure is a kind of measure that is invariant under translation in a group, and a group homomorphism is a function between two groups that preserves the group operations. A function is surjective if every element of the codomain is the image of at least one element of the domain.
More concisely: If `μ` is a finite Haar measure on the topological group `G`, and `f : G → H` is a continuous surjective group homomorphism, then `fᵀ*μ` is a Haar measure on `H`. (Here, `fᵀ` denotes the pushforward measure induced by `f`.)
|
MeasureTheory.isMulRightInvariant_map_smul
theorem MeasureTheory.isMulRightInvariant_map_smul :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Semigroup G] [inst_2 : MeasurableMul G]
{μ : MeasureTheory.Measure G} {α : Type u_4} [inst_3 : SMul α G] [inst_4 : SMulCommClass α Gᵐᵒᵖ G]
[inst_5 : MeasurableSpace α] [inst_6 : MeasurableSMul α G] [inst_7 : μ.IsMulRightInvariant] (a : α),
(MeasureTheory.Measure.map (fun x => a • x) μ).IsMulRightInvariant
The theorem `MeasureTheory.isMulRightInvariant_map_smul` states that for any semigroup `G` with a right invariant measure `μ`, if a scalar multiplication action (denoted as `a • x`) on `G` preserves multiplication and is also measurable, then the image measure under this action is still a right invariant measure. This is assuming that `G` is equipped with a structure that allows for multiplication to be measurable, the scalar multiplication action to be measurable, and the scalar multiplication to commute with `G`'s multiplication.
More concisely: If `G` is a semigroup with a right invariant measure `μ`, and scalar multiplication `a • x` on `G` preserves multiplication, is measurable, and commutes with `G`'s multiplication, then the image measure under this action is still right invariant.
|
MeasureTheory.Measure.isAddHaarMeasure_map
theorem MeasureTheory.Measure.isAddHaarMeasure_map :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsAddHaarMeasure] [inst_4 : BorelSpace G]
[inst_5 : TopologicalAddGroup G] {H : Type u_4} [inst_6 : AddGroup H] [inst_7 : TopologicalSpace H]
[inst_8 : MeasurableSpace H] [inst_9 : BorelSpace H] [inst_10 : T2Space H] [inst_11 : TopologicalAddGroup H]
(f : G →+ H),
Continuous ⇑f →
Function.Surjective ⇑f →
Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H) →
(MeasureTheory.Measure.map (⇑f) μ).IsAddHaarMeasure
This theorem states that for any additive group `G` with a topological space, a measurable space, a Borel space, a topological additive group, and an associated additive Haar measure `μ`, and for any other additive group `H` with a topological space, a measurable space, a Borel space, a T2 space (i.e., a Hausdorff space), and a topological additive group, if there is a continuous surjective group homomorphism `f : G →+ H` such that the limit of `f` tends towards the filter generated by complements to compact sets in `H` as the input `G` tends towards the filter generated by complements to compact sets in `G`, then the measure of `H` obtained by pushing forward `μ` by `f` is an additive Haar measure. This theorem essentially states that Haar measures are preserved under continuous surjective proper group homomorphisms.
More concisely: Given additive groups `G` and `H` with associated Haar measures `μ` and `ν`, if `f : G →+ H` is a continuous surjective group homomorphism with the property that the limit of `f(C)` is the filter of complements to compact sets in `H` as `C` approaches the filter of complements to compact sets in `G`, then `ν` is the pushforward of `μ` under `f`.
|
MeasureTheory.map_add_right_eq_self
theorem MeasureTheory.map_add_right_eq_self :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Add G] (μ : MeasureTheory.Measure G)
[inst_2 : μ.IsAddRightInvariant] (g : G), MeasureTheory.Measure.map (fun x => x + g) μ = μ
This theorem states that for any type `G` that has a measurable space structure and an addition operation, for any measure `μ` on `G` that is right-invariant under addition, and for any element `g` of `G`, the pushforward of `μ` along the map that adds `g` to each element is just `μ` itself. In other words, if a measure does not change when we shift all points in the space by a fixed amount, then applying this shift and measuring gives the same result as measuring without shifting.
More concisely: For any right-invariant measure `μ` on a measurable additive group `G`, the pushforward of `μ` under the translation by any element `g` in `G` is equal to `μ` itself.
|
MeasureTheory.measure_preimage_add
theorem MeasureTheory.measure_preimage_add :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsAddLeftInvariant] (g : G) (A : Set G),
↑↑μ ((fun h => g + h) ⁻¹' A) = ↑↑μ A
This theorem, `MeasureTheory.measure_preimage_add`, states that for any type `G` that has a measurable space structure, an addition group structure, and a measurable addition structure, and for any measure `μ` on `G` that is left-invariant under addition, and for any element `g` of `G` and any set `A` of `G`, the measure of the preimage of `A` under the function that adds `g` to every element, is equal to the measure of `A`.
In simple words, it states that if we have a measure that doesn't change when we shift everything by adding a fixed element, then the measure of a set is equal to the measure of the shifted set. In mathematical terms, it verifies the property $\mu(g + A) = \mu(A)$ where $\mu$ is a left-invariant measure on a group `G`, `g` is an element of `G`, and `A` is a subset of `G`.
More concisely: A left-invariant measure on a group is unchanged when shifting the set by an element: $\mu(g + A) = \mu(A)$.
|
MeasureTheory.forall_measure_preimage_add_right_iff
theorem MeasureTheory.forall_measure_preimage_add_right_iff :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Add G] [inst_2 : MeasurableAdd G]
(μ : MeasureTheory.Measure G),
(∀ (g : G) (A : Set G), MeasurableSet A → ↑↑μ ((fun h => h + g) ⁻¹' A) = ↑↑μ A) ↔ μ.IsAddRightInvariant
This theorem, named "MeasureTheory.forall_measure_preimage_add_right_iff", states that for any type `G` that has a `MeasurableSpace` structure, an addition operation, and satisfies the property `MeasurableAdd`, and for any measure `μ` on `G`, the measure `μ` is right invariant under addition if and only if for every element `g` of `G` and for every measurable set `A` of `G`, the measure of the preimage of `A` under the function that adds `g` to every element is equal to the measure of `A`.
In simpler terms, it means that shifting a set by adding a fixed element does not change its measure.
More concisely: For any measurable space `(G, Σ)` with addition operation and MeasurableAdd property, measure `μ` is right invariant if and only if for all `g in G` and measurable `A in Σ`, the measure of `{x in G | x + g in A}` equals the measure of `A`.
|
MeasureTheory.isAddRightInvariant_map_vadd
theorem MeasureTheory.isAddRightInvariant_map_vadd :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddSemigroup G] [inst_2 : MeasurableAdd G]
{μ : MeasureTheory.Measure G} {α : Type u_4} [inst_3 : VAdd α G] [inst_4 : VAddCommClass α Gᵃᵒᵖ G]
[inst_5 : MeasurableSpace α] [inst_6 : MeasurableVAdd α G] [inst_7 : μ.IsAddRightInvariant] (a : α),
(MeasureTheory.Measure.map (fun x => a +ᵥ x) μ).IsAddRightInvariant
The theorem `MeasureTheory.isAddRightInvariant_map_vadd` states that for any measurable space `G` with an add semigroup structure and a measurable addition operation, for any right invariant measure `μ` on `G`, for any type `α` which supports addition with `G` that is commutative and measurable, then the image of this measure under the addition operation is also right invariant. This assumes that the addition action preserves the structure of the set. This essentially means that moving the entire set (measured by `μ`) by a fixed amount (`a` from the set `α`) doesn't change the measure (size) of the set.
More concisely: For any measurable space `(G, Σ, μ)` with an add semigroup structure and measurable addition, if `μ` is a right invariant measure and `α` is a commutative type supporting measurable addition with `G`, then the image measure of `μ` under the addition operation with `α` is right invariant.
|
MeasureTheory.measure_univ_of_isMulLeftInvariant
theorem MeasureTheory.measure_univ_of_isMulLeftInvariant :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G] [inst_3 : Group G]
[inst_4 : TopologicalGroup G] [inst_5 : WeaklyLocallyCompactSpace G] [inst_6 : NoncompactSpace G]
(μ : MeasureTheory.Measure G) [inst_7 : μ.IsOpenPosMeasure] [inst_8 : μ.IsMulLeftInvariant], ↑↑μ Set.univ = ⊤
This theorem states that in a noncompact locally compact group, a left-invariant measure, which assigns positive value to open sets, assigns infinite measure to the universal set. Here, a "noncompact locally compact group" refers to a topological group that is locally compact but not compact, a "left-invariant measure" is a measure that remains the same after left multiplication, and the "universal set" refers to the set containing all elements of the group. The theorem thereby asserts that the total measure of all elements in such a group, under the given conditions, is infinite.
More concisely: In a noncompact locally compact group, every left-invariant measure assigns infinite measure to the group's universal set.
|
MeasureTheory.Measure.isAddHaarMeasure_of_isCompact_nonempty_interior
theorem MeasureTheory.Measure.isAddHaarMeasure_of_isCompact_nonempty_interior :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalAddGroup G] [inst_4 : BorelSpace G] (μ : MeasureTheory.Measure G)
[inst_5 : μ.IsAddLeftInvariant] (K : Set G),
IsCompact K → (interior K).Nonempty → ↑↑μ K ≠ 0 → ↑↑μ K ≠ ⊤ → μ.IsAddHaarMeasure
The theorem `MeasureTheory.Measure.isAddHaarMeasure_of_isCompact_nonempty_interior` states that for a given type `G` that is a measurable space, an additive group, a topological space, a topological additive group, and a Borel space, if a measure `μ` that is left-invariant assigns positive, but not infinite, mass to some compact set `K` whose interior is not empty, then this measure `μ` is an additive Haar measure. Here, a set is said to be compact if for every nontrivial filter that contains the set, there exists an element in the set such that every set of the filter meets every neighborhood of that element. The interior of a set is the largest open subset of that set. A measure is said to be additive Haar if it satisfies the properties of both additivity and Haar.
More concisely: If a left-invariant measure on a measurable space, additive group, topological space, and Borel space assigns positive, finite mass to some compact, non-empty set with non-empty interior, then it is an additive Haar measure.
|
AddEquiv.isAddHaarMeasure_map
theorem AddEquiv.isAddHaarMeasure_map :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsAddHaarMeasure] [inst_4 : BorelSpace G]
[inst_5 : TopologicalAddGroup G] {H : Type u_4} [inst_6 : AddGroup H] [inst_7 : TopologicalSpace H]
[inst_8 : MeasurableSpace H] [inst_9 : BorelSpace H] [inst_10 : TopologicalAddGroup H] (e : G ≃+ H),
Continuous ⇑e → Continuous ⇑e.symm → (MeasureTheory.Measure.map (⇑e) μ).IsAddHaarMeasure
This theorem, titled `AddEquiv.isAddHaarMeasure_map`, states that for any type `G` with a measurable space structure, an additive group structure, and a topological space structure, given a measure `μ` on `G` that has the property of being an Add Haar measure, and given that `G` also has a Borel space structure and a topological additive group structure; and for any type `H` which has similar structures, given an additive equivalence `e` from `G` to `H`, if both the map `e` and its inverse are continuous, then the pushforward (the image) of the measure `μ` under the map `e` is also an Add Haar measure on `H`.
In mathematical terms, if `μ` is a Haar measure on a topological additive group `G` and `e` is a continuous group isomorphism from `G` to another topological additive group `H`, then the pushforward of `μ` by `e` is a Haar measure on `H`.
More concisely: If `μ` is a Haar measure on the topological additive group `G`, and `e` is a continuous group isomorphism from `G` to another topological additive group `H`, then the pushforward of `μ` by `e` is a Haar measure on `H`.
|
MeasureTheory.isAddLeftInvariant_map_vadd
theorem MeasureTheory.isAddLeftInvariant_map_vadd :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddSemigroup G] [inst_2 : MeasurableAdd G]
{μ : MeasureTheory.Measure G} {α : Type u_4} [inst_3 : VAdd α G] [inst_4 : VAddCommClass α G G]
[inst_5 : MeasurableSpace α] [inst_6 : MeasurableVAdd α G] [inst_7 : μ.IsAddLeftInvariant] (a : α),
(MeasureTheory.Measure.map (fun x => a +ᵥ x) μ).IsAddLeftInvariant
This theorem states that given a left invariant measure on an additive semigroup, if we transform this measure under a left additive action (which preserves addition), the resulting measure is still left invariant. This holds for any type `G` that has the structure of a MeasurableSpace, an AddSemigroup, and a MeasurableAdd, and it also uses a measure `μ` on `G` that is left invariant under addition. The left additive action is specified by a vector addition operation `+ᵥ` that involves an additional type `α`, which is itself a MeasurableSpace and supports MeasurableVAdd with `G`. The left invariance of the transformed measure is asserted for every element `a` of `α`.
More concisely: Given a left invariant measure `μ` on a MeasurableSpace `(G, Σ)` that is an AddSemigroup with MeasurableAdd, and a left additive action `+ᵥ` of a MeasurableSpace `α` on `G`, the transformed measure `μ ∘ F` is left invariant, where `F : α → G` is the function induced by `+ᵥ`.
|
MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant'
theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant' :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
{μ : MeasureTheory.Measure G} [inst_3 : Group G] [inst_4 : TopologicalGroup G] [inst_5 : μ.IsMulLeftInvariant]
{U : Set G}, (interior U).Nonempty → ↑↑μ U ≠ ⊤ → ∀ {K : Set G}, IsCompact K → ↑↑μ K < ⊤
The theorem states that in the context of a measurable, topological group `G` that is also a Borel space, if we have a left-invariant measure `μ`, then for any set `U` within `G`, if the interior of `U` is nonempty and the measure of `U` under `μ` is finite (not infinity), then for any compact set `K` within `G`, the measure of `K` under `μ` is also finite. This theorem relates properties of measure theory and topological groups, establishing a connection between the finite measure of sets with nonempty interior and the finite measure of compact sets under a left-invariant measure.
More concisely: In a measurable, topological group endowed with a left-invariant finite measure, any set with nonempty interior and finite measure contains a compact subset with finite measure.
|
MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed
theorem MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
{μ : MeasureTheory.Measure G} [inst_3 : Group G] [inst_4 : TopologicalGroup G] [inst_5 : LocallyCompactSpace G]
[inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_7 : μ.InnerRegularCompactLTTop] {k : Set G},
IsCompact k → IsClosed k → Filter.Tendsto (fun g => ↑↑μ (g • k \ k)) (nhds 1) (nhds 0)
This theorem, named `MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed`, states that in the context of a measurable, topological group `G` (with Borel, topological, and group structures, which is also locally compact), given a measure `μ` that adheres to certain properties (i.e., it is finite on compact sets and has a property called InnerRegularCompactLTTop), and a set `k` within `G` that is both compact and closed, the measure of the symmetric difference between the set `k` and its translation by an element `g` of the group, denoted as `g • k \ k`, tends to zero as `g` tends to the identity element `1` of the group. In mathematical terms, as we move `k` by `g` closer and closer to `k` itself (i.e., as `g` approaches `1`), the measure of the resulting difference between `k` and its translation becomes smaller and smaller, approaching zero.
More concisely: Given a locally compact, measurable, topological group `G` with a finite, InnerRegularCompactLTTop measure `μ`, the measure of the symmetric difference between a fixed compact and closed set `k` in `G` and its translation by `g` approaches zero as `g` converges to the identity element in `G`.
|
MeasureTheory.measurePreserving_add_left
theorem MeasureTheory.measurePreserving_add_left :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Add G] [inst_2 : MeasurableAdd G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsAddLeftInvariant] (g : G),
MeasureTheory.MeasurePreserving (fun x => g + x) μ μ
This theorem states that for any group `G` equipped with an addition operation and a `MeasureTheory.Measure μ` that is invariant under left addition, the function `(fun x => g + x)` preserves the measure `μ`. In other words, when we shift every element in a set by a fixed amount `g` in the group `G`, the measure of the set remains unchanged.
More concisely: For any group `G` with invariant measure `μ` under left addition, the function `x ↔ g + x` preserves the measure `μ`, that is, `μ (set.image (fun x => g + x) s) = μ s` for any set `s` in `G`.
|
MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_compact
theorem MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_compact :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
{μ : MeasureTheory.Measure G} [inst_3 : AddGroup G] [inst_4 : TopologicalAddGroup G]
[inst_5 : μ.IsAddLeftInvariant] (K : Set G), IsCompact K → ↑↑μ K ≠ 0 → μ.IsOpenPosMeasure
This theorem states that if a left-invariant measure assigns a non-zero value to a compact set in a topological group with a Borel sigma algebra, then it assigns a non-zero value to any open set in the same group. More specifically, for any type `G` which has a measurable structure, a topological structure, is a Borel space, is an additive group, and a topological additive group, and for any measure `μ` on `G` that is left-invariant, if there is a compact set `K` such that the measure of `K` is non-zero, then the measure is a positive measure on all open sets.
In mathematical terms, a measure is said to be left-invariant if it is invariant under the left translation action of the group, meaning that the measure of a set is the same as the measure of its translate by any group element. A set is defined as compact if every open cover of the set has a finite subcover. And, a positive measure on open sets means that every non-empty open set has positive measure.
More concisely: If a left-invariant measure on a topological group with a Borel sigma algebra, which is a Borel space, an additive group, and a topological additive group, assigns a non-zero value to any compact set, then it is a positive measure on all open sets.
|
MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact
theorem MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
{μ : MeasureTheory.Measure G} [inst_3 : Group G] [inst_4 : TopologicalGroup G] [inst_5 : μ.IsMulLeftInvariant]
(K : Set G), IsCompact K → ↑↑μ K ≠ 0 → μ.IsOpenPosMeasure
The theorem `MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact` states that for any type `G` that has a measurable space, topological space, Borel space structure, and a measure `μ` which is left-invariant under group multiplication, if a compact set `K` has a non-zero `μ` measure, then any open set in `G` also has a non-zero `μ` measure. This means that if a left-invariant measure assigns a positive measure to a compact set, it also assigns a positive measure to any open set.
More concisely: If `μ` is a left-invariant measure on a compact, measurable and topological space `(G, Σ, μ)` with non-zero measure on a compact set `K`, then any open set in `G` has non-zero measure.
|
MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant
theorem MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
{μ : MeasureTheory.Measure G} [inst_3 : AddGroup G] [inst_4 : TopologicalAddGroup G]
[inst_5 : μ.IsAddLeftInvariant] (U : Set G),
IsOpen U → U.Nonempty → ↑↑μ U ≠ ⊤ → ∀ {K : Set G}, IsCompact K → ↑↑μ K < ⊤
This theorem states that if you have a left-invariant measure (a measure that remains unchanged under left translation of the group elements) that assigns a finite measure to a nonempty open set in a topological add group, then it will assign a finite measure to any compact set in the group. This is valid for any type `G` that has a measurable space structure, a topological space structure, a Borel space structure, an add group structure, and a topological add group structure.
More concisely: If a left-invariant measure on a topological add group assigns a finite measure to a nonempty open set, then it assigns a finite measure to any compact set.
|
MeasureTheory.map_add_left_eq_self
theorem MeasureTheory.map_add_left_eq_self :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Add G] (μ : MeasureTheory.Measure G)
[inst_2 : μ.IsAddLeftInvariant] (g : G), MeasureTheory.Measure.map (fun x => g + x) μ = μ
The theorem `MeasureTheory.map_add_left_eq_self` says that for any type `G` equipped with a measurable space structure and an addition operation, given a measure `μ` on `G` that is left-invariant under addition, and any element `g` of `G`, the pushforward of the measure `μ` under the map `x ↦ g + x` is equal to the original measure `μ`. In other words, adding a fixed element on the left to every point in `G` does not change the measure `μ`, reflecting the left-invariance of the measure.
More concisely: For any measurable space `(G, Σ)` with addition operation `+` and left-invariant measure `μ`, we have `μ ∘ (λ x, g + x) = μ`.
|
MeasureTheory.map_mul_right_eq_self
theorem MeasureTheory.map_mul_right_eq_self :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Mul G] (μ : MeasureTheory.Measure G)
[inst_2 : μ.IsMulRightInvariant] (g : G), MeasureTheory.Measure.map (fun x => x * g) μ = μ
The theorem `MeasureTheory.map_mul_right_eq_self` states that for every type `G` equipped with a measurable space structure and a multiplication operation, every measure `μ` on that type which is right multiplication invariant, and every element `g` of the type `G`, the pushforward of the measure `μ` by the function `(fun x => x * g)` (which multiplies every element by `g` on the right) is equal to the original measure `μ`. This is saying that, intuitively, the measure of sets doesn't change if we multiply each element in the set by a fixed element on the right.
More concisely: For any measurable space `(G, Σ, μ)` and measurable function `x ↦ x * g` on `G`, if `μ` is right multiplication invariant, then `μ = ∫(x ↦ μ(dx)) * g`.
|
MeasureTheory.isMulLeftInvariant_map_smul
theorem MeasureTheory.isMulLeftInvariant_map_smul :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Semigroup G] [inst_2 : MeasurableMul G]
{μ : MeasureTheory.Measure G} {α : Type u_4} [inst_3 : SMul α G] [inst_4 : SMulCommClass α G G]
[inst_5 : MeasurableSpace α] [inst_6 : MeasurableSMul α G] [inst_7 : μ.IsMulLeftInvariant] (a : α),
(MeasureTheory.Measure.map (fun x => a • x) μ).IsMulLeftInvariant
The theorem `MeasureTheory.isMulLeftInvariant_map_smul` states that for any measurable space `G` with an associated semigroup structure and a multiplication operation that is measurable, given a left invariant measure `μ` over `G` and a scalar type `α` such that `α` and `G` form a `SMul` (scalar multiplication) type with `G` and `α` commuting in their multiplication, and which is measurable in its scalar multiplication, if the measure `μ` is mul-left-invariant, then the image of `μ` under scalar multiplication by any element `a` from `α` is also mul-left-invariant. In simpler terms, if a measure is left invariant and we apply a scalar multiplication operation, the resulting measure remains left invariant, assuming that the scalar multiplication operation preserves multiplication.
More concisely: If `μ` is a left-invariant measure on the measurable semigroup `G` with a commuting scalar type `α` and measurable scalar multiplication, then the image of `μ` under scalar multiplication by any `a` in `α` is also left-invariant.
|
MulEquiv.isHaarMeasure_map
theorem MulEquiv.isHaarMeasure_map :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsHaarMeasure] [inst_4 : BorelSpace G] [inst_5 : TopologicalGroup G]
{H : Type u_4} [inst_6 : Group H] [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H]
[inst_9 : BorelSpace H] [inst_10 : TopologicalGroup H] (e : G ≃* H),
Continuous ⇑e → Continuous ⇑e.symm → (MeasureTheory.Measure.map (⇑e) μ).IsHaarMeasure
The theorem `MulEquiv.isHaarMeasure_map` states that given a continuous multiplicative equivalence `e` from a topological group `G` to a topological group `H`, if the measure `μ` on `G` is a Haar measure (a measure invariant under left translations), then the pushforward of the measure `μ` through `e` is a Haar measure on `H`. This holds if the function `e` and its inverse are both continuous, i.e., the transformation and its inverse do not cause "jumps" in the measure.
More concisely: If `e: G → H` is a continuous, bijective, and measurable function between topological groups `G` and `H`, such that both `e` and `e⁻¹` are continuous and `μ` is a Haar measure on `G`, then `μ ∘ e⁻¹` is a Haar measure on `H`.
|
MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant
theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [inst_2 : BorelSpace G]
{μ : MeasureTheory.Measure G} [inst_3 : Group G] [inst_4 : TopologicalGroup G] [inst_5 : μ.IsMulLeftInvariant]
(U : Set G), IsOpen U → U.Nonempty → ↑↑μ U ≠ ⊤ → ∀ {K : Set G}, IsCompact K → ↑↑μ K < ⊤
This theorem states that if you have a measure on a topological group that is left-invariant (i.e., the measure of a set doesn't change if you shift the whole set by multiplying it by a group element), and if this measure assigns a finite value ("mass") to a nonempty open set, then it will also assign a finite value to any compact set. In terms of measure theory and topology, this theorem provides a kind of finiteness condition for left-invariant measures on topological groups, under the assumption of finiteness for open sets. The theorem applies to any measurable topological group and any measure that is left-invariant with respect to the group operation.
More concisely: If a left-invariant measure on a measurable topological group assigns a finite mass to some nonempty open set, then it assigns a finite mass to every compact set.
|
MeasureTheory.Measure.isHaarMeasure_map
theorem MeasureTheory.Measure.isHaarMeasure_map :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsHaarMeasure] [inst_4 : BorelSpace G] [inst_5 : TopologicalGroup G]
{H : Type u_4} [inst_6 : Group H] [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H]
[inst_9 : BorelSpace H] [inst_10 : T2Space H] [inst_11 : TopologicalGroup H] (f : G →* H),
Continuous ⇑f →
Function.Surjective ⇑f →
Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H) →
(MeasureTheory.Measure.map (⇑f) μ).IsHaarMeasure
This theorem states that the image of a Haar measure under a continuous surjective proper group homomorphism is again a Haar measure. Specifically, for a given group `G` with a measurable space, topological space, a Haar measure `μ`, and Borel and topological group properties, and a target group `H` with similar properties, if there exists a homomorphism `f` from `G` to `H` that is continuous, surjective, and tends towards the filter of the complement of compact sets in `G` to the same in `H`, then the pushforward of the measure `μ` under `f` is again a Haar measure.
More concisely: If `f` is a continuous, surjective, and properly discontinuous group homomorphism between locally compact Abelian groups `G` and `H`, then the pushforward measure of `μ`, the Haar measure on `G`, is a Haar measure on `H`.
|
MeasureTheory.Measure.map_inv_eq_self
theorem MeasureTheory.Measure.map_inv_eq_self :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Inv G] (μ : MeasureTheory.Measure G)
[inst_2 : μ.IsInvInvariant], MeasureTheory.Measure.map Inv.inv μ = μ
This theorem states that for any type `G` that has a measurable space structure and an inversion operation (`Inv`), and for any measure `μ` on `G` that is invariant under inversion (`MeasureTheory.Measure.IsInvInvariant`), the pushforward of the measure `μ` under the inversion map is equal to `μ` itself. In simpler terms, it says that if a measure doesn't change when you 'flip' all the elements in the space it's defined on, then applying the 'flipping' transformation itself to the measure doesn't change the measure.
More concisely: For any measurable space `(G, Σ)` with an inversion operation `Inv` and a measure `μ` that is invariant under `Inv`, the pushforward measure `μ ∘ Inv` equals `μ`.
|
MeasureTheory.measure_preimage_add_right
theorem MeasureTheory.measure_preimage_add_right :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsAddRightInvariant] (g : G) (A : Set G),
↑↑μ ((fun h => h + g) ⁻¹' A) = ↑↑μ A
This theorem, named `MeasureTheory.measure_preimage_add_right`, is a statement in the field of measure theory regarding the invariance of a measure under the action of addition from the right. Specifically, for any type `G` that has a measurable space structure, an add group structure, and a measurable addition operation, any measure `μ` on `G` that is right-addition invariant, any element `g` of `G`, and any set `A` of `G`, the measure of the preimage of `A` under the function that adds `g` to every element is equal to the measure of `A` itself. This theorem asserts that if you shift each point in a set by some fixed amount, the measure of the set does not change.
More concisely: For any right-addition invariant measure μ on the measurable add group G, the measure of the preimage of a measurable set A under the right shift by g is equal to the measure of A.
|
MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior
theorem MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalGroup G] [inst_4 : BorelSpace G] (μ : MeasureTheory.Measure G)
[inst_5 : μ.IsMulLeftInvariant] (K : Set G),
IsCompact K → (interior K).Nonempty → ↑↑μ K ≠ 0 → ↑↑μ K ≠ ⊤ → μ.IsHaarMeasure
The theorem states that for any measurable, topological group with Borel space structure, if a measure is left-invariant and assigns a positive and finite mass to a compact set with non-empty interior, then this measure is a Haar measure. Here, a set is considered compact if for every nontrivial filter that contains the set, there exists a point in the set such that every set of the filter meets every neighborhood of the point. The interior of a set refers to the largest open subset of the set. A Haar measure is a kind of measure that is left-invariant, meaning the measure of a set does not change if the set is shifted left or right.
More concisely: In a measurable, topological group with a Borel space structure, a left-invariant measure assigning positive and finite mass to a compact set with non-empty interior is a Haar measure.
|
MeasureTheory.Measure.neg_neg
theorem MeasureTheory.Measure.neg_neg :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : MeasurableNeg G]
(μ : MeasureTheory.Measure G), μ.neg.neg = μ
This theorem states that for any type `G` which has a measurable space structure, an involutive negation operation, and a measurable negation operation, and for any measure `μ` on `G`, applying the operation `MeasureTheory.Measure.neg` twice to `μ` will yield `μ` back. Here, `MeasureTheory.Measure.neg` is a function mapping a measure `μ` to another measure defined by `μ` evaluated at the pointwise negation of the set `A`. This theorem is essentially stating that the double negation operation is an identity for the `MeasureTheory.Measure.neg` operation.
More concisely: For any measurable space `(G, Σ)` with a measurable involutive negation operation, if `μ` is a measure on `G`, then `MeasureTheory.Measure.neg (MeasureTheory.Measure.neg μ) = μ`.
|
MeasureTheory.measurePreserving_add_right
theorem MeasureTheory.measurePreserving_add_right :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Add G] [inst_2 : MeasurableAdd G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsAddRightInvariant] (g : G),
MeasureTheory.MeasurePreserving (fun x => x + g) μ μ
This theorem states that for any type `G` that has a measurable space structure, an addition operation, and a measurable addition property, and for any measure `μ` on `G` that is add-right invariant, the function that adds any given element `g` of `G` to `x` is measure-preserving under `μ`. In simpler terms, adding a fixed element `g` to any element `x` from the measure space does not change the measure of the set.
More concisely: For any measurable additive group `(G, +)` with a measure `μ` that is right-invariant, the translation map `x ↦ x + g` is a measure-preserving function for all `g ∈ G`.
|
MeasureTheory.measure_preimage_mul
theorem MeasureTheory.measure_preimage_mul :
∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul G]
(μ : MeasureTheory.Measure G) [inst_3 : μ.IsMulLeftInvariant] (g : G) (A : Set G),
↑↑μ ((fun h => g * h) ⁻¹' A) = ↑↑μ A
This theorem, referred to as `MeasureTheory.measure_preimage_mul`, states that for any type `G` possessing a `MeasurableSpace` structure, a `Group` structure, and a `MeasurableMul` structure, any `MeasureTheory.Measure` `μ` that is `MulLeftInvariant` and any element `g` of `G` and set `A` of `G`, the measure of the preimage of `A` under the function that multiplies `g` to the left (`fun h => g * h`) is equal to the measure of `A`. In other words, the left multiplication by `g` does not change the measure of the set `A` which is a property often needed in measure theory as applied to groups.
More concisely: For any measurable space `(G, Σ)` with a group and MeasurableMul structure, and any MulLeftInvariant measure `μ` on `(G, Σ)`, left multiplication by any group element `g` preserves the measure: `μ(g⁻¹(A)) = μ(A)` for all sets `A` in `Σ`.
|