QuotientAddGroup.integral_eq_integral_automorphize
theorem QuotientAddGroup.integral_eq_integral_automorphize :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalAddGroup G] [inst_4 : BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G}
{𝓕 : Set G},
MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ →
∀ [inst_5 : Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [inst_7 : BorelSpace (G ⧸ Γ)] {E : Type u_2}
[inst_8 : NormedAddCommGroup E] [inst_9 : NormedSpace ℝ E] [inst_10 : μ.IsAddRightInvariant] {f : G → E},
MeasureTheory.Integrable f μ →
MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f)
(MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) →
∫ (x : G), f x ∂μ =
∫ (x : G ⧸ Γ),
QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)
This theorem, often referred to as a simple version of the "Unfolding Trick", states the following: Given a subgroup Γ of an additive group G and a function f defined on G, if the measure μ is right-invariant and integrable over f with respect to G, and the function f automorphized over the quotient group G/Γ is almost everywhere strongly measurable, then the integral of f over G with respect to μ is equal to the integral of the automorphized function over the quotient group G/Γ. This condition holds true when the set 𝓕 is a fundamental domain for the action of Γ on G under the right-invariant measure μ.
More concisely: Given a right-invariant measure μ on an additive group G, a subgroup Γ, and a function f integrable over G with respect to μ, if f automorphized over G/Γ is almost everywhere strongly measurable, then the integral of f over G equals the integral of its automorphized version over G/Γ, provided that Γ acts on G through a fundamental domain under μ.
|
MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map
theorem MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map :
∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalGroup G] [inst_4 : BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
∀ [inst_5 : Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [inst_7 : BorelSpace (G ⧸ Γ)]
[inst_8 : μ.IsMulRightInvariant],
(MeasureTheory.Measure.map QuotientGroup.mk μ).AbsolutelyContinuous
(MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕))
This theorem, `MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map`, states that given a quotient space `G ⧸ Γ` where `Γ` is a countable subgroup of a group `G`, and a right-invariant measure `μ` on `G` which is restricted to a fundamental domain `𝓕` (denoted as `μ_𝓕`), any set in the quotient space which has zero `μ_𝓕`-measure also has zero measure under the pushforward of `μ` by the quotient map. This holds true even if `Γ` is infinite, in which case the pushforward of `μ` by the quotient map can take the value `∞` on any open set in the quotient space. The conditions of the theorem also require that `G` is a topological group with a Borel sigma algebra, and the measure `μ` is right-invariant.
More concisely: Given a topological group `G` with a countable subgroup `Γ`, a right-invariant Borel measure `μ` on `G`, and a fundamental domain `𝓕`, any set in the quotient space `G ⧸ Γ` with zero `μ_𝓕`-measure has zero pushforward measure under the quotient map from `G` to `G ⧸ Γ`, even if `Γ` is infinite and the pushforward measure can take the value `∞` on open sets.
|
QuotientGroup.integral_mul_eq_integral_automorphize_mul
theorem QuotientGroup.integral_mul_eq_integral_automorphize_mul :
∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalGroup G] [inst_4 : BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
∀ [inst_5 : Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [inst_7 : BorelSpace (G ⧸ Γ)] {K : Type u_2}
[inst_8 : NormedField K] [inst_9 : NormedSpace ℝ K] [inst_10 : μ.IsMulRightInvariant] {f : G → K},
MeasureTheory.Integrable f μ →
∀ {g : G ⧸ Γ → K},
MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
essSup (fun x => ↑‖g x‖₊) (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) ≠ ⊤ →
MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f)
(MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
∫ (x : G), g ↑x * f x ∂μ =
∫ (x : G ⧸ Γ),
g x *
QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)
This theorem, known as the "Unfolding Trick", states that given a subgroup `Γ` of a group `G`, the integral of a function `f` on `G` multiplied by the lift to `G` of a function `g` on the quotient `G ⧸ Γ` with respect to a right-invariant measure `μ` on `G`, is equal to the integral over the quotient of the automorphization of `f` times `g`. Essentially, this theorem allows for movement between the whole group `G` and the quotient `G ⧸ Γ` by describing the interaction between functions and measures on these spaces. Pre-conditions include the fact that `f` is integrable with respect to `μ`, and `g` is almost everywhere strongly measurable with respect to the pushforward measure of `μ` under the quotient map. Furthermore, the essential supremum of the norm of `g` must not be infinite and the automorphization of `f` must be almost everywhere strongly measurable with respect the previously mentioned pushforward measure. The theorem is a powerful tool in measure theory and group theory, allowing for integration over the quotient group by summing over orbits.
More concisely: Given a right-invariant measure `μ` on a group `G`, a subgroup `Γ`, a function `f` integrable with respect to `μ` on `G`, a function `g` almost everywhere strongly measurable with respect to the pushforward measure of `μ` on `G ⧸ Γ`, and with essential supremum of the norm of `g` finite, the integral of `f ∘ Aut(×) (p) (g)` over `G ⧸ Γ` is equal to the integral of `f` on `G` multiplied by the integral of `g` on `G ⧸ Γ` with respect to `μ` on `G` and the quotient measure on `G ⧸ Γ`.
|
essSup_comp_quotientGroup_mk
theorem essSup_comp_quotientGroup_mk :
∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalGroup G] [inst_4 : BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
∀ [inst_5 : Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [inst_7 : BorelSpace (G ⧸ Γ)]
[inst_8 : μ.IsMulRightInvariant] {g : G ⧸ Γ → ENNReal},
AEMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
essSup g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
The theorem `essSup_comp_quotientGroup_mk` states that for any group `G` equipped with a measure `μ`, a topological space structure, a group topology, and a Borel σ-algebra, given a subgroup `Γ` of `G` and a set `𝓕` that is a fundamental domain for the action of `Γ` on `G` (with respect to `μ`), if the measure `μ` is right-invariant and `g` is a function from the quotient group `G ⧸ Γ` to the extended nonnegative real numbers that is almost everywhere measurable with respect to the pushforward of the restriction of `μ` to `𝓕`, then the essential supremum of `g` with respect to this pushforward measure is equal to the essential supremum of the lift of `g` to `G` with respect to the measure `μ`. This relates the notion of essential supremum in the quotient space to the essential supremum on the universal cover, and is a useful fact in the theory of measurable dynamics.
More concisely: Given a group `G` with measure `μ`, topology, and Borel σ-algebra, a subgroup `Γ`, a fundamental domain `𝓕`, a right-invariant `μ`, and an almost everywhere measurable function `g` on the quotient group `G ⧸ Γ` with respect to `μ`, the essential supremum of `g` with respect to the pushforward measure equals the essential supremum of the lift of `g` to `G` with respect to `μ`.
|
MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map
theorem MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalAddGroup G] [inst_4 : BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G}
{𝓕 : Set G},
MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ →
∀ [inst_5 : Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [inst_7 : BorelSpace (G ⧸ Γ)]
[inst_8 : μ.IsAddRightInvariant],
(MeasureTheory.Measure.map QuotientAddGroup.mk μ).AbsolutelyContinuous
(MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕))
This theorem states that, given an additive quotient space `G/Γ` where `Γ` is countable, and the restriction of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`. If a set in the quotient has measure zero under `μ` restricted to `𝓕`, then it also has measure zero under the measure `μ` folded under the quotient by the canonical map from `G` to `G/Γ`. This theorem highlights that if `Γ` is infinite, then the folded map will map any open set in the quotient to infinity. This theorem is relevant to the study of measure theory in additive groups and quotient spaces.
More concisely: Given an additive quotient space `G/Γ` with a countable index `Γ`, and a right-invariant measure `μ` on `G`, if a set has measure zero in `μ` restricted to a fundamental domain `𝓕`, then it also has measure zero under `μ` when folded under the quotient map from `G` to `G/Γ`.
|
QuotientAddGroup.integral_mul_eq_integral_automorphize_mul
theorem QuotientAddGroup.integral_mul_eq_integral_automorphize_mul :
∀ {G' : Type u_1} [inst : AddGroup G'] [inst_1 : MeasurableSpace G'] [inst_2 : TopologicalSpace G']
[inst_3 : TopologicalAddGroup G'] [inst_4 : BorelSpace G'] {μ' : MeasureTheory.Measure G'} {Γ' : AddSubgroup G'}
[inst_5 : Countable ↥Γ'] [inst_6 : MeasurableSpace (G' ⧸ Γ')] [inst_7 : BorelSpace (G' ⧸ Γ')] {𝓕' : Set G'}
{K : Type u_2} [inst_8 : NormedField K] [inst_9 : NormedSpace ℝ K] [inst_10 : μ'.IsAddRightInvariant]
{f : G' → K},
MeasureTheory.Integrable f μ' →
∀ {g : G' ⧸ Γ' → K},
MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) →
essSup (fun x => ↑‖g x‖₊) (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) ≠ ⊤ →
MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f)
(MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) →
MeasureTheory.IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ' →
∫ (x : G'), g ↑x * f x ∂μ' =
∫ (x : G' ⧸ Γ'),
g x *
QuotientAddGroup.automorphize f
x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')
This theorem, often referred to as the "Unfolding Trick", states the following: Given an additive subgroup `Γ'` of an additive group `G'`, the integral of a function `f` on `G'` multiplied by the lift to `G'` of a function `g` on the quotient space `G' ⧸ Γ'` with respect to a right-invariant measure `μ'` on `G'`, is equal to the integral over the quotient space of the automorphization of `f` times `g`.
In more detail, if `f` is a measurable and integrable function on `G'` and `g` is a function on `G' ⧸ Γ'` that is almost everywhere strongly measurable, and the essential supremum of `g` is finite, the theorem states that the integral over `G'` of `g` times `f` with respect to `μ'` is equal to the integral over `G' ⧸ Γ'` of `g` times the automorphization of `f`. This holds under the precondition that `Γ'` is a fundamental domain of `μ'`.
More concisely: Given a measurable and integrable function `f` on an additive group `G` and a strongly measurable function `g` on the quotient space `G / Γ` with finite essential supreme, where `Γ` is a fundamental domain of a right-invariant measure `μ` on `G`, the integral of `g * (automorphism of f)` over `G / Γ` equals the integral of `g * f` over `G` with respect to `μ`.
|
essSup_comp_quotientAddGroup_mk
theorem essSup_comp_quotientAddGroup_mk :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalAddGroup G] [inst_4 : BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G}
{𝓕 : Set G},
MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ →
∀ [inst_5 : Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [inst_7 : BorelSpace (G ⧸ Γ)]
[inst_8 : μ.IsAddRightInvariant] {g : G ⧸ Γ → ENNReal},
AEMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) →
essSup g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
This theorem states that for an additive group `G` with topology `inst_2`, topological group structure `inst_3`, Borel space structure `inst_4`, and an additively right-invariant measure `μ`, given any additive subgroup `Γ` and a set `𝓕` that forms a fundamental domain for `Γ` in `G`, if `g` is a function from the quotient group `G ⧸ Γ` to the extended nonnegative reals that is almost everywhere measurable with respect to the measure `μ` restricted to `𝓕` and pushed forward by the canonical quotient map, then the essential supremum (essSup) of `g` with respect to this pushforward measure is the same as the essential supremum of the lift of `g` to `G` with respect to the original measure `μ`.
In simpler terms, this theorem provides a way to calculate the essential supremum of a function defined on a quotient of a group by comparing it to the essential supremum of its lift on the original group, under specific conditions involving measures and almost everywhere measurability.
More concisely: Given an additive group `G` with topology, topological group structure, Borel space structure, an additively right-invariant measure `μ`, an additive subgroup `Γ` with fundamental domain `𝓕`, and a function `g` on the quotient `G ⧸ Γ` that is almost everywhere measurable with respect to `μ` restricted to `𝓕` and pushed forward by the canonical quotient map, the essential supremum of `g` is equal to the essential supremum of `g`'s lift to `G`.
|
QuotientGroup.integral_eq_integral_automorphize
theorem QuotientGroup.integral_eq_integral_automorphize :
∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalGroup G] [inst_4 : BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
∀ [inst_5 : Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [inst_7 : BorelSpace (G ⧸ Γ)] {E : Type u_2}
[inst_8 : NormedAddCommGroup E] [inst_9 : NormedSpace ℝ E] [inst_10 : μ.IsMulRightInvariant] {f : G → E},
MeasureTheory.Integrable f μ →
MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f)
(MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
∫ (x : G), f x ∂μ =
∫ (x : G ⧸ Γ),
QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)
The theorem `QuotientGroup.integral_eq_integral_automorphize` states the *Unfolding Trick* in the context of group theory and measure theory. Given a subgroup `Γ` of a group `G`, and a function `f` from `G` to a normed additive commutative group `E`, if `f` is integrable with respect to a right-invariant measure `μ` on `G`, and the automorphization of `f` is almost everywhere strongly measurable with respect to the pushforward of the restriction of `μ` to a fundamental domain `𝓕` of `Γ`, then the integral of `f` over `G` with respect to `μ` is equal to the integral over the quotient group `G ⧸ Γ` of the automorphization of `f` with respect to the pushforward of the restriction of `μ` to `𝓕`. In other words, the integral over the whole group `G` is the same as summing over the `Γ` orbits in the quotient group `G ⧸ Γ`.
More concisely: Given a subgroup `Γ` of a group `G`, a right-invariant measure `μ` on `G`, a normed additive commutative group `E`, an integrable function `f : G -> E`, and the automorphization `f ∘ γ` strongly measurable with respect to `μ` on a fundamental domain `𝓕` of `Γ`, the integral of `f` over `G` equals the integral of `f ∘ γ` over `G ⧸ Γ` with respect to the pushforward of `μ` to `G ⧸ Γ` through the quotient map.
|