Haar quotient measure #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we consider properties of fundamental domains and measures for the action of a
subgroup of a group G
on G
itself.
Main results #
-
measure_theory.is_fundamental_domain.smul_invariant_measure_map
: given a subgroupΓ
of a topological groupG
, the pushforward to the coset spaceG ⧸ Γ
of the restriction of a both left- and right-invariant measure onG
to a fundamental domain𝓕
is aG
-invariant measure onG ⧸ Γ
. -
measure_theory.is_fundamental_domain.is_mul_left_invariant_map
: given a normal subgroupΓ
of a topological groupG
, the pushforward to the quotient groupG ⧸ Γ
of the restriction of a both left- and right-invariant measure onG
to a fundamental domain𝓕
is a left-invariant measure onG ⧸ Γ
.
Note that a group G
with Haar measure that is both left and right invariant is called
unimodular.
Measurability of the action of the additive topological group G
on the left-coset
space G/Γ
.
Measurability of the action of the topological group G
on the left-coset space G/Γ
.
The pushforward to the coset space G ⧸ Γ
of the restriction of a both left- and
right-invariant measure on an additive topological group G
to a fundamental domain 𝓕
is a
G
-invariant measure on G ⧸ Γ
.
The pushforward to the coset space G ⧸ Γ
of the restriction of a both left- and right-
invariant measure on G
to a fundamental domain 𝓕
is a G
-invariant measure on G ⧸ Γ
.
Assuming Γ
is a normal subgroup of an additive topological group G
, the
pushforward to the quotient group G ⧸ Γ
of the restriction of a both left- and right-invariant
measure on G
to a fundamental domain 𝓕
is a left-invariant measure on G ⧸ Γ
.
Assuming Γ
is a normal subgroup of a topological group G
, the pushforward to the quotient
group G ⧸ Γ
of the restriction of a both left- and right-invariant measure on G
to a
fundamental domain 𝓕
is a left-invariant measure on G ⧸ Γ
.
Given a normal subgroup Γ
of an additive topological group G
with Haar measure
μ
, which is also right-invariant, and a finite volume fundamental domain 𝓕
, the pushforward
to the quotient group G ⧸ Γ
of the restriction of μ
to 𝓕
is a multiple of Haar measure on
G ⧸ Γ
.
Given a normal subgroup Γ
of a topological group G
with Haar measure μ
, which is also
right-invariant, and a finite volume fundamental domain 𝓕
, the pushforward to the quotient
group G ⧸ Γ
of the restriction of μ
to 𝓕
is a multiple of Haar measure on G ⧸ Γ
.
Given a normal subgroup Γ
of an additive
topological group G
with Haar measure μ
, which is also right-invariant, and a finite volume
fundamental domain 𝓕
, the quotient map to G ⧸ Γ
is measure-preserving between appropriate
multiples of Haar measure on G
and G ⧸ Γ
.
Given a normal subgroup Γ
of a topological group G
with Haar measure μ
, which is also
right-invariant, and a finite volume fundamental domain 𝓕
, the quotient map to G ⧸ Γ
is
measure-preserving between appropriate multiples of Haar measure on G
and G ⧸ Γ
.
The ess_sup
of a function g
on the additive quotient space G ⧸ Γ
with respect
to the pushforward of the restriction, μ_𝓕
, of a right-invariant measure μ
to a fundamental
domain 𝓕
, is the same as the ess_sup
of g
's lift to the universal cover G
with respect
to μ
.
The ess_sup
of a function g
on the quotient space G ⧸ Γ
with respect to the pushforward
of the restriction, μ_𝓕
, of a right-invariant measure μ
to a fundamental domain 𝓕
, is the
same as the ess_sup
of g
's lift to the universal cover G
with respect to μ
.
Given a quotient space G ⧸ Γ
where Γ
is countable
, and the restriction,
μ_𝓕
, of a right-invariant measure μ
on G
to a fundamental domain 𝓕
, a set
in the quotient which has μ_𝓕
-measure zero, also has measure zero under the
folding of μ
under the quotient. Note that, if Γ
is infinite, then the folded map
will take the value ∞
on any open set in the quotient!
Given an additive quotient space G ⧸ Γ
where Γ
is countable
, and the
restriction, μ_𝓕
, of a right-invariant measure μ
on G
to a fundamental domain 𝓕
, a set
in the quotient which has μ_𝓕
-measure zero, also has measure zero under the
folding of μ
under the quotient. Note that, if Γ
is infinite, then the folded map
will take the value ∞
on any open set in the quotient!
This is a simple version of the Unfolding Trick: Given a subgroup Γ
of an
additive group G
, the integral of a function f
on G
with respect to a right-invariant
measure μ
is equal to the integral over the quotient G ⧸ Γ
of the automorphization of f
.
This is a simple version of the Unfolding Trick: Given a subgroup Γ
of a group G
, the
integral of a function f
on G
with respect to a right-invariant measure μ
is equal to the
integral over the quotient G ⧸ Γ
of the automorphization of f
.
This is the Unfolding Trick: Given a subgroup Γ
of a group G
, the integral of a
function f
on G
times 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
.
This is the Unfolding Trick: Given an additive subgroup Γ'
of an additive group G'
, the
integral of a function f
on G'
times 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
.