MeasureTheory.Measure.absolutelyContinuous_isAddHaarMeasure
theorem MeasureTheory.Measure.absolutelyContinuous_isAddHaarMeasure :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G]
[inst_6 : SecondCountableTopology G] (μ ν : MeasureTheory.Measure G) [inst_7 : MeasureTheory.SigmaFinite μ]
[inst_8 : μ.IsAddLeftInvariant] [inst : ν.IsAddHaarMeasure], μ.AbsolutelyContinuous ν
This theorem states that in the context of a topological space G that has the structure of an additive group, a topological additive group, a measurable space, a Borel space, a locally compact space, and a space with second-countable topology, given two measures `μ` and `ν` on the space G, where `μ` is sigma-finite and left-invariant under addition, and `ν` is an additive Haar measure, the measure `μ` is absolutely continuous with respect to the measure `ν`. In mathematical terms, this means that if a set has measure zero under `ν`, then it also has measure zero under `μ`.
More concisely: In a topological group G endowed with a sigma-finite left-invariant measure μ and an additive Haar measure ν, μ is absolutely continuous with respect to ν.
|
MeasureTheory.Measure.absolutelyContinuous_isHaarMeasure
theorem MeasureTheory.Measure.absolutelyContinuous_isHaarMeasure :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G]
[inst_6 : SecondCountableTopology G] (μ ν : MeasureTheory.Measure G) [inst_7 : MeasureTheory.SigmaFinite μ]
[inst_8 : μ.IsMulLeftInvariant] [inst : ν.IsHaarMeasure], μ.AbsolutelyContinuous ν
This theorem states that in the context of a second countable group `G` that is locally compact and a Borel space, any invariant sigma-finite measure `μ` is absolutely continuous with respect to a Haar measure `ν`. Here, `μ` is assumed to be left-invariant under multiplication, and `ν` is assumed to be a Haar measure. In other words, if every set of measure zero under `ν` also has measure zero under `μ` (which is the definition of `μ` being absolutely continuous with respect to `ν`), then in these topological and algebraic conditions, `μ` will shadow `ν` to the effect that if `ν` doesn't notice a set (assigns it measure zero), then `μ` won't either.
More concisely: In a second countable, locally compact group endowed with a Haar measure, every left-invariant sigma-finite Borel measure is absolutely continuous with respect to the Haar measure.
|
MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport
theorem MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
[inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsMulLeftInvariant],
∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
This theorem states that if we are given two left-invariant measures, say `μ'` and `μ`, which are finite on compact sets in a topological group `G`, then they coincide in a specific way. This coincidence implies that the measures assign the same value to the integral of continuous functions with compact support, apart from a multiplicative constant `c`. In other words, there exists a constant `c` such that for any continuous function `f` with compact support, the integral of `f` with respect to `μ'` is equal to the integral of `f` with respect to `c • μ`. Here, `c • μ` denotes the measure `μ` scaled by the constant `c`.
More concisely: Given two finite left-invariant measures `μ'` and `μ` on a compact set of a topological group `G`, there exists a constant `c` such that for all continuous functions `f` with compact support, the integral of `f` with respect to `μ'` equals `c *` the integral of `f` with respect to `μ`.
|
MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular
theorem MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G]
(μ' μ : MeasureTheory.Measure G) [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ']
[inst_8 : μ'.IsMulLeftInvariant] [inst_9 : μ.Regular] [inst_10 : μ'.Regular], μ' = μ'.haarScalarFactor μ • μ
The theorem, "Uniqueness of left-invariant measures," states that for any topological space G that is also a Group, TopologicalGroup, Measurable Space, Borel Space, and Locally Compact Space, if we have two measures μ' and μ, where μ is a Haar measure, and both measures are finite on compacts and regular. If additionally μ' is left-invariant, then these two measures coincide up to a multiplicative constant, specifically the Haar scalar factor of μ' with respect to μ times μ.
More concisely: Given a topological group G that is a Measurable Space, Borel Space, Locally Compact Space, and equipped with a Haar measure μ, if there exists another finite and regular measure μ' that is left-invariant, then μ' equals μ up to a multiplicative constant, specifically the Haar scalar factor of μ' with respect to μ.
|
IsCompact.measure_eq_biInf_integral_hasCompactSupport
theorem IsCompact.measure_eq_biInf_integral_hasCompactSupport :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {k : Set X},
IsCompact k →
∀ (μ : MeasureTheory.Measure X) [inst_3 : MeasureTheory.IsFiniteMeasureOnCompacts μ]
[inst_4 : μ.InnerRegularCompactLTTop] [inst_5 : LocallyCompactSpace X] [inst_6 : RegularSpace X],
↑↑μ k =
⨅ f,
⨅ (_ : Continuous f),
⨅ (_ : HasCompactSupport f),
⨅ (_ : Set.EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)
The theorem `IsCompact.measure_eq_biInf_integral_hasCompactSupport` states that in a locally compact, regular space (a topological space where every point has a compact neighborhood and for any two disjoint closed sets there exists a disjoint open set separating them), which has an inner regular measure (a measure that assigns to each measurable set the infimum of the measure of the compact subsets that cover it), the measure of a compact set `k` is equal to the infimum of the integrals of all compactly supported functions (functions that are equal to zero outside a compact set) that are equal to `1` on `k`. This holds for the measure of `k` in any finite measure space where the measure is finite on compact sets.
More concisely: In a locally compact, regular space with finite measure on compact sets that has an inner regular measure, the measure of a compact set equals the infimum of integrals of compactly supported functions equal to 1 on that set.
|
MeasureTheory.Measure.isHaarMeasure_eq_smul
theorem MeasureTheory.Measure.isHaarMeasure_eq_smul :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G]
[inst_6 : SecondCountableTopology G] (μ' μ : MeasureTheory.Measure G) [inst_7 : μ.IsHaarMeasure]
[inst_8 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_9 : μ'.IsMulLeftInvariant],
μ' = μ'.haarScalarFactor μ • μ
This theorem, named `MeasureTheory.Measure.isHaarMeasure_eq_smul`, states that in the context of a second countable group `G` that is also a topological space, a group, a topological group, a measurable space, a Borel space, and a locally compact space, for any two Haar measures `μ'` and `μ`, where `μ` is a Haar measure and `μ'` is a measure that is finite on compacts and left invariant under multiplication, `μ'` is equal to `μ'` scaled by the Haar scalar factor of `μ`. In simpler terms, two Haar measures are equal up to a multiplicative constant in a second countable group.
More concisely: In a second countable, locally compact group endowed with its Borel sigma-algebra, any two Haar measures are equal up to a multiplicative constant.
|
MeasureTheory.Measure.haarScalarFactor_eq_one_of_isProbabilityMeasure
theorem MeasureTheory.Measure.haarScalarFactor_eq_one_of_isProbabilityMeasure :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G]
(μ' μ : MeasureTheory.Measure G) [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
[inst_7 : MeasureTheory.IsProbabilityMeasure μ'] [inst_8 : μ.IsHaarMeasure] [inst : μ'.IsHaarMeasure], μ' = μ
This theorem, named "MeasureTheory.Measure.haarScalarFactor_eq_one_of_isProbabilityMeasure", establishes the uniqueness of Haar measures in the context of probability measures. In particular, it states that if we have two Haar measures, 'μ' and 'μ'', both of which are probability measures on a locally compact topological group 'G' with a Borel measurable space, then 'μ' and 'μ'' are identical.
More concisely: If two Haar measures, μ and μ', are both probability measures on a locally compact topological group G, then μ = μ'.
|
MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo
theorem MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {μ ν : MeasureTheory.Measure G}
[inst_5 : MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts ν]
[inst_7 : μ.IsMulLeftInvariant] [inst_8 : ν.IsMulRightInvariant] [inst_9 : ν.IsOpenPosMeasure] {f g : G → ℝ},
Continuous f →
HasCompactSupport f →
Continuous g →
HasCompactSupport g →
0 ≤ g →
∀ {x₀ : G},
g x₀ ≠ 0 →
∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
The theorem states that in a topological group `G` with a left invariant measure `μ` and a right invariant measure `ν`, given any continuous functions `f` and `g` that have compact support and `g` is non-negative, and a fixed point `x₀` in `G` where the value of `g` is not zero, the integral of `f` with respect to `μ` can be expressed as a product of a scaling factor, which is the integral of `g` with respect to `μ`, and the integral with respect to `ν` of the function `f` multiplied by the reciprocal of another integral, taken with respect to `ν`, of `g` applied to the product of the inverse of a group element `z` and `y`.
More concisely: In a topological group `G` with left invariant measure `μ` and right invariant measure `ν`, for any continuous functions `f` and `g` with compact support and `g(x_0) ≠ 0`, the integral of `f` with respect to `μ` equals the product of the integral of `g` with respect to `μ`, and the integral of `f(z \* y) / g(z \* y)` with respect to `ν`, where `z` is any element in `G` and `y = x_0`.
|
MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular
theorem MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G]
(μ' μ : MeasureTheory.Measure G) [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ']
[inst_8 : μ'.IsMulLeftInvariant] [inst_9 : μ.InnerRegular] [inst_10 : μ'.InnerRegular],
μ' = μ'.haarScalarFactor μ • μ
This theorem, known as the **Uniqueness of left-invariant measures**, states that for any type 'G' that is a topological space, a group, a topological group, a measurable space and a Borel space, and is locally compact, if we have two left-invariant measures (μ' and μ), which are finite on compact sets and have inner regularity, then these two measures coincide up to a multiplicative constant. The multiplicative constant is given by the haar scalar factor of μ' with respect to μ. This theorem asserts the uniqueness of such measures up to scaling, which is a key property in the theory of Haar measures in locally compact groups.
More concisely: In a locally compact topological group endowed with the Borel sigma-algebra and having finite, inner regular left-invariant measures, any two such measures are equal up to a multiplicative constant, determined by their Haar scalar factors.
|
MeasureTheory.continuous_integral_apply_inv_mul
theorem MeasureTheory.continuous_integral_apply_inv_mul :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : LocallyCompactSpace G] [inst_2 : Group G]
[inst_3 : TopologicalGroup G] [inst_4 : MeasurableSpace G] [inst_5 : BorelSpace G] {μ : MeasureTheory.Measure G}
[inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ] {E : Type u_2} [inst_7 : NormedAddCommGroup E]
[inst_8 : NormedSpace ℝ E] {g : G → E},
Continuous g → HasCompactSupport g → Continuous fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ
This theorem states that for a topological group `G` that is locally compact, and a measurable space `G` that has the Borel sigma-algebra and a measure `μ` which is finite on compact sets, the parameterized integral function `x ↦ ∫ y, g (y⁻¹ * x) ∂μ` is continuous when `g` is a continuous function with compact support. Here, `E` is a normed addition commutative group and a normed space over the real numbers. The continuity of the integral function is achieved under the conditions that the function `g` is continuous and has compact support.
More concisely: For a locally compact, topological group `G` with a finite Borel measure `μ` on its Borel sigma-algebra, the parameterized integral `x ↦ ∫ y, g (y⁻¹ * x) ∂μ` is a continuous function on `G` when `g` is a continuous function with compact support.
|
MeasureTheory.Measure.haarScalarFactor_pos_of_isOpenPosMeasure
theorem MeasureTheory.Measure.haarScalarFactor_pos_of_isOpenPosMeasure :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
[inst_6 : μ'.IsHaarMeasure], 0 < μ'.haarScalarFactor μ
This theorem states that for any type `G` that has properties of a topological space, a group, a topological group, a measurable space, and a Borel space, if we have two measures `μ'` and `μ` that are both Haar measures (a type of measure invariant under shifts in the group), then the Haar scalar factor between these two measures is strictly greater than zero. This scalar factor represents a consistent scaling factor between the two measures. The theorem asserts that in the given conditions, this factor is always positive.
More concisely: For any type `G` endowed with the structures of a topological space, a group, a topological group, a measurable space, and a Borel space, if `μ'` and `μ` are both Haar measures on `G`, then their Haar scalar factors are positively comparable.
|
MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top
theorem MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G]
(μ' μ : MeasureTheory.Measure G) [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ']
[inst_8 : μ'.IsMulLeftInvariant] [inst_9 : μ.InnerRegularCompactLTTop] [inst_10 : μ'.InnerRegularCompactLTTop]
{s : Set G}, ↑↑μ s ≠ ⊤ → ↑↑μ' s ≠ ⊤ → ↑↑μ' s = μ'.haarScalarFactor μ • ↑↑μ s
This theorem, titled "Uniqueness of left-invariant measures", states that for any type `G` which is a topological space, a group, a topological group, a measurable space, a Borel space, and a locally compact space, given two left-invariant measures `μ'` and `μ` where `μ` is a Haar measure and both measures are finite on compact sets and inner regular for finite measure sets with respect to compact sets, for any set `s` of `G`, if `μ` or `μ'` of `s` is not infinite, then `μ'` of `s` is equal to the product of `μ'`'s Haar scalar factor with respect to `μ` and `μ` of `s`. This implies that these two measures coincide in the sense that they give the same value to finite measure sets, up to a multiplicative constant.
More concisely: Given two finite, inner regular, left-invariant measures `μ'` and `μ` on a locally compact topological group `G`, if `μ` is a Haar measure, then `μ'` and `μ` agree on finite measure sets up to a multiplicative constant.
|