Fundamental domain of a group action #
A set s is said to be a fundamental domain of an action of a group G on a measurable space α
with respect to a measure μ if
-
sis a measurable set; -
the sets
g • sover allg : Gcover almost all points of the whole space; -
the sets
g • s, are pairwise a.e. disjoint, i.e.,μ (g₁ • s ∩ g₂ • s) = 0wheneverg₁ ≠ g₂; we require this forg₂ = 1in the definition, then deduce it for any twog₁ ≠ g₂.
In this file we prove that in case of a countable group G and a measure preserving action, any two
fundamental domains have the same measure, and for a G-invariant function, its integrals over any
two fundamental domains are equal to each other.
We also generate additive versions of all theorems in this file using the to_additive attribute.
structure
measure_theory.is_add_fundamental_domain
(G : Type u_1)
{α : Type u_2}
[has_zero G]
[has_vadd G α]
[measurable_space α]
(s : set α)
(μ : measure_theory.measure α . "volume_tac") :
Prop
- measurable_set : measurable_set s
- ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x ∈ s
- ae_disjoint : ∀ (g : G), g ≠ 0 → ⇑μ ((g +ᵥ s) ∩ s) = 0
A measurable set s is a fundamental domain for an additive action of an additive group G
on a measurable space α with respect to a measure α if the sets g +ᵥ s, g : G, are pairwise
a.e. disjoint and cover the whole space.
structure
measure_theory.is_fundamental_domain
(G : Type u_1)
{α : Type u_2}
[has_one G]
[has_scalar G α]
[measurable_space α]
(s : set α)
(μ : measure_theory.measure α . "volume_tac") :
Prop
- measurable_set : measurable_set s
- ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s
- ae_disjoint : ∀ (g : G), g ≠ 1 → ⇑μ (g • s ∩ s) = 0
A measurable set s is a fundamental domain for an action of a group G on a measurable
space α with respect to a measure α if the sets g • s, g : G, are pairwise a.e. disjoint and
cover the whole space.
theorem
measure_theory.is_fundamental_domain.mk'
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
(h_meas : measurable_set s)
(h_exists : ∀ (x : α), ∃! (g : G), g • x ∈ s) :
If for each x : α, exactly one of g • x, g : G, belongs to a measurable set s, then s
is a fundamental domain for the action of G on α.
theorem
measure_theory.is_add_fundamental_domain.mk'
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
(h_meas : measurable_set s)
(h_exists : ∀ (x : α), ∃! (g : G), g +ᵥ x ∈ s) :
If for each x : α, exactly one of g +ᵥ x, g : G, belongs to a measurable set
s, then s is a fundamental domain for the additive action of G on α.
theorem
measure_theory.is_add_fundamental_domain.Union_vadd_ae_eq
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.is_add_fundamental_domain G s μ) :
theorem
measure_theory.is_fundamental_domain.Union_smul_ae_eq
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.is_fundamental_domain G s μ) :
theorem
measure_theory.is_add_fundamental_domain.mono
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.is_add_fundamental_domain G s μ)
{ν : measure_theory.measure α}
(hle : ν ≪ μ) :
theorem
measure_theory.is_fundamental_domain.mono
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.is_fundamental_domain G s μ)
{ν : measure_theory.measure α}
(hle : ν ≪ μ) :
theorem
measure_theory.is_add_fundamental_domain.measurable_set_vadd
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
(h : measure_theory.is_add_fundamental_domain G s μ)
(g : G) :
measurable_set (g +ᵥ s)
theorem
measure_theory.is_fundamental_domain.measurable_set_smul
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
(h : measure_theory.is_fundamental_domain G s μ)
(g : G) :
measurable_set (g • s)
theorem
measure_theory.is_fundamental_domain.pairwise_ae_disjoint
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
(h : measure_theory.is_fundamental_domain G s μ) :
theorem
measure_theory.is_add_fundamental_domain.pairwise_ae_disjoint
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
(h : measure_theory.is_add_fundamental_domain G s μ) :
theorem
measure_theory.is_fundamental_domain.sum_restrict_of_ac
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
{ν : measure_theory.measure α}
(h : measure_theory.is_fundamental_domain G s μ)
(hν : ν ≪ μ) :
measure_theory.measure.sum (λ (g : G), ν.restrict (g • s)) = ν
theorem
measure_theory.is_add_fundamental_domain.sum_restrict_of_ac
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
{ν : measure_theory.measure α}
(h : measure_theory.is_add_fundamental_domain G s μ)
(hν : ν ≪ μ) :
measure_theory.measure.sum (λ (g : G), ν.restrict (g +ᵥ s)) = ν
theorem
measure_theory.is_add_fundamental_domain.lintegral_eq_tsum_of_ac
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
{ν : measure_theory.measure α}
(h : measure_theory.is_add_fundamental_domain G s μ)
(hν : ν ≪ μ)
(f : α → ℝ≥0∞) :
theorem
measure_theory.is_fundamental_domain.lintegral_eq_tsum_of_ac
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
{ν : measure_theory.measure α}
(h : measure_theory.is_fundamental_domain G s μ)
(hν : ν ≪ μ)
(f : α → ℝ≥0∞) :
theorem
measure_theory.is_fundamental_domain.set_lintegral_eq_tsum'
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
(h : measure_theory.is_fundamental_domain G s μ)
(f : α → ℝ≥0∞)
(t : set α) :
theorem
measure_theory.is_add_fundamental_domain.set_lintegral_eq_tsum'
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
(h : measure_theory.is_add_fundamental_domain G s μ)
(f : α → ℝ≥0∞)
(t : set α) :
theorem
measure_theory.is_add_fundamental_domain.set_lintegral_eq_tsum
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
(h : measure_theory.is_add_fundamental_domain G s μ)
(f : α → ℝ≥0∞)
(t : set α) :
theorem
measure_theory.is_fundamental_domain.set_lintegral_eq_tsum
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
(h : measure_theory.is_fundamental_domain G s μ)
(f : α → ℝ≥0∞)
(t : set α) :
theorem
measure_theory.is_add_fundamental_domain.measure_eq_tsum_of_ac
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
{ν : measure_theory.measure α}
(h : measure_theory.is_add_fundamental_domain G s μ)
(hν : ν ≪ μ)
(t : set α) :
theorem
measure_theory.is_fundamental_domain.measure_eq_tsum_of_ac
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
{ν : measure_theory.measure α}
(h : measure_theory.is_fundamental_domain G s μ)
(hν : ν ≪ μ)
(t : set α) :
theorem
measure_theory.is_fundamental_domain.measure_eq_tsum'
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
(h : measure_theory.is_fundamental_domain G s μ)
(t : set α) :
theorem
measure_theory.is_add_fundamental_domain.measure_eq_tsum'
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
(h : measure_theory.is_add_fundamental_domain G s μ)
(t : set α) :
theorem
measure_theory.is_add_fundamental_domain.measure_eq_tsum
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
(h : measure_theory.is_add_fundamental_domain G s μ)
(t : set α) :
theorem
measure_theory.is_fundamental_domain.measure_eq_tsum
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
(h : measure_theory.is_fundamental_domain G s μ)
(t : set α) :
@[protected]
theorem
measure_theory.is_add_fundamental_domain.set_lintegral_eq
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
(hs : measure_theory.is_add_fundamental_domain G s μ)
(ht : measure_theory.is_add_fundamental_domain G t μ)
(f : α → ℝ≥0∞)
(hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
@[protected]
theorem
measure_theory.is_fundamental_domain.set_lintegral_eq
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
(hs : measure_theory.is_fundamental_domain G s μ)
(ht : measure_theory.is_fundamental_domain G t μ)
(f : α → ℝ≥0∞)
(hf : ∀ (g : G) (x : α), f (g • x) = f x) :
theorem
measure_theory.is_add_fundamental_domain.measure_set_eq
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
(hs : measure_theory.is_add_fundamental_domain G s μ)
(ht : measure_theory.is_add_fundamental_domain G t μ)
{A : set α}
(hA₀ : measurable_set A)
(hA : ∀ (g : G), (λ (x : α), g +ᵥ x) ⁻¹' A = A) :
theorem
measure_theory.is_fundamental_domain.measure_set_eq
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
(hs : measure_theory.is_fundamental_domain G s μ)
(ht : measure_theory.is_fundamental_domain G t μ)
{A : set α}
(hA₀ : measurable_set A)
(hA : ∀ (g : G), (λ (x : α), g • x) ⁻¹' A = A) :
@[protected]
theorem
measure_theory.is_fundamental_domain.measure_eq
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
(hs : measure_theory.is_fundamental_domain G s μ)
(ht : measure_theory.is_fundamental_domain G t μ) :
If s and t are two fundamental domains of the same action, then their measures are equal.
@[protected]
theorem
measure_theory.is_add_fundamental_domain.measure_eq
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
(hs : measure_theory.is_add_fundamental_domain G s μ)
(ht : measure_theory.is_add_fundamental_domain G t μ) :
@[protected]
theorem
measure_theory.is_fundamental_domain.ae_measurable_on_iff
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
{β : Type u_3}
[measurable_space β]
(hs : measure_theory.is_fundamental_domain G s μ)
(ht : measure_theory.is_fundamental_domain G t μ)
{f : α → β}
(hf : ∀ (g : G) (x : α), f (g • x) = f x) :
ae_measurable f (μ.restrict s) ↔ ae_measurable f (μ.restrict t)
@[protected]
theorem
measure_theory.is_add_fundamental_domain.ae_measurable_on_iff
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
{β : Type u_3}
[measurable_space β]
(hs : measure_theory.is_add_fundamental_domain G s μ)
(ht : measure_theory.is_add_fundamental_domain G t μ)
{f : α → β}
(hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
ae_measurable f (μ.restrict s) ↔ ae_measurable f (μ.restrict t)
@[protected]
theorem
measure_theory.is_add_fundamental_domain.has_finite_integral_on_iff
{G : Type u_1}
{α : Type u_2}
{E : Type u_3}
[add_group G]
[add_action G α]
[measurable_space α]
[normed_group E]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
(hs : measure_theory.is_add_fundamental_domain G s μ)
(ht : measure_theory.is_add_fundamental_domain G t μ)
{f : α → E}
(hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
@[protected]
theorem
measure_theory.is_fundamental_domain.has_finite_integral_on_iff
{G : Type u_1}
{α : Type u_2}
{E : Type u_3}
[group G]
[mul_action G α]
[measurable_space α]
[normed_group E]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
(hs : measure_theory.is_fundamental_domain G s μ)
(ht : measure_theory.is_fundamental_domain G t μ)
{f : α → E}
(hf : ∀ (g : G) (x : α), f (g • x) = f x) :
@[protected]
theorem
measure_theory.is_fundamental_domain.integrable_on_iff
{G : Type u_1}
{α : Type u_2}
{E : Type u_3}
[group G]
[mul_action G α]
[measurable_space α]
[normed_group E]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
[measurable_space E]
(hs : measure_theory.is_fundamental_domain G s μ)
(ht : measure_theory.is_fundamental_domain G t μ)
{f : α → E}
(hf : ∀ (g : G) (x : α), f (g • x) = f x) :
@[protected]
theorem
measure_theory.is_add_fundamental_domain.integrable_on_iff
{G : Type u_1}
{α : Type u_2}
{E : Type u_3}
[add_group G]
[add_action G α]
[measurable_space α]
[normed_group E]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
[measurable_space E]
(hs : measure_theory.is_add_fundamental_domain G s μ)
(ht : measure_theory.is_add_fundamental_domain G t μ)
{f : α → E}
(hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
@[protected]
theorem
measure_theory.is_fundamental_domain.set_integral_eq
{G : Type u_1}
{α : Type u_2}
{E : Type u_3}
[group G]
[mul_action G α]
[measurable_space α]
[normed_group E]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[encodable G]
[measurable_space E]
[normed_space ℝ E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
(hs : measure_theory.is_fundamental_domain G s μ)
(ht : measure_theory.is_fundamental_domain G t μ)
{f : α → E}
(hf : ∀ (g : G) (x : α), f (g • x) = f x) :
@[protected]
theorem
measure_theory.is_add_fundamental_domain.set_integral_eq
{G : Type u_1}
{α : Type u_2}
{E : Type u_3}
[add_group G]
[add_action G α]
[measurable_space α]
[normed_group E]
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[encodable G]
[measurable_space E]
[normed_space ℝ E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
(hs : measure_theory.is_add_fundamental_domain G s μ)
(ht : measure_theory.is_add_fundamental_domain G t μ)
{f : α → E}
(hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :