mathlibdocumentation

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

• s is a measurable set;

• the sets g • s over all g : G cover almost all points of the whole space;

• the sets g • s, are pairwise a.e. disjoint, i.e., μ (g₁ • s ∩ g₂ • s) = 0 whenever g₁ ≠ g₂; we require this for g₂ = 1 in the definition, then deduce it for any two g₁ ≠ 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] [ α] (s : set α) (μ : . "volume_tac") :
Prop
• measurable_set :
• 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] [ α] (s : set α) (μ : . "volume_tac") :
Prop
• measurable_set :
• 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] [ α] {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] [ α] {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] [ α] {s : set α} {μ : measure_theory.measure α} (h : μ) :
(⋃ (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] [ α] {s : set α} {μ : measure_theory.measure α} (h : μ) :
(⋃ (g : G), g s) =ᵐ[μ] set.univ
theorem measure_theory.is_add_fundamental_domain.mono {G : Type u_1} {α : Type u_2} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} (h : μ) {ν : measure_theory.measure α} (hle : ν μ) :
theorem measure_theory.is_fundamental_domain.mono {G : Type u_1} {α : Type u_2} [group G] [ α] {s : set α} {μ : measure_theory.measure α} (h : μ) {ν : measure_theory.measure α} (hle : ν μ) :
theorem measure_theory.is_add_fundamental_domain.measurable_set_vadd {G : Type u_1} {α : Type u_2} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) (g : G) :
theorem measure_theory.is_fundamental_domain.measurable_set_smul {G : Type u_1} {α : Type u_2} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) (g : G) :
theorem measure_theory.is_fundamental_domain.pairwise_ae_disjoint {G : Type u_1} {α : Type u_2} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) :
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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) :
pairwise (λ (g₁ g₂ : G), μ ((g₁ +ᵥ s) (g₂ +ᵥ s)) = 0)
theorem measure_theory.is_fundamental_domain.sum_restrict_of_ac {G : Type u_1} {α : Type u_2} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] {ν : measure_theory.measure α} (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] {ν : measure_theory.measure α} (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] {ν : measure_theory.measure α} (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] {ν : measure_theory.measure α} (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] {ν : measure_theory.measure α} (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] {ν : measure_theory.measure α} (h : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] (h : μ) (t : set α) :
μ t = ∑' (g : G), μ (t g s)
theorem measure_theory.is_add_fundamental_domain.measure_eq_tsum' {G : Type u_1} {α : Type u_2} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] (h : μ) (t : set α) :
μ t = ∑' (g : G), μ (t (g +ᵥ s))
theorem measure_theory.is_add_fundamental_domain.measure_eq_tsum {G : Type u_1} {α : Type u_2} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] (h : μ) (t : set α) :
μ t = ∑' (g : G), μ ((g +ᵥ t) s)
theorem measure_theory.is_fundamental_domain.measure_eq_tsum {G : Type u_1} {α : Type u_2} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [encodable G] (h : μ) (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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] (hs : μ) (ht : μ) (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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] (hs : μ) (ht : μ) (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.measure_eq {G : Type u_1} {α : Type u_2} [group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] (hs : μ) (ht : μ) :
μ s = μ 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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] (hs : μ) (ht : μ) :
μ s = μ t
@[protected]
theorem measure_theory.is_fundamental_domain.ae_measurable_on_iff {G : Type u_1} {α : Type u_2} [group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] {β : Type u_3} (hs : μ) (ht : μ) {f : α → β} (hf : ∀ (g : G) (x : α), f (g x) = f x) :
(μ.restrict s) (μ.restrict t)
@[protected]
theorem measure_theory.is_add_fundamental_domain.ae_measurable_on_iff {G : Type u_1} {α : Type u_2} [add_group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] {β : Type u_3} (hs : μ) (ht : μ) {f : α → β} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
(μ.restrict s) (μ.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] [ α] [normed_group E] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] (hs : μ) (ht : μ) {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] [ α] [normed_group E] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] (hs : μ) (ht : μ) {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] [ α] [normed_group E] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] (hs : μ) (ht : μ) {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] [ α] [normed_group E] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] (hs : μ) (ht : μ) {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] [ α] [normed_group E] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] [ E] [borel_space E] (hs : μ) (ht : μ) {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] [ α] [normed_group E] {s t : set α} {μ : measure_theory.measure α} [ α] [encodable G] [ E] [borel_space E] (hs : μ) (ht : μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
(x : α) in s, f x μ = (x : α) in t, f x μ