MeasureTheory.Measure.haar.addHaarContent_self
theorem MeasureTheory.Measure.haar.addHaarContent_self :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
{K₀ : TopologicalSpace.PositiveCompacts G},
(fun s => ↑((MeasureTheory.Measure.haar.addHaarContent K₀).toFun s)) K₀.toCompacts = 1
The theorem `MeasureTheory.Measure.haar.addHaarContent_self` states that for any type `G` which is an additive group, a topological space, and a topological additive group, and any positive compact subset `K₀` of `G`, the value of `addHaarContent` function applied to `K₀` and then converted to a real number equals 1. In other words, the additive Haar content of a positive compact subset of a topological additive group is always 1 when evaluated on itself.
More concisely: For any positive compact subset `K₀` of a topological additive group `G`, the additive Haar content of `K₀` is equal to 1.
|
MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos
theorem MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
[inst_6 : LocallyCompactSpace G] [inst_7 : μ.InnerRegular] (E : Set G),
MeasurableSet E → 0 < ↑↑μ E → E - E ∈ nhds 0
**Steinhaus Theorem** states that in any locally compact group `G` equipped with an inner regular Haar measure `μ`, if we have any measurable set `E` whose measure is positive, then the difference set `E - E` forms a neighbourhood of the identity element `0`. In other words, for any point in `E`, the difference between this point and any other point in `E` is close to `0` in the sense of the topological space `G`. This theorem is a powerful tool in harmonic analysis and is a key component in the theory of locally compact groups.
More concisely: In a locally compact group `G` with an inner regular Haar measure `μ`, if `E` is a measurable set with positive measure, then for each point `x` in `E`, there exists a point `y` in `E` such that `x - y` is in the neighborhood of identity `0` in `G` (i.e., `(x - y) ∈ N(0)` for some open neighborhood `N(0)` of `0` in `G`).
|
MeasureTheory.Measure.regular_of_isAddLeftInvariant
theorem MeasureTheory.Measure.regular_of_isAddLeftInvariant :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : SecondCountableTopology G]
{μ : MeasureTheory.Measure G} [inst_6 : MeasureTheory.SigmaFinite μ] [inst : μ.IsAddLeftInvariant] {K : Set G},
IsCompact K → (interior K).Nonempty → ↑↑μ K ≠ ⊤ → μ.Regular
This theorem states that for any type `G` which is an additive group (`AddGroup G`), equipped with a topology (`TopologicalSpace G`), and having the property that the operation of addition is continuous (`TopologicalAddGroup G`), measurable (`MeasurableSpace G`), a Borel space (`BorelSpace G`) and has a second countable topology (`SecondCountableTopology G`), and for any `σ-finite` measure `μ` (`MeasureTheory.SigmaFinite μ`) on `G` that is invariant under left addition (`μ.IsAddLeftInvariant`), if there exists a compact set `K` (`IsCompact K`) in `G` such that `K` has a non-empty interior (`(interior K).Nonempty`) and the measure of `K` under `μ` is not infinite (`μ K ≠ ⊤`), then the measure `μ` is regular (`μ.Regular`).
In simpler terms, to show that an invariant `σ-finite` measure is regular, it suffices to show that the measure is finite on some compact set with a non-empty interior.
More concisely: Given an additive group `G` with a topology, a `σ-finite` and left-invariant measure `μ`, if there exists a compact set `K` in `G` with non-empty interior and finite measure under `μ`, then `μ` is regular.
|
MeasureTheory.Measure.haar.addIndex_defined
theorem MeasureTheory.Measure.haar.addIndex_defined :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G] {K V : Set G},
IsCompact K → (interior V).Nonempty → ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g + h) ⁻¹' V}
The theorem `MeasureTheory.Measure.haar.addIndex_defined` states that for any type `G` with additive group structure and a topology compatible with this group structure, if `K` is a compact set and `V` is a set with nonempty interior, then there exists a natural number `n` which is the cardinality of a finite set `t` such that `K` is contained within the union over all `g` in `t` of the preimages under the function `h => g + h` of the set `V`. This essentially provides a measure for the covering of the compact set `K` with "shifted" versions of an open set `V`.
More concisely: For any compact set `K` and open set `V` in a topological additive group `G`, there exists a finite set `t` such that `K` is covered by the translations of `V` by elements in `t`.
|
MeasureTheory.Measure.haarMeasure_eq_iff
theorem MeasureTheory.Measure.haarMeasure_eq_iff :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : SecondCountableTopology G]
(K₀ : TopologicalSpace.PositiveCompacts G) (μ : MeasureTheory.Measure G) [inst_6 : MeasureTheory.SigmaFinite μ]
[inst_7 : μ.IsMulLeftInvariant], MeasureTheory.Measure.haarMeasure K₀ = μ ↔ ↑↑μ ↑K₀ = 1
This theorem states that for a given type `G` which forms a group, a topological space, a topological group, a measurable space, a Borel space, and has a second countable topology, if we have a positive compact subset `K₀` of this space and a sigma-finite measure `μ` on `G` which is left-invariant (i.e., for every measurable set and every group element, the measure of the set obtained by left multiplication by the group element equals the measure of the original set), then this measure `μ` equals the Haar measure defined by `K₀` if and only if the measure of the set `K₀` under `μ` equals 1. The Haar measure is a measure on the locally compact group `G`, scaled so that the Haar measure of `K₀` equals 1.
More concisely: Given a locally compact group G endowed with a second countable topology, a positive compact subset K₀, and a sigma-finite left-invariant measure μ, the measure μ is the Haar measure if and only if μ(K₀) = 1.
|
MeasureTheory.Measure.haar.index_defined
theorem MeasureTheory.Measure.haar.index_defined :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G] {K V : Set G},
IsCompact K → (interior V).Nonempty → ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
This theorem states that if `K` is a compact set and `V` has a nonempty interior in a topological group `G`, then there exists a well-defined index `(K : V)`. Concretely, there exists a finite set `t` such that the cardinality `n` of `t` satisfies that `K` is contained in the union of the preimages of `V` under left multiplication by elements of `t`.
More concisely: If `K` is a compact subset of a topological group `G` and `V` has nonempty interior, then there exists a finite set `t` such that `K` is covered by the left translates of `V` by elements of `t`.
|
MeasureTheory.Measure.addHaarMeasure_self
theorem MeasureTheory.Measure.addHaarMeasure_self :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G},
↑↑(MeasureTheory.Measure.addHaarMeasure K₀) ↑K₀ = 1
This theorem states that for any given additive group `G`, which also has the structures of a topological space, a topological additive group, a measurable space, and a Borel space, and given `K₀`, a positive compact subset of `G`, the Haar measure associated with `K₀` applied to `K₀` itself is 1. In other words, it asserts that the Haar measure of a positive compact set in the context of an additive topological group is normalized to 1.
More concisely: For any additive topological group endowed with a translation-invariant Borel measure, the Haar measure of any positive compact subset equals 1.
|
MeasureTheory.Measure.haar.index_pos
theorem MeasureTheory.Measure.haar.index_pos :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G]
(K : TopologicalSpace.PositiveCompacts G) {V : Set G},
(interior V).Nonempty → 0 < MeasureTheory.Measure.haar.index (↑K) V
The theorem `MeasureTheory.Measure.haar.index_pos` states that for any topological group `G`, given a nonempty compact subset `K` of `G` and any set `V` whose interior is non-empty, the Haar index of `K` with respect to `V` is positive. The Haar index, denoted `(K : V)`, is the smallest number of translations of `V` necessary to cover `K`. In this context, a group is a mathematical structure that combines an associative operation and an identity element with the ability to find an inverse for every element, and a topological group is a group that is also a topological space in a way such that the group's operations are continuous functions.
More concisely: For any topological group `G`, the Haar index of a nonempty compact subset `K` with respect to an open set `V` of `G` is a positive number.
|
MeasureTheory.Measure.haarMeasure_unique
theorem MeasureTheory.Measure.haarMeasure_unique :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : SecondCountableTopology G]
(μ : MeasureTheory.Measure G) [inst_6 : MeasureTheory.SigmaFinite μ] [inst_7 : μ.IsMulLeftInvariant]
(K₀ : TopologicalSpace.PositiveCompacts G), μ = ↑↑μ ↑K₀ • MeasureTheory.Measure.haarMeasure K₀
This theorem, referred to as the Uniqueness of left-invariant measures, states that in a second-countable locally compact group, any σ-finite measure that is left-invariant is simply a scalar multiple of the Haar measure. This implies that all left-invariant measures are essentially "equivalent" in the sense that they are rescalings of each other. Note that this condition is slightly weaker than requiring the measure to be a Haar measure, in particular, the measure is not required to be non-zero. The theorem also has an alternate version that does not assume second-countability.
More concisely: In a second-countable locally compact group, any σ-finite left-invariant measure is proportional to the Haar measure.
|
Mathlib.MeasureTheory.Measure.Haar.Basic._auxLemma.30
theorem Mathlib.MeasureTheory.Measure.Haar.Basic._auxLemma.30 : ∀ {r₁ r₂ : NNReal}, (r₁ ≤ r₂) = (↑r₁ ≤ ↑r₂)
This theorem, in the context of measure theory in the Haar package of Mathlib, states that for any two non-negative real numbers `r₁` and `r₂`, the proposition that `r₁` is less than or equal to `r₂` is equivalent to the proposition that the real number equivalent of `r₁` is less than or equal to the real number equivalent of `r₂`. In other words, the order relation on the non-negative real numbers is the same as the order relation on the corresponding real numbers.
More concisely: For any non-negative real numbers `r₁` and `r₂`, `r₁ ≤ r₂` if and only if their real numbers representations `ℝ(r₁)` and `ℝ(r₂)` satisfy `ℝ(r₁) ≤ ℝ(r₂)`.
|
MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos
theorem MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
[inst_6 : LocallyCompactSpace G] [inst_7 : μ.InnerRegular] (E : Set G),
MeasurableSet E → 0 < ↑↑μ E → E / E ∈ nhds 1
**Steinhaus Theorem** states that in the context of a locally compact group `G` that possesses an inner regular Haar measure `μ`, given any measurable set `E` with positive measure, the quotient set `E / E` (which represents the set of all ratios from `E`) becomes a neighborhood of the identity element `1`. This theorem is instrumental in demonstrating important properties of locally compact groups and their measures.
More concisely: In a locally compact group `G` with an inner regular Haar measure `μ`, given any measurable set `E` with positive measure, the quotient set `E / E` contains a neighborhood of the identity element `1`.
|
MeasureTheory.Measure.haar.addIndex_pos
theorem MeasureTheory.Measure.haar.addIndex_pos :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
(K : TopologicalSpace.PositiveCompacts G) {V : Set G},
(interior V).Nonempty → 0 < MeasureTheory.Measure.haar.addIndex (↑K) V
This theorem states that for any additive group `G` equipped with a topological space structure and a topological addition operation, given a non-empty positive compact set `K` and any set `V` whose interior is non-empty, the additive version of the Haar index of the sets `K` and `V` is strictly positive. The Haar index, in this context, is defined as the infimum of the size of finite coverings of `K` by translates of `V`.
More concisely: For any additive group `G` with a topology and compact, non-empty set `K`, if the interior of set `V` is non-empty, then the Haar index of `K` and `V` is strictly positive.
|
MeasureTheory.Measure.haar.haarContent_self
theorem MeasureTheory.Measure.haar.haarContent_self :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G]
{K₀ : TopologicalSpace.PositiveCompacts G},
(fun s => ↑((MeasureTheory.Measure.haar.haarContent K₀).toFun s)) K₀.toCompacts = 1
This theorem, named `MeasureTheory.Measure.haar.haarContent_self`, states that for any Group `G` with a topology `inst_1` making it a TopologicalSpace, and `inst_2` making it a TopologicalGroup, and for any `K₀` as a positive compact subset of `G`, applying the `haarContent` function on `K₀` and then converting it to a real number will yield 1. In the context of Measure Theory, this implies that the Haar measure of a topological group on its own positive compact set is equal to 1.
More concisely: For any topological group equiped with a Haar measure, the Haar measure of any positive compact subset is equal to 1.
|
MeasureTheory.Measure.haar.is_left_invariant_haarContent
theorem MeasureTheory.Measure.haar.is_left_invariant_haarContent :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G]
{K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G),
(fun s => ↑((MeasureTheory.Measure.haar.haarContent K₀).toFun s))
(TopologicalSpace.Compacts.map (fun b => g * b) ⋯ K) =
(fun s => ↑((MeasureTheory.Measure.haar.haarContent K₀).toFun s)) K
This theorem, named `is_left_invariant_haarContent`, establishes the left invariance property of the Haar content, a concept in the field of measure theory. Specifically, it states that for any given topological group `G`, any positive compact subset `K₀` of `G`, any element `g` from `G`, and any compact subset `K` of `G`, the Haar content of the image of `K` under the map `b ↦ g * b` is equal to the Haar content of `K` itself. This essentially means that the Haar content is invariant under left multiplication by elements of the group.
More concisely: For any topological group G, compact subset K0, and element g in G, the Haar content of g * K is equal to the Haar content of K.
|
Mathlib.MeasureTheory.Measure.Haar.Basic._auxLemma.34
theorem Mathlib.MeasureTheory.Measure.Haar.Basic._auxLemma.34 : ∀ {p q : NNReal}, (↑p = ↑q) = (p = q)
The theorem `Mathlib.MeasureTheory.Measure.Haar.Basic._auxLemma.34` states that for every two non-negative real numbers `p` and `q` (represented as `NNReal`), the statement that their real number equivalents (obtained by the coercion `↑`) are equal is equivalent to the statement that `p` and `q` themselves are equal. This theorem essentially confirms that the equality of `p` and `q` in the `NNReal` type corresponds directly to their equality as real numbers.
More concisely: The theorem asserts that two non-negative real numbers `p` and `q` are equal if and only if their real number representations `↑p` and `↑q` are equal.
|
MeasureTheory.Measure.haarMeasure_self
theorem MeasureTheory.Measure.haarMeasure_self :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G},
↑↑(MeasureTheory.Measure.haarMeasure K₀) ↑K₀ = 1
This theorem states that for any given type `G` that is a group, a topological space, a topological group, a measurable space, and a Borel space, and any positive compact `K₀` in this space, the Haar measure of `K₀` is equal to 1. The Haar measure is a special kind of measure that is used in the theory of locally compact topological groups.
More concisely: For any type `G` that is a locally compact topological group endowed with a Haar measure, the Haar measure of any positive compact subset `K₀` is equal to 1.
|
MeasureTheory.Measure.haar.is_left_invariant_addHaarContent
theorem MeasureTheory.Measure.haar.is_left_invariant_addHaarContent :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
{K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G),
(fun s => ↑((MeasureTheory.Measure.haar.addHaarContent K₀).toFun s))
(TopologicalSpace.Compacts.map (fun b => g + b) ⋯ K) =
(fun s => ↑((MeasureTheory.Measure.haar.addHaarContent K₀).toFun s)) K
This theorem, `MeasureTheory.Measure.haar.is_left_invariant_addHaarContent`, establishes the left invariance property of the additive Haar content on a topological additive group. Specifically, it states that for any type `G` which forms an additive group and a topological additive group, and for any positive compact `K₀` in `G` and any compact `K` in `G`, the additive Haar content of the translation of `K` by an element `g` of `G` is the same as the additive Haar content of `K`. In other words, translating a compact set by adding an element doesn't change its additive Haar content, thus making the Haar content invariant under translation (`g + b` where `b` is an element of the compact set). This reflects one of the fundamental properties of the Haar measure in the context of additive topological groups.
More concisely: The additive Haar content of a compact set in an additive topological group is unchanged under translation by an element of the group.
|
MeasureTheory.Measure.addHaarMeasure_unique
theorem MeasureTheory.Measure.addHaarMeasure_unique :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : SecondCountableTopology G]
(μ : MeasureTheory.Measure G) [inst_6 : MeasureTheory.SigmaFinite μ] [inst_7 : μ.IsAddLeftInvariant]
(K₀ : TopologicalSpace.PositiveCompacts G), μ = ↑↑μ ↑K₀ • MeasureTheory.Measure.addHaarMeasure K₀
This theorem, known as the "Uniqueness of Left-Invariant Measures," states that in a second-countable, locally compact additive group, any σ-finite left-invariant measure is a scalar multiple of the additive Haar measure. The theorem does not require the measure to be non-zero, making it slightly weaker than if we assume the measure to be an additive Haar measure. For a version of this theorem without the second-countability assumption, refer to `isAddHaarMeasure_eq_smul_of_regular`.
More concisely: In a second-countable, locally compact additive group, any σ-finite left-invariant measure is equal to a scalar multiple of the additive Haar measure.
|
MeasureTheory.Measure.regular_of_isMulLeftInvariant
theorem MeasureTheory.Measure.regular_of_isMulLeftInvariant :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : SecondCountableTopology G]
{μ : MeasureTheory.Measure G} [inst_6 : MeasureTheory.SigmaFinite μ] [inst : μ.IsMulLeftInvariant] {K : Set G},
IsCompact K → (interior K).Nonempty → ↑↑μ K ≠ ⊤ → μ.Regular
The theorem `MeasureTheory.Measure.regular_of_isMulLeftInvariant` states that for a given set `K` in a group `G` with a topology, topological group structure, a measurable space structure, a Borel measurable space structure, and a second countable topology, if the measure `μ` of the group is sigma-finite and left invariant under multiplication, then to establish that this measure is regular, it suffices to show that `μ` is finite on `K`, where `K` is compact and has a non-empty interior. A regular measure is one that captures a balance between "smallness" of sets and "largeness" of their complements. This balance is of particular importance in measure theory and topological spaces.
More concisely: For a sigma-finite, left-invariant measure `μ` on a second countable, topological group `(G, τ)` with a measurable space structure and Borel algebra, if `μ` is finite on some compact, non-empty set `K` with a non-empty interior, then `μ` is a regular measure.
|