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_scalar 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 : 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 μ) :
(⋃ (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_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 μ) :
pairwise (λ (g₁ g₂ : G), μ (g₁ s g₂ s) = 0)
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 μ) :
pairwise (λ (g₁ g₂ : G), μ ((g₁ +ᵥ s) (g₂ +ᵥ s)) = 0)
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∞) :
∫⁻ (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 α μ] [encodable G] {ν : measure_theory.measure α} (h : measure_theory.is_fundamental_domain G s μ) (hν : ν μ) (f : α → ℝ≥0∞) :
∫⁻ (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 α μ] [encodable G] (h : measure_theory.is_fundamental_domain G s μ) (f : α → ℝ≥0∞) (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 α μ] [encodable G] (h : measure_theory.is_add_fundamental_domain G s μ) (f : α → ℝ≥0∞) (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 α μ] [encodable G] (h : measure_theory.is_add_fundamental_domain G s μ) (f : α → ℝ≥0∞) (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 α μ] [encodable G] (h : measure_theory.is_fundamental_domain G s μ) (f : α → ℝ≥0∞) (t : set α) :
∫⁻ (x : α) in t, f x μ = ∑' (g : G), ∫⁻ (x : α) in g t s, f (g⁻¹ x) μ
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 α) :
ν t = ∑' (g : G), ν (t (g +ᵥ s))
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 α) :
ν 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 α μ] [encodable 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 α μ] [encodable G] (h : measure_theory.is_fundamental_domain G s μ) (t : set α) :
μ t = ∑' (g : G), μ (g t s)
@[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) :
∫⁻ (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 α μ] [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) :
∫⁻ (x : α) in s, f x μ = ∫⁻ (x : α) in t, f x μ
@[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.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) :
@[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) :
@[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_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]
@[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) :
(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_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) :
(x : α) in s, f x μ = (x : α) in t, f x μ