Fundamental domain of a group action #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
-
sis a measurable set; -
the sets
g • sover allg : Gcover almost all points of the whole space; -
the sets
g • s, are pairwise a.e. disjoint, i.e.,μ (g₁ • s ∩ g₂ • s) = 0wheneverg₁ ≠ g₂; we require this forg₂ = 1in the definition, then deduce it for any twog₁ ≠ 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 groupmeasure_theory.fundamental_frontier: Fundamental frontier of a set under the action of a group. Elements ofsthat belong to some other translate ofs.measure_theory.fundamental_interior: Fundamental interior of a set under the action of a group. Elements ofsthat do not belong to any other translate ofs.
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
- null_measurable_set : measure_theory.null_measurable_set s μ
- ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x ∈ s
- ae_disjoint : pairwise (measure_theory.ae_disjoint μ on λ (g : G), g +ᵥ s)
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
- null_measurable_set : measure_theory.null_measurable_set s μ
- ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s
- ae_disjoint : pairwise (measure_theory.ae_disjoint μ on λ (g : G), g • s)
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.
theorem
measure_theory.is_add_fundamental_domain.mk_of_measure_univ_le
{G : Type u_1}
{α : Type u_3}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
[countable G]
(h_meas : measure_theory.null_measurable_set 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) μ μ)
(h_measure_univ_le : ⇑μ set.univ ≤ ∑' (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]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
[countable G]
(h_meas : measure_theory.null_measurable_set 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) μ μ)
(h_measure_univ_le : ⇑μ set.univ ≤ ∑' (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]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.is_add_fundamental_domain G s μ) :
theorem
measure_theory.is_fundamental_domain.Union_smul_ae_eq
{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 μ) :
theorem
measure_theory.is_add_fundamental_domain.mono
{G : Type u_1}
{α : Type u_3}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.is_add_fundamental_domain G s μ)
{ν : measure_theory.measure α}
(hle : ν.absolutely_continuous μ) :
theorem
measure_theory.is_fundamental_domain.mono
{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 μ)
{ν : 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]
[mul_action G α]
[measurable_space α]
[mul_action H β]
[measurable_space β]
{s : set α}
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
(h : measure_theory.is_fundamental_domain G s μ)
{f : β → α}
(hf : measure_theory.measure.quasi_measure_preserving f ν μ)
{e : G → H}
(he : function.bijective e)
(hef : ∀ (g : G), function.semiconj f (has_smul.smul (e g)) (has_smul.smul g)) :
measure_theory.is_fundamental_domain H (f ⁻¹' s) ν
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]
[add_action G α]
[measurable_space α]
[add_action H β]
[measurable_space β]
{s : set α}
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
(h : measure_theory.is_add_fundamental_domain G s μ)
{f : β → α}
(hf : measure_theory.measure.quasi_measure_preserving f ν μ)
{e : G → H}
(he : function.bijective e)
(hef : ∀ (g : G), function.semiconj f (has_vadd.vadd (e g)) (has_vadd.vadd g)) :
measure_theory.is_add_fundamental_domain H (f ⁻¹' s) ν
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]
[mul_action G α]
[measurable_space α]
[mul_action H β]
[measurable_space β]
{s : set α}
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
(h : measure_theory.is_fundamental_domain G s μ)
(f : α ≃ β)
(hf : measure_theory.measure.quasi_measure_preserving ⇑(f.symm) ν μ)
(e : H ≃ G)
(hef : ∀ (g : H), function.semiconj ⇑f (has_smul.smul (⇑e g)) (has_smul.smul g)) :
measure_theory.is_fundamental_domain H (⇑f '' s) ν
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]
[add_action G α]
[measurable_space α]
[add_action H β]
[measurable_space β]
{s : set α}
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
(h : measure_theory.is_add_fundamental_domain G s μ)
(f : α ≃ β)
(hf : measure_theory.measure.quasi_measure_preserving ⇑(f.symm) ν μ)
(e : H ≃ G)
(hef : ∀ (g : H), function.semiconj ⇑f (has_vadd.vadd (⇑e g)) (has_vadd.vadd g)) :
measure_theory.is_add_fundamental_domain H (⇑f '' s) ν
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_add_fundamental_domain.pairwise_ae_disjoint_of_ac
{G : Type u_1}
{α : Type u_3}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ ν : measure_theory.measure α}
(h : measure_theory.is_add_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.smul_of_comm
{G : Type u_1}
{α : Type u_3}
[group G]
[mul_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
{G' : Type u_2}
[group G']
[mul_action G' α]
[measurable_space G']
[has_measurable_smul G' α]
[measure_theory.smul_invariant_measure G' α μ]
[smul_comm_class G' G α]
(h : measure_theory.is_fundamental_domain G s μ)
(g : G') :
measure_theory.is_fundamental_domain G (g • s) μ
theorem
measure_theory.is_add_fundamental_domain.vadd_of_comm
{G : Type u_1}
{α : Type u_3}
[add_group G]
[add_action G α]
[measurable_space α]
{s : set α}
{μ : measure_theory.measure α}
{G' : Type u_2}
[add_group G']
[add_action G' α]
[measurable_space G']
[has_measurable_vadd G' α]
[measure_theory.vadd_invariant_measure G' α μ]
[vadd_comm_class G' G α]
(h : measure_theory.is_add_fundamental_domain G s μ)
(g : G') :
measure_theory.is_add_fundamental_domain G (g +ᵥ s) μ
theorem
measure_theory.is_fundamental_domain.null_measurable_set_smul
{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 α μ]
(h : measure_theory.is_fundamental_domain G s μ)
(g : G) :
measure_theory.null_measurable_set (g • s) μ
theorem
measure_theory.is_add_fundamental_domain.null_measurable_set_vadd
{G : Type u_1}
{α : Type u_3}
[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 μ)
(g : G) :
measure_theory.null_measurable_set (g +ᵥ s) μ
theorem
measure_theory.is_add_fundamental_domain.restrict_restrict
{G : Type u_1}
{α : Type u_3}
[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 μ)
(g : G)
(t : set α) :
theorem
measure_theory.is_fundamental_domain.restrict_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 α μ]
(h : measure_theory.is_fundamental_domain G s μ)
(g : G)
(t : set α) :
theorem
measure_theory.is_fundamental_domain.smul
{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 α μ]
(h : measure_theory.is_fundamental_domain G s μ)
(g : G) :
measure_theory.is_fundamental_domain G (g • s) μ
theorem
measure_theory.is_add_fundamental_domain.vadd
{G : Type u_1}
{α : Type u_3}
[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 μ)
(g : G) :
measure_theory.is_add_fundamental_domain G (g +ᵥ s) μ
theorem
measure_theory.is_fundamental_domain.sum_restrict_of_ac
{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]
{ν : measure_theory.measure α}
(h : measure_theory.is_fundamental_domain G s μ)
(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]
[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 μ) :
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]
[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) :
theorem
measure_theory.is_fundamental_domain.lintegral_eq_tsum_of_ac
{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]
{ν : measure_theory.measure α}
(h : measure_theory.is_fundamental_domain G s μ)
(hν : ν.absolutely_continuous μ)
(f : α → ennreal) :
theorem
measure_theory.is_fundamental_domain.sum_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]
(h : measure_theory.is_fundamental_domain G s μ) :
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]
[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 μ) :
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]
[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) :
theorem
measure_theory.is_add_fundamental_domain.lintegral_eq_tsum
{G : Type u_1}
{α : Type u_3}
[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) :
theorem
measure_theory.is_add_fundamental_domain.lintegral_eq_tsum'
{G : Type u_1}
{α : Type u_3}
[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) :
theorem
measure_theory.is_fundamental_domain.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) :
theorem
measure_theory.is_fundamental_domain.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) :
theorem
measure_theory.is_add_fundamental_domain.lintegral_eq_tsum''
{G : Type u_1}
{α : Type u_3}
[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) :
theorem
measure_theory.is_add_fundamental_domain.set_lintegral_eq_tsum
{G : Type u_1}
{α : Type u_3}
[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 α) :
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 α) :
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 α) :
theorem
measure_theory.is_add_fundamental_domain.set_lintegral_eq_tsum'
{G : Type u_1}
{α : Type u_3}
[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 α) :
theorem
measure_theory.is_add_fundamental_domain.measure_eq_tsum_of_ac
{G : Type u_1}
{α : Type u_3}
[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 μ)
(t : set α) :
theorem
measure_theory.is_fundamental_domain.measure_eq_tsum_of_ac
{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]
{ν : measure_theory.measure α}
(h : measure_theory.is_fundamental_domain G s μ)
(hν : ν.absolutely_continuous μ)
(t : set α) :
theorem
measure_theory.is_fundamental_domain.measure_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 μ)
(t : set α) :
theorem
measure_theory.is_add_fundamental_domain.measure_eq_tsum'
{G : Type u_1}
{α : Type u_3}
[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 α) :
theorem
measure_theory.is_add_fundamental_domain.measure_eq_tsum
{G : Type u_1}
{α : Type u_3}
[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 α) :
theorem
measure_theory.is_fundamental_domain.measure_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 μ)
(t : set α) :
theorem
measure_theory.is_add_fundamental_domain.measure_zero_of_invariant
{G : Type u_1}
{α : Type u_3}
[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) :
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) :
theorem
measure_theory.is_fundamental_domain.measure_eq_card_smul_of_smul_ae_eq_self
{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]
[finite G]
(h : measure_theory.is_fundamental_domain G s μ)
(t : set α)
(ht : ∀ (g : G), g • t =ᵐ[μ] t) :
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]
[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]
[finite G]
(h : measure_theory.is_add_fundamental_domain G s μ)
(t : set α)
(ht : ∀ (g : G), g +ᵥ t =ᵐ[μ] t) :
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) :
@[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) :
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) :
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) :
@[protected]
theorem
measure_theory.is_fundamental_domain.measure_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 μ) :
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]
[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 μ) :
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]
[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]
{β : Type u_2}
[topological_space β]
[topological_space.pseudo_metrizable_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_strongly_measurable_on_iff
{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]
{β : Type u_2}
[topological_space β]
[topological_space.pseudo_metrizable_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]
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]
[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]
(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) :
@[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]
[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]
theorem
measure_theory.is_fundamental_domain.integrable_on_iff
{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]
(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]
theorem
measure_theory.is_add_fundamental_domain.integrable_on_iff
{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]
(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) :
theorem
measure_theory.is_fundamental_domain.integral_eq_tsum_of_ac
{G : Type u_1}
{α : Type u_3}
{E : Type u_5}
[group G]
[mul_action G α]
[measurable_space α]
[normed_add_comm_group E]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ]
[countable G]
{ν : measure_theory.measure α}
[normed_space ℝ E]
[complete_space E]
(h : measure_theory.is_fundamental_domain G s μ)
(hν : ν.absolutely_continuous μ)
(f : α → E)
(hf : measure_theory.integrable f ν) :
theorem
measure_theory.is_add_fundamental_domain.integral_eq_tsum_of_ac
{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 : set α}
{μ : measure_theory.measure α}
[measurable_space G]
[has_measurable_vadd G α]
[measure_theory.vadd_invariant_measure G α μ]
[countable G]
{ν : measure_theory.measure α}
[normed_space ℝ E]
[complete_space E]
(h : measure_theory.is_add_fundamental_domain G s μ)
(hν : ν.absolutely_continuous μ)
(f : α → E)
(hf : measure_theory.integrable f ν) :
theorem
measure_theory.is_add_fundamental_domain.integral_eq_tsum
{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 : 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]
(h : measure_theory.is_add_fundamental_domain G s μ)
(f : α → E)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.is_fundamental_domain.integral_eq_tsum
{G : Type u_1}
{α : Type u_3}
{E : Type u_5}
[group G]
[mul_action G α]
[measurable_space α]
[normed_add_comm_group E]
{s : 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]
(h : measure_theory.is_fundamental_domain G s μ)
(f : α → E)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.is_add_fundamental_domain.integral_eq_tsum'
{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 : 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]
(h : measure_theory.is_add_fundamental_domain G s μ)
(f : α → E)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.is_fundamental_domain.integral_eq_tsum'
{G : Type u_1}
{α : Type u_3}
{E : Type u_5}
[group G]
[mul_action G α]
[measurable_space α]
[normed_add_comm_group E]
{s : 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]
(h : measure_theory.is_fundamental_domain G s μ)
(f : α → E)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.is_fundamental_domain.integral_eq_tsum''
{G : Type u_1}
{α : Type u_3}
{E : Type u_5}
[group G]
[mul_action G α]
[measurable_space α]
[normed_add_comm_group E]
{s : 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]
(h : measure_theory.is_fundamental_domain G s μ)
(f : α → E)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.is_add_fundamental_domain.integral_eq_tsum''
{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 : 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]
(h : measure_theory.is_add_fundamental_domain G s μ)
(f : α → E)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.is_fundamental_domain.set_integral_eq_tsum
{G : Type u_1}
{α : Type u_3}
{E : Type u_5}
[group G]
[mul_action G α]
[measurable_space α]
[normed_add_comm_group E]
{s : 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]
(h : measure_theory.is_fundamental_domain G s μ)
{f : α → E}
{t : set α}
(hf : measure_theory.integrable_on f t μ) :
theorem
measure_theory.is_add_fundamental_domain.set_integral_eq_tsum
{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 : 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]
(h : measure_theory.is_add_fundamental_domain G s μ)
{f : α → E}
{t : set α}
(hf : measure_theory.integrable_on f t μ) :
theorem
measure_theory.is_add_fundamental_domain.set_integral_eq_tsum'
{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 : 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]
(h : measure_theory.is_add_fundamental_domain G s μ)
{f : α → E}
{t : set α}
(hf : measure_theory.integrable_on f t μ) :
theorem
measure_theory.is_fundamental_domain.set_integral_eq_tsum'
{G : Type u_1}
{α : Type u_3}
{E : Type u_5}
[group G]
[mul_action G α]
[measurable_space α]
[normed_add_comm_group E]
{s : 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]
(h : measure_theory.is_fundamental_domain G s μ)
{f : α → E}
{t : set α}
(hf : measure_theory.integrable_on f t μ) :
@[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) :
@[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) :
theorem
measure_theory.is_add_fundamental_domain.measure_le_of_pairwise_disjoint
{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.null_measurable_set t μ)
(hd : pairwise (measure_theory.ae_disjoint μ on λ (g : G), (g +ᵥ 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]
[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.null_measurable_set t μ)
(hd : pairwise (measure_theory.ae_disjoint μ on λ (g : G), g • 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]
[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) :
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) :
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) :
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]
[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) :
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.
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.
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.
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.
theorem
measure_theory.fundamental_frontier_subset
{G : Type u_1}
{α : Type u_3}
[group G]
[mul_action G α]
{s : set α} :
theorem
measure_theory.add_fundamental_frontier_subset
{G : Type u_1}
{α : Type u_3}
[add_group G]
[add_action G α]
{s : set α} :
theorem
measure_theory.add_fundamental_interior_subset
{G : Type u_1}
{α : Type u_3}
[add_group G]
[add_action G α]
{s : set α} :
theorem
measure_theory.fundamental_interior_subset
{G : Type u_1}
{α : Type u_3}
[group G]
[mul_action G α]
{s : set α} :
theorem
measure_theory.disjoint_fundamental_interior_fundamental_frontier
(G : Type u_1)
{α : Type u_3}
[group G]
[mul_action G α]
(s : set α) :
theorem
measure_theory.disjoint_add_fundamental_interior_add_fundamental_frontier
(G : Type u_1)
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α) :
@[simp]
theorem
measure_theory.add_fundamental_interior_union_add_fundamental_frontier
(G : Type u_1)
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α) :
@[simp]
theorem
measure_theory.fundamental_interior_union_fundamental_frontier
(G : Type u_1)
{α : Type u_3}
[group G]
[mul_action G α]
(s : set α) :
@[simp]
theorem
measure_theory.fundamental_frontier_union_fundamental_interior
(G : Type u_1)
{α : Type u_3}
[group G]
[mul_action G α]
(s : set α) :
@[simp]
theorem
measure_theory.sdiff_fundamental_interior
(G : Type u_1)
{α : Type u_3}
[group G]
[mul_action G α]
(s : set α) :
@[simp]
theorem
measure_theory.sdiff_add_fundamental_interior
(G : Type u_1)
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α) :
@[simp]
theorem
measure_theory.sdiff_fundamental_frontier
(G : Type u_1)
{α : Type u_3}
[group G]
[mul_action G α]
(s : set α) :
@[simp]
theorem
measure_theory.sdiff_add_fundamental_frontier
(G : Type u_1)
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α) :
@[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.add_fundamental_frontier_vadd
(G : Type u_1)
{H : Type u_2}
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α)
[add_group H]
[add_action H α]
[vadd_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) :
@[simp]
theorem
measure_theory.add_fundamental_interior_vadd
(G : Type u_1)
{H : Type u_2}
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α)
[add_group H]
[add_action H α]
[vadd_comm_class H G α]
(g : H) :
theorem
measure_theory.pairwise_disjoint_add_fundamental_interior
(G : Type u_1)
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α) :
pairwise (disjoint on λ (g : G), g +ᵥ measure_theory.add_fundamental_interior G s)
theorem
measure_theory.pairwise_disjoint_fundamental_interior
(G : Type u_1)
{α : Type u_3}
[group G]
[mul_action G α]
(s : set α) :
pairwise (disjoint on λ (g : G), g • measure_theory.fundamental_interior G s)
@[protected]
theorem
measure_theory.null_measurable_set.add_fundamental_frontier
(G : Type u_1)
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α)
[countable G]
[measurable_space G]
[measurable_space α]
[has_measurable_vadd G α]
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure G α μ]
(hs : measure_theory.null_measurable_set s μ) :
@[protected]
theorem
measure_theory.null_measurable_set.fundamental_frontier
(G : Type u_1)
{α : Type u_3}
[group G]
[mul_action G α]
(s : set α)
[countable G]
[measurable_space G]
[measurable_space α]
[has_measurable_smul G α]
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure G α μ]
(hs : measure_theory.null_measurable_set s μ) :
@[protected]
theorem
measure_theory.null_measurable_set.fundamental_interior
(G : Type u_1)
{α : Type u_3}
[group G]
[mul_action G α]
(s : set α)
[countable G]
[measurable_space G]
[measurable_space α]
[has_measurable_smul G α]
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure G α μ]
(hs : measure_theory.null_measurable_set s μ) :
@[protected]
theorem
measure_theory.null_measurable_set.add_fundamental_interior
(G : Type u_1)
{α : Type u_3}
[add_group G]
[add_action G α]
(s : set α)
[countable G]
[measurable_space G]
[measurable_space α]
[has_measurable_vadd G α]
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure G α μ]
(hs : measure_theory.null_measurable_set s μ) :
theorem
measure_theory.is_fundamental_domain.measure_fundamental_frontier
{G : Type u_1}
{α : Type u_3}
[countable G]
[group G]
[mul_action G α]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.is_fundamental_domain G s μ) :
⇑μ (measure_theory.fundamental_frontier G s) = 0
theorem
measure_theory.is_add_fundamental_domain.measure_add_fundamental_frontier
{G : Type u_1}
{α : Type u_3}
[countable G]
[add_group G]
[add_action G α]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.is_add_fundamental_domain G s μ) :
⇑μ (measure_theory.add_fundamental_frontier G s) = 0
theorem
measure_theory.is_fundamental_domain.measure_fundamental_interior
{G : Type u_1}
{α : Type u_3}
[countable G]
[group G]
[mul_action G α]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.is_fundamental_domain G s μ) :
⇑μ (measure_theory.fundamental_interior G s) = ⇑μ s
theorem
measure_theory.is_add_fundamental_domain.measure_add_fundamental_interior
{G : Type u_1}
{α : Type u_3}
[countable G]
[add_group G]
[add_action G α]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.is_add_fundamental_domain G s μ) :
⇑μ (measure_theory.add_fundamental_interior G s) = ⇑μ s
@[protected]
theorem
measure_theory.is_fundamental_domain.fundamental_interior
{G : Type u_1}
{α : Type u_3}
[countable G]
[group G]
[mul_action G α]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.is_fundamental_domain G s μ)
[measurable_space G]
[has_measurable_smul G α]
[measure_theory.smul_invariant_measure G α μ] :