mathlib documentation

measure_theory.group.fundamental_domain

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

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

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_smul G α] [measurable_space α] (s : set α) (μ : measure_theory.measure α . "volume_tac") :
Prop

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 : measure_theory.null_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 : measure_theory.null_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 μ) :
(⋃ (g : G), g +ᵥ s) =ᵐ[μ] set.univ
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 μ) :
(⋃ (g : G), g s) =ᵐ[μ] set.univ
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 α μ] [countable G] {ν : measure_theory.measure α} (h : measure_theory.is_add_fundamental_domain G s μ) (hν : ν.absolutely_continuous μ) (f : α → ennreal) :
∫⁻ (x : α), f x ν = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ν
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 α μ] [countable G] {ν : measure_theory.measure α} (h : measure_theory.is_fundamental_domain G s μ) (hν : ν.absolutely_continuous μ) (f : α → ennreal) :
∫⁻ (x : α), f x ν = ∑' (g : G), ∫⁻ (x : α) in g s, f x ν
theorem measure_theory.is_fundamental_domain.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 α μ] [countable G] (h : measure_theory.is_fundamental_domain G s μ) (f : α → ennreal) :
∫⁻ (x : α), f x μ = ∑' (g : G), ∫⁻ (x : α) in g s, f x μ
theorem measure_theory.is_add_fundamental_domain.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 α μ] [countable G] (h : measure_theory.is_add_fundamental_domain G s μ) (f : α → ennreal) :
∫⁻ (x : α), f x μ = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x μ
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 α μ] [countable G] (h : measure_theory.is_fundamental_domain G s μ) (f : α → ennreal) (t : set α) :
∫⁻ (x : α) in t, f x μ = ∑' (g : G), ∫⁻ (x : α) in t g s, f x μ
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 α μ] [countable G] (h : measure_theory.is_add_fundamental_domain G s μ) (f : α → ennreal) (t : set α) :
∫⁻ (x : α) in t, f x μ = ∑' (g : G), ∫⁻ (x : α) in t (g +ᵥ s), f x μ
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 α μ] [countable G] (h : measure_theory.is_add_fundamental_domain G s μ) (f : α → ennreal) (t : set α) :
∫⁻ (x : α) in t, f x μ = ∑' (g : G), ∫⁻ (x : α) in (g +ᵥ t) s, f (-g +ᵥ x) μ
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 α μ] [countable G] (h : measure_theory.is_fundamental_domain G s μ) (f : α → ennreal) (t : set α) :
∫⁻ (x : α) in t, f x μ = ∑' (g : G), ∫⁻ (x : α) in g t s, f (g⁻¹ x) μ
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 α μ] [countable G] (h : measure_theory.is_fundamental_domain G s μ) (t : set α) :
μ t = ∑' (g : G), μ (t g s)
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 α μ] [countable G] (h : measure_theory.is_fundamental_domain G s μ) (t : set α) :
μ t = ∑' (g : G), μ (g t s)
theorem measure_theory.is_add_fundamental_domain.measure_zero_of_invariant {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 α μ] [countable G] (h : measure_theory.is_add_fundamental_domain G s μ) (t : set α) (ht : ∀ (g : G), g +ᵥ t = t) (hts : μ (t s) = 0) :
μ t = 0
theorem measure_theory.is_fundamental_domain.measure_zero_of_invariant {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 α μ] [countable G] (h : measure_theory.is_fundamental_domain G s μ) (t : set α) (ht : ∀ (g : G), g t = t) (hts : μ (t s) = 0) :
μ t = 0
@[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 α μ] [countable G] (hs : measure_theory.is_add_fundamental_domain G s μ) (ht : measure_theory.is_add_fundamental_domain G t μ) (f : α → ennreal) (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
∫⁻ (x : α) in s, f x μ = ∫⁻ (x : α) in t, 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 α μ] [countable G] (hs : measure_theory.is_fundamental_domain G s μ) (ht : measure_theory.is_fundamental_domain G t μ) (f : α → ennreal) (hf : ∀ (g : G) (x : α), f (g x) = f x) :
∫⁻ (x : α) in s, f x μ = ∫⁻ (x : α) in t, 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 α μ] [countable 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) :
μ (A s) = μ (A t)
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 α μ] [countable 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) :
μ (A s) = μ (A t)
@[protected]

If s and t are two fundamental domains of the same action, then their measures are equal.

@[protected]

If s and t are two fundamental domains of the same action, then their measures are equal.

@[protected]
@[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_add_comm_group E] {s t : set α} {μ : measure_theory.measure α} [measurable_space G] [has_measurable_smul G α] [measure_theory.smul_invariant_measure G α μ] [countable 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]
@[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_add_comm_group E] {s t : set α} {μ : measure_theory.measure α} [measurable_space G] [has_measurable_smul G α] [measure_theory.smul_invariant_measure G α μ] [countable G] [normed_space E] [complete_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) :
(x : α) in s, f x μ = (x : α) in t, 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_add_comm_group E] {s t : set α} {μ : measure_theory.measure α} [measurable_space G] [has_measurable_vadd G α] [measure_theory.vadd_invariant_measure G α μ] [countable G] [normed_space E] [complete_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) :
(x : α) in s, f x μ = (x : α) in t, f x μ
theorem measure_theory.is_fundamental_domain.ess_sup_measure_restrict {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 α μ] [countable G] (hs : measure_theory.is_fundamental_domain G s μ) {f : α → ennreal} (hf : ∀ (γ : G) (x : α), f x) = f x) :
ess_sup f (μ.restrict s) = ess_sup f μ

If f is invariant under the action of a countable group G, and μ is a G-invariant measure with a fundamental domain s, then the ess_sup of f restricted to s is the same as that of f on all of its domain.

theorem measure_theory.is_add_fundamental_domain.ess_sup_measure_restrict {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 α μ] [countable G] (hs : measure_theory.is_add_fundamental_domain G s μ) {f : α → ennreal} (hf : ∀ (γ : G) (x : α), f +ᵥ x) = f x) :
ess_sup f (μ.restrict s) = ess_sup f μ

If f is invariant under the action of a countable additive group G, and μ is a G-invariant measure with a fundamental domain s, then the ess_sup of f restricted to s is the same as that of f on all of its domain.