# 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.

## Main declarations #

• `measure_theory.is_fundamental_domain`: Predicate for a set to be a fundamental domain of the action of a group
• `measure_theory.fundamental_frontier`: Fundamental frontier of a set under the action of a group. Elements of `s` that belong to some other translate of `s`.
• `measure_theory.fundamental_interior`: Fundamental interior of a set under the action of a group. Elements of `s` that do not belong to any other translate of `s`.
structure measure_theory.is_add_fundamental_domain (G : Type u_1) {α : Type u_2} [has_zero G] [ α] (s : set α) (μ : . "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] [ α] (s : set α) (μ : . "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] [ α] {s : set α} {μ : measure_theory.measure α} (h_meas : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} (h_meas : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} (h_meas : μ) (h_ae_covers : ∀ᵐ (x : α) μ, (g : G), g x s) (h_ae_disjoint : (g : G), g 1 (g s) s) (h_qmp : (g : 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] [ α] {s : set α} {μ : measure_theory.measure α} (h_meas : μ) (h_ae_covers : ∀ᵐ (x : α) μ, (g : G), g +ᵥ x s) (h_ae_disjoint : (g : G), g 0 (g +ᵥ s) s) (h_qmp : (g : G), ) :

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

theorem measure_theory.is_add_fundamental_domain.mk_of_measure_univ_le {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [countable G] (h_meas : μ) (h_ae_disjoint : (g : G), g 0 (g +ᵥ s) s) (h_qmp : (g : G), ) (h_measure_univ_le : ∑' (g : G), μ (g +ᵥ s)) :

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.

theorem measure_theory.is_fundamental_domain.mk_of_measure_univ_le {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [countable G] (h_meas : μ) (h_ae_disjoint : (g : G), g 1 (g s) s) (h_qmp : (g : G), ) (h_measure_univ_le : ∑' (g : G), μ (g s)) :

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_add_fundamental_domain.Union_vadd_ae_eq {G : Type u_1} {α : Type u_3} [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_3} [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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} (h : μ) {ν : measure_theory.measure α} (hle : ν.absolutely_continuous μ) :
theorem measure_theory.is_fundamental_domain.mono {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} (h : μ) {ν : measure_theory.measure α} (hle : ν.absolutely_continuous μ) :
theorem measure_theory.is_fundamental_domain.preimage_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [group G] [group H] [ α] [ β] {s : set α} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (h : μ) {f : β α} {e : G H} (he : function.bijective e) (hef : (g : G), (has_smul.smul (e g)) ) :
ν
theorem measure_theory.is_add_fundamental_domain.preimage_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [add_group G] [add_group H] [ α] [ β] {s : set α} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (h : μ) {f : β α} {e : G H} (he : function.bijective e) (hef : (g : G), (has_vadd.vadd (e g)) ) :
theorem measure_theory.is_fundamental_domain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [group G] [group H] [ α] [ β] {s : set α} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (h : μ) (f : α β) (hf : μ) (e : H G) (hef : (g : H), (has_smul.smul (e g)) ) :
ν
theorem measure_theory.is_add_fundamental_domain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [add_group G] [add_group H] [ α] [ β] {s : set α} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (h : μ) (f : α β) (hf : μ) (e : H G) (hef : (g : H), (has_vadd.vadd (e g)) ) :
theorem measure_theory.is_fundamental_domain.pairwise_ae_disjoint_of_ac {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ ν : measure_theory.measure α} (h : μ) (hν : ν.absolutely_continuous μ) :
pairwise (λ (g₁ g₂ : G), (g₁ s) (g₂ s))
theorem measure_theory.is_add_fundamental_domain.pairwise_ae_disjoint_of_ac {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {μ ν : measure_theory.measure α} (h : μ) (hν : ν.absolutely_continuous μ) :
pairwise (λ (g₁ g₂ : G), (g₁ +ᵥ s) (g₂ +ᵥ s))
theorem measure_theory.is_fundamental_domain.smul_of_comm {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} {G' : Type u_2} [group G'] [ α] [measurable_space G'] [ α] [ G α] (h : μ) (g : G') :
μ
theorem measure_theory.is_add_fundamental_domain.vadd_of_comm {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} {G' : Type u_2} [add_group G'] [ α] [measurable_space G'] [ α] [ G α] (h : μ) (g : G') :
theorem measure_theory.is_fundamental_domain.null_measurable_set_smul {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) (g : G) :
theorem measure_theory.is_add_fundamental_domain.null_measurable_set_vadd {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) (g : G) :
theorem measure_theory.is_add_fundamental_domain.restrict_restrict {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) (g : G) (t : set α) :
(μ.restrict t).restrict (g +ᵥ s) = μ.restrict ((g +ᵥ s) t)
theorem measure_theory.is_fundamental_domain.restrict_restrict {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) (g : G) (t : set α) :
(μ.restrict t).restrict (g s) = μ.restrict (g s t)
theorem measure_theory.is_fundamental_domain.smul {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) (g : G) :
μ
theorem measure_theory.is_add_fundamental_domain.vadd {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] (h : μ) (g : G) :
theorem measure_theory.is_fundamental_domain.sum_restrict_of_ac {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] {ν : measure_theory.measure α} (h : μ) (hν : ν.absolutely_continuous μ) :
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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] {ν : measure_theory.measure α} (h : μ) (hν : ν.absolutely_continuous μ) :
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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] {ν : measure_theory.measure α} (h : μ) (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_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] {ν : measure_theory.measure α} (h : μ) (hν : ν.absolutely_continuous μ) (f : α ennreal) :
∫⁻ (x : α), f x ν = ∑' (g : G), ∫⁻ (x : α) in g s, f x ν
theorem measure_theory.is_fundamental_domain.sum_restrict {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) :
measure_theory.measure.sum (λ (g : G), μ.restrict (g s)) = μ
theorem measure_theory.is_add_fundamental_domain.sum_restrict {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) :
measure_theory.measure.sum (λ (g : G), μ.restrict (g +ᵥ s)) = μ
theorem measure_theory.is_fundamental_domain.lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (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_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (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_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (f : α ennreal) (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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] {ν : measure_theory.measure α} (h : μ) (hν : ν.absolutely_continuous μ) (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_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] {ν : measure_theory.measure α} (h : μ) (hν : ν.absolutely_continuous μ) (t : set α) :
ν t = ∑' (g : G), ν (t g s)
theorem measure_theory.is_fundamental_domain.measure_eq_tsum' {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable 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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable 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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable 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_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (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_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (h : μ) (t : set α) (ht : (g : G), g t = t) (hts : μ (t s) = 0) :
μ t = 0
theorem measure_theory.is_fundamental_domain.measure_eq_card_smul_of_smul_ae_eq_self {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] [finite G] (h : μ) (t : set α) (ht : (g : G), g t =ᵐ[μ] t) :
μ t = μ (t s)

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`.

theorem measure_theory.is_add_fundamental_domain.measure_eq_card_smul_of_vadd_ae_eq_self {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] [finite G] (h : μ) (t : set α) (ht : (g : G), g +ᵥ t =ᵐ[μ] t) :
μ t = μ (t s)

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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) (ht : μ) (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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) (ht : μ) (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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) (ht : μ) {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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) (ht : μ) {A : set α} (hA₀ : measurable_set A) (hA : (g : G), (λ (x : α), g x) ⁻¹' A = A) :
μ (A s) = μ (A t)
@[protected]
theorem measure_theory.is_fundamental_domain.measure_eq {G : Type u_1} {α : Type u_3} [group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable 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_3} [add_group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable 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_fundamental_domain.ae_strongly_measurable_on_iff {G : Type u_1} {α : Type u_3} [group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] {β : Type u_2} (hs : μ) (ht : μ) {f : α β} (hf : (g : G) (x : α), f (g x) = f x) :
@[protected]
theorem measure_theory.is_add_fundamental_domain.ae_strongly_measurable_on_iff {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] {β : Type u_2} (hs : μ) (ht : μ) {f : α β} (hf : (g : G) (x : α), f (g +ᵥ x) = f x) :
@[protected]
theorem measure_theory.is_add_fundamental_domain.has_finite_integral_on_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [add_group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable 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_3} {E : Type u_5} [group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable 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_3} {E : Type u_5} [group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable 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_3} {E : Type u_5} [add_group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable 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_3} {E : Type u_5} [group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] [ 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_3} {E : Type u_5} [add_group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] [ E] (hs : μ) (ht : μ) {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_add_fundamental_domain.measure_le_of_pairwise_disjoint {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) (ht : μ) (hd : pairwise on λ (g : G), (g +ᵥ t) s)) :
μ t μ s

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`.

theorem measure_theory.is_fundamental_domain.measure_le_of_pairwise_disjoint {G : Type u_1} {α : Type u_3} [group G] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) (ht : μ) (hd : pairwise on λ (g : G), g t s)) :
μ t μ 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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) (htm : μ) (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] [ α] {s t : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) (htm : μ) (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] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) {f : α ennreal} (hf : (γ : G) (x : α), f x) = f x) :
(μ.restrict s) = μ

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_3} [add_group G] [ α] {s : set α} {μ : measure_theory.measure α} [ α] [countable G] (hs : μ) {f : α ennreal} (hf : (γ : G) (x : α), f +ᵥ x) = f x) :
(μ.restrict s) = μ

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] [ α] (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] [ α] (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] [ α] (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] [ α] (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] [ α] {s : set α} {x : α} :
x s (g : G) (hg : g 0), x g +ᵥ s
@[simp]
theorem measure_theory.mem_fundamental_frontier {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} {x : α} :
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] [ α] {s : set α} {x : α} :
x s (g : G), g 1 x g s
@[simp]
theorem measure_theory.mem_add_fundamental_interior {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} {x : α} :
x s (g : G), g 0 x g +ᵥ s
theorem measure_theory.fundamental_frontier_subset {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} :
theorem measure_theory.add_fundamental_frontier_subset {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} :
theorem measure_theory.add_fundamental_interior_subset {G : Type u_1} {α : Type u_3} [add_group G] [ α] {s : set α} :
theorem measure_theory.fundamental_interior_subset {G : Type u_1} {α : Type u_3} [group G] [ α] {s : set α} :
theorem measure_theory.disjoint_fundamental_interior_fundamental_frontier (G : Type u_1) {α : Type u_3} [group G] [ α] (s : set α) :
@[simp]
@[simp]
theorem measure_theory.fundamental_interior_union_fundamental_frontier (G : Type u_1) {α : Type u_3} [group G] [ α] (s : set α) :
@[simp]
theorem measure_theory.fundamental_frontier_union_fundamental_interior (G : Type u_1) {α : Type u_3} [group G] [ α] (s : set α) :
@[simp]
theorem measure_theory.sdiff_fundamental_interior (G : Type u_1) {α : Type u_3} [group G] [ α] (s : set α) :
@[simp]
theorem measure_theory.sdiff_add_fundamental_interior (G : Type u_1) {α : Type u_3} [add_group G] [ α] (s : set α) :
@[simp]
theorem measure_theory.sdiff_fundamental_frontier (G : Type u_1) {α : Type u_3} [group G] [ α] (s : set α) :
@[simp]
theorem measure_theory.sdiff_add_fundamental_frontier (G : Type u_1) {α : Type u_3} [add_group G] [ α] (s : set α) :
@[simp]
theorem measure_theory.fundamental_frontier_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [group G] [ α] (s : set α) [group H] [ α] [ α] (g : H) :
@[simp]
theorem measure_theory.add_fundamental_frontier_vadd (G : Type u_1) {H : Type u_2} {α : Type u_3} [add_group G] [ α] (s : set α) [add_group H] [ α] [ α] (g : H) :
@[simp]
theorem measure_theory.fundamental_interior_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [group G] [ α] (s : set α) [group H] [ α] [ α] (g : H) :
@[simp]
theorem measure_theory.add_fundamental_interior_vadd (G : Type u_1) {H : Type u_2} {α : Type u_3} [add_group G] [ α] (s : set α) [add_group H] [ α] [ α] (g : H) :
theorem measure_theory.pairwise_disjoint_add_fundamental_interior (G : Type u_1) {α : Type u_3} [add_group G] [ α] (s : set α) :
pairwise (disjoint on λ (g : G),
theorem measure_theory.pairwise_disjoint_fundamental_interior (G : Type u_1) {α : Type u_3} [group G] [ α] (s : set α) :
pairwise (disjoint on λ (g : G),
@[protected]
theorem measure_theory.null_measurable_set.add_fundamental_frontier (G : Type u_1) {α : Type u_3} [add_group G] [ α] (s : set α) [countable G] [ α] {μ : measure_theory.measure α} (hs : μ) :
@[protected]
theorem measure_theory.null_measurable_set.fundamental_frontier (G : Type u_1) {α : Type u_3} [group G] [ α] (s : set α) [countable G] [ α] {μ : measure_theory.measure α} (hs : μ) :
@[protected]
theorem measure_theory.null_measurable_set.fundamental_interior (G : Type u_1) {α : Type u_3} [group G] [ α] (s : set α) [countable G] [ α] {μ : measure_theory.measure α} (hs : μ) :
@[protected]
theorem measure_theory.null_measurable_set.add_fundamental_interior (G : Type u_1) {α : Type u_3} [add_group G] [ α] (s : set α) [countable G] [ α] {μ : measure_theory.measure α} (hs : μ) :
theorem measure_theory.is_fundamental_domain.measure_fundamental_frontier {G : Type u_1} {α : Type u_3} [countable G] [group G] [ α] {μ : measure_theory.measure α} {s : set α} (hs : μ) :
theorem measure_theory.is_fundamental_domain.measure_fundamental_interior {G : Type u_1} {α : Type u_3} [countable G] [group G] [ α] {μ : measure_theory.measure α} {s : set α} (hs : μ) :
= μ s
theorem measure_theory.is_add_fundamental_domain.measure_add_fundamental_interior {G : Type u_1} {α : Type u_3} [countable G] [add_group G] [ α] {μ : measure_theory.measure α} {s : set α} (hs : μ) :
= μ s
@[protected]
theorem measure_theory.is_fundamental_domain.fundamental_interior {G : Type u_1} {α : Type u_3} [countable G] [group G] [ α] {μ : measure_theory.measure α} {s : set α} (hs : μ) [ α]  :