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

• MeasureTheory.IsFundamentalDomain: Predicate for a set to be a fundamental domain of the action of a group
• MeasureTheory.fundamentalFrontier: Fundamental frontier of a set under the action of a group. Elements of s that belong to some other translate of s.
• MeasureTheory.fundamentalInterior: 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 MeasureTheory.IsAddFundamentalDomain (G : Type u_1) {α : Type u_2} [Zero G] [VAdd G α] [MeasurableSpace α] (s : Set α) (μ : autoParam (MeasureTheory.Measure α) _auto✝) : 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.

• nullMeasurableSet : MeasureTheory.NullMeasurableSet s
• ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x ∈ s
• aedisjoint : Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g +ᵥ s)

structure MeasureTheory.IsFundamentalDomain (G : Type u_1) {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] (s : Set α) (μ : autoParam (MeasureTheory.Measure α) _auto✝) : 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.

• nullMeasurableSet : MeasureTheory.NullMeasurableSet s
• ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s
• aedisjoint : Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g • s)

theorem MeasureTheory.IsAddFundamentalDomain.mk' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h_meas : MeasureTheory.NullMeasurableSet s) (h_exists : ∀ (x : α), ∃! (g : G), g +ᵥ x ∈ s) : MeasureTheory.IsAddFundamentalDomain G 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 MeasureTheory.IsFundamentalDomain.mk' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h_meas : MeasureTheory.NullMeasurableSet s) (h_exists : ∀ (x : α), ∃! (g : G), g • x ∈ s) : MeasureTheory.IsFundamentalDomain G 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 MeasureTheory.IsAddFundamentalDomain.mk'' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h_meas : MeasureTheory.NullMeasurableSet s) (h_ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x ∈ s) (h_ae_disjoint : ∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving fun (x : α) => g +ᵥ x) : MeasureTheory.IsAddFundamentalDomain G s

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

theorem MeasureTheory.IsFundamentalDomain.mk'' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h_meas : MeasureTheory.NullMeasurableSet s) (h_ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s) (h_ae_disjoint : ∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving fun (x : α) => g • x) : MeasureTheory.IsFundamentalDomain G s

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

theorem MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [Countable G] (h_meas : MeasureTheory.NullMeasurableSet s) (h_ae_disjoint : ∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving fun (x : α) => g +ᵥ x) (h_measure_univ_le : ↑↑μ Set.univ ≤ ∑' (g : G), ↑↑μ (g +ᵥ s)) : MeasureTheory.IsAddFundamentalDomain 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 MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [Countable G] (h_meas : MeasureTheory.NullMeasurableSet s) (h_ae_disjoint : ∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving fun (x : α) => g • x) (h_measure_univ_le : ↑↑μ Set.univ ≤ ∑' (g : G), ↑↑μ (g • s)) : MeasureTheory.IsFundamentalDomain 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 MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s) : ⋃ (g : G), g +ᵥ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ

abbrev MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq.match_1 {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {s : Set α} : ∀ (x : α) (motive : (∃ (g : G), g +ᵥ x ∈ s) → Prop) (x_1 : ∃ (g : G), g +ᵥ x ∈ s), (∀ (g : G) (hg : g +ᵥ x ∈ s), motive (_ : ∃ (g : G), g +ᵥ x ∈ s)) → motive x_1

Equations

• (_ : motive x) = (_ : motive x)

theorem MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s) : ⋃ (g : G), g • s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ

