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.

Main declarations #

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_3} [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_3} [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_fundamental_domain.mk'' {G : Type u_1} {α : Type u_3} [group G] [mul_action G α] [measurable_space α] {s : set α} {μ : measure_theory.measure α} (h_meas : measure_theory.null_measurable_set s μ) (h_ae_covers : ∀ᵐ (x : α) μ, (g : G), g x s) (h_ae_disjoint : (g : G), g 1 measure_theory.ae_disjoint μ (g s) s) (h_qmp : (g : G), measure_theory.measure.quasi_measure_preserving (has_smul.smul g) μ μ) :

For s to be a fundamental domain, it's enough to check ae_disjoint (g • s) s for g ≠ 1.

theorem measure_theory.is_add_fundamental_domain.mk'' {G : Type u_1} {α : Type u_3} [add_group G] [add_action G α] [measurable_space α] {s : set α} {μ : measure_theory.measure α} (h_meas : measure_theory.null_measurable_set s μ) (h_ae_covers : ∀ᵐ (x : α) μ, (g : G), g +ᵥ x s) (h_ae_disjoint : (g : G), g 0 measure_theory.ae_disjoint μ (g +ᵥ s) s) (h_qmp : (g : G), measure_theory.measure.quasi_measure_preserving (has_vadd.vadd g) μ μ) :

For s to be a fundamental domain, it's enough to check ae_disjoint (g +ᵥ s) s for g ≠ 0.

If a measurable space has a finite measure μ and a countable additive group G acts quasi-measure-preservingly, then to show that a set s is a fundamental domain, it is sufficient to check that its translates g +ᵥ s are (almost) disjoint and that the sum ∑' g, μ (g +ᵥ s) is sufficiently large.

If a measurable space has a finite measure μ and a countable group G acts quasi-measure-preservingly, then to show that a set s is a fundamental domain, it is sufficient to check that its translates g • s are (almost) disjoint and that the sum ∑' g, μ (g • s) is sufficiently large.

theorem measure_theory.is_fundamental_domain.pairwise_ae_disjoint_of_ac {G : Type u_1} {α : Type u_3} [group G] [mul_action G α] [measurable_space α] {s : set α} {μ ν : measure_theory.measure α} (h : measure_theory.is_fundamental_domain G s μ) (hν : ν.absolutely_continuous μ) :
pairwise (λ (g₁ g₂ : G), measure_theory.ae_disjoint ν (g₁ s) (g₂ s))
theorem measure_theory.is_fundamental_domain.set_lintegral_eq_tsum' {G : Type u_1} {α : Type u_3} [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_fundamental_domain.set_lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [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_zero_of_invariant {G : Type u_1} {α : Type u_3} [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

Given a measure space with an action of a finite group G, the measure of any G-invariant set is determined by the measure of its intersection with a fundamental domain for the action of G.

Given a measure space with an action of a finite additive group G, the measure of any G-invariant set is determined by the measure of its intersection with a fundamental domain for the action of G.

@[protected]
theorem measure_theory.is_add_fundamental_domain.set_lintegral_eq {G : Type u_1} {α : Type u_3} [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_3} [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_3} [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_3} [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]
theorem measure_theory.is_fundamental_domain.set_integral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [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_3} {E : Type u_5} [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 μ

If the additive action of a countable group G admits an invariant measure μ with a fundamental domain s, then every null-measurable set t such that the sets g +ᵥ t ∩ s are pairwise a.e.-disjoint has measure at most μ s.

If the action of a countable group G admits an invariant measure μ with a fundamental domain s, then every null-measurable set t such that the sets g • t ∩ s are pairwise a.e.-disjoint has measure at most μ s.

theorem measure_theory.is_fundamental_domain.exists_ne_one_smul_eq {G : Type u_1} {α : Type u_3} [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 μ) (htm : measure_theory.null_measurable_set t μ) (ht : μ s < μ t) :
(x : α) (H : x t) (y : α) (H : y t) (g : G) (H : g 1), g x = y

If the action of a countable group G admits an invariant measure μ with a fundamental domain s, then every null-measurable set t of measure strictly greater than μ s contains two points x y such that g • x = y for some g ≠ 1.

theorem measure_theory.is_add_fundamental_domain.exists_ne_zero_vadd_eq {G : Type u_1} {α : Type u_3} [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 μ) (htm : measure_theory.null_measurable_set t μ) (ht : μ s < μ t) :
(x : α) (H : x t) (y : α) (H : y t) (g : G) (H : g 0), g +ᵥ x = y

If the additive action of a countable group G admits an invariant measure μ with a fundamental domain s, then every null-measurable set t of measure strictly greater than μ s contains two points x y such that g +ᵥ x = y for some g ≠ 0.

theorem measure_theory.is_fundamental_domain.ess_sup_measure_restrict {G : Type u_1} {α : Type u_3} [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.

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.

Interior/frontier of a fundamental domain #

def measure_theory.add_fundamental_frontier (G : Type u_1) {α : Type u_3} [add_group G] [add_action G α] (s : set α) :
set α

The boundary of a fundamental domain, those points of the domain that also lie in a nontrivial translate.

Equations
def measure_theory.fundamental_frontier (G : Type u_1) {α : Type u_3} [group G] [mul_action G α] (s : set α) :
set α

The boundary of a fundamental domain, those points of the domain that also lie in a nontrivial translate.

Equations
def measure_theory.fundamental_interior (G : Type u_1) {α : Type u_3} [group G] [mul_action G α] (s : set α) :
set α

The interior of a fundamental domain, those points of the domain not lying in any translate.

Equations
def measure_theory.add_fundamental_interior (G : Type u_1) {α : Type u_3} [add_group G] [add_action G α] (s : set α) :
set α

The interior of a fundamental domain, those points of the domain not lying in any translate.

Equations
@[simp]
theorem measure_theory.mem_add_fundamental_frontier {G : Type u_1} {α : Type u_3} [add_group G] [add_action G α] {s : set α} {x : α} :
@[simp]
theorem measure_theory.mem_fundamental_frontier {G : Type u_1} {α : Type u_3} [group G] [mul_action G α] {s : set α} {x : α} :
x measure_theory.fundamental_frontier G s x s (g : G) (hg : g 1), x g s
@[simp]
theorem measure_theory.mem_fundamental_interior {G : Type u_1} {α : Type u_3} [group G] [mul_action G α] {s : set α} {x : α} :
@[simp]
theorem measure_theory.mem_add_fundamental_interior {G : Type u_1} {α : Type u_3} [add_group G] [add_action G α] {s : set α} {x : α} :
@[simp]
theorem measure_theory.fundamental_frontier_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [group G] [mul_action G α] (s : set α) [group H] [mul_action H α] [smul_comm_class H G α] (g : H) :
@[simp]
theorem measure_theory.fundamental_interior_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [group G] [mul_action G α] (s : set α) [group H] [mul_action H α] [smul_comm_class H G α] (g : H) :