theorem MeasureTheory.IsAddFundamentalDomain.measure_ne_zero {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [Countable G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] (hμ : μ ≠ 0) (h : MeasureTheory.IsAddFundamentalDomain G s) : ↑↑μ s ≠ 0

theorem MeasureTheory.IsFundamentalDomain.measure_ne_zero {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [Countable G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] (hμ : μ ≠ 0) (h : MeasureTheory.IsFundamentalDomain G s) : ↑↑μ s ≠ 0

theorem MeasureTheory.IsAddFundamentalDomain.mono {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s) {ν : MeasureTheory.Measure α} (hle : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : MeasureTheory.IsAddFundamentalDomain G s

theorem MeasureTheory.IsFundamentalDomain.mono {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s) {ν : MeasureTheory.Measure α} (hle : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : MeasureTheory.IsFundamentalDomain G s

theorem MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [AddGroup G] [AddGroup H] [AddAction G α] [MeasurableSpace α] [AddAction H β] [MeasurableSpace β] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (h : MeasureTheory.IsAddFundamentalDomain G s) {f : β → α} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f) {e : G → H} (he : Function.Bijective e) (hef : ∀ (g : G), Function.Semiconj f (fun (x : β) => e g +ᵥ x) fun (x : α) => g +ᵥ x) : MeasureTheory.IsAddFundamentalDomain H (f ⁻¹' s)

abbrev MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv.match_1 {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {f : β → α} (x : β) (motive : (∃ (g : G), g +ᵥ f x ∈ s) → Prop) : ∀ (x_1 : ∃ (g : G), g +ᵥ f x ∈ s), (∀ (g : G) (hg : g +ᵥ f x ∈ s), motive (_ : ∃ (g : G), g +ᵥ f x ∈ s)) → motive x_1

Equations

• (_ : motive x) = (_ : motive x)

theorem MeasureTheory.IsFundamentalDomain.preimage_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [Group G] [Group H] [MulAction G α] [MeasurableSpace α] [MulAction H β] [MeasurableSpace β] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (h : MeasureTheory.IsFundamentalDomain G s) {f : β → α} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f) {e : G → H} (he : Function.Bijective e) (hef : ∀ (g : G), Function.Semiconj f (fun (x : β) => e g • x) fun (x : α) => g • x) : MeasureTheory.IsFundamentalDomain H (f ⁻¹' s)

theorem MeasureTheory.IsAddFundamentalDomain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [AddGroup G] [AddGroup H] [AddAction G α] [MeasurableSpace α] [AddAction H β] [MeasurableSpace β] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α ≃ β) (hf : MeasureTheory.Measure.QuasiMeasurePreserving ⇑f.symm) (e : H ≃ G) (hef : ∀ (g : H), Function.Semiconj (⇑f) (fun (x : α) => e g +ᵥ x) fun (x : β) => g +ᵥ x) : MeasureTheory.IsAddFundamentalDomain H (⇑f '' s)

theorem MeasureTheory.IsFundamentalDomain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [Group G] [Group H] [MulAction G α] [MeasurableSpace α] [MulAction H β] [MeasurableSpace β] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (h : MeasureTheory.IsFundamentalDomain G s) (f : α ≃ β) (hf : MeasureTheory.Measure.QuasiMeasurePreserving ⇑f.symm) (e : H ≃ G) (hef : ∀ (g : H), Function.Semiconj (⇑f) (fun (x : α) => e g • x) fun (x : β) => g • x) : MeasureTheory.IsFundamentalDomain H (⇑f '' s)

theorem MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : Pairwise fun (g₁ g₂ : G) => MeasureTheory.AEDisjoint ν (g₁ +ᵥ s) (g₂ +ᵥ s)

theorem MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : Pairwise fun (g₁ g₂ : G) => MeasureTheory.AEDisjoint ν (g₁ • s) (g₂ • s)

theorem MeasureTheory.IsAddFundamentalDomain.vadd_of_comm {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {G' : Type u_6} [AddGroup G'] [AddAction G' α] [MeasurableSpace G'] [MeasurableVAdd G' α] [MeasureTheory.VAddInvariantMeasure G' α μ] [VAddCommClass G' G α] (h : MeasureTheory.IsAddFundamentalDomain G s) (g : G') : MeasureTheory.IsAddFundamentalDomain G (g +ᵥ s)

theorem MeasureTheory.IsFundamentalDomain.smul_of_comm {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {G' : Type u_6} [Group G'] [MulAction G' α] [MeasurableSpace G'] [MeasurableSMul G' α] [MeasureTheory.SMulInvariantMeasure G' α μ] [SMulCommClass G' G α] (h : MeasureTheory.IsFundamentalDomain G s) (g : G') : MeasureTheory.IsFundamentalDomain G (g • s)

theorem MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] (h : MeasureTheory.IsAddFundamentalDomain G s) (g : G) : MeasureTheory.NullMeasurableSet (g +ᵥ s)

theorem MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] (h : MeasureTheory.IsFundamentalDomain G s) (g : G) : MeasureTheory.NullMeasurableSet (g • s)

theorem MeasureTheory.IsAddFundamentalDomain.restrict_restrict {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] (h : MeasureTheory.IsAddFundamentalDomain G s) (g : G) (t : Set α) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ t) (g +ᵥ s) = MeasureTheory.Measure.restrict μ ((g +ᵥ s) ∩ t)

theorem MeasureTheory.IsFundamentalDomain.restrict_restrict {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] (h : MeasureTheory.IsFundamentalDomain G s) (g : G) (t : Set α) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ t) (g • s) = MeasureTheory.Measure.restrict μ (g • s ∩ t)

theorem MeasureTheory.IsAddFundamentalDomain.vadd {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] (h : MeasureTheory.IsAddFundamentalDomain G s) (g : G) : MeasureTheory.IsAddFundamentalDomain G (g +ᵥ s)

theorem MeasureTheory.IsFundamentalDomain.smul {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] (h : MeasureTheory.IsFundamentalDomain G s) (g : G) : MeasureTheory.IsFundamentalDomain G (g • s)

theorem MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : (MeasureTheory.Measure.sum fun (g : G) => MeasureTheory.Measure.restrict ν (g +ᵥ s)) = ν

theorem MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : (MeasureTheory.Measure.sum fun (g : G) => MeasureTheory.Measure.restrict ν (g • s)) = ν

theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂ν

theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν

theorem MeasureTheory.IsAddFundamentalDomain.sum_restrict {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) : (MeasureTheory.Measure.sum fun (g : G) => MeasureTheory.Measure.restrict μ (g +ᵥ s)) = μ

theorem MeasureTheory.IsFundamentalDomain.sum_restrict {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) : (MeasureTheory.Measure.sum fun (g : G) => MeasureTheory.Measure.restrict μ (g • s)) = μ

theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂μ

theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (-g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g⁻¹ • x) ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g • x) ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.set_lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α → ENNReal) (t : Set α) : ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in t ∩ (g +ᵥ s), f x ∂μ

theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) (f : α → ENNReal) (t : Set α) : ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.set_lintegral_eq_tsum' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α → ENNReal) (t : Set α) : ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) (f : α → ENNReal) (t : Set α) : ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) (t : Set α) : ↑↑ν t = ∑' (g : G), ↑↑ν (t ∩ (g +ᵥ s))

theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) (t : Set α) : ↑↑ν t = ∑' (g : G), ↑↑ν (t ∩ g • s)

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) (t : Set α) : ↑↑μ t = ∑' (g : G), ↑↑μ (t ∩ (g +ᵥ s))

theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) (t : Set α) : ↑↑μ t = ∑' (g : G), ↑↑μ (t ∩ g • s)

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) (t : Set α) : ↑↑μ t = ∑' (g : G), ↑↑μ ((g +ᵥ t) ∩ s)

theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) (t : Set α) : ↑↑μ t = ∑' (g : G), ↑↑μ (g • t ∩ s)

theorem MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s) (t : Set α) (ht : ∀ (g : G), g +ᵥ t = t) (hts : ↑↑μ (t ∩ s) = 0) : ↑↑μ t = 0

theorem MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s) (t : Set α) (ht : ∀ (g : G), g • t = t) (hts : ↑↑μ (t ∩ s) = 0) : ↑↑μ t = 0

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [Finite G] (h : MeasureTheory.IsAddFundamentalDomain G s) (t : Set α) (ht : ∀ (g : G), g +ᵥ t =ᶠ[MeasureTheory.Measure.ae μ] t) : ↑↑μ t = Nat.card G • ↑↑μ (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.

theorem MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [Finite G] (h : MeasureTheory.IsFundamentalDomain G s) (t : Set α) (ht : ∀ (g : G), g • t =ᶠ[MeasureTheory.Measure.ae μ] t) : ↑↑μ t = Nat.card G • ↑↑μ (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 MeasureTheory.IsAddFundamentalDomain.set_lintegral_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s) (ht : MeasureTheory.IsAddFundamentalDomain G t) (f : α → ENNReal) (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s) (ht : MeasureTheory.IsFundamentalDomain G t) (f : α → ENNReal) (hf : ∀ (g : G) (x : α), f (g • x) = f x) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.measure_set_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s) (ht : MeasureTheory.IsAddFundamentalDomain G t) {A : Set α} (hA₀ : MeasurableSet A) (hA : ∀ (g : G), (fun (x : α) => g +ᵥ x) ⁻¹' A = A) : ↑↑μ (A ∩ s) = ↑↑μ (A ∩ t)

theorem MeasureTheory.IsFundamentalDomain.measure_set_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s) (ht : MeasureTheory.IsFundamentalDomain G t) {A : Set α} (hA₀ : MeasurableSet A) (hA : ∀ (g : G), (fun (x : α) => g • x) ⁻¹' A = A) : ↑↑μ (A ∩ s) = ↑↑μ (A ∩ t)

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s) (ht : MeasureTheory.IsAddFundamentalDomain G t) : ↑↑μ s = ↑↑μ t

If s and t are two fundamental domains of the same action, then their measures are equal.

theorem MeasureTheory.IsFundamentalDomain.measure_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s) (ht : MeasureTheory.IsFundamentalDomain G t) : ↑↑μ s = ↑↑μ t

If s and t are two fundamental domains of the same action, then their measures are equal.

theorem MeasureTheory.IsAddFundamentalDomain.aEStronglyMeasurable_on_iff {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {β : Type u_6} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] (hs : MeasureTheory.IsAddFundamentalDomain G s) (ht : MeasureTheory.IsAddFundamentalDomain G t) {f : α → β} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s) ↔ MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ t)

theorem MeasureTheory.IsFundamentalDomain.aEStronglyMeasurable_on_iff {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {β : Type u_6} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] (hs : MeasureTheory.IsFundamentalDomain G s) (ht : MeasureTheory.IsFundamentalDomain G t) {f : α → β} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s) ↔ MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ t)

theorem MeasureTheory.IsAddFundamentalDomain.hasFiniteIntegral_on_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s) (ht : MeasureTheory.IsAddFundamentalDomain G t) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : MeasureTheory.HasFiniteIntegral f ↔ MeasureTheory.HasFiniteIntegral f

theorem MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s) (ht : MeasureTheory.IsFundamentalDomain G t) {f : α → E} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : MeasureTheory.HasFiniteIntegral f ↔ MeasureTheory.HasFiniteIntegral f

theorem MeasureTheory.IsAddFundamentalDomain.integrableOn_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s) (ht : MeasureTheory.IsAddFundamentalDomain G t) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : MeasureTheory.IntegrableOn f s ↔ MeasureTheory.IntegrableOn f t

theorem MeasureTheory.IsFundamentalDomain.integrableOn_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s) (ht : MeasureTheory.IsFundamentalDomain G t) {f : α → E} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : MeasureTheory.IntegrableOn f s ↔ MeasureTheory.IntegrableOn f t

theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) (f : α → E) (hf : MeasureTheory.Integrable f) : ∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f x ∂ν

theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s) (hν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) (f : α → E) (hf : MeasureTheory.Integrable f) : ∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g • s, f x ∂ν

theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α → E) (hf : MeasureTheory.Integrable f) : ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f x ∂μ

theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s) (f : α → E) (hf : MeasureTheory.Integrable f) : ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in g • s, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α → E) (hf : MeasureTheory.Integrable f) : ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (-g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s) (f : α → E) (hf : MeasureTheory.Integrable f) : ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g⁻¹ • x) ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'' {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s) (f : α → E) (hf : MeasureTheory.Integrable f) : ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum'' {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s) (f : α → E) (hf : MeasureTheory.Integrable f) : ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g • x) ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.set_integral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t) : ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ (g +ᵥ s), f x ∂μ

theorem MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t) : ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.set_integral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t) : ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t) : ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.set_integral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (hs : MeasureTheory.IsAddFundamentalDomain G s) (ht : MeasureTheory.IsAddFundamentalDomain G t) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

theorem MeasureTheory.IsFundamentalDomain.set_integral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (hs : MeasureTheory.IsFundamentalDomain G s) (ht : MeasureTheory.IsFundamentalDomain G t) {f : α → E} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s) (ht : MeasureTheory.NullMeasurableSet t) (hd : Pairwise (MeasureTheory.AEDisjoint μ on fun (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 MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s) (ht : MeasureTheory.NullMeasurableSet t) (hd : Pairwise (MeasureTheory.AEDisjoint μ on fun (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 MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s) (htm : MeasureTheory.NullMeasurableSet t) (ht : ↑↑μ s < ↑↑μ t) : ∃ x ∈ t, ∃ y ∈ t, ∃ (g : G), 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 MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s) (htm : MeasureTheory.NullMeasurableSet t) (ht : ↑↑μ s < ↑↑μ t) : ∃ x ∈ t, ∃ y ∈ t, ∃ (g : G), 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 MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s) {f : α → ENNReal} (hf : ∀ (γ : G) (x : α), f (γ +ᵥ x) = f x) : essSup f (MeasureTheory.Measure.restrict μ s) = essSup f μ

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.

theorem MeasureTheory.IsFundamentalDomain.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s) {f : α → ENNReal} (hf : ∀ (γ : G) (x : α), f (γ • x) = f x) : essSup f (MeasureTheory.Measure.restrict μ s) = essSup f μ

If f is invariant under the action of a countable group G, and μ is a G-invariant measure with a fundamental domain s, then the essSup of f restricted to s is the same as that of f on all of its domain.

Interior/frontier of a fundamental domain

def MeasureTheory.addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Set α

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

Equations

• MeasureTheory.addFundamentalFrontier G s = s ∩ ⋃ (g : G), ⋃ (_ : g ≠ 0), g +ᵥ s

def MeasureTheory.fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Set α

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

Equations

• MeasureTheory.fundamentalFrontier G s = s ∩ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s

def MeasureTheory.addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Set α

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

Equations

• MeasureTheory.addFundamentalInterior G s = s \ ⋃ (g : G), ⋃ (_ : g ≠ 0), g +ᵥ s

def MeasureTheory.fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Set α

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

Equations

• MeasureTheory.fundamentalInterior G s = s \ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s

@[simp]

theorem MeasureTheory.mem_addFundamentalFrontier {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {x : α} : x ∈ MeasureTheory.addFundamentalFrontier G s ↔ x ∈ s ∧ ∃ (g : G), g ≠ 0 ∧ x ∈ g +ᵥ s

@[simp]

theorem MeasureTheory.mem_fundamentalFrontier {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} {x : α} : x ∈ MeasureTheory.fundamentalFrontier G s ↔ x ∈ s ∧ ∃ (g : G), g ≠ 1 ∧ x ∈ g • s

@[simp]

theorem MeasureTheory.mem_addFundamentalInterior {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {x : α} : x ∈ MeasureTheory.addFundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 0 → x ∉ g +ᵥ s

@[simp]

theorem MeasureTheory.mem_fundamentalInterior {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} {x : α} : x ∈ MeasureTheory.fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s

theorem MeasureTheory.addFundamentalFrontier_subset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} : MeasureTheory.addFundamentalFrontier G s ⊆ s

theorem MeasureTheory.fundamentalFrontier_subset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} : MeasureTheory.fundamentalFrontier G s ⊆ s

theorem MeasureTheory.addFundamentalInterior_subset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} : MeasureTheory.addFundamentalInterior G s ⊆ s

theorem MeasureTheory.fundamentalInterior_subset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} : MeasureTheory.fundamentalInterior G s ⊆ s

theorem MeasureTheory.disjoint_addFundamentalInterior_addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Disjoint (MeasureTheory.addFundamentalInterior G s) (MeasureTheory.addFundamentalFrontier G s)

theorem MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Disjoint (MeasureTheory.fundamentalInterior G s) (MeasureTheory.fundamentalFrontier G s)

@[simp]

theorem MeasureTheory.addFundamentalInterior_union_addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : MeasureTheory.addFundamentalInterior G s ∪ MeasureTheory.addFundamentalFrontier G s = s

@[simp]

theorem MeasureTheory.fundamentalInterior_union_fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : MeasureTheory.fundamentalInterior G s ∪ MeasureTheory.fundamentalFrontier G s = s

@[simp]

theorem MeasureTheory.addFundamentalFrontier_union_addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : MeasureTheory.addFundamentalFrontier G s ∪ MeasureTheory.addFundamentalInterior G s = s

@[simp]

theorem MeasureTheory.fundamentalFrontier_union_fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : MeasureTheory.fundamentalFrontier G s ∪ MeasureTheory.fundamentalInterior G s = s

@[simp]

theorem MeasureTheory.sdiff_addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : s \ MeasureTheory.addFundamentalInterior G s = MeasureTheory.addFundamentalFrontier G s

@[simp]

theorem MeasureTheory.sdiff_fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : s \ MeasureTheory.fundamentalInterior G s = MeasureTheory.fundamentalFrontier G s

@[simp]

theorem MeasureTheory.sdiff_addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : s \ MeasureTheory.addFundamentalFrontier G s = MeasureTheory.addFundamentalInterior G s

@[simp]

theorem MeasureTheory.sdiff_fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : s \ MeasureTheory.fundamentalFrontier G s = MeasureTheory.fundamentalInterior G s

@[simp]

theorem MeasureTheory.addFundamentalFrontier_vadd (G : Type u_1) {H : Type u_2} {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) [AddGroup H] [AddAction H α] [VAddCommClass H G α] (g : H) : MeasureTheory.addFundamentalFrontier G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalFrontier G s

@[simp]

theorem MeasureTheory.fundamentalFrontier_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [Group G] [MulAction G α] (s : Set α) [Group H] [MulAction H α] [SMulCommClass H G α] (g : H) : MeasureTheory.fundamentalFrontier G (g • s) = g • MeasureTheory.fundamentalFrontier G s

@[simp]

theorem MeasureTheory.addFundamentalInterior_vadd (G : Type u_1) {H : Type u_2} {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) [AddGroup H] [AddAction H α] [VAddCommClass H G α] (g : H) : MeasureTheory.addFundamentalInterior G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalInterior G s

@[simp]

theorem MeasureTheory.fundamentalInterior_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [Group G] [MulAction G α] (s : Set α) [Group H] [MulAction H α] [SMulCommClass H G α] (g : H) : MeasureTheory.fundamentalInterior G (g • s) = g • MeasureTheory.fundamentalInterior G s

theorem MeasureTheory.pairwise_disjoint_addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Pairwise (Disjoint on fun (g : G) => g +ᵥ MeasureTheory.addFundamentalInterior G s)

theorem MeasureTheory.pairwise_disjoint_fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Pairwise (Disjoint on fun (g : G) => g • MeasureTheory.fundamentalInterior G s)

theorem MeasureTheory.NullMeasurableSet.addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) [Countable G] [MeasurableSpace G] [MeasurableSpace α] [MeasurableVAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (hs : MeasureTheory.NullMeasurableSet s) : MeasureTheory.NullMeasurableSet (MeasureTheory.addFundamentalFrontier G s)

theorem MeasureTheory.NullMeasurableSet.fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) [Countable G] [MeasurableSpace G] [MeasurableSpace α] [MeasurableSMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (hs : MeasureTheory.NullMeasurableSet s) : MeasureTheory.NullMeasurableSet (MeasureTheory.fundamentalFrontier G s)

theorem MeasureTheory.NullMeasurableSet.addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) [Countable G] [MeasurableSpace G] [MeasurableSpace α] [MeasurableVAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (hs : MeasureTheory.NullMeasurableSet s) : MeasureTheory.NullMeasurableSet (MeasureTheory.addFundamentalInterior G s)

theorem MeasureTheory.NullMeasurableSet.fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) [Countable G] [MeasurableSpace G] [MeasurableSpace α] [MeasurableSMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (hs : MeasureTheory.NullMeasurableSet s) : MeasureTheory.NullMeasurableSet (MeasureTheory.fundamentalInterior G s)

theorem MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier {G : Type u_1} {α : Type u_3} [Countable G] [AddGroup G] [AddAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.IsAddFundamentalDomain G s) : ↑↑μ (MeasureTheory.addFundamentalFrontier G s) = 0

theorem MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier {G : Type u_1} {α : Type u_3} [Countable G] [Group G] [MulAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.IsFundamentalDomain G s) : ↑↑μ (MeasureTheory.fundamentalFrontier G s) = 0

theorem MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalInterior {G : Type u_1} {α : Type u_3} [Countable G] [AddGroup G] [AddAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.IsAddFundamentalDomain G s) : ↑↑μ (MeasureTheory.addFundamentalInterior G s) = ↑↑μ s

theorem MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior {G : Type u_1} {α : Type u_3} [Countable G] [Group G] [MulAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.IsFundamentalDomain G s) : ↑↑μ (MeasureTheory.fundamentalInterior G s) = ↑↑μ s

theorem MeasureTheory.IsFundamentalDomain.fundamentalInterior {G : Type u_1} {α : Type u_3} [Countable G] [Group G] [MulAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.IsFundamentalDomain G s) [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] : MeasureTheory.IsFundamentalDomain G (MeasureTheory.fundamentalInterior G s)